-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePlane_comm {n : ℕ} (s : Simplex ℝ P (n + 2)) (i₁ i₂ : Fin (n + 3)) :
    s.mongePlane i₁ i₂ = s.mongePlane i₂ i₁

Proof state:
case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
⊢ ∃ a, a • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)

Tactic:
use -r

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₁ i₂ : Fin (n + 3)
r : ℝ
⊢ -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)

Proof state:
case e_a.e_p.e_s
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)
⊢ {i₁, i₂}ᶜ = {i₂, i₁}ᶜ

Tactic:
congr 1

Result:
case e_a.e_p.e_s.e_a
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)
⊢ {i₁, i₂} = {i₂, i₁}

Proof state:
case e_a.e_p.e_s.e_a
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)
⊢ {i₁, i₂} = {i₂, i₁}

Tactic:
exact pair_comm _ _

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₁ i₂ : Fin (n + 3)
⊢ s.mongePlane i₁ i₂ = s.mongePlane i₂ i₁

Tactic:
simp_rw [mongePlane_def]

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)
⊢ mk' (centroid ℝ {i₁, i₂}ᶜ s.points) (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓
      affineSpan ℝ (Set.range s.points) =
    mk' (centroid ℝ {i₂, i₁}ᶜ s.points) (Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁})ᗮ ⊓
      affineSpan ℝ (Set.range s.points)

Proof state:
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₁ i₂ : Fin (n + 3)
r : ℝ
⊢ -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)

Tactic:
rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

Result:
no goals

Proof state:
case e_a.e_direction.e_K.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₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝) ↔ ∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝

Tactic:
constructor

Result:
case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝) → ∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝

case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝) → ∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝

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)
⊢ mk' (centroid ℝ {i₁, i₂}ᶜ s.points) (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓
      affineSpan ℝ (Set.range s.points) =
    mk' (centroid ℝ {i₂, i₁}ᶜ s.points) (Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁})ᗮ ⊓
      affineSpan ℝ (Set.range s.points)

Tactic:
congr 3

Result:
case e_a.e_p.e_s
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)
⊢ {i₁, i₂}ᶜ = {i₂, i₁}ᶜ

case e_a.e_direction.e_K
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)
⊢ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂} = Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁}

Proof state:
case e_a.e_direction.e_K.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₁ i₂ : Fin (n + 3)
x✝ : V
⊢ x✝ ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂} ↔ x✝ ∈ Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁}

Tactic:
simp_rw [Submodule.mem_span_singleton]

Result:
case e_a.e_direction.e_K.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₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝) ↔ ∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝

Proof state:
case e_a.e_direction.e_K
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)
⊢ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂} = Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁}

Tactic:
ext

Result:
case e_a.e_direction.e_K.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₁ i₂ : Fin (n + 3)
x✝ : V
⊢ x✝ ∈ Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂} ↔ x✝ ∈ Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁}

Proof state:
case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝) → ∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝

case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝) → ∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝

Tactic:
all_goals rintro ⟨r, rfl⟩; use -r; rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

Result:
no goals

Proof state:
case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
x✝ : V
⊢ (∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝) → ∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝

Tactic:
rintro ⟨r, rfl⟩

Result:
case e_a.e_direction.e_K.h.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 + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
⊢ ∃ a, a • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)