feat(Archive/Imo/Imo2012Q5): IMO 2012 Q5

[zcyemi]

---

Add IMO 2012 Q5

• depends on: [Merged by Bors] - feat(Geometry/Euclidean/Altitude): add inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero #34157
• depends on: feat(Analysis/Convex/Between): add lemmas on convex combination of mem simplex interior #34156
• depends on: feat(Geometry/Euclidean/Triangle): add altitudeFoot lies strictly between endpoints for an obtuse angle #34155
• depends on: [Merged by Bors] - feat(LinearAlgebra/AffineSpace/Independent): Add affineCombination_eq_lineMap_iff_weight_lineMap #33852
• depends on: [Merged by Bors] - feat(Geometry/Euclidean/Sphere/Power): Add theorem about cospherical points on two intersecting lines #33479
• depends on: feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness #31500

[github-actions]

PR summary f760e25ec7

Import changes exceeding 2%

%	File
+3.77%	Mathlib.Geometry.Euclidean.Sphere.Power

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Euclidean.Sphere.Power	2146	2227	+81 (+3.77%)
Mathlib.Geometry.Euclidean.Triangle	2200	2201	+1 (+0.05%)

Import changes for all files

Files	Import difference
4 files Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Similarity Mathlib.Geometry.Euclidean.Triangle	1
Mathlib.Geometry.Euclidean.Sphere.Ptolemy	12
Mathlib.Geometry.Euclidean.Sphere.Power	81

---

Declarations diff

+ AffineIndependent.affineCombination_eq_iff_eq
+ AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap
+ C_mem_sphere_A
+ C_mem_sphere_B
+ Cospherical.restrict
+ Imo2012Q5Cfg
+ Isometry.cospherical
+ K'
+ K'_def
+ K_mem_sphere_B
+ K_ne_K'
+ L'
+ L'_def
+ L_mem_sphere_A
+ L_ne_L'
+ X_mem_CD
+ X_mem_interior
+ affineIndependent_iff_affineIndependent_of_sbtw
+ affineIndependent_of_sbtw_affineIndependent
+ affineIndependent_of_sbtw_affineIndependent_inv
+ affineIndependent_of_sbtw_sbtw
+ angle_lt_angle_of_angle_ge_pi_div_two
+ angle_lt_pi_div_two_of_angle_ge_pi_div_two
+ cosphereic_set_ω
+ cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi
+ dist_CA_eq_radius_A
+ dist_CB_eq_radius_B
+ dist_X_sphere_A
+ dist_X_sphere_B
+ hKXK'
+ hLXL'
+ h_A
+ h_ADX_eq_ADC
+ h_A_K_K'
+ h_B
+ h_BDX_eq_BDC
+ h_B_L_L'
+ h_C
+ h_K
+ h_K'
+ h_K'_B
+ h_K_B
+ h_L
+ h_L'
+ h_L'_A
+ h_L_A
+ h_angle_CDA
+ h_angle_CDB
+ h_power_ω_A
+ h_power_ω_B
+ h_sphere_A_radius
+ h_sphere_B_radius
+ h_sphere_ω_radius_nonneg
+ h_tangent_at_K_ω
+ h_tangent_at_L_ω
+ h_ω
+ hx
+ imo2012_q5
+ indep_ABX
+ inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero
+ mem_interior_of_lineMap_closedInterior_interior
+ mem_interior_of_lineMap_face_interior_face_interior_compl
+ mem_interior_of_lineMap_point_faceOpposite_interior
+ ne_of_affineIndependent_sbtw_sbtw
+ not_col_ABC
+ notcol_KXL
+ pow_X_A
+ pow_X_B
+ pow_X_eq
+ power_A_B
+ power_B_A
+ result
+ sbtw_K'KA
+ sbtw_L'LB
+ sbtw_orthogonalProjection_of_angle_ge_pi_div_two
+ someOrientation
+ sphere_A
+ sphere_B
+ sphere_a
+ sphere_b
+ sphere_ω
+ symm
+ symm_A_eq_B
+ symm_B_eq_A
+ symm_K'_eq_L'
+ symm_K_eq_L
+ symm_L'_eq_K'
+ symm_L_eq_K
+ v_XK
+ v_XK_def
+ v_XL
+ v_XL_def

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Geometry/Euclidean/Altitude): add inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero #34157
• feat(Analysis/Convex/Between): add lemmas on convex combination of mem simplex interior #34156
• feat(Geometry/Euclidean/Triangle): add altitudeFoot lies strictly between endpoints for an obtuse angle #34155
• [Merged by Bors] - feat(LinearAlgebra/AffineSpace/Independent): Add affineCombination_eq_lineMap_iff_weight_lineMap #33852
• [Merged by Bors] - feat(Geometry/Euclidean/Sphere/Power): Add theorem about cospherical points on two intersecting lines #33479
• feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness #31500
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.