`Compfiles/Imo2019P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

63 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2019, Problem 2

In triangle ABC, point A₁ lies on side BC and point B₁ lies on side AC. Let P and Q be points on segments AA₁ and BB₁, respectively, such that PQ is parallel to AB. Let P₁ be a point on line PB₁, such that B₁ lies strictly between P and P₁, and ∠PP₁C = ∠BAC. Similarly, let Q₁ be a point on line QA₁, such that A₁ lies strictly between Q and Q₁, and ∠CQ₁Q = ∠CBA.

Prove that points P, Q, P₁, and Q₁ are concyclic.

Imports (3)

Imported by 1 file

Compfiles.lean

structure Imo2019P2.Imo2019q2Cfg A configuration satisfying the conditions of the problem line 94 source
Source documentation
A configuration satisfying the conditions of the problem. We define this structure to avoid passing many hypotheses around as we build up information about the configuration; the final result for a statement of the problem not using this structure is then deduced from one in terms of this structure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor
3 instances, coercions and auxiliary constants left out.
```
structure Imo2019q2Cfg where
…
```
def Imo2019P2.someOrientation A default choice of orientation, for lemmas that need to pick one line 115 source
Source documentation
A default choice of orientation, for lemmas that need to pick one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Module.Oriented, Fin
Proof uses: Module.Oriented.mk, Module.Basis.orientation, Module.finBasisOfFinrankEq
34 instances, coercions and auxiliary constants left out.
```
def someOrientation  [hd2 : Fact (finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2) :=
…
```
def Imo2019P2.Imo2019q2Cfg.symm The configuration has symmetry, allowing results proved for one point to be applied for another (where the informal solution says "similarly") line 126 source
Source documentation
The configuration has symmetry, allowing results proved for one point to be applied for another (where the informal solution says "similarly").

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg
Proof uses: Imo2019P2.Imo2019q2Cfg.mk, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.B₁, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.P₁, Imo2019P2.Imo2019q2Cfg.wbtw_A_B₁_C, Imo2019P2.Imo2019q2Cfg.wbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.wbtw_B_Q_B₁, Imo2019P2.Imo2019q2Cfg.wbtw_A_P_A₁, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, Imo2019P2.Imo2019q2Cfg.C_ne_Q₁, Imo2019P2.Imo2019q2Cfg.sbtw_P_B₁_P₁, Imo2019P2.Imo2019q2Cfg.C_ne_P₁
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def symm : Imo2019q2Cfg V Pt where
…
```
Mentions: Imo2019P2.Imo2019q2Cfg
theorem Imo2019P2.Imo2019q2Cfg.A_ne_B line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Ne, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.B
Proof uses: Function.Injective.ne, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Imo2019P2.Imo2019q2Cfg.C, Matrix.vecEmpty, AffineIndependent.injective, Imo2019P2.Imo2019q2Cfg.affineIndependent_ABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.B_ne_C line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Ne, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Function.Injective.ne, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Imo2019P2.Imo2019q2Cfg.A, Matrix.vecEmpty, AffineIndependent.injective, Imo2019P2.Imo2019q2Cfg.affineIndependent_ABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.not_collinear_ABC line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Not, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.B, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Iff.mp, AffineIndependent, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, affineIndependent_iff_not_collinear_set, Imo2019P2.Imo2019q2Cfg.affineIndependent_ABC
24 instances, coercions and auxiliary constants left out.
def Imo2019P2.Imo2019q2Cfg.triangleABC ABC as a Triangle line 169 source
Source documentation
ABC as a Triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Affine.Triangle
Proof uses: Affine.Simplex.mk, OfNat.ofNat, Nat, Matrix.vecCons, Nat.succ, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.C, Matrix.vecEmpty, Imo2019P2.Imo2019q2Cfg.affineIndependent_ABC
19 instances, coercions and auxiliary constants left out.
```
def triangleABC : Triangle ℝ Pt :=
…
```
theorem Imo2019P2.Imo2019q2Cfg.A_mem_circumsphere line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Membership.mem, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.A
Proof uses: Affine.Simplex.mem_circumsphere, Fin, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.B_mem_circumsphere line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Membership.mem, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.B
Proof uses: Affine.Simplex.mem_circumsphere, Fin, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.C_mem_circumsphere line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Membership.mem, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Affine.Simplex.mem_circumsphere, Fin, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.symm_triangleABC line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Eq, Affine.Triangle, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.symm, Affine.Simplex.reindex, OfNat.ofNat, Nat, Equiv.swap, Fin, HAdd.hAdd
Proof uses: Affine.Simplex.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, Affine.Simplex.points, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail, False.elim and 3 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.symm_triangleABC_circumsphere line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Eq, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.symm
Proof uses: Eq.mpr, Affine.Simplex.reindex, Equiv.swap, Fin, HAdd.hAdd, id, congrArg, Affine.Triangle, Imo2019P2.Imo2019q2Cfg.symm_triangleABC, Affine.Simplex.circumsphere_reindex, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2019P2.Imo2019q2Cfg.A₂ A₂ is the second point of intersection of the ray AA₁ with the circumcircle of ABC line 189 source
Source documentation
A₂ is the second point of intersection of the ray AA₁ with the circumcircle of ABC.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg
Proof uses: EuclideanGeometry.Sphere.secondInter, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.A, VSub.vsub, Imo2019P2.Imo2019q2Cfg.A₁
11 instances, coercions and auxiliary constants left out.
```
def A₂ : Pt :=
…
```
def Imo2019P2.Imo2019q2Cfg.B₂ B₂ is the second point of intersection of the ray BB₁ with the circumcircle of ABC line 193 source
Source documentation
B₂ is the second point of intersection of the ray BB₁ with the circumcircle of ABC.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg
Proof uses: EuclideanGeometry.Sphere.secondInter, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.B, VSub.vsub, Imo2019P2.Imo2019q2Cfg.B₁
11 instances, coercions and auxiliary constants left out.
```
def B₂ : Pt :=
…
```
theorem Imo2019P2.Imo2019q2Cfg.A₂_mem_circumsphere line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Membership.mem, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Iff.mpr, EuclideanGeometry.Sphere.secondInter, Imo2019P2.Imo2019q2Cfg.A, VSub.vsub, Imo2019P2.Imo2019q2Cfg.A₁, EuclideanGeometry.Sphere.secondInter_mem, Imo2019P2.Imo2019q2Cfg.A_mem_circumsphere
14 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.B₂_mem_circumsphere line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Membership.mem, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.B₂
Proof uses: Iff.mpr, EuclideanGeometry.Sphere.secondInter, Imo2019P2.Imo2019q2Cfg.B, VSub.vsub, Imo2019P2.Imo2019q2Cfg.B₁, EuclideanGeometry.Sphere.secondInter_mem, Imo2019P2.Imo2019q2Cfg.B_mem_circumsphere
14 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.symm_A₂ line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Eq, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.symm, Imo2019P2.Imo2019q2Cfg.B₂
Proof uses: id, EuclideanGeometry.Sphere.secondInter, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.A, VSub.vsub, Imo2019P2.Imo2019q2Cfg.A₁, Eq.mpr, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.B₁, congrFun', congrArg, EuclideanGeometry.Sphere, Imo2019P2.Imo2019q2Cfg.symm_triangleABC_circumsphere, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.QP_parallel_BA line 204 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, AffineSubspace.Parallel, affineSpan, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.Q, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A
Proof uses: Eq.mpr, id, Eq, congrArg, Set.pair_comm, Imo2019P2.Imo2019q2Cfg.PQ_parallel_AB
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.A_ne_A₁ line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Ne, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.A₁
Proof uses: Eq, Not, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.B, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.not_collinear_ABC, Eq.mp, congrArg, Set.insert_comm, Wbtw.collinear, Imo2019P2.Imo2019q2Cfg.wbtw_B_A₁_C
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.collinear_PAA₁A₂ line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.A₁, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Eq.mpr, EuclideanGeometry.Sphere.secondInter, Affine.Simplex.circumsphere, OfNat.ofNat, Nat, Imo2019P2.Imo2019q2Cfg.triangleABC, VSub.vsub, id, Eq, congrArg, Imo2019P2.Imo2019q2Cfg.A₂.eq_1, propext, Collinear.collinear_insert_iff_of_ne, EuclideanGeometry.Sphere.secondInter_collinear, Set.mem_insert, Set.mem_insert_of_mem, Imo2019P2.Imo2019q2Cfg.A_ne_A₁, Set.insert_comm, Wbtw.collinear, Imo2019P2.Imo2019q2Cfg.wbtw_A_P_A₁
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.A₁_ne_C line 220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Ne, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Eq, Sbtw, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, EuclideanGeometry.angle, OfNat.ofNat, Sbtw.angle₂₃₁_eq_zero, Eq.mp, congrArg, EuclideanGeometry.angle_ne_zero_of_not_collinear, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.not_collinear_ABC, EuclideanGeometry.angle_comm, Imo2019P2.Imo2019q2Cfg.angle_CQ₁Q_eq_angle_CBA
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.B₁_ne_C line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Ne, Imo2019P2.Imo2019q2Cfg.B₁, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Imo2019P2.Imo2019q2Cfg.A₁_ne_C, Imo2019P2.Imo2019q2Cfg.symm
6 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Not, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.C, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.Q
Proof uses: Imo2019P2.Imo2019q2Cfg.Q₁, affineSpan_pair_le_of_mem_of_mem, Imo2019P2.Imo2019q2Cfg.A₁, Wbtw.mem_affineSpan, Wbtw.symm, Imo2019P2.Imo2019q2Cfg.wbtw_B_A₁_C, Sbtw.right_mem_affineSpan, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, Collinear, collinear_triple_of_mem_affineSpan_pair, left_mem_affineSpan_pair, Imo2019P2.Imo2019q2Cfg.not_collinear_ABC, Or.elim, Eq, EuclideanGeometry.angle, Imo2019P2.Imo2019q2Cfg.A, OfNat.ofNat, Real.pi, Eq.mp, Or and 10 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.Q_ne_B line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Ne, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B
Proof uses: Eq, Not, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.C, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB, Eq.mp, congrArg, right_mem_affineSpan_pair
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁ line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, AffineSubspace.SOppSide, affineSpan, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.C, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.Q₁
Proof uses: Sbtw.sOppSide_of_notMem_of_mem, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB, Wbtw.mem_affineSpan, Wbtw.symm, Imo2019P2.Imo2019q2Cfg.wbtw_B_A₁_C
30 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign line 257 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, SignType, Real.Angle.sign, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B and 1 more
Proof uses: Eq.mpr, Imo2019P2.Imo2019q2Cfg.A₁, id, congrArg, Real.Angle, Eq.symm, Sbtw.oangle_eq_right, Sbtw.symm, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, Neg.neg, AffineSubspace.SOppSide.oangle_sign_eq_neg, affineSpan, Insert.insert, Set, Singleton.singleton, left_mem_affineSpan_pair, Wbtw.mem_affineSpan, Wbtw.symm, Imo2019P2.Imo2019q2Cfg.wbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁ and 14 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, Real.Angle, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A
Proof uses: EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq, Imo2019P2.Imo2019q2Cfg.angle_CQ₁Q_eq_angle_CBA, Imo2019P2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign
26 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.A₁_ne_B line 280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.B
Proof uses: Wbtw, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.wbtw_A_P_A₁, AffineSubspace, affineSpan, Insert.insert, Set, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.Q, Eq.mpr, Submodule, AffineSubspace.direction, id, congrArg, propext, AffineSubspace.eq_iff_direction_eq_of_mem, left_mem_affineSpan_pair, Wbtw.mem_affineSpan, Eq.mp and 44 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.sbtw_B_A₁_C line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Sbtw, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.C
Proof uses: And.intro, Wbtw, And, Ne, Imo2019P2.Imo2019q2Cfg.wbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.A₁_ne_B, Imo2019P2.Imo2019q2Cfg.A₁_ne_C
26 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.sbtw_A_B₁_C line 312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Sbtw, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.B₁, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Imo2019P2.Imo2019q2Cfg.sbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.symm
23 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂ line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Sbtw, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: EuclideanGeometry.Sphere.sbtw_secondInter, Affine.Simplex.circumsphere, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.A_mem_circumsphere, Eq.mpr, LT.lt, Dist.dist, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.radius, Max.max, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.C, eq_of_heq, LT, HEq, Eq.refl, HEq.refl, Eq.symm, id, Affine.Simplex.points and 14 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.sbtw_B_B₁_B₂ line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Sbtw, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.B₁, Imo2019P2.Imo2019q2Cfg.B₂
Proof uses: Eq.mpr, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.symm, id, congrArg, Eq.symm, Imo2019P2.Imo2019q2Cfg.symm_A₂, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.A₂_ne_A line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.A
Proof uses: Ne.symm, Sbtw.left_ne_right, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂
24 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.A₂_ne_P line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.P
Proof uses: Ne.symm, Sbtw.trans_wbtw_left_ne, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂, Imo2019P2.Imo2019q2Cfg.wbtw_A_P_A₁
38 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.A₂_ne_B line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.B
Proof uses: Sbtw, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.C, Singleton.singleton, collinear_insert_insert_of_mem_affineSpan_pair, Sbtw.left_mem_affineSpan, Eq.mp, congrArg, Sbtw.right_mem_affineSpan, Imo2019P2.Imo2019q2Cfg.sbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.not_collinear_ABC, Collinear.subset, of_eq_true, LE.le, Eq.trans and 9 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.A₂_ne_C line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.C
Proof uses: Sbtw, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.B, Singleton.singleton, collinear_insert_insert_of_mem_affineSpan_pair, Sbtw.left_mem_affineSpan, Eq.mp, congrArg, Imo2019P2.Imo2019q2Cfg.sbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.not_collinear_ABC, Collinear.subset, of_eq_true, LE.le, Eq.trans, And and 8 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.B₂_ne_B line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.B₂, Imo2019P2.Imo2019q2Cfg.B
Proof uses: Eq.mpr, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.symm, id, congrArg, Eq.symm, Imo2019P2.Imo2019q2Cfg.symm_A₂, Imo2019P2.Imo2019q2Cfg.A₂_ne_A
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.B₂_ne_Q line 350 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.B₂, Imo2019P2.Imo2019q2Cfg.Q
Proof uses: Eq.mpr, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.symm, id, congrArg, Eq.symm, Imo2019P2.Imo2019q2Cfg.symm_A₂, Imo2019P2.Imo2019q2Cfg.A₂_ne_P
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.B₂_ne_A₂ line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.B₂, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Sbtw, Affine.Simplex.points, Imo2019P2.Imo2019q2Cfg.triangleABC, Fin, HAdd.hAdd, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_B_A₁_C, Imo2019P2.Imo2019q2Cfg.B₁, Imo2019P2.Imo2019q2Cfg.sbtw_A_B₁_C, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Singleton.singleton, EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan, Affine.Simplex.circumsphere, Eq.mpr, id, congrArg and 12 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.wbtw_B_Q_B₂ line 363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Wbtw, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B₂
Proof uses: Wbtw.trans_left, Imo2019P2.Imo2019q2Cfg.B₁, Sbtw.wbtw, Imo2019P2.Imo2019q2Cfg.sbtw_B_B₁_B₂, Imo2019P2.Imo2019q2Cfg.wbtw_B_Q_B₁
27 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂ line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Module.Oriented, Fin, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.A₂ and 2 more
Proof uses: EuclideanGeometry.two_zsmul_oangle_of_parallel, Imo2019P2.Imo2019q2Cfg.QP_parallel_BA, Eq.mpr, AffineSubspace.Parallel, affineSpan, Insert.insert, Set, Singleton.singleton, eq_of_heq, Ring, AddCommGroup, Module, AddTorsor, AffineSubspace, HEq, Eq.refl, HEq.refl, Eq.symm, Imo2019P2.Imo2019q2Cfg.A₁, id and 15 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂ line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Not, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Module.Oriented, Fin, Imo2019P2.someOrientation, Eq.mpr, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A, id, congrArg, propext, EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, AffineIndependent, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Eq.symm, affineIndependent_iff_not_collinear_set, EuclideanGeometry.Cospherical, EuclideanGeometry.Cospherical.subset, Metric.sphere and 23 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂ line 393 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Ne, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Sbtw, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.A, Singleton.singleton, Sbtw.right_mem_affineSpan, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂, affineSpan_pair_le_of_left_mem, Sbtw.left_mem_affineSpan, Eq.mp, congrArg, Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂, collinear_triple_of_mem_affineSpan_pair, Imo2019P2.Imo2019q2Cfg.P and 2 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.affineIndependent_QPA₂ line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, AffineIndependent, Fin, Nat.succ, Matrix.vecCons, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.A₂, Matrix.vecEmpty
Proof uses: Iff.mpr, Not, Collinear, Insert.insert, Set, Singleton.singleton, affineIndependent_iff_not_collinear_set, Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
27 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.affineIndependent_PQB₂ line 406 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, AffineIndependent, Fin, Nat.succ, Matrix.vecCons, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B₂, Matrix.vecEmpty
Proof uses: Eq.mpr, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.symm, id, congrArg, Eq.symm, Imo2019P2.Imo2019q2Cfg.symm_A₂, Imo2019P2.Imo2019q2Cfg.affineIndependent_QPA₂
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2019P2.Imo2019q2Cfg.triangleQPA₂ QPA₂ as a Triangle line 410 source
Source documentation
QPA₂ as a Triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Affine.Triangle
Proof uses: Affine.Simplex.mk, Matrix.vecCons, Nat.succ, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.A₂, Matrix.vecEmpty, Imo2019P2.Imo2019q2Cfg.affineIndependent_QPA₂
24 instances, coercions and auxiliary constants left out.
```
def triangleQPA₂ : Triangle ℝ Pt := ⟨_, cfg.affineIndependent_QPA₂⟩
```
def Imo2019P2.Imo2019q2Cfg.trianglePQB₂ PQB₂ as a Triangle line 413 source
Source documentation
PQB₂ as a Triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Affine.Triangle
Proof uses: Affine.Simplex.mk, Matrix.vecCons, Nat.succ, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B₂, Matrix.vecEmpty, Imo2019P2.Imo2019q2Cfg.affineIndependent_PQB₂
24 instances, coercions and auxiliary constants left out.
```
def trianglePQB₂ : Triangle ℝ Pt := ⟨_, cfg.affineIndependent_PQB₂⟩
```
theorem Imo2019P2.Imo2019q2Cfg.symm_triangleQPA₂ line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Affine.Triangle, Imo2019P2.Imo2019q2Cfg.triangleQPA₂, Imo2019P2.Imo2019q2Cfg.symm, Imo2019P2.Imo2019q2Cfg.trianglePQB₂
Proof uses: id, Eq.mpr, Affine.Simplex.mk, Matrix.vecCons, Nat.succ, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B₂, Matrix.vecEmpty, Imo2019P2.Imo2019q2Cfg.affineIndependent_PQB₂, Imo2019P2.Imo2019q2Cfg.A₂, Fin, HAdd.hAdd, AffineIndependent, congrArg, congrFun', Affine.Simplex, Affine.Simplex.mk.congr_simp, Affine.Simplex.ext, List and 21 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Imo2019P2.Imo2019q2Cfg.ω ω is the circle containing Q, P and A₂, which will be shown also to contain B₂, P₁ and Q₁ line 420 source
Source documentation
ω is the circle containing Q, P and A₂, which will be shown also to contain B₂, P₁ and Q₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, EuclideanGeometry.Sphere
Proof uses: Affine.Simplex.circumsphere, Imo2019P2.Imo2019q2Cfg.triangleQPA₂
20 instances, coercions and auxiliary constants left out.
```
def ω : Sphere Pt := cfg.triangleQPA₂.circumsphere
```
theorem Imo2019P2.Imo2019q2Cfg.P_mem_ω line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Membership.mem, EuclideanGeometry.Sphere, Imo2019P2.Imo2019q2Cfg.ω, Imo2019P2.Imo2019q2Cfg.P
Proof uses: Affine.Simplex.mem_circumsphere, Imo2019P2.Imo2019q2Cfg.triangleQPA₂, Fin, HAdd.hAdd
26 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.Q_mem_ω line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Membership.mem, EuclideanGeometry.Sphere, Imo2019P2.Imo2019q2Cfg.ω, Imo2019P2.Imo2019q2Cfg.Q
Proof uses: Affine.Simplex.mem_circumsphere, Imo2019P2.Imo2019q2Cfg.triangleQPA₂, Fin, HAdd.hAdd
26 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂ line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Module.Oriented, Fin, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.A₂ and 1 more
Proof uses: Trans.trans, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, EuclideanGeometry.Sphere.two_zsmul_oangle_eq, Affine.Simplex.circumsphere, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.B_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.A_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.B₂_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.A₂_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.A_ne_B, Ne.symm, Imo2019P2.Imo2019q2Cfg.A₂_ne_A, Imo2019P2.Imo2019q2Cfg.B₂_ne_B, Imo2019P2.Imo2019q2Cfg.B₂_ne_A₂, Eq.mpr, id, congrArg, Wbtw.oangle_eq_left and 4 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.cospherical_QPB₂A₂ line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, EuclideanGeometry.Cospherical, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.B₂, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Module.Oriented, Fin, Imo2019P2.someOrientation, EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂, Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
25 instances, coercions and auxiliary constants left out.
theorem Imo2019P2.Imo2019q2Cfg.symm_ω line 453 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, EuclideanGeometry.Sphere, Imo2019P2.Imo2019q2Cfg.ω, Imo2019P2.Imo2019q2Cfg.symm
Proof uses: Eq.mpr, Affine.Simplex.circumsphere, Imo2019P2.Imo2019q2Cfg.triangleQPA₂, id, congrArg, Imo2019P2.Imo2019q2Cfg.ω.eq_1, Imo2019P2.Imo2019q2Cfg.trianglePQB₂, Affine.Triangle, Imo2019P2.Imo2019q2Cfg.symm_triangleQPA₂, EuclideanGeometry.circumsphere_eq_of_cospherical, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.B₂, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.A₂, Fact.out, Imo2019P2.Imo2019q2Cfg.cospherical_QPB₂A₂, of_eq_true and 26 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Module.Oriented, Fin, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.A₁ and 2 more
Proof uses: Trans.trans, Eq.mpr, id, congrArg, Sbtw.oangle_eq_right, Sbtw.symm, Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂, Eq.refl, EuclideanGeometry.Sphere.two_zsmul_oangle_eq, Affine.Simplex.circumsphere, Imo2019P2.Imo2019q2Cfg.triangleABC, Imo2019P2.Imo2019q2Cfg.C_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.A₂_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.B_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.A_mem_circumsphere, Imo2019P2.Imo2019q2Cfg.A₂_ne_C, Imo2019P2.Imo2019q2Cfg.A₂_ne_A, Imo2019P2.Imo2019q2Cfg.B_ne_C, Ne.symm, Imo2019P2.Imo2019q2Cfg.A_ne_B
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁ line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Module.Oriented, Fin, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.A₂, Imo2019P2.Imo2019q2Cfg.A₁ and 1 more
Proof uses: Trans.trans, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA, Eq.mpr, id, congrArg, Imo2019P2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA, Eq.refl, Sbtw.oangle_eq_right, Sbtw.symm, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁
44 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.not_collinear_CA₂A₁ line 486 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Not, Collinear, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.A₂, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.A₁
Proof uses: Module.Oriented, Fin, Imo2019P2.someOrientation, Eq.mpr, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A, id, congrArg, propext, EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA, Set.pair_comm, Set.insert_comm, Imo2019P2.Imo2019q2Cfg.not_collinear_ABC
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂ line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, EuclideanGeometry.Cospherical, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.A₁, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.C, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.A₂
Proof uses: Module.Oriented, Fin, Imo2019P2.someOrientation, EuclideanGeometry.Cospherical.subset, of_eq_true, LE.le, Eq.trans, And, Membership.mem, True, congr, congrArg, Or, eq_self, or_true, true_or, and_self, EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁, Imo2019P2.Imo2019q2Cfg.not_collinear_CA₂A₁
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂ line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Module.Oriented, Fin, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.Q₁, Imo2019P2.Imo2019q2Cfg.A₂ and 1 more
Proof uses: Trans.trans, Imo2019P2.Imo2019q2Cfg.B, Imo2019P2.Imo2019q2Cfg.A, Imo2019P2.Imo2019q2Cfg.C, Imo2019P2.Imo2019q2Cfg.A₁, Eq.mpr, id, congrArg, Sbtw.oangle_eq_left, Sbtw.symm, Imo2019P2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁, Eq.refl, EuclideanGeometry.Cospherical.two_zsmul_oangle_eq, Imo2019P2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂, Sbtw.right_ne, Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂, Ne.symm, Imo2019P2.Imo2019q2Cfg.A₁_ne_C, Imo2019P2.Imo2019q2Cfg.A₂_ne_C, Imo2019P2.Imo2019q2Cfg.sbtw_B_A₁_C and 12 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.Q₁_mem_ω line 523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Membership.mem, EuclideanGeometry.Sphere, Imo2019P2.Imo2019q2Cfg.ω, Imo2019P2.Imo2019q2Cfg.Q₁
Proof uses: Module.Oriented, Fin, Imo2019P2.someOrientation, Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq, Imo2019P2.Imo2019q2Cfg.triangleQPA₂, of_decide_eq_true, Ne, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.P₁_mem_ω line 528 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Membership.mem, EuclideanGeometry.Sphere, Imo2019P2.Imo2019q2Cfg.ω, Imo2019P2.Imo2019q2Cfg.P₁
Proof uses: Eq.mpr, Imo2019P2.Imo2019q2Cfg.symm, id, congrArg, Eq.symm, Imo2019P2.Imo2019q2Cfg.symm_ω, Imo2019P2.Imo2019q2Cfg.Q₁_mem_ω
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2019P2.Imo2019q2Cfg.result line 530 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2019P2.Imo2019q2Cfg, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, EuclideanGeometry.Concyclic, Insert.insert, Set, Imo2019P2.Imo2019q2Cfg.P, Imo2019P2.Imo2019q2Cfg.Q, Imo2019P2.Imo2019q2Cfg.P₁, Singleton.singleton, Imo2019P2.Imo2019q2Cfg.Q₁
Proof uses: EuclideanGeometry.Concyclic.mk, Iff.mpr, EuclideanGeometry.Cospherical, Exists, EuclideanGeometry.Sphere, LE.le, Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.radius, EuclideanGeometry.cospherical_iff_exists_sphere, Exists.intro, Imo2019P2.Imo2019q2Cfg.ω, of_eq_true, Eq.trans, And, Membership.mem, True, congr, congrArg, Dist.dist and 7 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
problem Imo2019P2.imo2019_p2 line 543 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, AffineIndependent, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Wbtw, AffineSubspace.Parallel, affineSpan, Insert.insert, Set and 5 more
Proof uses: Imo2019P2.Imo2019q2Cfg.result, Imo2019P2.Imo2019q2Cfg.mk
30 instances, coercions and auxiliary constants left out.