awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)
have hi : i = 0
Tactic: have hi : i = 0 := Subsingleton.eq_zero i
-- 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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)
have hrange : Set.range s.points = {s.points i}
Tactic: have hrange : Set.range s.points = {s.points i} := by simp [hi]
-- 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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
hrange : Set.range s.points = {s.points i}
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)
have hmonge : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint
Tactic: obtain hmonge := s.mongePoint_mem_affineSpan
-- 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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
hrange : Set.range s.points = {s.points i}
hmonge : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)
have hmonge₁ : s.mongePoint = s.points i
Tactic: rw [hrange, mem_affineSpan_singleton] at hmonge
Cleared hypotheses: hmonge
-- 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
i : Fin (n + 1)
hn : ¬n = 0
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
have rw : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
Tactic: rw [sub_div, div_self (by simpa using hn), one_div]
-- 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
i : Fin (n + 1)
hn : ¬n = 0
rw : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
have rw₁ : 1 - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
Tactic: rw [sub_div, div_self (by simpa using hn), one_div]
-- 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
i : Fin (n + 1)
hn : ¬n = 0
rw : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
rw₁ : 1 - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
have rw₂ : HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹ = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
Tactic: rw [sub_div, div_self (by simpa using hn), one_div]
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
hn : ¬n = 0
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have this : HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
Tactic: have : ((n - 1) / n : ℝ) = 1 - (n : ℝ)⁻¹ := by
    rw [sub_div, div_self (by simpa using hn), one_div]
-- 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
i : Fin (n + 1)
hn : ¬n = 0
this : HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have neg : s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
  HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹ • (s.points i -ᵥ s.mongePoint)
Tactic: rw [this, sub_smul, one_smul]
-- 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
i : Fin (n + 1)
hn : ¬n = 0
this : HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
neg :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹ • (s.points i -ᵥ s.mongePoint)
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have neg₁ : s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
  HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ s.mongePoint) - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint)
Tactic: rw [this, sub_smul, one_smul]
-- 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
i : Fin (n + 1)
hn : ¬n = 0
this : HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
neg :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹ • (s.points i -ᵥ s.mongePoint)
neg₁ :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ s.mongePoint) - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint)
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have neg₂ : s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint)
Tactic: rw [this, sub_smul, one_smul]
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) = s.ninePointCircle.center
have apply : midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) -ᵥ s.circumcenter = s.ninePointCircle.center -ᵥ s.circumcenter
Tactic: apply vsub_left_cancel (p := s.circumcenter)
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) -ᵥ s.circumcenter = s.ninePointCircle.center -ᵥ s.circumcenter
have rw : HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (s.points i -ᵥ
              (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)) +ᵥ
          HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
        s.circumcenter) =
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: rw [ninePointCircle_center, midpoint_vsub, vadd_vsub, eulerPoint,
    mongePoint_eq_smul_vsub_vadd_circumcenter, ← centroid]
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have pos : ∀ (hn1 : n = 1),
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: by_cases hn1 : n = 1
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
pos :
  ∀ (hn1 : n = 1),
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (s.points i -ᵥ
                  (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                    s.circumcenter)) +ᵥ
              HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
            s.circumcenter) =
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have neg : ∀ (hn1 : ¬n = 1),
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: by_cases hn1 : n = 1
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : n = 1
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have pos : ∀ [hn : NeZero (R := ℕ) 1] (s : Simplex ℝ P 1) (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                    (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                (s.centroid -ᵥ s.circumcenter) +ᵥ
              s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1 / (↑1 : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: obtain rfl := hn1
Cleared hypotheses: n, hn, s, i, hn1
-- 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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                    (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                (s.centroid -ᵥ s.circumcenter) +ᵥ
              s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1 / (↑1 : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have pos : HSMul.hSMul (α := ℝ) 2⁻¹ (s.faceOppositeCentroid i -ᵥ s.centroid) +
    HSMul.hSMul (α := ℝ) 2⁻¹ (s.points i -ᵥ s.centroid) =
  0
Tactic: suffices (2⁻¹ : ℝ) • (s.faceOppositeCentroid i -ᵥ s.centroid) +
        (2⁻¹ : ℝ) • (s.points i -ᵥ s.centroid) = 0 by
      simpa [circumcenter_eq_centroid, centroid]
-- 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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (s.faceOppositeCentroid i -ᵥ s.centroid) +
      HSMul.hSMul (α := ℝ) 2⁻¹ (s.points i -ᵥ s.centroid) =
    0
have pos : HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹ (s.centroid -ᵥ s.points i) + (s.points i -ᵥ s.centroid)) = 0
Tactic: rw [faceOppositeCentroid_vsub_centroid_eq_smul_vsub, ← smul_add]
-- 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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
⊢ 1 < n
have x : n ≠ 0
Tactic: have _ := hn.out
-- 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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have hltn : 1 < n
Tactic: have hltn : 1 < n := by
    have _ := hn.out
    lia
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
⊢ (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
have push_cast : HSub.hSub (α := ℝ) (↑n : ℝ) 1 = HSub.hSub (α := ℝ) (↑n : ℝ) 1
Tactic: push_cast [hltn]
-- 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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
Tactic: have hnsub1 : (n - 1 : ℕ) = (n : ℝ) - 1 := by
    push_cast [hltn]
    rfl
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have neg : HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)) =
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: push_cast
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have rw : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
rw :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
have rw₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
  (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
Tactic: rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]