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 : 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₁
inl :
  ∀ (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)
inr :
  ∀ (hp : 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:
obtain rfl | hp := eq_or_ne p p₁

Premises used: eq_or_ne, rfl
-- 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
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
inl : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {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:
rw [h', dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff]

Premises used: zero_eq_dist, eq_comm, dist_self, 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
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, p₃}) p

Tactic:
left_mem_affineSpan_pair _ _ _

Premises used: Set.Mem, 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
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, p₃}) p

Tactic:
exact left_mem_affineSpan_pair _ _ _

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

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

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

Tactic:
have hpm : p ∉ line[ℝ, p₁, p₂] := orthogonalProjection_eq_self_iff.not.1 (Ne.symm hp)
-- 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 :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((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₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
⊢ Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
    Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)

Tactic:
rw [two_zsmul_oangle_orthogonalProjection_self _ hpm (right_mem_affineSpan_pair _ _ _)
          (h'.symm ▸ h₂.symm), eq_comm, oangle, Real.Angle.two_zsmul_eq_pi_iff, h'] at h

Premises used: EuclideanGeometry.oangle, Real.Angle.two_zsmul_eq_pi_iff, right_mem_affineSpan_pair, eq_comm, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self
-- 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 :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((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₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h₁ :
  Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
    Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)
⊢ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁

Tactic:
rw [two_zsmul_oangle_orthogonalProjection_self _ hpm (right_mem_affineSpan_pair _ _ _)
          (h'.symm ▸ h₂.symm), eq_comm, oangle, Real.Angle.two_zsmul_eq_pi_iff, h'] at h

Premises used: EuclideanGeometry.oangle, Real.Angle.two_zsmul_eq_pi_iff, right_mem_affineSpan_pair, eq_comm, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self
-- 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 :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((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₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h₁ :
  Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
    Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)
h'₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
⊢ p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)

Tactic:
rw [two_zsmul_oangle_orthogonalProjection_self _ hpm (right_mem_affineSpan_pair _ _ _)
          (h'.symm ▸ h₂.symm), eq_comm, oangle, Real.Angle.two_zsmul_eq_pi_iff, h'] at h

Premises used: EuclideanGeometry.oangle, Real.Angle.two_zsmul_eq_pi_iff, right_mem_affineSpan_pair, eq_comm, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self
-- 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 :
  HSMul.hSMul (α := ℤ) 2
      (∡ p₂ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) p) =
    HSMul.hSMul (α := ℤ) 2
      (∡ p (↑((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₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h₁ :
  Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
    Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)
h'₁ : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp₁ : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
⊢ p ∉ affineSpan ℝ {p₁, p₂}

Tactic:
rw [two_zsmul_oangle_orthogonalProjection_self _ hpm (right_mem_affineSpan_pair _ _ _)
          (h'.symm ▸ h₂.symm), eq_comm, oangle, Real.Angle.two_zsmul_eq_pi_iff, h'] at h

Premises used: EuclideanGeometry.oangle, Real.Angle.two_zsmul_eq_pi_iff, right_mem_affineSpan_pair, eq_comm, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self
-- 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 :
  Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(Real.pi / 2) : Real.Angle) ∨
    Orientation.oangle o (p -ᵥ p₁) (p₃ -ᵥ p₁) = (↑(-Real.pi / 2) : Real.Angle)
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
⊢ inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0

Tactic:
replace h := (Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero _).1 (.inr (.inr 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
h₂ : p₁ ≠ p₂
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
inr :
  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)
⊢ 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:
congr 1
-- 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' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
inr :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₁ ∧
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {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 [h', eq_comm, coe_orthogonalProjection_eq_iff_mem]

Premises used: eq_comm, EuclideanGeometry.coe_orthogonalProjection_eq_iff_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
h₂ : p₁ ≠ p₂
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₁ ∧
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)

Tactic:
⟨left_mem_affineSpan_pair _ _ _, ?_⟩

Premises used: left_mem_affineSpan_pair, And.intro
-- 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' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
inr : Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₁ ∧
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)

Tactic:
refine ⟨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
h₂ : p₁ ≠ p₂
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
inr :
  ∀ (u : V),
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃})) u →
      inner ℝ (p -ᵥ p₁) u = 0
⊢ Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)

Tactic:
rw [Submodule.mem_orthogonal']

Premises used: Submodule.mem_orthogonal'
-- 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' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
u : V
hu : Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃})) u
⊢ ∃ (r : ℝ), r • (p₁ -ᵥ p₃) = u

Tactic:
rw [direction_affineSpan, mem_vectorSpan_pair] at hu

Premises used: direction_affineSpan, mem_vectorSpan_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
h₂ : p₁ ≠ p₂
h' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
u : V
hu : ∃ (r : ℝ), r • (p₁ -ᵥ p₃) = u
inr : ∀ (r : ℝ), inner ℝ (p -ᵥ p₁) (r • (p₁ -ᵥ p₃)) = 0
⊢ inner ℝ (p -ᵥ p₁) u = 0

Tactic:
rcases hu with ⟨r, rfl⟩

Premises used: rfl
-- 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' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
r : ℝ
inr : r * -inner ℝ (p -ᵥ p₁) (-(p₁ -ᵥ p₃)) = 0
⊢ inner ℝ (p -ᵥ p₁) (r • (p₁ -ᵥ p₃)) = 0

Tactic:
rw [inner_smul_right, ← inner_neg_neg, inner_neg_left]

Premises used: inner_neg_neg, inner_smul_right, inner_neg_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' : (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P) = p₁
hp : p ≠ (↑((orthogonalProjection (affineSpan ℝ {p₁, p₂}) : (a : P) → ↥(affineSpan ℝ {p₁, p₂})) p) : P)
hpm : p ∉ affineSpan ℝ {p₁, p₂}
h : inner ℝ (p -ᵥ p₁) (p₃ -ᵥ p₁) = 0
r : ℝ
⊢ r * -inner ℝ (p -ᵥ p₁) (-(p₁ -ᵥ p₃)) = 0

Tactic:
simp [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
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₁
inl :
  ∀ (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)
inr :
  ∀ (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)
⊢ 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:
rcases h' with h' | 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
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 h'

Premises used: _private.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁