-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem eq_mongePoint_of_forall_mem_mongePlane {n : ℕ} {s : Simplex ℝ P (n + 2)} {i₁ : Fin (n + 3)}
    {p : P} (h : ∀ i₂, i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂) : p = s.mongePoint

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))
⊢ p -ᵥ s.mongePoint = 0

Tactic:
rw [hu, ← vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_univ _), Set.image_univ] at hi

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))
⊢ p -ᵥ s.mongePoint = 0

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))
hv : p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points)
⊢ p -ᵥ s.mongePoint = 0

Tactic:
exact Submodule.disjoint_def.1 (vectorSpan ℝ (Set.range s.points)).orthogonal_disjoint _ hv hi

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
⊢ ∀ (i : { i // i₁ ≠ i }), p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points ↑i})ᗮ

Tactic:
exact fun i => (Submodule.mem_inf.1 (h' i i.property)).1

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
i₂ : Fin (n + 3)
hne : i₁ ≠ i₂
⊢ p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
rw [← s.direction_mongePlane, vsub_right_mem_direction_iff_mem s.mongePoint_mem_mongePlane]

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
i₂ : Fin (n + 3)
hne : i₁ ≠ i₂
⊢ p ∈ s.mongePlane i₁ i₂

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
⊢ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})

Tactic:
ext x

Result:
case h
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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
x : V
⊢ x ∈ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} ↔ x ∈ (fun x => s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})

Proof state:
case 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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))
s₁ : Finset (Fin (n + 3)) := univ.erase i₁
i₂ : Fin (n + 3)
h₂ : i₂ ∈ s₁
⊢ p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points)

Tactic:
have h₁₂ : i₁ ≠ i₂ := (ne_of_mem_erase h₂).symm

Result:
case 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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))
s₁ : Finset (Fin (n + 3)) := univ.erase i₁
i₂ : Fin (n + 3)
h₂ : i₂ ∈ s₁
h₁₂ : i₁ ≠ i₂
⊢ p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points)

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))
s₁ : Finset (Fin (n + 3)) := univ.erase i₁
⊢ 0 < #s₁

Tactic:
simp [s₁, card_erase_of_mem]

Result:
no goals