-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePoint_mem_mongePlane {n : ℕ} (s : Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)} :
    s.mongePoint ∈ 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₁ i₂ : Fin (n + 3)
v : V
hv : v ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) v = 0

Tactic:
rcases Submodule.mem_span_singleton.mp hv with ⟨r, rfl⟩

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₁ i₂ : Fin (n + 3)
r : ℝ
hv : r • (s.points i₁ -ᵥ s.points i₂) ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) (r • (s.points i₁ -ᵥ s.points i₂)) = 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₁ i₂ : Fin (n + 3)
⊢ s.mongePoint ∈ s.mongePlane i₁ i₂

Tactic:
rw [mongePlane_def, mem_inf_iff, ← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _),
  direction_mk', Submodule.mem_orthogonal']

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₁ i₂ : Fin (n + 3)
⊢ (∀ u ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}, inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) u = 0) ∧
    s.mongePoint ∈ affineSpan ℝ (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₁ i₂ : Fin (n + 3)
⊢ ∀ u ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}, inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) u = 0

Tactic:
intro v hv

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₁ i₂ : Fin (n + 3)
v : V
hv : v ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) v = 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₁ i₂ : Fin (n + 3)
⊢ (∀ u ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}, inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) u = 0) ∧
    s.mongePoint ∈ affineSpan ℝ (Set.range s.points)

Tactic:
refine ⟨?_, s.mongePoint_mem_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 + 2)
i₁ i₂ : Fin (n + 3)
⊢ ∀ u ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}, inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) u = 0

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₁ i₂ : Fin (n + 3)
r : ℝ
hv : r • (s.points i₁ -ᵥ s.points i₂) ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) (r • (s.points i₁ -ᵥ s.points i₂)) = 0

Tactic:
rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]

Result:
no goals