awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl₂ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [h₁, h₂, h, neg_neg]
-- 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₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = (↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl : (↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
inl₁ : (↑(∠ p₁ p₂ p₃) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inl₂ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = - -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inl₃ : (↑(∠ p₄ p₅ p₆) : Real.Angle) = (↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [h₁, h₂, h, neg_neg]
-- 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₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr : ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
Tactic: 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₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
Tactic: rw [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₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr₁ : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [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₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = (↑(∠ p₄ p₅ p₆) : Real.Angle)
inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -∡ p₄ p₅ p₆
inr₁ : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr₂ : -(↑(∠ p₄ p₅ p₆) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [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₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆
have inr : ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
Tactic: 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₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
have inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
Tactic: rw [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₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
have inr₁ : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [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₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = -(↑(∠ p₁ p₂ p₃) : Real.Angle)
h₂ : ∡ p₄ p₅ p₆ = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
inr : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = ∡ p₄ p₅ p₆
inr₁ : -(↑(∠ p₁ p₂ p₃) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆
have inr₂ : -(↑(∠ p₄ p₅ p₆) : Real.Angle) = -(↑(∠ p₄ p₅ p₆) : Real.Angle)
Tactic: rw [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₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∠ p₁ p₂ p₃ = π / 2
have rw : ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0
Tactic: rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-- 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₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∠ p₃ p₂ p₁ = π / 2
have rw : ∠ p₁ p₂ p₃ = π / 2
Tactic: rw [angle_comm]
-- 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₂ p₃ = (↑(-π / 2) : Real.Angle)
⊢ ∠ p₁ p₂ p₃ = π / 2
have rw : ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫ = 0
Tactic: rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-- 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₂ p₃ = (↑(-π / 2) : Real.Angle)
⊢ ∠ p₃ p₂ p₁ = π / 2
have rw : ∠ p₁ p₂ p₃ = π / 2
Tactic: rw [angle_comm]
-- 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₂ p₃).sign = (∡ p₂ p₁ p₃).sign
have rw : (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
  -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
Tactic: rw [eq_comm, oangle, oangle, ← o.oangle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
    vsub_sub_vsub_cancel_left p₁ p₃ p₂, ← neg_vsub_eq_vsub_rev p₃ p₂, sub_eq_add_neg,
    neg_vsub_eq_vsub_rev p₂ p₁, add_comm, ← @neg_one_smul ℝ]
-- 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
⊢ (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
have nth_rw : (Orientation.oangle o (p₁ -ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
  -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
Tactic: nth_rw 2 [← one_smul ℝ (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
⊢ (Orientation.oangle o (p₁ -ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) + HSMul.hSMul (α := ℝ) (-1) (p₃ -ᵥ p₂))).sign =
    -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
have rw : HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-1) : SignType)
    (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign =
  -(Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
Tactic: rw [o.oangle_sign_smul_add_smul_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₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign
have rw : -(-∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
Tactic: rw [oangle_rev, Real.Angle.sign_neg, neg_neg]
-- 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₂ p₁).sign = (∡ p₃ p₂ p₁).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign
have rw₁ : - -(∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
Tactic: rw [oangle_rev, Real.Angle.sign_neg, neg_neg]
-- 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₂ p₁).sign = (∡ p₃ p₂ p₁).sign
rw₁ : - -(∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign
have rw₂ : (∡ p₃ p₂ p₁).sign = (∡ p₃ p₂ p₁).sign
Tactic: rw [oangle_rev, Real.Angle.sign_neg, neg_neg]
-- 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₂ p₃).sign = (∡ p₁ p₃ p₂).sign
have rw : (∡ p₃ p₂ p₁).sign = (∡ p₁ p₃ p₂).sign
Tactic: rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
-- 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₂ p₁).sign = (∡ p₁ p₃ p₂).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign
have rw₁ : -(∡ p₂ p₃ p₁).sign = (∡ p₁ p₃ p₂).sign
Tactic: rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
-- 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₂ p₁).sign = (∡ p₁ p₃ p₂).sign
rw₁ : -(∡ p₂ p₃ p₁).sign = (∡ p₁ p₃ p₂).sign
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign
have rw₂ : (∡ p₁ p₃ p₂).sign = (∡ p₁ p₃ p₂).sign
Tactic: rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
-- 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₃ p₁).sign = (∡ p₁ p₂ p₃).sign
have rw : -(∡ p₃ p₂ p₁).sign = (∡ p₁ p₂ p₃).sign
Tactic: rw [← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
-- 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₂ p₁).sign = (∡ p₁ p₂ p₃).sign
⊢ (∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign
have rw₁ : (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃).sign
Tactic: rw [← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
-- 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₂ p₃ = (↑π : Real.Angle) ↔ Sbtw ℝ p₁ p₂ p₃
have rw : ∠ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃
Tactic: rw [oangle_eq_pi_iff_angle_eq_pi, angle_eq_pi_iff_sbtw]
-- 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₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Sbtw ℝ p₁ p₂ p₃
have rw₁ : Sbtw ℝ p₁ p₂ p₃ ↔ Sbtw ℝ p₁ p₂ p₃
Tactic: rw [oangle_eq_pi_iff_angle_eq_pi, angle_eq_pi_iff_sbtw]
-- 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 : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₂ p₁ = (↑π : Real.Angle)
have rw : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
Tactic: rw [oangle_eq_pi_iff_oangle_rev_eq_pi, ← h.oangle₁₂₃_eq_pi]
-- 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 : Sbtw ℝ p₁ p₂ p₃
rw : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ ∡ p₃ p₂ p₁ = (↑π : Real.Angle)
have rw₁ : ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
Tactic: rw [oangle_eq_pi_iff_oangle_rev_eq_pi, ← h.oangle₁₂₃_eq_pi]
-- 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 : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₂ p₁ p₃ = 0
have pos : ∀ (hp₂p₁ : p₂ = p₁), ∡ p₂ p₁ p₃ = 0
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
h : Wbtw ℝ p₁ p₂ p₃
pos : ∀ (hp₂p₁ : p₂ = p₁), ∡ p₂ p₁ p₃ = 0
⊢ ∡ p₂ p₁ p₃ = 0
have neg : ∀ (hp₂p₁ : ¬p₂ = p₁), ∡ p₂ p₁ p₃ = 0
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
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
have pos : ∀ (hp₃p₁ : p₃ = p₁), ∡ p₂ p₁ p₃ = 0
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
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
pos : ∀ (hp₃p₁ : p₃ = p₁), ∡ p₂ p₁ p₃ = 0
⊢ ∡ p₂ p₁ p₃ = 0
have neg : ∀ (hp₃p₁ : ¬p₃ = p₁), ∡ p₂ p₁ p₃ = 0
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
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
have neg : ∠ p₂ p₁ p₃ = 0
Tactic: rw [oangle_eq_zero_iff_angle_eq_zero 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
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₁ p₂ = 0
have rw : ∡ p₂ p₁ p₃ = 0
Tactic: rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_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 : Wbtw ℝ p₁ p₂ p₃
rw : ∡ p₂ p₁ p₃ = 0
⊢ ∡ p₃ p₁ p₂ = 0
have rw₁ : Eq (α := Real.Angle) 0 0
Tactic: rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_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₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
have pos : ∀ (hp₁p₂ : p₁ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ 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
pos : ∀ (hp₁p₂ : p₁ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
have neg : ∀ (hp₁p₂ : ¬p₁ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ 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
hp₁p₂ : ¬p₁ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
have pos : ∀ (hp₃p₂ : p₃ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ 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
hp₁p₂ : ¬p₁ = p₂
pos : ∀ (hp₃p₂ : p₃ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
have neg : ∀ (hp₃p₂ : ¬p₃ = p₂), ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ 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
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
have neg : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
Tactic: rw [oangle_eq_zero_iff_angle_eq_zero hp₁p₂ hp₃p₂, angle_eq_zero_iff_ne_and_wbtw]
-- 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 pos : ∀ (hp₃p₂ : p₃ = p₂), ∡ p₁ p₂ p₃ = ∡ 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 : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
pos : ∀ (hp₃p₂ : p₃ = p₂), ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have neg : ∀ (hp₃p₂ : ¬p₃ = p₂), ∡ p₁ p₂ p₃ = ∡ 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 : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have pos : ∀ (hp₁'p₂ : p₁' = p₂), ∡ p₁ p₂ p₃ = ∡ 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 : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
pos : ∀ (hp₁'p₂ : p₁' = p₂), ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
have neg : ∀ (hp₁'p₂ : ¬p₁' = p₂), ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
Tactic: by_cases hp₁'p₂ : p₁' = p₂