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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ 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)

Tactic:
exact dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ h₂ h h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
⊢ 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)

Tactic:
(dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ h₃ ?_ h').symm

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁, Eq.symm
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
inr : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
⊢ 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)

Tactic:
refine (dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ h₃ ?_ h').symm

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁, Eq.symm
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
inr : HSMul.hSMul (α := ℤ) 2 (-∡ p p₁ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
inr₁ : -HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
inr₂ : -HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
inr₃ : -HSMul.hSMul (α := ℤ) 2 (-∡ p p₁ p₂) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
inr₄ : - -HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
inr₅ inr₆ : HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)

Tactic:
rw [oangle_rev, smul_neg, ← h, oangle_rev, smul_neg, neg_neg]

Premises used: EuclideanGeometry.oangle_rev, neg_neg, smul_neg
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
pos :
  ∀
    (h' :
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∨
        (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁),
    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)
neg :
  ∀
    (h' :
      ¬((↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∨
          (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁)),
    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)
⊢ 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)

Tactic:
by_cases h' : orthogonalProjection line[ℝ, p₁, p₂] p = p₁ ∨
      orthogonalProjection line[ℝ, p₁, p₃] p = p₁

Premises used: Real, Insert.insert, affineSpan, EuclideanGeometry.orthogonalProjection, Singleton.singleton, DFunLike.coe
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' :
  (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∨
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
⊢ 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)

Tactic:
dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₂ h₂ h₃ h h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₂
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' :
  (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∨
    (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
⊢ 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)

Tactic:
exact dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₂ h₂ h₃ h h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₂
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' :
  ¬((↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∨
      (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁)
⊢ ¬(↑((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 [not_or] at h'

Premises used: not_or
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' :
  ¬(↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∧
    ¬(↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
⊢ 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)

Tactic:
dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) h'.1 h'.2 ?_

Premises used: Set.Mem, EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq, left_mem_affineSpan_pair, And.right, And.left
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' :
  ¬(↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∧
    ¬(↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
neg :
  HSMul.hSMul (α := ℤ) 2
      (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p 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) =
    dist p (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P)

Tactic:
refine dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) h'.1 h'.2 ?_

Premises used: EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq, left_mem_affineSpan_pair, And.right, And.left
-- 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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
h' :
  ¬(↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁ ∧
    ¬(↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P) = p₁
neg :
  HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P))
neg₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
neg₂ neg₃ : HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
⊢ HSMul.hSMul (α := ℤ) 2
      (∡ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p₁ p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p p₁ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₃}) : (a : P) → ↥(affineSpan ℝ {p₁, p₃})) p) : P))

Tactic:
rw [(collinear_insert_of_mem_affineSpan_pair
          (orthogonalProjection_mem p)).two_zsmul_oangle_eq_left h'.1 h₂.symm,
      (collinear_insert_of_mem_affineSpan_pair
        (orthogonalProjection_mem p)).two_zsmul_oangle_eq_right h'.2 h₃.symm, h]

Premises used: Ne.symm, Collinear.two_zsmul_oangle_eq_right, And.right, And.left, collinear_insert_of_mem_affineSpan_pair, Collinear.two_zsmul_oangle_eq_left
-- 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)
pos :
  ∀
    (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)),
    HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
neg :
  ∀
    (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)),
    HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)

Tactic:
by_cases ho : (orthogonalProjection line[ℝ, p₁, p₂] p : P) =
      orthogonalProjection line[ℝ, p₁, p₃] p

Premises used: Real, Insert.insert, affineSpan, EuclideanGeometry.orthogonalProjection, Singleton.singleton, Subtype.val, DFunLike.coe
-- 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)
this : p = p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)

Tactic:
simp [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)
pos : p = p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)

Tactic:
suffices p = p₁ by simp [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)
⊢ 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)

Tactic:
have hs := orthogonalProjection_sup_of_orthogonalProjection_eq ho
-- 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₂, p₃] '' {0, 1}) ⊓ affineSpan ℝ (![p₁, p₂, p₃] '' {0, 2}))
    (affineSpan ℝ (![p₁, p₂, p₃] '' ({0, 1} ∩ {0, 2})))

Tactic:
(ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 2})

Premises used: Insert.insert, AffineIndependent.inf_affineSpan_eq_affineSpan_inter, Singleton.singleton, OfNat.ofNat
-- 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₂, p₃] '' {0, 1}
h₂ : {p₁, p₃} = ![p₁, p₂, p₃] '' {0, 2}
h₃ : {p₁} = ![p₁, p₂, p₃] '' ({0, 1} ∩ {0, 2})
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂} ⊓ affineSpan ℝ {p₁, p₃}) (affineSpan ℝ {p₁})

Tactic:
convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 2})

Premises used: Insert.insert, AffineIndependent.inf_affineSpan_eq_affineSpan_inter, Singleton.singleton, OfNat.ofNat
-- 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₂, p₃] '' {0, 1}

Tactic:
simp [Set.image_insert_eq]

Premises used: Set.image_insert_eq
-- 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₂, p₃] '' {0, 2}

Tactic:
simp [Set.image_insert_eq]

Premises used: Set.image_insert_eq
-- 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)
this : {p₁} = ![p₁, p₂, p₃] '' {0}
⊢ {p₁} = ![p₁, p₂, p₃] '' ({0, 1} ∩ {0, 2})

Tactic:
grind