-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem altitude_eq_mongePlane (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃)
    (h₂₃ : i₂ ≠ i₃) : t.altitude i₁ = t.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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : univ.erase i₁ = {i₂, i₃}
⊢ mk' (t.points i₁) (Submodule.span ℝ ((fun x => t.points i₂ -ᵥ x) '' (t.points '' ({i₂, i₃} \ {i₂}))))ᗮ ⊓
      affineSpan ℝ (Set.range t.points) =
    mk' (t.points i₁) (Submodule.span ℝ {t.points i₂ -ᵥ t.points i₃})ᗮ ⊓ affineSpan ℝ (Set.range t.points)

Tactic:
simp [h₂₃, Submodule.span_insert_eq_span]

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ altitude t i₁ = mongePlane t i₂ i₃

Tactic:
have hs : ({i₂, i₃}ᶜ : Finset (Fin 3)) = {i₁} := by decide +revert

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
⊢ altitude t i₁ = mongePlane t 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ {i₂, i₃}ᶜ = {i₁}

Tactic:
decide +revert

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : univ.erase i₁ = {i₂, i₃}
⊢ altitude t i₁ = mongePlane t i₂ i₃

Tactic:
rw [mongePlane_def, altitude_def, direction_affineSpan, hs, he, centroid_singleton, coe_insert,
  coe_singleton, vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_insert i₂ _)]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : univ.erase i₁ = {i₂, i₃}
⊢ mk' (t.points i₁) (Submodule.span ℝ ((fun x => t.points i₂ -ᵥ x) '' (t.points '' ({i₂, i₃} \ {i₂}))))ᗮ ⊓
      affineSpan ℝ (Set.range t.points) =
    mk' (t.points i₁) (Submodule.span ℝ {t.points i₂ -ᵥ t.points i₃})ᗮ ⊓ affineSpan ℝ (Set.range t.points)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
⊢ univ.erase i₁ = {i₂, i₃}

Tactic:
decide +revert

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
⊢ altitude t i₁ = mongePlane t i₂ i₃

Tactic:
have he : univ.erase i₁ = {i₂, i₃} := by decide +revert

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : univ.erase i₁ = {i₂, i₃}
⊢ altitude t i₁ = mongePlane t i₂ i₃