Compfiles/Imo2012P5.lean

GitHub source file

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

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

57 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2012, Problem 5

Let ABC be a triangle with ∠BCA = 90°, and let D be the foot of the altitude from C. Let X be a point in the interior of the segment CD. Let K be the point on the segment AX such that BK = BC. Similarly, let L be the point on the segment BX such that AL = AC. Let M be the point of intersection of AL and BK. Show that MK = ML.

Imports (5)
Imported by 1 file
  1. theorem cospherical_or_collinear_of_mul_dist_eq_mul_dist_of_sbtw The converse of the Intersecting Chords Theorem, stated with Sbtw line 52 source

    Source documentation

    The converse of the Intersecting Chords Theorem, stated with Sbtw.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Eq, HMul.hMul, Dist.dist, Sbtw, Or, EuclideanGeometry.Cospherical, Insert.insert, Set, Singleton.singleton, Collinear

    Proof uses: Or.imp, AffineIndependent, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Not, Affine.Simplex, Affine.Simplex.mk, EuclideanGeometry.Sphere.secondInter, Affine.Simplex.circumsphere, VSub.vsub, Eq.mpr, id, congrArg, propext, sbtw_comm, EuclideanGeometry.Sphere.sbtw_secondInter and 70 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

    Open to load the checked before-and-after goal states.

    theorem cospherical_or_collinear_of_mul_dist_eq_mul_dist_of_sbtw
  {a b c d p : P} (h : dist a p * dist b p = dist c p * dist d p)
  (hapb : Sbtw ℝ a p b) (hcpd : Sbtw ℝ c p d) :
    Cospherical {a, b, c, d} ∨ Collinear ℝ {a, b, c, d} := by
…

    Mentions: P, h

  2. structure Imo2012P5.Imo2012P5Cfg A configuration satisfying the conditions of the problem line 120 source

    Source documentation

    A configuration satisfying the conditions of the problem.

    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 Imo2012P5Cfg where
…
  3. def Imo2012P5.Imo2012P5Cfg.symm The symmetry of the configuration line 145 source

    Source documentation

    The symmetry of the configuration.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg

    Proof uses: Imo2012P5.Imo2012P5Cfg.mk, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.D, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.M, Imo2012P5.Imo2012P5Cfg.sbtw_CXD, Imo2012P5.Imo2012P5Cfg.wbtw_BLX, Imo2012P5.Imo2012P5Cfg.AL_eq_AC, Imo2012P5.Imo2012P5Cfg.wbtw_AKX, Imo2012P5.Imo2012P5Cfg.BK_eq_BC

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

    def symm : Imo2012P5Cfg V P where
…

    Mentions: Imo2012P5.Imo2012P5Cfg, P

  4. theorem Imo2012P5.Imo2012P5Cfg.A_ne_K line 166 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Ne, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.K

    Proof uses: Eq, Dist.dist, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.C, Eq.rec, Imo2012P5.Imo2012P5Cfg.BK_eq_BC, Eq.symm, HMul.hMul, HAdd.hAdd, Iff.mpr, EuclideanGeometry.angle, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, Imo2012P5.Imo2012P5Cfg.angle_BCA, Eq.mp, Eq.trans, congrFun' and 17 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  5. theorem Imo2012P5.Imo2012P5Cfg.B_ne_L line 174 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Ne, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.L

    Proof uses: Imo2012P5.Imo2012P5Cfg.A_ne_K, Imo2012P5.Imo2012P5Cfg.symm

    6 instances, coercions and auxiliary constants left out.

  6. theorem Imo2012P5.Imo2012P5Cfg.D_eq_orthogonalProjection line 177 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, Imo2012P5.Imo2012P5Cfg.D, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.A, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.B, ContinuousAffineMap, Subtype, Submodule, AffineSubspace.direction and 2 more

    Proof uses: Eq.mpr, Affine.Simplex.altitudeFoot, OfNat.ofNat, Nat, Affine.Simplex.mk, Matrix.vecCons, Nat.succ, Matrix.vecEmpty, Imo2012P5.Imo2012P5Cfg.affineIndependent_ABC, Fin, HAdd.hAdd, id, congrFun', congrArg, Imo2012P5.Imo2012P5Cfg.D_eq_altitudeFoot, Set.range, HSub.hSub, Affine.Simplex.points, Affine.Simplex.faceOpposite, Affine.Simplex.orthogonalProjectionSpan and 17 more

    107 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  7. def Imo2012P5.Imo2012P5Cfg.C' The reflection of C in line AB line 185 source

    Source documentation

    The reflection of C in line AB.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg

    Proof uses: AffineIsometryEquiv, EuclideanGeometry.reflection, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.A, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.C

    20 instances, coercions and auxiliary constants left out.

    noncomputable def C' : P :=
…

    Mentions: P

  8. theorem Imo2012P5.Imo2012P5Cfg.C'_def line 188 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, Imo2012P5.Imo2012P5Cfg.C', AffineIsometryEquiv, EuclideanGeometry.reflection, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.A, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.B, AffineSubspace.direction, Subtype, Membership.mem, Submodule and 1 more

    Proof uses: rfl

    37 instances, coercions and auxiliary constants left out.

  9. theorem Imo2012P5.Imo2012P5Cfg.symm_C' line 191 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, Imo2012P5.Imo2012P5Cfg.C', Imo2012P5.Imo2012P5Cfg.symm

    Proof uses: id, of_eq_true, AffineIsometryEquiv, EuclideanGeometry.reflection, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.B, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.A, AffineSubspace.direction, Subtype, Membership.mem, Submodule, Imo2012P5.Imo2012P5Cfg.C, Eq.trans, AffineSubspace, Nonempty, AffineSubspace.affineSpan_pair_comm, Submodule.HasOrthogonalProjection and 5 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  10. theorem Imo2012P5.Imo2012P5Cfg.D_eq_midpoint_CC' line 196 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, Imo2012P5.Imo2012P5Cfg.D, midpoint, Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.C'

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, midpoint_self, VSub.vsub, propext, midpoint_eq_midpoint_iff_vsub_eq_vsub, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.A, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.B, ContinuousAffineMap, Subtype, Submodule, AffineSubspace.direction and 9 more

    83 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  11. theorem Imo2012P5.Imo2012P5Cfg.sbtw_CXC' line 200 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.C'

    Proof uses: Wbtw.trans_sbtw_left, Imo2012P5.Imo2012P5Cfg.D, Eq.rec, midpoint, Eq, Wbtw, wbtw_midpoint, Eq.symm, Imo2012P5.Imo2012P5Cfg.D_eq_midpoint_CC', Imo2012P5.Imo2012P5Cfg.sbtw_CXD

    49 instances, coercions and auxiliary constants left out.

  12. def Imo2012P5.Imo2012P5Cfg.ωA line 203 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere

    Proof uses: EuclideanGeometry.Sphere.mk, Imo2012P5.Imo2012P5Cfg.A, Dist.dist, Imo2012P5.Imo2012P5Cfg.C

    7 instances, coercions and auxiliary constants left out.

  13. def Imo2012P5.Imo2012P5Cfg.ωB line 205 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere

    Proof uses: EuclideanGeometry.Sphere.mk, Imo2012P5.Imo2012P5Cfg.B, Dist.dist, Imo2012P5.Imo2012P5Cfg.C

    7 instances, coercions and auxiliary constants left out.

  14. theorem Imo2012P5.Imo2012P5Cfg.C_mem_ωA line 207 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωA, Imo2012P5.Imo2012P5Cfg.C

    Proof uses: rfl, Dist.dist, EuclideanGeometry.Sphere.center

    8 instances, coercions and auxiliary constants left out.

  15. theorem Imo2012P5.Imo2012P5Cfg.C_mem_ωB line 209 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.C

    Proof uses: rfl, Dist.dist, EuclideanGeometry.Sphere.center

    8 instances, coercions and auxiliary constants left out.

  16. theorem Imo2012P5.Imo2012P5Cfg.C'_mem_ωA line 211 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωA, Imo2012P5.Imo2012P5Cfg.C'

    Proof uses: id, Eq.mpr, Eq, Dist.dist, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.C, congrArg, dist_comm, AffineIsometryEquiv, EuclideanGeometry.reflection, affineSpan, Insert.insert, Set, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.B, AffineSubspace.direction, Subtype, Submodule, Imo2012P5.Imo2012P5Cfg.C'_def, EuclideanGeometry.dist_reflection_eq_of_mem and 1 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  17. theorem Imo2012P5.Imo2012P5Cfg.C'_mem_ωB line 217 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.C'

    Proof uses: Eq.rec, Imo2012P5.Imo2012P5Cfg.symm, Eq, Imo2012P5.Imo2012P5Cfg.C'_mem_ωA, Imo2012P5.Imo2012P5Cfg.symm_C'

    8 instances, coercions and auxiliary constants left out.

  18. theorem Imo2012P5.Imo2012P5Cfg.XA_lt_radius_ωA line 220 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, LT.lt, Dist.dist, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.A, EuclideanGeometry.Sphere.radius, Imo2012P5.Imo2012P5Cfg.ωA

    Proof uses: Eq, Imo2012P5.Imo2012P5Cfg.C', Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.C'_mem_ωA, id, Eq.mp, Max.max, congrArg, Eq.trans, max_self, Sbtw.dist_lt_max_dist, Imo2012P5.Imo2012P5Cfg.sbtw_CXC'

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  19. theorem Imo2012P5.Imo2012P5Cfg.XB_lt_radius_ωB line 225 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, LT.lt, Dist.dist, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.B, EuclideanGeometry.Sphere.radius, Imo2012P5.Imo2012P5Cfg.ωB

    Proof uses: Imo2012P5.Imo2012P5Cfg.XA_lt_radius_ωA, Imo2012P5.Imo2012P5Cfg.symm

    8 instances, coercions and auxiliary constants left out.

  20. theorem Imo2012P5.Imo2012P5Cfg.K_mem_ωB line 228 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.K

    Proof uses: id, Eq.mpr, Eq, Dist.dist, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.C, congr, congrArg, dist_comm, Imo2012P5.Imo2012P5Cfg.BK_eq_BC

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  21. theorem Imo2012P5.Imo2012P5Cfg.L_mem_ωA line 232 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωA, Imo2012P5.Imo2012P5Cfg.L

    Proof uses: Imo2012P5.Imo2012P5Cfg.K_mem_ωB, Imo2012P5.Imo2012P5Cfg.symm

    7 instances, coercions and auxiliary constants left out.

  22. def Imo2012P5.Imo2012P5Cfg.K' The second point on line AX with BC = BK' line 236 source

    Source documentation

    The second point on line AX with BC = BK'.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg

    Proof uses: EuclideanGeometry.Sphere.secondInter, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.K, VSub.vsub, Imo2012P5.Imo2012P5Cfg.X

    10 instances, coercions and auxiliary constants left out.

    noncomputable def K' := cfg.ωB.secondInter cfg.K (cfg.X -ᵥ cfg.K)
  23. def Imo2012P5.Imo2012P5Cfg.L' The second point on line BX with AC = AL' line 239 source

    Source documentation

    The second point on line BX with AC = AL'.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg

    Proof uses: EuclideanGeometry.Sphere.secondInter, Imo2012P5.Imo2012P5Cfg.ωA, Imo2012P5.Imo2012P5Cfg.L, VSub.vsub, Imo2012P5.Imo2012P5Cfg.X

    10 instances, coercions and auxiliary constants left out.

    noncomputable def L' := cfg.ωA.secondInter cfg.L (cfg.X -ᵥ cfg.L)
  24. theorem Imo2012P5.Imo2012P5Cfg.K'_mem_ωB line 241 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.K'

    Proof uses: Iff.mpr, EuclideanGeometry.Sphere.secondInter, Imo2012P5.Imo2012P5Cfg.K, VSub.vsub, Imo2012P5.Imo2012P5Cfg.X, EuclideanGeometry.Sphere.secondInter_mem, Imo2012P5.Imo2012P5Cfg.K_mem_ωB

    12 instances, coercions and auxiliary constants left out.

  25. theorem Imo2012P5.Imo2012P5Cfg.L'_mem_ωA line 244 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.ωA, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Imo2012P5.Imo2012P5Cfg.K'_mem_ωB, Imo2012P5.Imo2012P5Cfg.symm

    7 instances, coercions and auxiliary constants left out.

  26. theorem Imo2012P5.Imo2012P5Cfg.sbtw_KXK' line 247 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.K'

    Proof uses: EuclideanGeometry.Sphere.sbtw_secondInter, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.K_mem_ωB, Imo2012P5.Imo2012P5Cfg.XB_lt_radius_ωB

    13 instances, coercions and auxiliary constants left out.

  27. theorem Imo2012P5.Imo2012P5Cfg.sbtw_LXL' line 250 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Imo2012P5.Imo2012P5Cfg.sbtw_KXK', Imo2012P5.Imo2012P5Cfg.symm

    13 instances, coercions and auxiliary constants left out.

  28. theorem Imo2012P5.Imo2012P5Cfg.sbtw_AKX line 253 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.X

    Proof uses: And.intro, Wbtw, And, Ne, Imo2012P5.Imo2012P5Cfg.wbtw_AKX, Ne.symm, Imo2012P5.Imo2012P5Cfg.A_ne_K, Sbtw.ne_left, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.sbtw_KXK'

    20 instances, coercions and auxiliary constants left out.

  29. theorem Imo2012P5.Imo2012P5Cfg.sbtw_BLX line 256 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.X

    Proof uses: Imo2012P5.Imo2012P5Cfg.sbtw_AKX, Imo2012P5.Imo2012P5Cfg.symm

    13 instances, coercions and auxiliary constants left out.

  30. theorem Imo2012P5.Imo2012P5Cfg.KX_mul_K'X_eq_CX_mul_C'X line 259 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HMul.hMul, Dist.dist, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.C'

    Proof uses: EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical, Exists.intro, Exists, Membership.mem, Set, Insert.insert, Singleton.singleton, EuclideanGeometry.Sphere.center, Imo2012P5.Imo2012P5Cfg.ωB, EuclideanGeometry.Sphere.radius, of_eq_true, Eq.trans, And, EuclideanGeometry.Sphere, Or, True, forall_congr, implies_congr, congrArg, congr and 10 more

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  31. theorem Imo2012P5.Imo2012P5Cfg.LX_mul_L'X_eq_CX_mul_C'X line 265 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HMul.hMul, Dist.dist, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.L', Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.C'

    Proof uses: Eq.rec, Imo2012P5.Imo2012P5Cfg.symm, Imo2012P5.Imo2012P5Cfg.KX_mul_K'X_eq_CX_mul_C'X, Imo2012P5.Imo2012P5Cfg.symm_C'

    12 instances, coercions and auxiliary constants left out.

  32. theorem Imo2012P5.Imo2012P5Cfg.KX_mul_K'X_eq_LX_mul_L'X line 269 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HMul.hMul, Dist.dist, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Eq.trans, Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.C', Imo2012P5.Imo2012P5Cfg.KX_mul_K'X_eq_CX_mul_C'X, Eq.symm, Imo2012P5.Imo2012P5Cfg.LX_mul_L'X_eq_CX_mul_C'X

    12 instances, coercions and auxiliary constants left out.

  33. theorem Imo2012P5.Imo2012P5Cfg.ωA_IsTangentAt_CB line 273 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere.IsTangentAt, Imo2012P5.Imo2012P5Cfg.ωA, Imo2012P5.Imo2012P5Cfg.C, affineSpan, Insert.insert, Set, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.B

    Proof uses: EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two, Imo2012P5.Imo2012P5Cfg.angle_BCA, Imo2012P5.Imo2012P5Cfg.C_mem_ωA

    14 instances, coercions and auxiliary constants left out.

  34. theorem Imo2012P5.Imo2012P5Cfg.ωB_IsTangentAt_CA line 276 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere.IsTangentAt, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.C, affineSpan, Insert.insert, Set, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.A

    Proof uses: Imo2012P5.Imo2012P5Cfg.ωA_IsTangentAt_CB, Imo2012P5.Imo2012P5Cfg.symm

    14 instances, coercions and auxiliary constants left out.

  35. theorem Imo2012P5.Imo2012P5Cfg.sbtw_AKK' line 279 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K'

    Proof uses: Sbtw.trans_expand_left, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.sbtw_AKX, Imo2012P5.Imo2012P5Cfg.sbtw_KXK'

    21 instances, coercions and auxiliary constants left out.

  36. theorem Imo2012P5.Imo2012P5Cfg.sbtw_BLL' line 282 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Sbtw, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Imo2012P5.Imo2012P5Cfg.sbtw_AKK', Imo2012P5.Imo2012P5Cfg.symm

    13 instances, coercions and auxiliary constants left out.

  37. theorem Imo2012P5.Imo2012P5Cfg.A_mem_line_KK' line 285 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.K, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.A

    Proof uses: Eq.mpr, id, Eq, congrArg, AffineSubspace.affineSpan_pair_comm, Sbtw.left_mem_affineSpan, Imo2012P5.Imo2012P5Cfg.sbtw_AKK'

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  38. theorem Imo2012P5.Imo2012P5Cfg.B_mem_line_LL' line 289 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.L, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.L', Imo2012P5.Imo2012P5Cfg.B

    Proof uses: Imo2012P5.Imo2012P5Cfg.A_mem_line_KK', Imo2012P5.Imo2012P5Cfg.symm

    16 instances, coercions and auxiliary constants left out.

  39. theorem Imo2012P5.Imo2012P5Cfg.AC_sq_eq_AK_mul_AK' line 292 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HPow.hPow, Nat, Dist.dist, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.C, OfNat.ofNat, HMul.hMul, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K'

    Proof uses: EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant, Imo2012P5.Imo2012P5Cfg.ωB, Imo2012P5.Imo2012P5Cfg.K_mem_ωB, Imo2012P5.Imo2012P5Cfg.K'_mem_ωB, Imo2012P5.Imo2012P5Cfg.A_mem_line_KK', Eq.mpr, EuclideanGeometry.Sphere.IsTangentAt, affineSpan, Insert.insert, Set, Singleton.singleton, id, congrArg, AffineSubspace, AffineSubspace.affineSpan_pair_comm, Imo2012P5.Imo2012P5Cfg.ωB_IsTangentAt_CA

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  40. theorem Imo2012P5.Imo2012P5Cfg.BC_sq_eq_BL_mul_BL' line 298 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HPow.hPow, Nat, Dist.dist, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.C, OfNat.ofNat, HMul.hMul, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Imo2012P5.Imo2012P5Cfg.AC_sq_eq_AK_mul_AK', Imo2012P5.Imo2012P5Cfg.symm

    14 instances, coercions and auxiliary constants left out.

  41. theorem Imo2012P5.Imo2012P5Cfg.AL_sq_eq_AK_mul_AK' line 301 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HPow.hPow, Nat, Dist.dist, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.L, OfNat.ofNat, HMul.hMul, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K'

    Proof uses: Eq.rec, Imo2012P5.Imo2012P5Cfg.C, Imo2012P5.Imo2012P5Cfg.AC_sq_eq_AK_mul_AK', Eq.symm, Imo2012P5.Imo2012P5Cfg.AL_eq_AC

    22 instances, coercions and auxiliary constants left out.

  42. theorem Imo2012P5.Imo2012P5Cfg.BK_sq_eq_BL_mul_BL' line 304 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, HPow.hPow, Nat, Dist.dist, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.K, OfNat.ofNat, HMul.hMul, Imo2012P5.Imo2012P5Cfg.L, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Imo2012P5.Imo2012P5Cfg.AL_sq_eq_AK_mul_AK', Imo2012P5.Imo2012P5Cfg.symm

    14 instances, coercions and auxiliary constants left out.

  43. theorem Imo2012P5.Imo2012P5Cfg.not_collinear_ABX line 307 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Not, Collinear, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.B, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.X

    Proof uses: Imo2012P5.Imo2012P5Cfg.C, Collinear.subset, Imo2012P5.Imo2012P5Cfg.D, Eq.mp, congrArg, Eq.symm, propext, collinear_insert_iff_of_mem_affineSpan, mem_of_le_of_mem, AffineSubspace, affineSpan, affineSpan_mono, Sbtw.left_mem_affineSpan, Imo2012P5.Imo2012P5Cfg.sbtw_CXD, Membership.mem, Eq.mpr, ContinuousAffineMap, Subtype, Submodule, AffineSubspace.direction and 26 more

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

    Open to load the checked before-and-after goal states.

  44. theorem Imo2012P5.Imo2012P5Cfg.cospherical_KK'LL' line 321 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Cospherical, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.L, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.L'

    Proof uses: Or.elim, Collinear, cospherical_or_collinear_of_mul_dist_eq_mul_dist_of_sbtw, Imo2012P5.Imo2012P5Cfg.X, Imo2012P5.Imo2012P5Cfg.KX_mul_K'X_eq_LX_mul_L'X, Imo2012P5.Imo2012P5Cfg.sbtw_KXK', Imo2012P5.Imo2012P5Cfg.sbtw_LXL', id, False.elim, Imo2012P5.Imo2012P5Cfg.not_collinear_ABX, Collinear.subset, Imo2012P5.Imo2012P5Cfg.A, Imo2012P5.Imo2012P5Cfg.B, Eq.mp, congrArg, Eq.symm, propext, collinear_insert_iff_of_mem_affineSpan, mem_of_le_of_mem, AffineSubspace and 7 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

  45. theorem Imo2012P5.Imo2012P5Cfg.exists_sphere_supset_KK'LL' line 333 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Exists, EuclideanGeometry.Sphere, LE.le, Set, Insert.insert, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.L, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.L', Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.radius

    Proof uses: Iff.mp, EuclideanGeometry.Cospherical, EuclideanGeometry.cospherical_iff_exists_sphere, Imo2012P5.Imo2012P5Cfg.cospherical_KK'LL'

    12 instances, coercions and auxiliary constants left out.

  46. structure Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL' A sphere containing K, K', L, L' line 349 source

    Source documentation

    A sphere containing K, K', L, L'.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere

    3 instances, coercions and auxiliary constants left out.

    structure SphereWithKK'LL' (s : Sphere P) where
…

    Mentions: P

  47. theorem Imo2012P5.Imo2012P5Cfg.exists_sphereWithKK'LL' line 355 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Exists, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'

    Proof uses: LE.le, Set, Insert.insert, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K', Imo2012P5.Imo2012P5Cfg.L, Singleton.singleton, Imo2012P5.Imo2012P5Cfg.L', Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.radius, Imo2012P5.Imo2012P5Cfg.exists_sphere_supset_KK'LL', id, Membership.mem, Exists.intro, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.mk

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  48. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.symm line 366 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', Imo2012P5.Imo2012P5Cfg.symm

    Proof uses: Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.mk, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.L_mem, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.L'_mem, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.K_mem, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.K'_mem

    6 instances, coercions and auxiliary constants left out.

  49. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_AL line 372 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', EuclideanGeometry.Sphere.IsTangentAt, Imo2012P5.Imo2012P5Cfg.L, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.A, Singleton.singleton

    Proof uses: EuclideanGeometry.Sphere.isTangentAt_of_dist_sq_eq_power, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.L_mem, Eq.mpr, Eq, HPow.hPow, Nat, Dist.dist, OfNat.ofNat, EuclideanGeometry.Sphere.power, HMul.hMul, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.K', id, congrArg, Imo2012P5.Imo2012P5Cfg.AL_sq_eq_AK_mul_AK', EuclideanGeometry.Sphere.mul_dist_eq_power_of_radius_le_dist_center, EuclideanGeometry.Sphere.radius_nonneg_of_mem, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.K_mem, Imo2012P5.Imo2012P5Cfg.A_mem_line_KK', Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.K'_mem and 30 more

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

  50. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_BK line 387 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', EuclideanGeometry.Sphere.IsTangentAt, Imo2012P5.Imo2012P5Cfg.K, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.B, Singleton.singleton

    Proof uses: Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_AL, Imo2012P5.Imo2012P5Cfg.symm, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.symm

    14 instances, coercions and auxiliary constants left out.

  51. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_ML line 390 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', EuclideanGeometry.Sphere.IsTangentAt, Imo2012P5.Imo2012P5Cfg.L, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.M, Singleton.singleton

    Proof uses: LE.le, AffineSubspace, Imo2012P5.Imo2012P5Cfg.A, Eq.mpr, id, Eq, congrArg, Eq.symm, affineSpan_insert_eq_affineSpan, And.left, Membership.mem, Imo2012P5.Imo2012P5Cfg.B, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.M_mem_inf_AL_BK, affineSpan_mono, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_AL, EuclideanGeometry.Sphere.orthRadius, EuclideanGeometry.Sphere.IsTangentAt.mk, right_mem_affineSpan_pair, LE.le.trans

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  52. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_MK line 397 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', EuclideanGeometry.Sphere.IsTangentAt, Imo2012P5.Imo2012P5Cfg.K, affineSpan, Insert.insert, Set, Imo2012P5.Imo2012P5Cfg.M, Singleton.singleton

    Proof uses: Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_ML, Imo2012P5.Imo2012P5Cfg.symm, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.symm

    14 instances, coercions and auxiliary constants left out.

  53. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.power_M_eq_ML_sq line 400 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', Eq, EuclideanGeometry.Sphere.power, Imo2012P5.Imo2012P5Cfg.M, HPow.hPow, Nat, Dist.dist, Imo2012P5.Imo2012P5Cfg.L, OfNat.ofNat

    Proof uses: EuclideanGeometry.Sphere.IsTangentAt.power_eq_dist_sq, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.isTangentAt_ML

    12 instances, coercions and auxiliary constants left out.

  54. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.power_M_eq_MK_sq line 403 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', Eq, EuclideanGeometry.Sphere.power, Imo2012P5.Imo2012P5Cfg.M, HPow.hPow, Nat, Dist.dist, Imo2012P5.Imo2012P5Cfg.K, OfNat.ofNat

    Proof uses: Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.power_M_eq_ML_sq, Imo2012P5.Imo2012P5Cfg.symm, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.symm

    12 instances, coercions and auxiliary constants left out.

  55. theorem Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.MK_eq_ML line 406 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', Eq, Dist.dist, Imo2012P5.Imo2012P5Cfg.M, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.L

    Proof uses: Iff.mp, HPow.hPow, Nat, OfNat.ofNat, sq_eq_sq₀, dist_nonneg, Eq.trans, EuclideanGeometry.Sphere.power, Eq.symm, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.power_M_eq_MK_sq, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.power_M_eq_ML_sq

    22 instances, coercions and auxiliary constants left out.

  56. theorem Imo2012P5.Imo2012P5Cfg.MK_eq_ML line 412 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2012P5.Imo2012P5Cfg, Eq, Dist.dist, Imo2012P5.Imo2012P5Cfg.M, Imo2012P5.Imo2012P5Cfg.K, Imo2012P5.Imo2012P5Cfg.L

    Proof uses: Exists.elim, EuclideanGeometry.Sphere, Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL', Imo2012P5.Imo2012P5Cfg.exists_sphereWithKK'LL', Imo2012P5.Imo2012P5Cfg.SphereWithKK'LL'.MK_eq_ML

    8 instances, coercions and auxiliary constants left out.

  57. problem Imo2012P5.imo2012_p5 line 419 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, EuclideanGeometry.angle, HDiv.hDiv, Real.pi, Affine.Simplex.altitudeFoot, Affine.Simplex.mk and 11 more

    Proof uses: Imo2012P5.Imo2012P5Cfg.MK_eq_ML, Imo2012P5.Imo2012P5Cfg.mk

    68 instances, coercions and auxiliary constants left out.