`Compfiles/Usa2000P5.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

31 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2000, Problem 5

Let A₁A₂A₃ be a triangle, and let ω₁ be a circle in its plane passing through A₁ and A₂. Suppose there exist circles ω₂,ω₃,⋯,ω₇ such that for k=2,3,⋯,7, circle ωₖ is externally tangent to ωₖ₋₁ and passes through Aₖ and Aₖ₊₁ (indices mod 3).

Prove that ω₇ = ω₁.

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2000P5.Circle line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: EuclideanGeometry.Sphere, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal
10 instances, coercions and auxiliary constants left out.
def Usa2000P5.ExternallyTangent line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2000P5.Circle
Proof uses: Eq, Real, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, EuclideanGeometry.Sphere.center, HAdd.hAdd, EuclideanGeometry.Sphere.radius
15 instances, coercions and auxiliary constants left out.
abbrev Usa2000P5.Point line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
abbrev Usa2000P5.leftVertex line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin
9 instances, coercions and auxiliary constants left out.
abbrev Usa2000P5.rightVertex line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin
Proof uses: HAdd.hAdd
16 instances, coercions and auxiliary constants left out.
abbrev Usa2000P5.circleCenter line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Usa2000P5.Circle, Usa2000P5.Point
Proof uses: EuclideanGeometry.Sphere.center, EuclideanSpace, Real, ENNReal
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance Usa2000P5.(instance at line 51) line 51 source
instance Usa2000P5.(instance at line 56) line 56 source
abbrev Usa2000P5.sideAngle line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, Real.Angle
Proof uses: EuclideanGeometry.oangle, ENNReal, Real, Usa2000P5.rightVertex, Usa2000P5.leftVertex, Usa2000P5.circleCenter
25 instances, coercions and auxiliary constants left out.
abbrev Usa2000P5.turnAngle line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Real.Angle
Proof uses: EuclideanGeometry.oangle, ENNReal, Real, Usa2000P5.leftVertex, Usa2000P5.rightVertex, HAdd.hAdd
29 instances, coercions and auxiliary constants left out.
lemma Usa2000P5.external_tangent_at_shared_point line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2000P5.Circle, Usa2000P5.Point, Membership.mem, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Usa2000P5.ExternallyTangent, EuclideanGeometry.Sphere.IsExtTangentAt
Proof uses: EuclideanGeometry.Sphere.IsExtTangentAt.mk, Eq.mpr, Wbtw, EuclideanGeometry.Sphere.center, Eq, HAdd.hAdd, Dist.dist, id, congrArg, Eq.symm, propext, dist_add_dist_eq_iff, EuclideanGeometry.Sphere.radius, Iff.mp, EuclideanGeometry.Sphere, EuclideanGeometry.mem_sphere', EuclideanGeometry.mem_sphere
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.center_mem_perpBisector line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, And, Membership.mem, EuclideanSpace, Real, ENNReal, HAdd.hAdd, AffineSubspace, AffineSubspace.perpBisector, Usa2000P5.leftVertex, Usa2000P5.rightVertex, Usa2000P5.circleCenter
Proof uses: Iff.mpr, Eq, Dist.dist, AffineSubspace.mem_perpBisector_iff_dist_eq', EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere, And.left, And.right
93 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.side_oangle_add_eq_zero line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2000P5.Point, Membership.mem, AffineSubspace, Real, OfNat.ofNat, ENNReal, Fin, Nat, AffineSubspace.perpBisector, Eq, Real.Angle, HAdd.hAdd, EuclideanGeometry.oangle
Proof uses: Dist.dist, Iff.mp, AffineSubspace.mem_perpBisector_iff_dist_eq, EuclideanGeometry.oangle_eq_oangle_of_dist_eq, Eq.mpr, id, congrArg, Eq.symm, EuclideanGeometry.oangle_add_oangle_rev
95 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.fin_succ_cast_zmod3 line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LT.lt, Eq, ZMod, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Nat.cast_one, Nat.cast_add, HMod.hMod, propext, ZMod.natCast_eq_natCast_iff'
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.rightVertex_eq_leftVertex_succ line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, LT.lt, Eq, Usa2000P5.rightVertex, Usa2000P5.leftVertex, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Usa2000P5.fin_succ_cast_zmod3, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.leftVertex_mem_circle line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, And, Membership.mem, EuclideanSpace, Real, ENNReal, HAdd.hAdd, Usa2000P5.leftVertex
Proof uses: id, And.left
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.rightVertex_mem_circle line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, And, Membership.mem, EuclideanSpace, Real, ENNReal, HAdd.hAdd, Usa2000P5.rightVertex
Proof uses: id, And.right
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.rightVertex_mem_next_circle line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, And, Membership.mem, EuclideanSpace, Real, ENNReal, HAdd.hAdd, LT.lt, Usa2000P5.rightVertex
Proof uses: Eq.mpr, Usa2000P5.leftVertex, id, Eq, congrArg, Usa2000P5.rightVertex_eq_leftVertex_succ, Usa2000P5.leftVertex_mem_circle
56 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.tangent_at_shared_vertex line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, LT.lt, Usa2000P5.ExternallyTangent, HAdd.hAdd, And, Membership.mem, EuclideanSpace, Real, ENNReal, EuclideanGeometry.Sphere.IsExtTangentAt, Usa2000P5.rightVertex
Proof uses: Usa2000P5.external_tangent_at_shared_point, Usa2000P5.rightVertex_mem_circle, Usa2000P5.rightVertex_mem_next_circle
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.vertex_ne_01 line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, AffineIndependent, Real, ENNReal, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne
Proof uses: id, Function.Injective.ne, AffineIndependent.injective, of_decide_eq_true, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
82 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.vertex_ne_12 line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, AffineIndependent, Real, ENNReal, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne
Proof uses: id, Function.Injective.ne, AffineIndependent.injective, of_decide_eq_true, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
82 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.vertex_ne_20 line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, AffineIndependent, Real, ENNReal, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne
Proof uses: id, Function.Injective.ne, AffineIndependent.injective, of_decide_eq_true, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
82 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.adjacent_vertices_ne line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, AffineIndependent, Real, ENNReal, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne, Usa2000P5.leftVertex, Usa2000P5.rightVertex
Proof uses: List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Usa2000P5.vertex_ne_01, eq_of_heq, List.Mem.tail, Usa2000P5.vertex_ne_12, Usa2000P5.vertex_ne_20 and 5 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.collinear_perpBisector_eq A line intersects a nondegenerate perpendicular bisector at most once line 154 source
Source comment
A line intersects a nondegenerate perpendicular bisector at most once.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2000P5.Point, Ne, Membership.mem, AffineSubspace, Real, OfNat.ofNat, ENNReal, Fin, Nat, AffineSubspace.perpBisector, Collinear, Insert.insert, Set, Singleton.singleton, Eq
Proof uses: Decidable.byContradiction, Not, LE.le, affineSpan, affineSpan_pair_le_of_mem_of_mem, Collinear.mem_affineSpan_of_mem_of_ne, of_eq_true, Eq.trans, Or, True, congr, congrArg, eq_self, true_or, or_true, Iff.mp, AffineSubspace.left_mem_perpBisector
99 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma collinear_perpBisector_eq {a b p q : Point}
    (hab : a ≠ b)
    (hp : p ∈ AffineSubspace.perpBisector a b)
    (hq : q ∈ AffineSubspace.perpBisector a b)
    (hcol : Collinear ℝ ({p, a, q} : Set Point)) :
    p = q := by
…
```
Mentions: Usa2000P5.Point
lemma Usa2000P5.centers_eq_of_oangle_eq Equal side angles force equal centers line 169 source
Source comment
Equal side angles force equal centers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, AffineIndependent, Real, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, And, Membership.mem, EuclideanSpace, HAdd.hAdd, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanGeometry.Sphere.center
Proof uses: Ne, Ne.symm, Usa2000P5.vertex_ne_01, EuclideanGeometry.Sphere.ne_center_of_mem_of_mem_of_ne, And.left, And.right, EuclideanGeometry.oangle_add, add_left_cancel, Eq.mpr, id, Eq.trans, congr, congrArg, congrFun', add_zero, Eq.mp, Collinear, Insert.insert, Set, Singleton.singleton and 14 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma centers_eq_of_oangle_eq
    {A : ZMod 3 → Point} {ω : Fin 7 → Circle}
    (hABC : AffineIndependent ℝ ![A 0, A 1, A 2])
    (hA : ∀ i : Fin 7, (A i ∈ ω i ∧ A (i + 1) ∈ ω i))
    (hangle : EuclideanGeometry.oangle (A 1) (A 0) (ω 0).center =
      EuclideanGeometry.oangle (A 1) (A 0) (ω 6).center) :
    (ω 0).center = (ω 6).center := by
…
```
Mentions: Usa2000P5.Point, Usa2000P5.Circle
lemma Usa2000P5.shared_vertex_sbtw The shared vertex lies strictly between tangent centers line 201 source
Source comment
The shared vertex lies strictly between tangent centers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, AffineIndependent, Real, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LT.lt, Usa2000P5.ExternallyTangent, HAdd.hAdd, And, Membership.mem, EuclideanSpace, Sbtw, Usa2000P5.circleCenter and 1 more
Proof uses: And.intro, Wbtw, Ne, EuclideanGeometry.Sphere.IsExtTangentAt.wbtw, Usa2000P5.tangent_at_shared_vertex, EuclideanGeometry.Sphere.ne_center_of_mem_of_mem_of_ne, Usa2000P5.leftVertex, Usa2000P5.rightVertex_mem_circle, Usa2000P5.leftVertex_mem_circle, Ne.symm, Usa2000P5.adjacent_vertices_ne, Eq.mpr, id, Eq, congrArg, Usa2000P5.rightVertex_eq_leftVertex_succ, Usa2000P5.rightVertex_mem_next_circle
107 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma shared_vertex_sbtw
    {A : ZMod 3 → Point} {ω : Fin 7 → Circle}
    (hABC : AffineIndependent ℝ ![A 0, A 1, A 2])
    (hTangent : ∀ i, i < 6 → ExternallyTangent (ω i) (ω (i + 1)))
    (hA : ∀ i : Fin 7, (A i ∈ ω i ∧ A (i + 1) ∈ ω i))
    (i : Fin 7) (hi : i < 6) :
    Sbtw ℝ (circleCenter ω i) (rightVertex A i) (circleCenter ω (i + 1)) := by
…
```
Mentions: Usa2000P5.Point, Usa2000P5.Circle, Usa2000P5.ExternallyTangent, Usa2000P5.circleCenter, Usa2000P5.rightVertex
lemma Usa2000P5.directed_angle_step One straight-center step for directed angles line 219 source
Source comment
One straight-center step for directed angles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2000P5.Point, Ne, Membership.mem, AffineSubspace, Real, OfNat.ofNat, ENNReal, Fin, Nat, AffineSubspace.perpBisector, Sbtw, Eq, Real.Angle, HAdd.hAdd, EuclideanGeometry.oangle, Real.pi
Proof uses: Usa2000P5.side_oangle_add_eq_zero, EuclideanGeometry.oangle_add, Sbtw.left_ne, Sbtw.right_ne, Eq.mp, congrArg, Sbtw.oangle₁₂₃_eq_pi, Eq.trans, Eq.symm, Trans.trans, Eq.mpr, id, Eq.refl, zero_add
115 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma directed_angle_step {a b c u v : Point}
    (hab : a ≠ b) (hcb : c ≠ b)
    (hu : u ∈ AffineSubspace.perpBisector a b)
    (hsbtw : Sbtw ℝ u b v) :
    EuclideanGeometry.oangle b a u + EuclideanGeometry.oangle c b v +
      EuclideanGeometry.oangle a b c = (Real.pi : Real.Angle) := by
…
```
Mentions: Usa2000P5.Point
lemma Usa2000P5.directed_angle_recurrence One tangency advances the side angle line 258 source
Source comment
One tangency advances the side angle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, AffineIndependent, Real, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LT.lt, Usa2000P5.ExternallyTangent, HAdd.hAdd, And, Membership.mem, EuclideanSpace, Eq, Real.Angle and 6 more
Proof uses: Ne, Eq.mpr, Usa2000P5.leftVertex, id, congrArg, Usa2000P5.rightVertex_eq_leftVertex_succ, Ne.symm, Usa2000P5.adjacent_vertices_ne, Usa2000P5.directed_angle_step, Usa2000P5.center_mem_perpBisector, Usa2000P5.shared_vertex_sbtw
128 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma directed_angle_recurrence
    {A : ZMod 3 → Point} {ω : Fin 7 → Circle}
    (hABC : AffineIndependent ℝ ![A 0, A 1, A 2])
    (hTangent : ∀ i, i < 6 → ExternallyTangent (ω i) (ω (i + 1)))
    (hA : ∀ i : Fin 7, (A i ∈ ω i ∧ A (i + 1) ∈ ω i))
    (i : Fin 7) (hi : i < 6) :
    sideAngle A ω i +
        EuclideanGeometry.oangle (rightVertex A (i + 1)) (rightVertex A i)
          (circleCenter ω (i + 1)) +
      turnAngle A i = (Real.pi : Real.Angle) := by
…
```
Mentions: Usa2000P5.Point, Usa2000P5.Circle, Usa2000P5.ExternallyTangent, Usa2000P5.sideAngle, Usa2000P5.rightVertex, Usa2000P5.circleCenter, Usa2000P5.turnAngle
lemma Usa2000P5.side_oangle_eq_after_six line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, AffineIndependent, Real, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LT.lt, Usa2000P5.ExternallyTangent, HAdd.hAdd, And, Membership.mem, EuclideanSpace, Eq, Real.Angle and 1 more
Proof uses: Usa2000P5.turnAngle, Real.pi, Usa2000P5.leftVertex, Usa2000P5.rightVertex, Eq.symm, Usa2000P5.rightVertex_eq_leftVertex_succ, Eq.mpr, EuclideanGeometry.oangle, Usa2000P5.circleCenter, id, congrFun', congrArg, EuclideanGeometry.oangle.congr_simp, Eq.refl, Usa2000P5.directed_angle_recurrence, Eq.mp, zero_add, of_decide_eq_true, Bool, Decidable.decide and 3 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Usa2000P5.circle_eq_of_center_eq line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Usa2000P5.Point, Fin, Usa2000P5.Circle, And, Membership.mem, EuclideanSpace, Real, ENNReal, HAdd.hAdd, Eq, EuclideanGeometry.Sphere.center
Proof uses: Iff.mp, EuclideanGeometry.Sphere, EuclideanGeometry.Sphere.center_eq_iff_eq_of_mem, And.left
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
problem Usa2000P5.usa2000_p5 line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, EuclideanSpace, Real, Fin, AffineIndependent, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Usa2000P5.Circle, LT.lt, Usa2000P5.ExternallyTangent, HAdd.hAdd, And, Membership.mem, Eq
Proof uses: Usa2000P5.circle_eq_of_center_eq, Usa2000P5.centers_eq_of_oangle_eq, Usa2000P5.side_oangle_eq_after_six
100 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.