awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ insert t.orthocenter (Set.range t.points) \ {t.orthocenter}
⊢ Set.range p ⊆ Set.range t.points

Tactic:
rw [Set.insert_diff_self_of_notMem ho] at hs

Premises used: Set.insert_diff_self_of_notMem
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Set.range p = Set.range t.points

Tactic:
Set.eq_of_subset_of_card_le hs ?_

Premises used: Set.eq_of_subset_of_card_le
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)
⊢ Set.range p = Set.range t.points

Tactic:
refine Set.eq_of_subset_of_card_le hs ?_

Premises used: Set.eq_of_subset_of_card_le
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card (Fin 3)
neg₁ neg₂ : Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) ≤ Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1))
⊢ Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)

Tactic:
rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]

Premises used: AffineIndependent.injective, Set.card_range_of_injective, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)
⊢ Set.range p = Set.range t.points

Tactic:
classical
    refine Set.eq_of_subset_of_card_le hs ?_
    rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
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
⊢ ∃ (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)

Premises used: EuclideanGeometry.exists_of_range_subset_orthocentricSystem
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₃
right :
  ∀ p₁ ∈ Set.range p,
    dist p₁ ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
      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

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

Premises used: Affine.Simplex.points, Affine.Simplex.circumcenter_mem_affineSpan, Real, Affine.Simplex.circumcenter, Set.image_subset_range, Insert.insert, EuclideanGeometry.reflection, affineSpan, Set.image, affineSpan_mono, Singleton.singleton, DFunLike.coe, EuclideanGeometry.reflection_mem_of_le_of_mem
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
right :
  ∀ (i : Fin 3),
    dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
      Simplex.circumradius t
⊢ dist p₁ ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t

Tactic:
rcases hp₁ with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
⊢ i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
have h₁₂₃ := h₁₂₃ i
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
right₁ :
  ∀ (h₁₂₃ : i = i₂ ∨ 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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₁
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₂
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₃
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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

Tactic:
rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
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

Tactic:
repeat' rcases h₁₂₃ with h₁₂₃ | h₁₂₃
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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 t.orthocenter ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t

Tactic:
Triangle.dist_orthocenter_reflection_circumcenter t hj₂₃

Premises used: Affine.Triangle.dist_orthocenter_reflection_circumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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

Tactic:
convert! Triangle.dist_orthocenter_reflection_circumcenter t hj₂₃

Premises used: Affine.Triangle.dist_orthocenter_reflection_circumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₃
right : dist (t.points j₂) (Simplex.circumcenter t) = Simplex.circumradius t
⊢ dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (Simplex.circumcenter t)) =
    Simplex.circumradius t

Tactic:
rw [← h₂, dist_reflection_eq_of_mem _
       (mem_affineSpan ℝ (Set.mem_image_of_mem _ (Set.mem_insert _ _)))]

Premises used: Real, mem_affineSpan, EuclideanGeometry.dist_reflection_eq_of_mem, Set.mem_image_of_mem, Set.mem_insert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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 (t.points j₂) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
t.dist_circumcenter_eq_circumradius _

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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 (t.points j₂) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
exact t.dist_circumcenter_eq_circumradius _

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₃
right : dist (t.points j₃) (Simplex.circumcenter t) = Simplex.circumradius t
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃})) : (a : P) → P) (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 _))))]

Premises used: Set.mem_singleton, Real, Set.mem_insert_of_mem, mem_affineSpan, EuclideanGeometry.dist_reflection_eq_of_mem, Set.mem_image_of_mem
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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 (t.points j₃) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
t.dist_circumcenter_eq_circumradius _

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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 (t.points j₃) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
exact t.dist_circumcenter_eq_circumradius _

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
right : ∀ p₁ ∈ Set.range p, dist p₁ (Simplex.circumcenter t) = 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

Tactic:
use t.circumcenter, t.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, Affine.Simplex.circumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
⊢ p₁ ∈ Set.range t.points

Tactic:
rw [hs] at hp₁