awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ ≠ i₃
h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
have 2 : ∀
  (h₁₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))
  (h₂₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2
Tactic: fin_cases i₃
Cleared hypotheses: i₃, h₁₃, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ ≠ i₃
h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
2 :
  ∀
    (h₁₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
have 2₁ : ∀
  (h₁₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩))
  (h₂₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2
Tactic: fin_cases i₃
Cleared hypotheses: i₃, h₁₃, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ ≠ i₃
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
have 2 : ∀
  (h₁₃ h₂₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2
Tactic: fin_cases i₃
Cleared hypotheses: i₃, h₁₃, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ ≠ i₃
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
2 :
  ∀
    (h₁₃ h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
have 2₁ : ∀
  (h₁₃ h₂₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2
Tactic: fin_cases i₃
Cleared hypotheses: i₃, h₁₃, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ ≠ i₃
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
2 :
  ∀
    (h₁₃ h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
h_1 :
  ∀
    (h₁₃ h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
have 2₁ : ∀
  (h₁₃ h₂₃ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
    π / 2
Tactic: fin_cases i₃
Cleared hypotheses: i₃, h₁₃, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
i : Fin 3
⊢ dist (t.points i) (Simplex.centroid t) = 2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
have rw : (↑2 : ℝ) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
  2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
Tactic: rw [Affine.Simplex.dist_point_centroid]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
i : Fin 3
⊢ (↑2 : ℝ) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
have norm_cast : 2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
  2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
i : Fin 3
⊢ dist (t.points i) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
have rw : HAdd.hAdd (α := ℝ) (↑2 : ℝ) 1 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
  3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
Tactic: rw [Affine.Simplex.dist_point_faceOppositeCentroid]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
i : Fin 3
⊢ HAdd.hAdd (α := ℝ) (↑2 : ℝ) 1 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
have norm_cast : (↑(HAdd.hAdd (α := ℕ) 2 1) : ℝ) * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i) =
  3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
⊢ { center := s.center, radius := s.radius } = s
have center : center { center := s.center, radius := s.radius : Sphere P } = s.center
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
center : Sphere.center { center := s.center, radius := s.radius : Sphere P } = s.center
⊢ { center := s.center, radius := s.radius } = s
have radius : radius { center := s.center, radius := s.radius : Sphere P } = s.radius
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
⊢ s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius
have rw : s₁ ≠ s₂ ↔ ¬(s₁.center = s₂.center ∧ s₁.radius = s₂.radius)
Tactic: rw [← not_and_or, ← Sphere.ext_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
rw : s₁ ≠ s₂ ↔ ¬(s₁.center = s₂.center ∧ s₁.radius = s₂.radius)
⊢ s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius
have rw₁ : s₁ ≠ s₂ ↔ ¬s₁ = s₂
Tactic: rw [← not_and_or, ← Sphere.ext_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
⊢ s₁.center = s₂.center ↔ s₁ = s₂
have refine : ∀ (h : s₁.center = s₂.center), s₁.radius = s₂.radius
Tactic: refine ⟨fun h => Sphere.ext h ?_, fun h => h ▸ rfl⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (hypothesis)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius
have hs₃ : dist p s₁.center = s₁.radius
Tactic: rw [mem_sphere] at hs₁ hs₂
Cleared hypotheses: hs₁, hs₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (hypothesis)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
hs₃ : dist p s₁.center = s₁.radius
⊢ s₁.radius = s₂.radius
have hs₄ : dist p s₂.center = s₂.radius
Tactic: rw [mem_sphere] at hs₁ hs₂
Cleared hypotheses: hs₁, hs₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : dist p s₁.center = s₁.radius
hs₂ : dist p s₂.center = s₂.radius
h : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius
have rw : dist p s₁.center = s₂.radius
Tactic: rw [← hs₁, ← hs₂, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : dist p s₁.center = s₁.radius
hs₂ : dist p s₂.center = s₂.radius
h : s₁.center = s₂.center
rw : dist p s₁.center = s₂.radius
⊢ s₁.radius = s₂.radius
have rw₁ : dist p s₁.center = dist p s₂.center
Tactic: rw [← hs₁, ← hs₂, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : dist p s₁.center = s₁.radius
hs₂ : dist p s₂.center = s₂.radius
h : s₁.center = s₂.center
rw : dist p s₁.center = s₂.radius
rw₁ : dist p s₁.center = dist p s₂.center
⊢ s₁.radius = s₂.radius
have rw₂ : dist p s₂.center = dist p s₂.center
Tactic: rw [← hs₁, ← hs₂, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ s.center = dist p₂ s.center
have rw : s.radius = dist p₂ s.center
Tactic: rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
rw : s.radius = dist p₂ s.center
⊢ dist p₁ s.center = dist p₂ s.center
have rw₁ : s.radius = s.radius
Tactic: rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist s.center p₁ = dist s.center p₂
have rw : s.radius = dist s.center p₂
Tactic: rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
rw : s.radius = dist s.center p₂
⊢ dist s.center p₁ = dist s.center p₂
have rw₁ : s.radius = s.radius
Tactic: rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
⊢ Cospherical ps ↔ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
have refine_1 : ∀ (h : Cospherical ps), ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
refine_1 : ∀ (h : Cospherical ps), ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps ↔ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
have refine_2 : ∀ (h : ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius), Cospherical ps
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
h : Cospherical ps
⊢ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
have refine_1 : ∀ (c : P) (r : ℝ) (h : ∀ p ∈ ps, dist p c = r), ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
Tactic: rcases h with ⟨c, r, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
ps : Set P
h : ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
have refine_2 : ∀ (s : Sphere P) (h : ps ⊆ Metric.sphere s.center s.radius), Cospherical ps
Tactic: rcases h with ⟨s, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
hc : Cospherical ps₂
⊢ Cospherical ps₁
have rcases : ∀ (c : P) (r : ℝ) (hcr : ∀ p ∈ ps₂, dist p c = r), Cospherical ps₁
Tactic: rcases hc with ⟨c, r, hcr⟩
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
P : Type u_2
inst : MetricSpace P
p : P
⊢ Cospherical (P := P) {p}
have h : ∃ (radius : ℝ), ∀ (p_1 : P), Membership.mem (γ := Set P) {p} p_1 → dist p_1 p = radius
Tactic: use p
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
hps : Cospherical ps
⊢ Cospherical (f '' ps)
have rcases : ∀ (c : E) (r : ℝ) (hc : ∀ p ∈ ps, dist p c = r), Cospherical (f '' ps)
Tactic: rcases hps with ⟨c, r, hc⟩
Cleared hypotheses: hps
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
⊢ Cospherical (f '' ps)
have refine : ∀ p ∈ f '' ps, dist p (f c) = r
Tactic: refine ⟨f c, r, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
p : E
hp : p ∈ ps
⊢ dist (f p) (f c) = r
have rw : dist p c = r
Tactic: rw [hf.dist_eq, hc p hp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MetricSpace E
inst_1 : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
p : E
hp : p ∈ ps
rw : dist p c = r
⊢ dist (f p) (f c) = r
have rw₁ : r = r
Tactic: rw [hf.dist_eq, hc p hp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
S₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
hps : Cospherical ps
hS : S₁ ≤ S₂
⊢ Cospherical (P := ↥S₂) ((⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂) '' ps)
have refine : Isometry.{u_2, u_2} (α := ↥S₁) (β := ↥S₂) (⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂)
Tactic: refine Isometry.cospherical ?_ hps
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
⊢ (Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius
have refine : ∀ (h : 0 ≤ s.radius), (Metric.sphere s.center s.radius).Nonempty
Tactic: refine ⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
⊢ (Metric.sphere s.center s.radius).Nonempty
have obtain : ∀ (v : V) (hv : Membership.mem (γ := Set V) (Metric.sphere 0 s.radius) v), (Metric.sphere s.center s.radius).Nonempty
Tactic: obtain ⟨v, hv⟩ := (NormedSpace.sphere_nonempty (x := (0 : V)) (r := s.radius)).2 h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
v : V
hv : Membership.mem (γ := Set V) (Metric.sphere 0 s.radius) v
⊢ (Metric.sphere s.center s.radius).Nonempty
have refine : v +ᵥ s.center ∈ Metric.sphere s.center s.radius
Tactic: refine ⟨v +ᵥ s.center, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₂ p : P
⊢ dist p (midpoint ℝ p p₂) = (norm (E := ℝ) 2)⁻¹ * dist p p₂
have inl : dist (midpoint ℝ p p₂) p = (norm (E := ℝ) 2)⁻¹ * dist p p₂
Tactic: rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]