awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
h₁ : {p₁} = ![p₁, p₂, p₃] '' {0}
⊢ {p₁} = ![p₁, p₂, p₃] '' ({0, 1} ∩ {0, 2})

Tactic:
suffices {p₁} = ![p₁, p₂, p₃] '' {0} by grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ {p₁} = ![p₁, p₂, p₃] '' {0}

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})

Tactic:
have hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁} := by
      convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 2})
      · simp [Set.image_insert_eq]
      · simp [Set.image_insert_eq]
      · suffices {p₁} = ![p₁, p₂, p₃] '' {0} by grind
        simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
rw : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ ({p₁, p₂} ∪ {p₁, p₃})) ⊤
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤

Tactic:
rw [← AffineSubspace.span_union]

Premises used: AffineSubspace.span_union
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range ![p₁, p₂, p₃])) ⊤

Tactic:
ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_

Premises used: Iff.mpr, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
h₁ : {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]
convert! : Fintype.card (Fin (Nat.succ 0).succ.succ) = finrank ℝ V + 1
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ ({p₁, p₂} ∪ {p₁, p₃})) ⊤

Tactic:
convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_

Premises used: Iff.mpr, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
h₁ : Eq (α := Set P) {p₃, p₁, p₂} {p₃, p₂, p₁}
⊢ {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
⊢ Eq (α := Set P) {p₃, p₁, p₂} {p₃, p₂, p₁}

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
⊢ Fintype.card (Fin (Nat.succ 0).succ.succ) = finrank ℝ V + 1

Tactic:
simpa using Fact.out

Premises used: Fact.out
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤

Tactic:
have hsup : line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃] = ⊤ := by
      rw [← AffineSubspace.span_union]
      convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_
      · simp
        grind
      · simpa using Fact.out
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
this :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁

Tactic:
simpa using this
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
suffices :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁

Tactic:
suffices (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈ affineSpan ℝ {p₁} by
        simpa using this
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)

Tactic:
have hi : (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈
          line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] :=
        ⟨orthogonalProjection_mem _, ho ▸ orthogonalProjection_mem _⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
hi :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hi :
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
        (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁})
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)

Tactic:
rwa [hinf] at hi
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁

Tactic:
have hp : orthogonalProjection (line[ℝ, p₁, p₂]) p = p₁ := by
      suffices (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈ affineSpan ℝ {p₁} by
        simpa using this
      have hi : (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈
          line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] :=
        ⟨orthogonalProjection_mem _, ho ▸ orthogonalProjection_mem _⟩
      rwa [hinf] at hi
-- Module: Mathlib.Geometry.Euclidean.Angle.Bisector
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h :
  dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
ho :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
hs :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hinf : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})
hsup : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) ⊤
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P) =
    p₁

Tactic:
rw [← orthogonalProjection_sup_of_orthogonalProjection_eq ho] at hp

Premises used: EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq