-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem OrthocentricSystem.affineIndependent {s : Set P} (ho : OrthocentricSystem s) {p : Fin 3 → P}
    (hps : Set.range p ⊆ s) (hpi : Function.Injective p) : AffineIndependent ℝ p

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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

Tactic:
rw [hst] at hps

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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

Proof state:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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)
c : P
left✝ : c ∈ affineSpan ℝ (Set.range t.points)
hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
⊢ AffineIndependent ℝ p

Tactic:
exact Cospherical.affineIndependent ⟨c, t.circumradius, hc⟩ Set.Subset.rfl hpi

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p

Tactic:
rcases ho with ⟨t, hto, hst⟩

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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

Tactic:
rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto hps hpi with ⟨c, _, hc⟩

Result:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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)
c : P
left✝ : c ∈ affineSpan ℝ (Set.range t.points)
hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
⊢ AffineIndependent ℝ p