awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs
have rw : HMul.hMul (α := ℝ) |if i ∈ signs then -1 else 1|
      |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
    s.exradius signs =
  s.exradius signs
Tactic: rw [touchpoint,
    ← abs_signedInfDist_eq_dist_of_mem_affineSpan_range i h.excenter_mem_affineSpan_range,
    h.signedInfDist_excenter, abs_mul, abs_mul, abs_of_nonneg (s.exradius_nonneg signs)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ HMul.hMul (α := ℝ) |if i ∈ signs then -1 else 1|
        |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
have simp : |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
    s.exradius signs =
  s.exradius signs
Tactic: simp only [abs_ite, abs_neg, abs_one, ite_self, one_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
have inl : ∀ (h' : LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
  |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
Tactic: rcases lt_trichotomy 0 (∑ i, s.excenterWeightsUnnorm signs i) with h' | h' | h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
inl :
  ∀ (h' : LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
    |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
        s.exradius signs =
      s.exradius signs
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
have inr : ∀ (h' : Eq (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
  |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
Tactic: rcases lt_trichotomy 0 (∑ i, s.excenterWeightsUnnorm signs i) with h' | h' | h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
inl :
  ∀ (h' : LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
    |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
        s.exradius signs =
      s.exradius signs
inr :
  ∀ (h' : Eq (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
    |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
        s.exradius signs =
      s.exradius signs
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
have inr₁ : ∀ (h' : LT.lt (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0),
  |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
Tactic: rcases lt_trichotomy 0 (∑ i, s.excenterWeightsUnnorm signs i) with h' | h' | h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw : (s.exsphere signs).IsTangentAt
  (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.excenter signs)) :
    P)
  (affineSpan ℝ (Set.range (s.faceOpposite i).points))
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₁ : (s.exsphere signs).IsTangentAt
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.excenter signs)) :
    P)
  (affineSpan ℝ (Set.range (s.faceOpposite i).points))
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₂ : (s.exsphere signs).IsTangentAt
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.exsphere signs).center) :
    P)
  (affineSpan ℝ (Set.range (s.faceOpposite i).points))
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₃ : dist (s.exsphere signs).center
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P) =
  (s.exsphere signs).radius
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₃ :
  dist (s.exsphere signs).center
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₄ : dist (s.exsphere signs).center
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P) =
  (s.exsphere signs).radius
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₃ :
  dist (s.exsphere signs).center
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₄ :
  dist (s.exsphere signs).center
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₅ : dist (s.excenter signs)
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P) =
  (s.exsphere signs).radius
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₃ :
  dist (s.exsphere signs).center
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₄ :
  dist (s.exsphere signs).center
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₅ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    (s.exsphere signs).radius
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₆ : dist (s.excenter signs)
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P) =
  s.exradius signs
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₃ :
  dist (s.exsphere signs).center
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₄ :
  dist (s.exsphere signs).center
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₅ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    (s.exsphere signs).radius
rw₆ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    s.exradius signs
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₇ : dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₃ :
  dist (s.exsphere signs).center
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₄ :
  dist (s.exsphere signs).center
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₅ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    (s.exsphere signs).radius
rw₆ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    s.exradius signs
rw₇ : dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
have rw₈ : s.exradius signs = s.exradius signs
Tactic: rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ p = s.touchpoint signs i
have rw : (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.exsphere signs).center) :
    P) =
  s.touchpoint signs i
Tactic: rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw :
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P) =
    s.touchpoint signs i
⊢ p = s.touchpoint signs i
have rw₁ : Eq.{u_2 + 1} (α := P)
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.exsphere signs).center) :
    P)
  (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
        (s.excenter signs)) :
    P)
Tactic: rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]