-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem affineSpan_pair_eq_altitude_iff {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2))
    (p : P) :
    line[ℝ, p, s.points i] = s.altitude i ↔
      p ≠ s.points i ∧
        p ∈ affineSpan ℝ (Set.range s.points) ∧
          p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).directionᗮ

Proof state:
case mpr.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ Submodule.span ℝ {p -ᵥ s.points i} = (s.altitude i).direction

Tactic:
refine Submodule.eq_of_le_of_finrank_eq ?_ ?_

Result:
case mpr.intro.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ Submodule.span ℝ {p -ᵥ s.points i} ≤ (s.altitude i).direction

case mpr.intro.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank ℝ ↥(Submodule.span ℝ {p -ᵥ s.points i}) = finrank ℝ ↥(s.altitude i).direction

Proof state:
case mp.left
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
⊢ False

Tactic:
have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]

Result:
case mp.left
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
hd : finrank ℝ ↥(s.altitude i).direction = 0
⊢ False

Proof state:
case mpr.intro.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank ℝ ↥(Submodule.span ℝ {p -ᵥ s.points i}) = finrank ℝ ↥(s.altitude i).direction

Tactic:
rw [finrank_direction_altitude, finrank_span_set_eq_card]

Result:
case mpr.intro.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ #{p -ᵥ s.points i}.toFinset = 1

case mpr.intro.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ LinearIndepOn ℝ id {p -ᵥ s.points i}

Proof state:
case mpr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
⊢ p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧
        p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ →
    vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
rintro ⟨hne, h⟩

Result:
case mpr.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h :
  p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ p -ᵥ s.points i ≠ 0

Tactic:
simpa using hne

Result:
no goals

Proof state:
case mpr.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h :
  p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude] at h

Result:
case mpr.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
⊢ finrank ℝ ↥(s.altitude i).direction = 0

Tactic:
rw [← h, finrank_bot]

Result:
no goals

Proof state:
case mpr.intro.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ Submodule.span ℝ {p -ᵥ s.points i} ≤ (s.altitude i).direction

Tactic:
rw [Submodule.span_le]

Result:
case mpr.intro.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ {p -ᵥ s.points i} ⊆ ↑(s.altitude i).direction

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧
        p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ

Tactic:
constructor

Result:
case mp
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction →
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧
        p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ

case mpr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
⊢ p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧
        p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ →
    vectorSpan ℝ {p, s.points i} = (s.altitude i).direction