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
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
⊢ ∃ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
      ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
have inl : ∀ (i₁ i₂ i₃ j₂ j₃ : Fin 3),
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ (h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) (h₁ : p i₁ = t.orthocenter) (hj₂₃ : j₂ ≠ j₃)
          (h₂ : t.points j₂ = p i₂) (h₃ : t.points j₃ = p i₃),
          ∃ (c : P),
            Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
              ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
Tactic: rcases exists_of_range_subset_orthocentricSystem ho hps hpi with
    (⟨i₁, i₂, i₃, j₂, j₃, _, _, _, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
inl :
  ∀ (i₁ i₂ i₃ j₂ j₃ : Fin 3),
    i₁ ≠ i₂ →
      i₁ ≠ i₃ →
        i₂ ≠ i₃ →
          ∀ (h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) (h₁ : p i₁ = t.orthocenter) (hj₂₃ : j₂ ≠ j₃)
            (h₂ : t.points j₂ = p i₂) (h₃ : t.points j₃ = p i₃),
            ∃ (c : P),
              Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
                ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
⊢ ∃ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
      ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
have inr : ∀ (hs : Set.range p = Set.range t.points),
  ∃ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
      ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
Tactic: rcases exists_of_range_subset_orthocentricSystem ho hps hpi with
    (⟨i₁, i₂, i₃, j₂, j₃, _, _, _, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ ∃ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
      ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
have right : ∀ p₁ ∈ Set.range p,
  dist p₁ ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
Tactic: use reflection (affineSpan ℝ (t.points '' {j₂, j₃})) t.circumcenter,
      reflection_mem_of_le_of_mem (affineSpan_mono ℝ (Set.image_subset_range _ _))
        t.circumcenter_mem_affineSpan
-- 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
p₁ : P
hp₁ : p₁ ∈ Set.range p
⊢ dist p₁ ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : ∀ (i : Fin 3),
  dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
Tactic: rcases hp₁ with ⟨i, rfl⟩
Cleared hypotheses: p₁, hp₁
-- 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have h₁₂₄ : i = i₁ ∨ i = i₂ ∨ i = i₃
Tactic: have h₁₂₃ := h₁₂₃ 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : ∀ (h₁₂₃ : i = i₁),
  dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
right :
  ∀ (h₁₂₃ : i = i₁),
    dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
      Simplex.circumradius t
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right₁ : ∀ (h₁₂₃ : i = i₂ ∨ i = i₃),
  dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : dist (p i₁) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
  Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: i, 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₂ ∨ i = i₃
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : ∀ (h₁₂₃ : i = i₂),
  dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₂ ∨ i = i₃
right :
  ∀ (h₁₂₃ : i = i₂),
    dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
      Simplex.circumradius t
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right₁ : ∀ (h₁₂₃ : i = i₃),
  dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₂
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
  Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: i, 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₃
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
  Simplex.circumradius t
Tactic: rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: i, 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : dist (p i₁) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
  Simplex.circumradius t
Tactic: repeat' rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: i, 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
right :
  dist (p i₁) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right₁ : dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
  Simplex.circumradius t
Tactic: repeat' rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: i, 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃_1 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
right :
  dist (p i₁) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
right₁ :
  dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right₂ : dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
  Simplex.circumradius t
Tactic: repeat' rcases h₁₂₃ with h₁₂₃ | h₁₂₃
Cleared hypotheses: i, 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : dist (t.points j₂) (Simplex.circumcenter t) = Simplex.circumradius t
Tactic: rw [← h₂, dist_reflection_eq_of_mem _
       (mem_affineSpan ℝ (Set.mem_image_of_mem _ (Set.mem_insert _ _)))]
-- 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left : i₁ ≠ i₂
left_1 : i₁ ≠ i₃
left_2 : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t
have right : dist (t.points j₃) (Simplex.circumcenter t) = Simplex.circumradius t
Tactic: rw [← h₃,
        dist_reflection_eq_of_mem _
          (mem_affineSpan ℝ
            (Set.mem_image_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))]
-- 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
⊢ ∃ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c ∧
      ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
have right : ∀ p₁ ∈ Set.range p, dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t
Tactic: use t.circumcenter, t.circumcenter_mem_affineSpan
-- 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
p₁ : P
hp₁ : p₁ ∈ Set.range p
⊢ dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t
have hp₂ : p₁ ∈ Set.range t.points
Tactic: rw [hs] at hp₁
Cleared hypotheses: hp₁
-- 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
p₁ : P
hp₁ : p₁ ∈ Set.range t.points
⊢ dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t
have right : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), dist (t.points i) (Simplex.circumcenter t) = Simplex.circumradius t
Tactic: rcases hp₁ with ⟨i, rfl⟩
Cleared hypotheses: p₁, hp₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p
have rcases : ∀ (t : Triangle ℝ P) (hto : t.orthocenter ∉ Set.range t.points) (hst : s = insert t.orthocenter (Set.range t.points)),
  AffineIndependent ℝ p
Tactic: rcases ho with ⟨t, hto, hst⟩
Cleared hypotheses: ho
-- 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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
⊢ AffineIndependent ℝ p
have hps₁ : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
Tactic: rw [hst] at hps
Cleared hypotheses: hps, hto, hst
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hpi : Function.Injective p
t : Triangle ℝ P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
⊢ AffineIndependent ℝ p
have rcases : ∀ (c : P),
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c →
    ∀ (hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t), AffineIndependent ℝ p
Tactic: rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto hps hpi with ⟨c, _, hc⟩
-- 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
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)
have ha : AffineIndependent ℝ p
Tactic: have ha := ho.affineIndependent hps hpi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)
have rcases : ∀ (t : Triangle ℝ P),
  t.orthocenter ∉ Set.range t.points →
    ∀ (hts : s = insert t.orthocenter (Set.range t.points)),
      Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)
Tactic: rcases ho with ⟨t, _, hts⟩
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
have rw : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (insert t.orthocenter (Set.range t.points)))
  (affineSpan ℝ (Set.range t.points))
Tactic: rw [hts, affineSpan_insert_eq_affineSpan ℝ t.orthocenter_mem_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
rw :
  Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (insert t.orthocenter (Set.range t.points)))
    (affineSpan ℝ (Set.range t.points))
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
have rw₁ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) (affineSpan ℝ (Set.range t.points))
Tactic: rw [hts, affineSpan_insert_eq_affineSpan ℝ t.orthocenter_mem_affineSpan]