awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
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‖
⊢ 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) + (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‖
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‖
rw₆ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) + (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) -
      (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‖
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‖
rw₆ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₇ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
          HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) -
        (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 - (s.centroid -ᵥ s.circumcenter)) -
      (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‖
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‖
rw₆ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₇ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
          HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₈ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter - (s.centroid -ᵥ s.circumcenter)) -
        (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.centroid) - (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‖
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‖
rw₆ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₇ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
          HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₈ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter - (s.centroid -ᵥ s.circumcenter)) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₉ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.centroid) - (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₁₀ : ‖s.centroid -ᵥ s.points i - (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‖
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‖
rw₆ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₇ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
          HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₈ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter - (s.centroid -ᵥ s.circumcenter)) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₉ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.centroid) - (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁₀ : ‖s.centroid -ᵥ s.points i - (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₁₁ : ‖s.circumcenter -ᵥ s.points i‖ = ‖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
⊢ s.ninePointCircle = s.medial.circumsphere
have a : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center ∧
  Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
Tactic: apply s.medial.circumsphere_unique_dist_eq.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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center ∧
    Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
have a : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center
Tactic: constructor
-- 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
a : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center ∧
    Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
have a₁ : Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
Tactic: constructor
-- 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
⊢ Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
have a : ∀ (y : Fin (n + 1)), s.medial.points y ∈ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
Tactic: rw [Set.range_subset_iff]
-- 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).eulerPoint = s.eulerPoint ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
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).eulerPoint = s.eulerPoint ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have h₁ : ∀ (i : Fin (m + 1)), (s.reindex e).eulerPoint i = (s.eulerPoint ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
Tactic: ext 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
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (↑((s.restrict S hS).eulerPoint i) : P) = s.eulerPoint i
have this : Nonempty.{u_2 + 1} ↥S
Tactic: haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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)
⊢ s.points i -ᵥ s.eulerPoint i = (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have rw : s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
  (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
Tactic: rw [eulerPoint, vsub_vadd_eq_vsub_sub]
-- 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)
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have pos : ∀ (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)
Tactic: by_cases hn : n = 0
-- 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)
pos :
  ∀ (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)
⊢ 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 : ∀ (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)
Tactic: by_cases hn : n = 0
-- 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
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
have pos : ∀ (s : Simplex ℝ P 0) (i : 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)
Tactic: obtain rfl := hn
Cleared hypotheses: n, s, i, hn
-- 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)
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)
have this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
Tactic: have : Subsingleton (Fin (0 + 1)) := inferInstanceAs (Subsingleton (Fin 1))