awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₁)
have inr : Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)
Tactic: refine ⟨left_mem_affineSpan_pair _ _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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 (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))ᗮ (p -ᵥ p₁)
have inr : ∀ (u : V),
  Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃})) u →
    inner ℝ (p -ᵥ p₁) u = 0
Tactic: rw [Submodule.mem_orthogonal']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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
⊢ inner ℝ (p -ᵥ p₁) u = 0
have hu₁ : ∃ (r : ℝ), r • (p₁ -ᵥ p₃) = u
Tactic: rw [direction_affineSpan, mem_vectorSpan_pair] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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
⊢ inner ℝ (p -ᵥ p₁) u = 0
have inr : ∀ (r : ℝ), inner ℝ (p -ᵥ p₁) (r • (p₁ -ᵥ p₃)) = 0
Tactic: rcases hu with ⟨r, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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 : ℝ
⊢ inner ℝ (p -ᵥ p₁) (r • (p₁ -ᵥ p₃)) = 0
have inr : r * -inner ℝ (p -ᵥ p₁) (-(p₁ -ᵥ p₃)) = 0
Tactic: rw [inner_smul_right, ← inner_neg_neg, inner_neg_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
have 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)
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
⊢ 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)
have 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)
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
have inr : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
Tactic: refine (dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ h₃ ?_ h').symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
have inr : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
have inr₁ : -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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
have inr₂ : -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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
have inr₃ : -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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
have inr₄ : - -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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₂)
have inr₅ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₃)
⊢ 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)
have 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)
Tactic: by_cases h' : orthogonalProjection line[ℝ, p₁, p₂] p = p₁ ∨
      orthogonalProjection line[ℝ, p₁, p₃] p = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h' : orthogonalProjection line[ℝ, p₁, p₂] p = p₁ ∨
      orthogonalProjection line[ℝ, p₁, p₃] p = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (hypothesis)
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)
have 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₁
Tactic: rw [not_or] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
have 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))
Tactic: refine dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) h'.1 h'.2 ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₁
⊢ 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))
have neg : HSMul.hSMul (α := ℤ) 2 (∡ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₃)
⊢ 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))
have neg₂ : HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have 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₃)
Tactic: by_cases ho : (orthogonalProjection line[ℝ, p₁, p₂] p : P) =
      orthogonalProjection line[ℝ, p₁, p₃] p
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Bisector (goal)
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₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ p) = HSMul.hSMul (α := ℤ) 2 (∡ p p₁ p₃)
have 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₃)
Tactic: by_cases ho : (orthogonalProjection line[ℝ, p₁, p₂] p : P) =
      orthogonalProjection line[ℝ, p₁, p₃] p