-- 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 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
h : 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.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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p ≠ s.points i

case mp.right
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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ

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
⊢ {p -ᵥ s.points i} ⊆ ↑(s.altitude i).direction

Tactic:
simpa using h

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
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
p : P
⊢ affineSpan ℝ {p, s.points i} = s.altitude i ↔
    p ≠ s.points i ∧
      p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' ↑(univ.erase i))).directionᗮ

Tactic:
rw [eq_iff_direction_eq_of_mem (mem_affineSpan ℝ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))
    (s.mem_altitude _),
  ← vsub_right_mem_direction_iff_mem (mem_affineSpan ℝ (Set.mem_range_self i)) p,
  direction_affineSpan, direction_affineSpan, direction_affineSpan]

Result:
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)))ᗮ

Proof state:
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)))ᗮ

Tactic:
intro h

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
h : 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)))ᗮ

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
⊢ #{p -ᵥ s.points i}.toFinset = 1

Tactic:
simp

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 ∈ (s.altitude i).direction
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _),
  Set.insert_diff_of_mem _ (Set.mem_singleton _),
  Set.diff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]

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
⊢ Submodule.span ℝ {p -ᵥ s.points i} = (s.altitude i).direction

Proof state:
case mp.right
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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ

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

Result:
case mp.right
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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p -ᵥ s.points i ∈ vectorSpan ℝ {p, s.points i}

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
hd : finrank ℝ ↥(s.altitude i).direction = 0
⊢ False

Tactic:
simp at hd

Result:
no goals

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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p ≠ s.points i

Tactic:
intro heq

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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
heq : p = s.points i
⊢ False

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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
heq : p = s.points i
⊢ False

Tactic:
rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h

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
⊢ False

Proof state:
case mp.right
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 : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p -ᵥ s.points i ∈ vectorSpan ℝ {p, s.points i}

Tactic:
exact
  vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Result:
no goals