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)
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₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P) =
    p₁
pos : Membership.mem (γ := AffineSubspace ℝ P) ⊤ p
⊢ p = p₁

Tactic:
rw [← hp, eq_comm, orthogonalProjection_eq_self_iff, hsup]

Premises used: eq_comm, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- 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₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P) =
    p₁
⊢ Membership.mem (γ := AffineSubspace ℝ P) ⊤ p

Tactic:
AffineSubspace.mem_top ℝ V p

Premises used: Real, Set.Mem, AffineSubspace.mem_top
-- 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₂} ⊔ affineSpan ℝ {p₁, p₃}) :
            (a : P) → ↥(affineSpan ℝ {p₁, p₂} ⊔ affineSpan ℝ {p₁, p₃}))
          p) :
      P) =
    p₁
⊢ Membership.mem (γ := AffineSubspace ℝ P) ⊤ p

Tactic:
exact AffineSubspace.mem_top ℝ V p

Premises used: Real, AffineSubspace.mem_top
-- 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)
⊢ ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)

Tactic:
have hp := oangle_eq_of_dist_orthogonalProjection_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) ho h
-- 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)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
⊢ Ne (α := Fin 3) 1 0

Tactic:
decide
-- 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)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
⊢ p₂ ≠ p₁

Tactic:
have h₂₁ : p₂ ≠ p₁ := ha.injective.ne (by decide : (1 : Fin 3) ≠ 0)
-- 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)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
⊢ Ne (α := Fin 3) 2 0

Tactic:
decide
-- 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)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
⊢ p₃ ≠ p₁

Tactic:
have h₃₁ : p₃ ≠ p₁ := ha.injective.ne (by decide : (2 : Fin 3) ≠ 0)
-- 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁

Tactic:
rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h

Premises used: Real, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, eq_comm, left_mem_affineSpan_pair
-- 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
⊢ ¬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)

Tactic:
rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h

Premises used: Real, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, eq_comm, left_mem_affineSpan_pair
-- 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, 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)
⊢ ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)

Tactic:
rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h

Premises used: Real, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, eq_comm, left_mem_affineSpan_pair
-- 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, 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)
hp₁ :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
⊢ p₂ ≠ p₁

Tactic:
rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h

Premises used: Real, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, eq_comm, left_mem_affineSpan_pair
-- 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, 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)
hp₁ :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₂ : p₂ ≠ p₁
⊢ p₃ ≠ p₁

Tactic:
rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h

Premises used: Real, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, eq_comm, left_mem_affineSpan_pair
-- 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
h₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, 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)
hp₁ :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₂ : p₂ ≠ p₁
h₃₂ : p₃ ≠ p₁
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁

Tactic:
rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h

Premises used: Real, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, eq_comm, left_mem_affineSpan_pair
-- 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 : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, 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)
hp_1 :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ False

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)
hp :
  ∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p =
    ∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) ≠ p₁

Tactic:
have hp₁ : orthogonalProjection line[ℝ, p₁, p₂] p ≠ p₁ := by
      intro hp
      rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h
      grind