awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
hui : Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
huj : Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
⊢ insert t₀.orthocenter (t₀.points '' {j₁, j₂, j₃}) = insert (t₀.points j₁) (t.points '' {i₁, i₂, i₃})
have simp_rw : Eq (α := Set P) {t₀.orthocenter, t₀.points j₁, t₀.points j₂, t₀.points j₃}
  {t₀.points j₁, t₀.orthocenter, t₀.points j₂, t₀.points j₃}
Tactic: simp_rw [Set.image_insert_eq, Set.image_singleton, h₁, ← h₂, ← h₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
hui : Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
huj : Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
⊢ Eq (α := Set P) {t₀.orthocenter, t₀.points j₁, t₀.points j₂, t₀.points j₃}
    {t₀.points j₁, t₀.orthocenter, t₀.points j₂, t₀.points j₃}
have rw : Eq (α := Set P) {t₀.points j₁, t₀.orthocenter, t₀.points j₂, t₀.points j₃}
  {t₀.points j₁, t₀.orthocenter, t₀.points j₂, t₀.points j₃}
Tactic: rw [Set.insert_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
⊢ s = insert t.orthocenter (Set.range t.points)
have inl : t₀.points j₁ = t.orthocenter
Tactic: suffices h : t₀.points j₁ = t.orthocenter by
      have hui : (Set.univ : Set (Fin 3)) = {i₁, i₂, i₃} := by ext x; simpa using h₁₂₃ x
      have huj : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by ext x; simpa using hj₁₂₃ x
      rw [← h, ht₀s, ← Set.image_univ, huj, ← Set.image_univ, hui]
      simp_rw [Set.image_insert_eq, Set.image_singleton, h₁, ← h₂, ← h₃]
      rw [Set.insert_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
hs : Set.range t.points = Set.range t₀.points
⊢ s = insert t.orthocenter (Set.range t.points)
have inr : s = insert t.orthocenter (Set.range t₀.points)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
hs : Set.range t.points = Set.range t₀.points
⊢ s = insert t.orthocenter (Set.range t₀.points)
have h : t.orthocenter = t₀.orthocenter
Tactic: convert! ht₀s using 2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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 : ℕ
s : Simplex ℝ P n
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.ninePointCircle.center
have rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
  ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)
Tactic: rw [ninePointCircle_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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 : ℕ
s : Simplex ℝ P n
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)
have refine : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points)))
  ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))
Tactic: refine AffineSubspace.vadd_mem_of_mem_direction ?_ s.circumcenter_mem_affineSpan
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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 : ℕ
s : Simplex ℝ P n
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points)))
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))
have h : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points))) (s.centroid -ᵥ s.circumcenter)
Tactic: apply Submodule.smul_mem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (hypothesis)
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).ninePointCircle = s.ninePointCircle
have h : n = m
Tactic: have h : n = m := by simpa using Fin.equiv_iff_eq.mp ⟨e⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
⊢ (s.reindex e).ninePointCircle = s.ninePointCircle
have center : (s.reindex e).ninePointCircle.center = s.ninePointCircle.center
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
center : (s.reindex e).ninePointCircle.center = s.ninePointCircle.center
⊢ (s.reindex e).ninePointCircle = s.ninePointCircle
have radius : (s.reindex e).ninePointCircle.radius = s.ninePointCircle.radius
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).ninePointCircle =
    { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }
have center : (s.map f.toAffineMap sorry).ninePointCircle.center =
  Sphere.center { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
center :
  (s.map f.toAffineMap ⋯).ninePointCircle.center =
    Sphere.center { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }
⊢ (s.map f.toAffineMap ⋯).ninePointCircle =
    { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }
have radius : (s.map f.toAffineMap sorry).ninePointCircle.radius =
  Sphere.radius.{u_4} (P := P₂)
    ({ center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius } : Sphere P₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ Eq (α := Sphere ↥S) ((s.restrict S hS).ninePointCircle (n := n))
    { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯, radius := s.ninePointCircle.radius }
have center : (↑(Sphere.center ((s.restrict S hS).ninePointCircle (n := n))) : P) =
  (↑(Sphere.center
        { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center sorry,
          radius := s.ninePointCircle.radius : Sphere ↥S }) :
    P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
center :
  (↑(Sphere.center ((s.restrict S hS).ninePointCircle (n := n))) : P) =
    (↑(Sphere.center
          { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯,
            radius := s.ninePointCircle.radius : Sphere ↥S }) :
      P)
⊢ Eq (α := Sphere ↥S) ((s.restrict S hS).ninePointCircle (n := n))
    { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯, radius := s.ninePointCircle.radius }
have radius : Sphere.radius.{u_2} (P := ↥S) ((s.restrict S hS).ninePointCircle (n := n)) =
  Sphere.radius
    { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center sorry, radius := s.ninePointCircle.radius }
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i ∈ s.ninePointCircle
have rw : dist (s.faceOppositeCentroid i)
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) =
  dist s.circumcenter (s.points i) / (↑n : ℝ)
Tactic: rw [mem_sphere, ninePointCircle_center, ninePointCircle_radius,
    ← dist_circumcenter_eq_circumradius' s i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
⊢ dist (s.faceOppositeCentroid i)
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) =
    dist s.circumcenter (s.points i) / (↑n : ℝ)
have simp_rw : ‖s.faceOppositeCentroid i -ᵥ
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
  ‖s.circumcenter -ᵥ s.points i‖ / (↑n : ℝ)
Tactic: simp_rw [dist_eq_norm_vsub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
⊢ ‖s.faceOppositeCentroid i -ᵥ
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖ / (↑n : ℝ)
have rw : (↑n : ℝ) *
    ‖s.faceOppositeCentroid i -ᵥ
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [eq_div_iff_mul_eq (by simpa using NeZero.ne n), mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
⊢ (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have nth_rw : norm (E := ℝ) (↑n : ℝ) *
    ‖s.faceOppositeCentroid i -ᵥ
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: nth_rw 1 [show (n : ℝ) = ‖(n : ℝ)‖ by simp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have rw : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
      (s.faceOppositeCentroid i -ᵥ
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
rw :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have rw₁ : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
      (s.faceOppositeCentroid i -ᵥ s.circumcenter -
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
rw :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter -
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have rw₂ : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
      HSMul.hSMul (α := ℝ) (↑n : ℝ) ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
rw :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter -
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₂ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        HSMul.hSMul (α := ℝ) (↑n : ℝ) ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have rw₃ : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
      ((↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ))) • (s.centroid -ᵥ s.circumcenter)‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
rw :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter -
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₂ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        HSMul.hSMul (α := ℝ) (↑n : ℝ) ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₃ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        ((↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ))) • (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have rw₄ : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 • (s.centroid -ᵥ s.circumcenter)‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.NinePointCircle (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
i : Fin (n + 1)
rw :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter -
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₂ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        HSMul.hSMul (α := ℝ) (↑n : ℝ) ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₃ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        ((↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ))) • (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₄ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 • (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
have rw₅ : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
      (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) +
        HSMul.hSMul (α := ℝ) 1 (s.centroid -ᵥ s.circumcenter))‖ =
  ‖s.circumcenter -ᵥ s.points i‖
Tactic: rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]