Collinearity in an isosceles triangle

Stream: maths

[Brisal]

In an isosceles triangle ABC, the angle bisector of the top angle meets BC at M. Then I draw a line inside the triangle parallel to the base, meeting AB at D and AC at E. Let P be the midpoint of DE. How can I prove in Lean4 that A, P, M are collinear?Does Lean4 have a theorem that can solve this problem?

[Aaron Liu]

this should follow from that the angle bisector is the median

[Brisal]

The natural language of this problem has many representations, but I haven't found a suitable tactic in Lean4 to prove it. Do you have any experience with this?

Aaron Liu said:

this should follow from that the angle bisector is the median

[Aaron Liu]

do you have a statement of the problem yet?

[Brisal]

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Tangent
import Mathlib.Geometry.Euclidean.Triangle


open Affine Affine.Simplex EuclideanGeometry Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]

example {A B C D E M P : Pt}
  (hABC : AffineIndependent ℝ ![A, B, C])
  (hM : M = midpoint ℝ B C)
  (hD : D = midpoint ℝ A B)
  (hE : E = midpoint ℝ A C)
  (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
  (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  sorry

Perhaps it's this kind of situation: here I didn't define AM as the angle bisector, but I defined M as the midpoint of BC (which should be equivalent).

[Joseph Myers]

I think the basic fact you need is purely affine: given a vertex A of a simplex, an affine subspace parallel to the opposite face (and contained in the affine subspace spanned by the vertices of the simplex) intersects all the edges from A (the affine spans of A and another vertex) in the same ratio (i.e. the intersections are all given by lineMap with the same ratio argument). Once you have that, this specific problem should just be a matter of manipulating vectors for an explicit calculation of expressions for various vectors from A.

[Aaron Liu]

I'll type out a solution when I'm back at a keyboard

[Aaron Liu]

You might see some unused hypotheses

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Tangent
import Mathlib.Geometry.Euclidean.Triangle


open Affine Affine.Simplex EuclideanGeometry Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]

example {A B C D E M P : Pt}
    (hABC : AffineIndependent ℝ ![A, B, C])
    (hM : M = midpoint ℝ B C)
    (hD : D = midpoint ℝ A B)
    (hE : E = midpoint ℝ A C)
    (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
    (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  suffices h : P = midpoint ℝ A M by
    rw [h]
    apply collinear_triple_of_mem_affineSpan_pair
      (mem_affineSpan ℝ (Set.mem_insert A {M}))
      (mem_affineSpan ℝ (Set.mem_insert_of_mem A (Set.mem_singleton M)))
    apply Wbtw.mem_affineSpan
    apply wbtw_midpoint
  rw [hP, hD, hE, hM]
  apply vsub_left_injective A
  simp [midpoint_vsub]

[Brisal]

Aaron Liu said:

You might see some unused hypotheses

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Tangent
import Mathlib.Geometry.Euclidean.Triangle


open Affine Affine.Simplex EuclideanGeometry Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]

example {A B C D E M P : Pt}
    (hABC : AffineIndependent ℝ ![A, B, C])
    (hM : M = midpoint ℝ B C)
    (hD : D = midpoint ℝ A B)
    (hE : E = midpoint ℝ A C)
    (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
    (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  suffices h : P = midpoint ℝ A M by
    rw [h]
    apply collinear_triple_of_mem_affineSpan_pair
      (mem_affineSpan ℝ (Set.mem_insert A {M}))
      (mem_affineSpan ℝ (Set.mem_insert_of_mem A (Set.mem_singleton M)))
    apply Wbtw.mem_affineSpan
    apply wbtw_midpoint
  rw [hP, hD, hE, hM]
  apply vsub_left_injective A
  simp [midpoint_vsub]

Can this kind of proof be made more general? For example, instead of defining D and E as midpoints, I only know that line DE is parallel to BC. Would that still work? Something like that.

example {A B C D E M P : Pt}
    (hABC : AffineIndependent ℝ ![A, B, C])
    (hM : M = midpoint ℝ B C)
    (hD : D ∈ line[ℝ, A, B])
    (hE : E ∈ line[ℝ, A, C])
    (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
    (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  sorry

[Aaron Liu]

That sounds still work but now you need a different proof

[Jovan Gerbscheid]

I think we are still missing the (aa) similarity theorem in mathlib, but with that we can do this proof:

Triangle ABC is similar to ADE. And (degenerate) triangle MBC is similar to PDE. So, AMBC is similar to APDE. So, angle BAM equals angle DAP, so angle MAP equals 0, so AMP are collinear.

[Jovan Gerbscheid]

Hmm, although the theorem about glueing two similarities in general depends on the two similarities being oriented ths same, and we don't yet have this notion in mathlib :(

[Aaron Liu]

I don't think we need an orientation to prove this

[Jovan Gerbscheid]

Indeed, but I still want the notion of oriented similarities in mathlib :sweat_smile:

[Aaron Liu]

can we get an affine equation solver

[Aaron Liu]

some of these are very tedious

[Jovan Gerbscheid]

Isn't that grind?

[Aaron Liu]

I don't know I haven't tried it

[Aaron Liu]

grind failed

[Jovan Gerbscheid]

Oh right you need to put it in vector form somehow first

[Aaron Liu]

well here we go

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Tangent
import Mathlib.Geometry.Euclidean.Triangle


open Affine Affine.Simplex EuclideanGeometry Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)
variable [AddCommGroup V] [Module ℝ V] [AddTorsor V Pt]

example {A B C D E M P : Pt}
    (hM : M = midpoint ℝ B C)
    (hD : D ∈ line[ℝ, A, B])
    (hE : E ∈ line[ℝ, A, C])
    (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
    (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  obtain ⟨v, hv⟩ := h_Parallel
  subst hP hM
  have hcb : C -ᵥ B ∈ (affineSpan ℝ {B, C}).direction :=
    AffineSubspace.vsub_mem_direction
      (right_mem_affineSpan_pair ℝ B C)
      (left_mem_affineSpan_pair ℝ B C)
  have hed : E -ᵥ D ∈ (affineSpan ℝ {D, E}).direction :=
    AffineSubspace.vsub_mem_direction
      (right_mem_affineSpan_pair ℝ D E)
      (left_mem_affineSpan_pair ℝ D E)
  rw [hv, AffineSubspace.map_direction, AffineEquiv.linear_toAffineMap,
    AffineEquiv.linear_constVAdd, LinearEquiv.refl_toLinearMap, Submodule.map_id] at hcb
  rw [direction_affineSpan] at hcb hed
  have hs : Module.finrank ℝ (vectorSpan ℝ {D, E}) ≤ 1 :=
    (finrank_vectorSpan_insert_le_set ℝ {E} D).trans (by simp)
  rw [finrank_le_one_iff] at hs
  obtain ⟨s, hs⟩ := hs
  obtain ⟨bd, hbd⟩ := hs ⟨C -ᵥ B, hcb⟩
  obtain ⟨de, hde⟩ := hs ⟨E -ᵥ D, hed⟩
  rw [← Subtype.coe_inj, Submodule.coe_smul] at hbd hde
  rw [← vsub_vadd D A, vadd_left_mem_affineSpan_pair] at hD
  rw [← vsub_vadd E A, vadd_left_mem_affineSpan_pair] at hE
  obtain ⟨d, hd⟩ := hD
  obtain ⟨e, he⟩ := hE
  have head : E -ᵥ A = d • (B -ᵥ A) + de • s := by
    rw [hd, hde, add_comm, vsub_add_vsub_cancel]
  have heae : E -ᵥ A = e • (B -ᵥ A) + e • bd • s := by
    rw [← he, hbd, ← smul_add, add_comm, vsub_add_vsub_cancel]
  have hdae : D -ᵥ A = e • (C -ᵥ A) - de • s := by
    rw [he, hde, vsub_sub_vsub_cancel_left]
  have hdad : D -ᵥ A = d • (C -ᵥ A) - d • bd • s := by
    rw [← hd, hbd, ← smul_sub, vsub_sub_vsub_cancel_left]
  obtain deq | dne := eq_or_ne d e
  · suffices hm : midpoint ℝ D E = d • (midpoint ℝ B C -ᵥ A) +ᵥ A by
      rw [hm]
      apply collinear_triple_of_mem_affineSpan_pair
        (mem_affineSpan ℝ (Set.mem_insert A {midpoint ℝ B C}))
        (mem_affineSpan ℝ (Set.mem_insert_of_mem A (Set.mem_singleton (midpoint ℝ B C))))
      apply vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan
      · apply mem_affineSpan
        exact Set.mem_insert A {midpoint ℝ B C}
      · apply Submodule.smul_mem
        apply vsub_mem_vectorSpan
        · exact Set.mem_insert_of_mem A (Set.mem_singleton (midpoint ℝ B C))
        · exact Set.mem_insert A {midpoint ℝ B C}
    apply vsub_left_injective A
    dsimp only
    rw [midpoint_vsub, vadd_vsub, midpoint_vsub, ← hd, ← he, deq]
    module
  · have u₁ := head.symm.trans heae
    have u₂ := hdae.symm.trans hdad
    rw [← eq_sub_iff_add_eq, add_sub_assoc, ← sub_eq_iff_eq_add', ← sub_smul,
      ← mul_smul, ← sub_smul, ← eq_inv_smul_iff₀ (sub_ne_zero.2 dne), ← mul_smul] at u₁
    rw [sub_eq_iff_eq_add', ← add_sub_left_comm, ← sub_eq_iff_eq_add', ← sub_smul,
      ← mul_smul, ← sub_smul, ← eq_inv_smul_iff₀ (sub_ne_zero.2 dne.symm), ← mul_smul] at u₂
    rw [collinear_iff_of_mem (Set.mem_insert A {midpoint ℝ B C, midpoint ℝ D E})]
    refine ⟨s, ?_⟩
    rw [Set.forall_mem_insert, Set.forall_mem_insert]
    refine ⟨⟨0, by simp⟩,
      ⟨midpoint ℝ ((d - e)⁻¹ * (e * bd - de)) ((e - d)⁻¹ * (de - d * bd)), ?_⟩,
      fun _ h => ⟨midpoint ℝ (d * (d - e)⁻¹ * (e * bd - de)) (e * (e - d)⁻¹ * (de - d * bd)), ?_⟩⟩
    · apply vsub_left_injective A
      simp [midpoint_eq_smul_add, midpoint_vsub, u₁, u₂]
      module
    · rw [Set.mem_singleton_iff] at h
      subst h
      apply vsub_left_injective A
      simp [midpoint_eq_smul_add, midpoint_vsub, ← hd, ← he, u₁, u₂]
      module

[Aaron Liu]

I wonder if there's a way to avoid splitting on d = e

[Brisal]

Aaron Liu said:

well here we go

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Tangent
import Mathlib.Geometry.Euclidean.Triangle


open Affine Affine.Simplex EuclideanGeometry Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)
variable [AddCommGroup V] [Module ℝ V] [AddTorsor V Pt]

example {A B C D E M P : Pt}
    (hM : M = midpoint ℝ B C)
    (hD : D ∈ line[ℝ, A, B])
    (hE : E ∈ line[ℝ, A, C])
    (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
    (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  obtain ⟨v, hv⟩ := h_Parallel
  subst hP hM
  have hcb : C -ᵥ B ∈ (affineSpan ℝ {B, C}).direction :=
    AffineSubspace.vsub_mem_direction
      (right_mem_affineSpan_pair ℝ B C)
      (left_mem_affineSpan_pair ℝ B C)
  have hed : E -ᵥ D ∈ (affineSpan ℝ {D, E}).direction :=
    AffineSubspace.vsub_mem_direction
      (right_mem_affineSpan_pair ℝ D E)
      (left_mem_affineSpan_pair ℝ D E)
  rw [hv, AffineSubspace.map_direction, AffineEquiv.linear_toAffineMap,
    AffineEquiv.linear_constVAdd, LinearEquiv.refl_toLinearMap, Submodule.map_id] at hcb
  rw [direction_affineSpan] at hcb hed
  have hs : Module.finrank ℝ (vectorSpan ℝ {D, E}) ≤ 1 :=
    (finrank_vectorSpan_insert_le_set ℝ {E} D).trans (by simp)
  rw [finrank_le_one_iff] at hs
  obtain ⟨s, hs⟩ := hs
  obtain ⟨bd, hbd⟩ := hs ⟨C -ᵥ B, hcb⟩
  obtain ⟨de, hde⟩ := hs ⟨E -ᵥ D, hed⟩
  rw [← Subtype.coe_inj, Submodule.coe_smul] at hbd hde
  rw [← vsub_vadd D A, vadd_left_mem_affineSpan_pair] at hD
  rw [← vsub_vadd E A, vadd_left_mem_affineSpan_pair] at hE
  obtain ⟨d, hd⟩ := hD
  obtain ⟨e, he⟩ := hE
  have head : E -ᵥ A = d • (B -ᵥ A) + de • s := by
    rw [hd, hde, add_comm, vsub_add_vsub_cancel]
  have heae : E -ᵥ A = e • (B -ᵥ A) + e • bd • s := by
    rw [← he, hbd, ← smul_add, add_comm, vsub_add_vsub_cancel]
  have hdae : D -ᵥ A = e • (C -ᵥ A) - de • s := by
    rw [he, hde, vsub_sub_vsub_cancel_left]
  have hdad : D -ᵥ A = d • (C -ᵥ A) - d • bd • s := by
    rw [← hd, hbd, ← smul_sub, vsub_sub_vsub_cancel_left]
  obtain deq | dne := eq_or_ne d e
  · suffices hm : midpoint ℝ D E = d • (midpoint ℝ B C -ᵥ A) +ᵥ A by
      rw [hm]
      apply collinear_triple_of_mem_affineSpan_pair
        (mem_affineSpan ℝ (Set.mem_insert A {midpoint ℝ B C}))
        (mem_affineSpan ℝ (Set.mem_insert_of_mem A (Set.mem_singleton (midpoint ℝ B C))))
      apply vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan
      · apply mem_affineSpan
        exact Set.mem_insert A {midpoint ℝ B C}
      · apply Submodule.smul_mem
        apply vsub_mem_vectorSpan
        · exact Set.mem_insert_of_mem A (Set.mem_singleton (midpoint ℝ B C))
        · exact Set.mem_insert A {midpoint ℝ B C}
    apply vsub_left_injective A
    dsimp only
    rw [midpoint_vsub, vadd_vsub, midpoint_vsub, ← hd, ← he, deq]
    module
  · have u₁ := head.symm.trans heae
    have u₂ := hdae.symm.trans hdad
    rw [← eq_sub_iff_add_eq, add_sub_assoc, ← sub_eq_iff_eq_add', ← sub_smul,
      ← mul_smul, ← sub_smul, ← eq_inv_smul_iff₀ (sub_ne_zero.2 dne), ← mul_smul] at u₁
    rw [sub_eq_iff_eq_add', ← add_sub_left_comm, ← sub_eq_iff_eq_add', ← sub_smul,
      ← mul_smul, ← sub_smul, ← eq_inv_smul_iff₀ (sub_ne_zero.2 dne.symm), ← mul_smul] at u₂
    rw [collinear_iff_of_mem (Set.mem_insert A {midpoint ℝ B C, midpoint ℝ D E})]
    refine ⟨s, ?_⟩
    rw [Set.forall_mem_insert, Set.forall_mem_insert]
    refine ⟨⟨0, by simp⟩,
      ⟨midpoint ℝ ((d - e)⁻¹ * (e * bd - de)) ((e - d)⁻¹ * (de - d * bd)), ?_⟩,
      fun _ h => ⟨midpoint ℝ (d * (d - e)⁻¹ * (e * bd - de)) (e * (e - d)⁻¹ * (de - d * bd)), ?_⟩⟩
    · apply vsub_left_injective A
      simp [midpoint_eq_smul_add, midpoint_vsub, u₁, u₂]
      module
    · rw [Set.mem_singleton_iff] at h
      subst h
      apply vsub_left_injective A
      simp [midpoint_eq_smul_add, midpoint_vsub, ← hd, ← he, u₁, u₂]
      module

It seems that some problems that are obviously true in natural language can be quite complex to prove in Lean4.

[Jovan Gerbscheid]

Surely B ≠ C should imply D ≠ E?

[Aaron Liu]

then I need to add that to the assumptions

[Jovan Gerbscheid]

Ah right, but if those are all equal the result should be trivial no?

[Aaron Liu]

but you need a bit of proving

[Aaron Liu]

how about you try it

[Jovan Gerbscheid]

Ah sorry, I thought you were talking about D and E instead of d and e.

I did try to write a basic affine equation solver tactic in terms of already existing tactics. It uses a function I called toVector that sends things from the affine space into the vector space, so that we can then call a linear equation solver. Then the tactic consists of applying a fixes simp set, and then calling module (or linear_combination (norm := module)).

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Tangent
import Mathlib.Geometry.Euclidean.Triangle


open Affine Affine.Simplex EuclideanGeometry Module

open scoped Affine EuclideanGeometry Real

variable {V : Type*} {Pt : Type*}
variable [AddCommGroup V] [AddTorsor V Pt]

noncomputable def toVector (P : Pt) : V := P -ᵥ Classical.ofNonempty

theorem toVector_eq_toVector (P₁ P₂ : Pt) : toVector P₁ = toVector P₂ ↔ P₁ = P₂ := vsub_left_cancel_iff

theorem toVector_vadd (v : V) (P : Pt) : toVector (v +ᵥ P) = v + toVector P := by
  unfold toVector
  rw [vadd_vsub_assoc]

theorem vsub_eq_toVector_sub_toVector (P₁ P₂ : Pt) : P₁ -ᵥ P₂ = toVector P₁ - toVector P₂ := by
  unfold toVector
  rw [vsub_sub_vsub_cancel_right]

variable [Module ℝ V]

theorem toVector_lineMap (A B : Pt) (r : ℝ) : toVector (AffineMap.lineMap A B r) = (1 - r) • toVector A + r • toVector B := by
  unfold toVector
  rw [AffineMap.lineMap_apply, vadd_vsub_assoc, ← sub_eq_sub_iff_add_eq_add, ← smul_sub, sub_smul, one_smul, sub_sub_cancel_left, ← smul_neg]
  simp

theorem toVector_midpoint (A B : Pt) : toVector (midpoint ℝ A B) = (1/2 : ℝ) • toVector A + (1/2 : ℝ) • toVector B := by
  unfold midpoint
  rw [toVector_lineMap]
  norm_num

example {A B C D E M P : Pt}
    (hM : M = midpoint ℝ B C)
    (hD : D ∈ line[ℝ, A, B])
    (hE : E ∈ line[ℝ, A, C])
    (h_Parallel : line[ℝ, D, E] ∥ line[ℝ, B, C])
    (hP : P = midpoint ℝ D E) : Collinear ℝ {A, M, P} := by
  obtain ⟨v, hv⟩ := h_Parallel
  subst hP hM
  have hcb : C -ᵥ B ∈ (affineSpan ℝ {B, C}).direction :=
    AffineSubspace.vsub_mem_direction
      (right_mem_affineSpan_pair ℝ B C)
      (left_mem_affineSpan_pair ℝ B C)
  have hed : E -ᵥ D ∈ (affineSpan ℝ {D, E}).direction :=
    AffineSubspace.vsub_mem_direction
      (right_mem_affineSpan_pair ℝ D E)
      (left_mem_affineSpan_pair ℝ D E)
  rw [hv, AffineSubspace.map_direction, AffineEquiv.linear_toAffineMap,
    AffineEquiv.linear_constVAdd, LinearEquiv.refl_toLinearMap, Submodule.map_id] at hcb
  rw [direction_affineSpan] at hcb hed
  have hs : Module.finrank ℝ (vectorSpan ℝ {D, E}) ≤ 1 :=
    (finrank_vectorSpan_insert_le_set ℝ {E} D).trans (by simp)
  rw [finrank_le_one_iff] at hs
  obtain ⟨s, hs⟩ := hs
  obtain ⟨bd, hbd⟩ := hs ⟨C -ᵥ B, hcb⟩
  obtain ⟨de, hde⟩ := hs ⟨E -ᵥ D, hed⟩
  rw [← Subtype.coe_inj, Submodule.coe_smul] at hbd hde
  push_cast at hbd hde
  rw [← vsub_vadd D A, vadd_left_mem_affineSpan_pair] at hD
  rw [← vsub_vadd E A, vadd_left_mem_affineSpan_pair] at hE
  obtain ⟨d, hd⟩ := hD
  obtain ⟨e, he⟩ := hE
  have head : E -ᵥ A = d • (B -ᵥ A) + de • s := by
    rw [hd, hde, add_comm, vsub_add_vsub_cancel]
  have heae : E -ᵥ A = e • (B -ᵥ A) + e • bd • s := by
    rw [← he, hbd, ← smul_add, add_comm, vsub_add_vsub_cancel]
  have hdae : D -ᵥ A = e • (C -ᵥ A) - de • s := by
    rw [he, hde, vsub_sub_vsub_cancel_left]
  have hdad : D -ᵥ A = d • (C -ᵥ A) - d • bd • s := by
    rw [← hd, hbd, ← smul_sub, vsub_sub_vsub_cancel_left]
  obtain deq | dne := eq_or_ne d e
  · suffices hm : midpoint ℝ D E = d • (midpoint ℝ B C -ᵥ A) +ᵥ A by
      rw [hm]
      apply collinear_triple_of_mem_affineSpan_pair
        (mem_affineSpan ℝ (Set.mem_insert A {midpoint ℝ B C}))
        (mem_affineSpan ℝ (Set.mem_insert_of_mem A (Set.mem_singleton (midpoint ℝ B C))))
      apply vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan
      · apply mem_affineSpan
        exact Set.mem_insert A {midpoint ℝ B C}
      · apply Submodule.smul_mem
        apply vsub_mem_vectorSpan
        · exact Set.mem_insert_of_mem A (Set.mem_singleton (midpoint ℝ B C))
        · exact Set.mem_insert A {midpoint ℝ B C}
    subst deq
    simp only [vsub_eq_toVector_sub_toVector, toVector_vadd, toVector_midpoint, ← toVector_eq_toVector (Pt := Pt)] at he hd ⊢
    linear_combination (norm := module) (-1/2 : ℝ) • he - (1/2 : ℝ) • hd
  · have u₁ := head.symm.trans heae
    have u₂ := hdae.symm.trans hdad
    rw [← eq_sub_iff_add_eq, add_sub_assoc, ← sub_eq_iff_eq_add', ← sub_smul,
      ← mul_smul, ← sub_smul, ← eq_inv_smul_iff₀ (sub_ne_zero.2 dne), ← mul_smul] at u₁
    rw [sub_eq_iff_eq_add', ← add_sub_left_comm, ← sub_eq_iff_eq_add', ← sub_smul,
      ← mul_smul, ← sub_smul, ← eq_inv_smul_iff₀ (sub_ne_zero.2 dne.symm), ← mul_smul] at u₂
    rw [collinear_iff_of_mem (Set.mem_insert A {midpoint ℝ B C, midpoint ℝ D E})]
    refine ⟨s, ?_⟩
    rw [Set.forall_mem_insert, Set.forall_mem_insert]
    refine ⟨⟨0, by simp⟩,
      ⟨midpoint ℝ ((d - e)⁻¹ * (e * bd - de)) ((e - d)⁻¹ * (de - d * bd)), ?_⟩,
      fun _ h => ⟨midpoint ℝ (d * (d - e)⁻¹ * (e * bd - de)) (e * (e - d)⁻¹ * (de - d * bd)), ?_⟩⟩
    · apply vsub_left_injective A
      simp [midpoint_eq_smul_add, midpoint_vsub, u₁, u₂]
      module
    · rw [Set.mem_singleton_iff] at h
      subst h
      apply vsub_left_injective A
      simp [midpoint_eq_smul_add, midpoint_vsub, ← hd, ← he, u₁, u₂]
      module