awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have h₁ : p₁ = p₂
Tactic: rw [hp₁'p₂, wbtw_self_iff] at h
Cleared hypotheses: h, hp₁p₂, hp₃p₂, hp₁'p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : ¬p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have neg : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₁ + ∡ p₁ p₂ p₃
Tactic: rw [← oangle_add hp₁'p₂ hp₁p₂ hp₃p₂, h.oangle₃₁₂_eq_zero, zero_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : ¬p₁' = p₂
neg : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₁ + ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have neg₁ : ∡ p₁ p₂ p₃ = 0 + ∡ p₁ p₂ p₃
Tactic: rw [← oangle_add hp₁'p₂ hp₁p₂ hp₃p₂, h.oangle₃₁₂_eq_zero, zero_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : ¬p₁' = p₂
neg : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₁ + ∡ p₁ p₂ p₃
neg₁ : ∡ p₁ p₂ p₃ = 0 + ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have neg₂ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [← oangle_add hp₁'p₂ hp₁p₂ hp₃p₂, h.oangle₃₁₂_eq_zero, zero_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'
have rw : -∡ p₃ p₂ p₁ = ∡ p₁ p₂ p₃'
Tactic: rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
rw : -∡ p₃ p₂ p₁ = ∡ p₁ p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'
have rw₁ : -∡ p₃' p₂ p₁ = ∡ p₁ p₂ p₃'
Tactic: rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
rw : -∡ p₃ p₂ p₁ = ∡ p₁ p₂ p₃'
rw₁ : -∡ p₃' p₂ p₁ = ∡ p₁ p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'
have rw₂ : ∡ p₁ p₂ p₃' = ∡ p₁ p₂ p₃'
Tactic: rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
have pos : ∀ (h : p₁ = p₂), ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: by_cases h : p₁ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
pos : ∀ (h : p₁ = p₂), ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
have neg : ∀ (h : ¬p₁ = p₂), ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: by_cases h : p₁ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃
have rw : ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [midpoint_comm, oangle_midpoint_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
rw : ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
⊢ ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃
have rw₁ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [midpoint_comm, oangle_midpoint_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
have pos : ∀ (h : p₃ = p₂), ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
Tactic: by_cases h : p₃ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
pos : ∀ (h : p₃ = p₂), ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
have neg : ∀ (h : ¬p₃ = p₂), ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
Tactic: by_cases h : p₃ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃
have rw : ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
Tactic: rw [midpoint_comm, oangle_midpoint_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
rw : ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
⊢ ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃
have rw₁ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [midpoint_comm, oangle_midpoint_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₁'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + (↑π : Real.Angle)
have rw : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + ∡ p₁ p₂ p₁'
Tactic: rw [← h.oangle₁₂₃_eq_pi, oangle_add_swap h.left_ne h.right_ne hp₃p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₁'
hp₃p₂ : p₃ ≠ p₂
rw : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + ∡ p₁ p₂ p₁'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + (↑π : Real.Angle)
have rw₁ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [← h.oangle₁₂₃_eq_pi, oangle_add_swap h.left_ne h.right_ne hp₃p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + (↑π : Real.Angle)
have rw : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ∡ p₃' p₂ p₃
Tactic: rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
rw : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ∡ p₃' p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + (↑π : Real.Angle)
have rw₁ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
have rw : ∡ p₁' p₂ p₃ + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
Tactic: rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
rw : ∡ p₁' p₂ p₃ + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
have rw₁ : ∡ p₁' p₂ p₃' + (↑π : Real.Angle) + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
Tactic: rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
rw : ∡ p₁' p₂ p₃ + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₁ : ∡ p₁' p₂ p₃' + (↑π : Real.Angle) + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
have rw₂ : ∡ p₁' p₂ p₃' + ((↑π : Real.Angle) + (↑π : Real.Angle)) = ∡ p₁' p₂ p₃'
Tactic: rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
rw : ∡ p₁' p₂ p₃ + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₁ : ∡ p₁' p₂ p₃' + (↑π : Real.Angle) + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₂ : ∡ p₁' p₂ p₃' + ((↑π : Real.Angle) + (↑π : Real.Angle)) = ∡ p₁' p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
have rw₃ : ∡ p₁' p₂ p₃' + 0 = ∡ p₁' p₂ p₃'
Tactic: rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
rw : ∡ p₁' p₂ p₃ + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₁ : ∡ p₁' p₂ p₃' + (↑π : Real.Angle) + (↑π : Real.Angle) = ∡ p₁' p₂ p₃'
rw₂ : ∡ p₁' p₂ p₃' + ((↑π : Real.Angle) + (↑π : Real.Angle)) = ∡ p₁' p₂ p₃'
rw₃ : ∡ p₁' p₂ p₃' + 0 = ∡ p₁' p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
have rw₄ : ∡ p₁' p₂ p₃' = ∡ p₁' p₂ p₃'
Tactic: rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
| p₂
have rw : ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₂ : P)
Tactic: rw [← AffineEquiv.pointReflection_self ℝ p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂
have conv_rhs : Ne (α := P) ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ : P)
  ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₂ : P)
Tactic: conv_rhs => rw [← AffineEquiv.pointReflection_self ℝ p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)
have h₂₃' : (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂
Tactic: have h₂₃' : (AffineEquiv.pointReflection ℝ p₂) p₃ ≠ p₂ := by
    conv_rhs => rw [← AffineEquiv.pointReflection_self ℝ p₂]
    rw [(AffineEquiv.pointReflection ℝ p₂).injective.ne_iff]
    exact h₃₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
h₂₃' : (AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃ ≠ p₂
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)
have rw : ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = (↑π : Real.Angle)
Tactic: rw [← sub_eq_iff_eq_add', oangle_sub_left h₁₂ h₃₂ h₂₃']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₁) p₂ p₃ = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)
have rw : ∡ p₁ p₂ p₃ + -(↑π : Real.Angle) = ∡ p₁ p₂ p₃ + (↑π : Real.Angle)
Tactic: rw [oangle_rev, oangle_pointReflection_right h₃₂ h₁₂, neg_add, ← oangle_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have pos : ∀ (hp₃p₂ : p₃ = p₂), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: by_cases hp₃p₂ : p₃ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
pos : ∀ (hp₃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 : ∀ (hp₃p₂ : ¬p₃ = p₂), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: by_cases hp₃p₂ : p₃ = p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg : ∀ (hw : Wbtw ℝ p₁ p₂ p₁'), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
neg : ∀ (hw : Wbtw ℝ 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₁ : ∀ (hw : Wbtw ℝ p₂ p₁' p₁), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
neg : ∀ (hw : Wbtw ℝ p₁ p₂ p₁'), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₁ : ∀ (hw : Wbtw ℝ 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₂ : ∀ (hw : Wbtw ℝ p₁' p₁ p₂), HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have hw' : Sbtw ℝ p₁ p₂ p₁'
Tactic: have hw' : Sbtw ℝ p₁ p₂ p₁' := ⟨hw, hp₁p₂.symm, hp₁'p₂.symm⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
hw' : Sbtw ℝ p₁ p₂ p₁'
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃ + (↑π : Real.Angle)) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
hw' : Sbtw ℝ p₁ p₂ p₁'
neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃ + (↑π : Real.Angle)) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (↑π : Real.Angle) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
hw' : Sbtw ℝ p₁ p₂ p₁'
neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃ + (↑π : Real.Angle)) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (↑π : Real.Angle) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg₂ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + 0 = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
hw' : Sbtw ℝ p₁ p₂ p₁'
neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃ + (↑π : Real.Angle)) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (↑π : Real.Angle) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
neg₂ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) + 0 = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg₃ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃)
Tactic: rw [hw.oangle_eq_left hp₁'p₂]