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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
x : V
⊢ (∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))) ↔
    ∃ (x_1 : Fin (n + 2 + 1)),
      (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x_1 ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
have h₁ : (∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))) →
  ∃ (x_1 : Fin (n + 2 + 1)),
    (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x_1 ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
Tactic: constructor
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
x : V
h₁ :
  (∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))) →
    ∃ (x_1 : Fin (n + 2 + 1)),
      (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x_1 ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
⊢ (∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))) ↔
    ∃ (x_1 : Fin (n + 2 + 1)),
      (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x_1 ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
have h₂ : (∃ (x_1 : Fin (n + 2 + 1)),
    (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x_1 ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x) →
  ∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))
Tactic: constructor
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
i : { i : Fin (n + 3) // i₁ ≠ i }
w : Fin (n + 2 + 1)
⊢ ∃ (x : Fin (n + 2 + 1)),
    (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x ∧ x ≠ i₁) ∧
      s.points i₁ -ᵥ s.points x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))
have left : Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ (↑i : Fin (n + 3)) ∧ (↑i : Fin (n + 3)) ≠ i₁
Tactic: use i, ⟨Set.mem_univ _, i.property.symm⟩
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
i : { i : Fin (n + 3) // i₁ ≠ i }
w : Fin (n + 2 + 1)
left : Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ (↑i : Fin (n + 3)) ∧ (↑i : Fin (n + 3)) ≠ i₁
⊢ ∃ (x : Fin (n + 2 + 1)),
    (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x ∧ x ≠ i₁) ∧
      s.points i₁ -ᵥ s.points x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))
have right : s.points i₁ -ᵥ s.points (↑i : Fin (n + 3)) = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))
Tactic: use i, ⟨Set.mem_univ _, i.property.symm⟩
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi_1 :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
i : Fin (n + 2 + 1)
hi : i ≠ i₁
⊢ ∃ (i_1 : { i : Fin (n + 3) // i₁ ≠ i }), s.points i₁ -ᵥ s.points i = s.points i₁ -ᵥ s.points (↑i_1 : Fin (n + 3))
have w : { i : Fin (n + 3) // i₁ ≠ i }
Tactic: use ⟨i, hi.symm⟩
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi_1 :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
i : Fin (n + 2 + 1)
hi : i ≠ i₁
w : { i : Fin (n + 3) // i₁ ≠ i }
⊢ ∃ (i_1 : { i : Fin (n + 3) // i₁ ≠ i }), s.points i₁ -ᵥ s.points i = s.points i₁ -ᵥ s.points (↑i_1 : Fin (n + 3))
have h₁ : s.points i₁ -ᵥ s.points i =
  s.points i₁ -ᵥ s.points (↑(Subtype.mk (p := fun (i : Fin (n + 3)) ↦ i₁ ≠ i) i sorry) : Fin (n + 3))
Tactic: use ⟨i, hi.symm⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
⊢ p -ᵥ s.mongePoint = 0
have hu : Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
  ((fun (x : P) ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁}))
Tactic: have hu :
    ⋃ i : { i // i₁ ≠ i }, ({s.points i₁ -ᵥ s.points i} : Set V) =
      (s.points i₁ -ᵥ ·) '' s.points '' (Set.univ \ {i₁}) := by
    rw [Set.image_image]
    ext x
    simp_rw [Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_diff_singleton]
    constructor
    · rintro ⟨i, rfl⟩
      use i, ⟨Set.mem_univ _, i.property.symm⟩
    · rintro ⟨i, ⟨-, hi⟩, rfl⟩
      use ⟨i, hi.symm⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
hu :
  Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
    ((fun (x : P) ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁}))
⊢ p -ᵥ s.mongePoint = 0
have hi₁ : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
Tactic: rw [hu, ← vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_univ _), Set.image_univ] at hi
Cleared hypotheses: hi, hu
-- 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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
    ((fun (x : P) ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
have obtain : ∀ (i₂ : Fin (n + 3)) (h₂ : i₂ ∈ s₁),
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
Tactic: obtain ⟨i₂, h₂⟩ := card_pos.1 (show 0 < #s₁ by simp [s₁, card_erase_of_mem])
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
    ((fun (x : P) ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
i₂ : Fin (n + 3)
h₂ : i₂ ∈ s₁
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
have h₁₂ : i₁ ≠ i₂
Tactic: have h₁₂ : i₁ ≠ i₂ := (ne_of_mem_erase h₂).symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
    ((fun (x : P) ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁}))
⊢ p -ᵥ s.mongePoint = 0
have hv : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
Tactic: have hv : p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points) := by
    let s₁ : Finset (Fin (n + 3)) := univ.erase i₁
    obtain ⟨i₂, h₂⟩ := card_pos.1 (show 0 < #s₁ by simp [s₁, card_erase_of_mem])
    have h₁₂ : i₁ ≠ i₂ := (ne_of_mem_erase h₂).symm
    exact (Submodule.mem_inf.1 (h' i₂ h₁₂)).2
-- 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
t : Triangle ℝ P
⊢ t.orthocenter = HSMul.hSMul (α := ℝ) 3 (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
have rw : HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 2 1) : ℝ) (↑(HSub.hSub (α := ℕ) 2 1) : ℝ) •
      (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ
    circumcenter t =
  HSMul.hSMul (α := ℝ) 3 (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
Tactic: rw [orthocenter_eq_mongePoint, mongePoint_eq_smul_vsub_vadd_circumcenter]
-- 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
t : Triangle ℝ P
⊢ t.orthocenter -ᵥ circumcenter t = ∑ i : Fin (2 + 1), (t.points i -ᵥ circumcenter t)
have rw : t.orthocenter -ᵥ circumcenter t = HAdd.hAdd (α := ℕ) 0 1 • (mongePoint t -ᵥ circumcenter t)
Tactic: rw [← t.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, zero_add, one_smul,
    orthocenter_eq_mongePoint]
-- 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
t : Triangle ℝ P
rw : t.orthocenter -ᵥ circumcenter t = HAdd.hAdd (α := ℕ) 0 1 • (mongePoint t -ᵥ circumcenter t)
rw₁ : t.orthocenter -ᵥ circumcenter t = HSMul.hSMul (α := ℕ) 1 (mongePoint t -ᵥ circumcenter t)
⊢ t.orthocenter -ᵥ circumcenter t = ∑ i : Fin (2 + 1), (t.points i -ᵥ circumcenter t)
have rw₂ : t.orthocenter -ᵥ circumcenter t = mongePoint t -ᵥ circumcenter t
Tactic: rw [← t.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, zero_add, one_smul,
    orthocenter_eq_mongePoint]
-- 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
t : Triangle ℝ P
rw : t.orthocenter -ᵥ circumcenter t = HAdd.hAdd (α := ℕ) 0 1 • (mongePoint t -ᵥ circumcenter t)
rw₁ : t.orthocenter -ᵥ circumcenter t = HSMul.hSMul (α := ℕ) 1 (mongePoint t -ᵥ circumcenter t)
rw₂ : t.orthocenter -ᵥ circumcenter t = mongePoint t -ᵥ circumcenter t
⊢ t.orthocenter -ᵥ circumcenter t = ∑ i : Fin (2 + 1), (t.points i -ᵥ circumcenter t)
have rw₃ : mongePoint t -ᵥ circumcenter t = mongePoint t -ᵥ circumcenter t
Tactic: rw [← t.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, zero_add, one_smul,
    orthocenter_eq_mongePoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ altitude t i₁ = mongePlane t i₂ i₃
have hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
Tactic: have hs : ({i₂, i₃}ᶜ : Finset (Fin 3)) = {i₁} := by decide +revert
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
⊢ altitude t i₁ = mongePlane t i₂ i₃
have he : Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}
Tactic: have he : ({i₁}ᶜ : Set (Fin 3)) = {i₂, i₃} := by grind
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : Eq (α := Finset (Fin 3)) {i₂, i₃}ᶜ {i₁}
he : Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}
⊢ altitude t i₁ = mongePlane t i₂ i₃
have rw : Eq (α := AffineSubspace ℝ P)
  (mk' (t.points i₁) (Submodule.span ℝ ((fun (x : P) ↦ t.points i₂ -ᵥ x) '' t.points '' ({i₂, i₃} \ {i₂})))ᗮ ⊓
    affineSpan ℝ (Set.range t.points))
  (mk' (t.points i₁) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points))
Tactic: rw [mongePlane_def, altitude_def, direction_affineSpan, hs, he, centroid_singleton,
    vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_insert i₂ _)]
-- 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
t : Triangle ℝ P
i₁ : Fin 3
⊢ t.orthocenter ∈ altitude t i₁
have obtain : ∀ (i₂ i₃ : Fin 3) (h₁₂ : i₁ ≠ i₂) (h₂₃ : i₂ ≠ i₃) (h₁₃ : i₁ ≠ i₃), t.orthocenter ∈ altitude t i₁
Tactic: obtain ⟨i₂, i₃, h₁₂, h₂₃, h₁₃⟩ : ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
    decide +revert
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ t.orthocenter ∈ altitude t i₁
have rw : mongePoint t ∈ mongePlane t i₂ i₃
Tactic: rw [orthocenter_eq_mongePoint, t.altitude_eq_mongePlane 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
⊢ p = t.orthocenter
have obtain : ∀ (i₃ : Fin 3) (h₂₃ : i₂ ≠ i₃) (h₁₃ : i₁ ≠ i₃), p = t.orthocenter
Tactic: obtain ⟨i₃, h₂₃, h₁₃⟩ : ∃ i₃, i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
    clear h₁ h₂
    decide +revert
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p = t.orthocenter
have h₃ : p ∈ mongePlane t i₃ i₂
Tactic: rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁
Cleared hypotheses: h₁, h₂₃, h₁₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p = t.orthocenter
have h₃ : p ∈ mongePlane t i₃ i₁
Tactic: rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂
Cleared hypotheses: h₂, 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
i : Fin 3
hi : i₃ ≠ i
⊢ p ∈ mongePlane t i₃ i
have inl : ∀ (hi : i₃ ≠ i₁), p ∈ mongePlane t i₃ i₁
Tactic: obtain rfl | rfl : i₁ = i ∨ i₂ = i := by lia
Cleared hypotheses: i, hi
-- 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
i : Fin 3
hi : i₃ ≠ i
inl : ∀ (hi : i₃ ≠ i₁), p ∈ mongePlane t i₃ i₁
⊢ p ∈ mongePlane t i₃ i
have inr : ∀ (hi : i₃ ≠ i₂), p ∈ mongePlane t i₃ i₂
Tactic: obtain rfl | rfl : i₁ = i ∨ i₂ = i := by lia
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (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
t : Triangle ℝ P
i₁ i₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
i₃ : Fin 3
h₂ : p ∈ mongePlane t i₃ i₁
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p = mongePoint t
have ha : ∀ (i : Fin 3), i₃ ≠ i → p ∈ mongePlane t i₃ i
Tactic: have ha : ∀ i, i₃ ≠ i → p ∈ t.mongePlane i₃ i := by
    intro i hi
    obtain rfl | rfl : i₁ = i ∨ i₂ = i := by lia
    all_goals assumption
-- 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t
have rw : HDiv.hDiv (α := ℝ)
    (-∑ i₁_1 : PointsWithCircumcenterIndex 2,
        ∑ i₂_1 : PointsWithCircumcenterIndex 2,
          HSub.hSub (α := PointsWithCircumcenterIndex 2 → ℝ) (mongePointWeightsWithCircumcenter 0)
                (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₁_1 *
              HSub.hSub (α := PointsWithCircumcenterIndex 2 → ℝ) (mongePointWeightsWithCircumcenter 0)
                (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₂_1 *
            (dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1) *
              dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1)))
    2 =
  circumradius t * circumradius t
Tactic: rw [← mul_self_inj_of_nonneg dist_nonneg t.circumradius_nonneg,
    t.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter h,
    t.orthocenter_eq_mongePoint, mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
    dist_affineCombination t.pointsWithCircumcenter (sum_mongePointWeightsWithCircumcenter _)
      (sum_reflectionCircumcenterWeightsWithCircumcenter h)]