2d.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

32 declarations, 0 contain sorry, 0 declared as axioms

Imports (9)

Imported by 1 file

FormalConjecturesForMathlib.lean

instance Module.orientedEuclideanSpaceFinTwo Oriented angles make sense in 2d line 39 source
Source documentation
Oriented angles make sense in 2d.
Note: this can't blindly be added to mathlib as it creates an "instance diamond" with an instance for modules satisfying is_empty.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Module.Oriented, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal
Proof uses: Module.Oriented.mk, Module.Basis.orientation, PiLp.basisFun
45 instances, coercions and auxiliary constants left out.
```
noncomputable instance Module.orientedEuclideanSpaceFinTwo : Module.Oriented ℝ ℝ² (Fin 2) :=
…
```
instance fact_finrank_euclideanSpace_fin_two Two dimensional euclidean space is two-dimensional line 43 source
Source documentation
Two dimensional euclidean space is two-dimensional.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fact, Eq, Nat, Module.finrank, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal
Proof uses: Fact.mk, finrank_euclideanSpace_fin
35 instances, coercions and auxiliary constants left out.
```
instance fact_finrank_euclideanSpace_fin_two : Fact (Module.finrank ℝ ℝ² = 2) :=
…
```
def EuclideanGeometry.NonTrilinear We say a subset A of points in the plane is non-trilinear if it contains no three points that lie on the same line line 60 source
Source documentation
We say a subset A of points in the plane is non-trilinear if it contains no three points that lie on the same line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Set
Proof uses: Set.Triplewise, Not, Collinear, Insert.insert, Singleton.singleton
14 instances, coercions and auxiliary constants left out.
```
def NonTrilinear (A : Set P) : Prop :=
…
```
def EuclideanGeometry.NonCollinearFor We say a subset S of points is non-collinear for $n$ points if it contains no $n$ points that lie on the same line line 65 source
Source documentation
We say a subset S of points is non-collinear for $n$ points if it contains no $n$ points that lie on the same line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Nat, Set
Proof uses: LE.le, Set.Finite, Eq, Set.ncard, Not, Collinear
13 instances, coercions and auxiliary constants left out.
```
def NonCollinearFor (n : ℕ) (S : Set P) : Prop :=
…
```
lemma EuclideanGeometry.NonCollinearFor.subset line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Nat, Set, LE.le, EuclideanGeometry.NonCollinearFor
Proof uses: Set.Finite, Eq, Set.ncard, LE.le.trans
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def EuclideanGeometry.ConvexIndep ConvexIndep S means that S consists of extremal points of its convex hull, i.e., the point set encloses a convex shape line 77 source
Source documentation
ConvexIndep S means that S consists of extremal points of its convex hull, i.e., the point set encloses a convex shape. Also known as a "convex-independent set".

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Membership.mem, Not, ClosureOperator, convexHull, ENNReal, SDiff.sdiff, Singleton.singleton
30 instances, coercions and auxiliary constants left out.
```
def ConvexIndep (S : Set ℝ²) : Prop :=
…
```
def EuclideanGeometry.HasConvexNGon The set P contains a convex n-gon line 82 source
Source documentation
The set P contains a convex n-gon. See also IsConvexPolygon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: Exists, Finset, And, Eq, Finset.card, LE.le, EuclideanGeometry.ConvexIndep
5 instances, coercions and auxiliary constants left out.
```
def HasConvexNGon (n : ℕ) (P : Set ℝ²) : Prop :=
…
```
def EuclideanGeometry.IsCcwConvexPolygon The statement that a sequence of points form a counter-clockwise convex polygon line 86 source
Source documentation
The statement that a sequence of points form a counter-clockwise convex polygon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Fact, Eq, Module.finrank
Proof uses: LT.lt, SignType, Real.Angle.sign, EuclideanGeometry.oangle
29 instances, coercions and auxiliary constants left out.
```
def IsCcwConvexPolygon (p : Fin n → P) : Prop :=
…
```
theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon, LT.lt, SignType, Real.Angle.sign, EuclideanGeometry.oangle
30 instances, coercions and auxiliary constants left out.
theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle' line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon, LT.lt, SignType, Real.Angle.sign, EuclideanGeometry.oangle
Proof uses: Eq.mpr, id, congrArg, EuclideanGeometry.oangle_rotate_sign
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle'' line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon, LT.lt, SignType, Real.Angle.sign, EuclideanGeometry.oangle
Proof uses: Eq.mpr, id, congrArg, Eq.symm, EuclideanGeometry.oangle_rotate_sign
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle_finRotate line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon, LE.le, SignType, Real.Angle.sign, EuclideanGeometry.oangle, Equiv.Perm, finRotate
Proof uses: HAdd.hAdd, Exists, Iff.mp, le_iff_exists_add', dite, Fin.last, Eq.mpr, id, congrArg, finRotate_last, Nat.succ, finRotate_apply_zero, EuclideanGeometry.IsCcwConvexPolygon.sign_oangle'', Fin.zero_lt_one, Fin.one_lt_last, Not, EuclideanGeometry.IsCcwConvexPolygon.sign_oangle', LT.lt, Ne, propext and 9 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.isCcwConvexPolygon_zero line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon
Proof uses: finZeroElim, LT.lt, SignType, Real.Angle.sign, EuclideanGeometry.oangle
29 instances, coercions and auxiliary constants left out.
theorem EuclideanGeometry.isCcwConvexPolygon_one line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon
Proof uses: LT.lt, Decidable.byContradiction, SignType, Real.Angle.sign, EuclideanGeometry.oangle, Not
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.isCcwConvexPolygon_two line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, EuclideanGeometry.IsCcwConvexPolygon
Proof uses: LT.lt, Decidable.byContradiction, SignType, Real.Angle.sign, EuclideanGeometry.oangle, Not
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.isCcwConvexPolygon_four' line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, Iff, EuclideanGeometry.IsCcwConvexPolygon, And, SignType, Real.Angle.sign, EuclideanGeometry.oangle
Proof uses: Iff.intro, LT.lt, of_eq_true, Eq.trans, True, congr, congrArg, eq_true_of_decide, Eq.refl, Bool, Bool.true, and_self, And.intro, EuclideanGeometry.IsCcwConvexPolygon.sign_oangle, EuclideanGeometry.IsCcwConvexPolygon.sign_oangle', LT.lt.trans, EuclideanGeometry.IsCcwConvexPolygon.sign_oangle'', List, List.Mem, List.finRange and 26 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.isCcwConvexPolygon_four line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, Iff, EuclideanGeometry.IsCcwConvexPolygon, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, And, SignType, Real.Angle.sign and 1 more
Proof uses: EuclideanGeometry.isCcwConvexPolygon_four'
28 instances, coercions and auxiliary constants left out.
def EuclideanGeometry.IsConvexPolygon The statement that a sequence of points form a convex polygon line 153 source
Source documentation
The statement that a sequence of points form a convex polygon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank
Proof uses: Or, EuclideanGeometry.IsCcwConvexPolygon, Neg.neg
27 instances, coercions and auxiliary constants left out.
```
def IsConvexPolygon {n : ℕ} (p : Fin n → P) : Prop :=
…
```
theorem EuclideanGeometry.isConvexPolygon_three_of_affineIndependent Three affine independent points always form a convex polygon line 157 source
Source documentation
Three affine independent points always form a convex polygon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, AffineIndependent, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, EuclideanGeometry.IsConvexPolygon
Proof uses: SignType, Real.Angle.sign, EuclideanGeometry.oangle, SignType.zero, False.elim, Eq.mp, And, Ne, Real.Angle, Real.pi, congrArg, Eq.symm, propext, Real.Angle.sign_ne_zero_iff, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent, Eq.refl, SignType.neg, Or.inr, EuclideanGeometry.IsCcwConvexPolygon, Neg.neg and 34 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem isConvexPolygon_three_of_affineIndependent {A B C : P}
    (hABC : AffineIndependent ℝ ![A, B, C]) : IsConvexPolygon ![A, B, C] := by
…
```
Mentions: EuclideanGeometry.IsConvexPolygon
theorem EuclideanGeometry.isConvexPolygon_three_iff_affineIndependent line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, Iff, EuclideanGeometry.IsConvexPolygon, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, AffineIndependent
Proof uses: Iff.intro, Eq.mpr, And, Ne, Real.Angle, EuclideanGeometry.oangle, Real.pi, id, congrArg, Eq.symm, propext, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent, SignType, Real.Angle.sign, Real.Angle.sign_ne_zero_iff, EuclideanGeometry.IsCcwConvexPolygon, Neg.neg, Or, Or.inl, EuclideanGeometry.IsCcwConvexPolygon.sign_oangle and 18 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem EuclideanGeometry.isConvexPolygon_triangle line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank, Affine.Triangle, EuclideanGeometry.IsConvexPolygon, HAdd.hAdd, Affine.Simplex.points
Proof uses: Matrix.vecCons, Nat.succ, Matrix.vecEmpty, funext, List, List.Mem, 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, Eq.refl, eq_of_heq and 13 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def EuclideanGeometry.triangle_area line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Module.Oriented, Fin, OfNat.ofNat, Nat, Fact, Eq, Module.finrank
Proof uses: HDiv.hDiv, LinearMap, RingHom.id, Orientation.areaForm, Module.Oriented.positiveOrientation, VSub.vsub
44 instances, coercions and auxiliary constants left out.
lemma EuclideanGeometry.triangle_area_eq_det line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, EuclideanGeometry.triangle_area, ENNReal, HDiv.hDiv, Matrix.det, Equiv, Matrix, Matrix.of, Matrix.vecCons, WithLp.ofLp, Matrix.vecEmpty
Proof uses: Eq.mpr, LinearMap, RingHom.id, Orientation.areaForm, Module.Oriented.positiveOrientation, VSub.vsub, id, congrArg, EuclideanGeometry.triangle_area.eq_1, AlternatingMap, Orientation.volumeForm, Orientation.areaForm_to_volumeForm, Module.Basis.det, OrthonormalBasis.toBasis, EuclideanSpace.basisFun, Orientation.volumeForm_robust, rfl, Orientation, Module.Basis.orientation, Module.Basis.toMatrix and 66 more
163 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def EuclideanGeometry.maximalDistinctDistancesFrom Documented declaration: maximalDistinctDistancesFrom line 211 source
Source documentation
Let $x_1,\ldots,x_n\in \mathbb{R}^2$ and let $R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}$, where the points are ordered such that $$R(x_1)\leq \cdots \leq R(x_n).$$ Let $g(n)$ be the maximum number of distinct values the $R(x_i)$ can take.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Eq, Finset.card, Finset.image, distinctDistancesFrom, ENNReal
12 instances, coercions and auxiliary constants left out.
```
noncomputable def maximalDistinctDistancesFrom (n : ℕ) : ℕ :=
…
```
def EuclideanGeometry.InGeneralPosition A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is in general position if no three are collinear and no four lie on a circle line 218 source
Source documentation
A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is in general position if no three are collinear and no four lie on a circle.
Stated for Set ℝ² so that infinite collections are covered; a Finset argument coerces.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: And, EuclideanGeometry.NonTrilinear, ENNReal, LE.le, Eq, Set.ncard, Not, EuclideanGeometry.Cospherical
24 instances, coercions and auxiliary constants left out.
```
def InGeneralPosition (X : Set ℝ²) : Prop :=
…
```
def EuclideanGeometry.IsRightAngled a b c are the vertices of a right-angled triangle: the (unoriented) angle at one of the three vertices equals π / 2 line 223 source
Source documentation
a b c are the vertices of a right-angled triangle: the (unoriented) angle at one of the three vertices equals π / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor
Proof uses: Or, Eq, EuclideanGeometry.angle, HDiv.hDiv, Real.pi, OfNat.ofNat
12 instances, coercions and auxiliary constants left out.
```
def IsRightAngled (a b c : P) : Prop :=
…
```
Mentions: c
def EuclideanGeometry.IsIsoscelesTrapezoid Documented declaration: IsIsoscelesTrapezoid line 233 source
Source documentation
a b c d are the vertices, in counter-clockwise order, of an isosceles trapezoid: they are in strictly convex position, the side ab is parallel to the side cd (the two bases), and the diagonals ac and bd have equal length. One pair of parallel sides together with equal diagonals is the classical characterization of an isosceles trapezoid; in particular it rules out non-rectangular parallelograms.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: And, EuclideanGeometry.IsCcwConvexPolygon, Nat.succ, ENNReal, Matrix.vecCons, Matrix.vecEmpty, AffineSubspace.Parallel, affineSpan, Insert.insert, Set, Singleton.singleton, Eq, Dist.dist
41 instances, coercions and auxiliary constants left out.
```
def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop :=
…
```
Mentions: c
def EuclideanGeometry.IsLine A line in the plane: an affine subspace of ℝ² whose direction is one-dimensional line 239 source
Source documentation
A line in the plane: an affine subspace of ℝ² whose direction is one-dimensional.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AffineSubspace, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal
Proof uses: Eq, Module.finrank, Subtype, Membership.mem, Submodule, AffineSubspace.direction
58 instances, coercions and auxiliary constants left out.
```
def IsLine (L : AffineSubspace ℝ ℝ²) : Prop :=
…
```
def IsIsosceles line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Dist
Proof uses: Or, Eq, Real, Dist.dist
def Set.IsIsosceles line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Dist, Set
Proof uses: And, Nonempty, Set.Triplewise, IsIsosceles
1 instances, coercions and auxiliary constants left out.
def Set.IsIsoscelesFree A set is isosceles-free if no three distinct points in it form an isosceles triangle line 251 source
Source documentation
A set is isosceles-free if no three distinct points in it form an isosceles triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Dist, Set
Proof uses: Set.Triplewise, Not, IsIsosceles
```
def Set.IsIsoscelesFree {α : Type*} [Dist α] (A : Set α) : Prop :=
…
```
theorem Set.IsIsoscelesFree.mono line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Dist, Set, LE.le, Set.IsIsoscelesFree
Proof uses: Set.Triplewise.mono, Not, IsIsosceles
2 instances, coercions and auxiliary constants left out.