awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : (o.oangle (y - x) y).sign = (o.oangle (HSMul.hSMul (α := ℝ) 1 y - x) y).sign
rw₁ rw₂ : (o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign
⊢ (o.oangle (y - x) y).sign = -(o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_sub_left x y 1, one_smul]

Premises used: Orientation.oangle_sign_smul_sub_left, one_smul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : -(o.oangle y x).sign = (o.oangle x y).sign
rw₁ : -(o.oangle y x).sign = (-o.oangle y x).sign
rw₂ rw₃ : -(o.oangle y x).sign = -(o.oangle y x).sign
⊢ (o.oangle y (y - x)).sign = (o.oangle x y).sign

Tactic:
rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]

Premises used: Real.Angle.sign_neg, Orientation.oangle_sign_sub_right_eq_neg, Orientation.oangle_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
rw : -(o.oangle y x).sign = (o.oangle x y).sign
rw₁ : -(o.oangle y x).sign = (-o.oangle y x).sign
rw₂ rw₃ : -(o.oangle y x).sign = -(o.oangle y x).sign
⊢ (o.oangle (x - y) x).sign = (o.oangle x y).sign

Tactic:
rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]

Premises used: Real.Angle.sign_neg, Orientation.oangle_sign_sub_left_eq_neg, Orientation.oangle_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
⊢ (o.oangle x (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₂ : SignType) (o.oangle x y).sign

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
simp_rw :
  (-o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-o.oangle y x).sign
simp_rw₁ :
  -(o.oangle y (r₁ • x + r₂ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
simp_rw₂ :
  -(o.oangle y (r₂ • y + r₁ • x)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
simp_rw₃ :
  -HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle y x).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (-(o.oangle y x).sign)
⊢ (o.oangle (r₁ • x + r₂ • y) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r₁ : SignType) (o.oangle x y).sign

Tactic:
simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right,
    mul_neg]

Premises used: Real.Angle.sign_neg, add_comm, Orientation.oangle_rev, HSMul.hSMul, Orientation.oangle_sign_smul_add_smul_right, mul_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
pos :
  ∀ (hr₁ : r₁ = 0),
    (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType)
        (o.oangle x y).sign
neg :
  ∀ (hr₁ : ¬r₁ = 0),
    (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType)
        (o.oangle x y).sign
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (r₁ * r₄ - r₂ * r₃) : SignType) (o.oangle x y).sign

Tactic:
by_cases hr₁ : r₁ = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
pos : ∀ (hn : x = y), |(o.oangle (y - x) y).toReal| < π / 2
neg : ∀ (hn : ¬x = y), |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
by_cases hn : x = y
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
simp [hn, Real.pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
rw : (o.oangle y x).sign
| (o.oangle (y - x) y).sign

Tactic:
rw [oangle_sign_sub_left_swap]

Premises used: Orientation.oangle_sign_sub_left_swap
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
conv_rhs : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle y x).sign
⊢ (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle (y - x) y).sign

Tactic:
conv_rhs => rw [oangle_sign_sub_left_swap]

Premises used: Orientation.oangle_sign_sub_left_swap
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
rw :
  (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign =
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign
rw₁ rw₂ : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign
⊢ (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle y x).sign

Tactic:
rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]

Premises used: Real.Angle.sign_pi_sub, Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
⊢ (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle (y - x) y).sign

Tactic:
have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := by
    conv_rhs => rw [oangle_sign_sub_left_swap]
    rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : (HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)).sign = (o.oangle (y - x) y).sign
⊢ o.oangle (y - x) y = (↑π : Real.Angle) ∨ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs

Premises used: Real.Angle.sign_two_zsmul_eq_sign_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : o.oangle (y - x) y = (↑π : Real.Angle) ∨ |(o.oangle (y - x) y).toReal| < π / 2
neg : ∀ (hs : o.oangle (y - x) y = (↑π : Real.Angle)), |(o.oangle (y - x) y).toReal| < π / 2
neg₁ : ∀ (hs : |(o.oangle (y - x) y).toReal| < π / 2), |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
rcases hs with (hs | hs)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : o.oangle (y - x) y = (↑π : Real.Angle)
⊢ y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (x - y)

Tactic:
rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sameRay_neg, neg_sub] at hs

Premises used: neg_sub, Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi, Orientation.oangle_eq_pi_iff_sameRay_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (x - y)
⊢ y ≠ 0

Tactic:
rcases hs with ⟨hy, -, hr⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (x - y)
hy : y ≠ 0
⊢ SameRay ℝ y (x - y)

Tactic:
rcases hs with ⟨hy, -, hr⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
hr : SameRay ℝ y (x - y)
⊢ ∃ (r : ℝ), 0 ≤ r ∧ r • y = x - y

Tactic:
rw [← exists_nonneg_left_iff_sameRay hy] at hr

Premises used: exists_nonneg_left_iff_sameRay
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
hr : ∃ (r : ℝ), 0 ≤ r ∧ r • y = x - y
neg : ∀ (r : ℝ) (hr0 : 0 ≤ r) (hr : r • y = x - y), |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
rcases hr with ⟨r, hr0, hr⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y = x - y
⊢ r • y + y = x

Tactic:
rw [eq_sub_iff_add_eq] at hr

Premises used: eq_sub_iff_add_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y + y = x
⊢ r • y + HSMul.hSMul (α := ℝ) 1 y = x

Tactic:
nth_rw 2 [← one_smul ℝ y] at hr

Premises used: Real, one_smul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y + HSMul.hSMul (α := ℝ) 1 y = x
⊢ (r + 1) • y = x

Tactic:
rw [← add_smul] at hr

Premises used: add_smul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ r = 0

Tactic:
rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),
      mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h

Premises used: Iff.mpr, norm_smul, Left.add_pos_of_nonneg_of_pos, mul_left_eq_self₀, norm_ne_zero_iff, add_eq_right, abs_of_pos, or_iff_left, one_pos, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : (r + 1) • y = x
h₁ : r = 0
⊢ 0 ≤ r

Tactic:
rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),
      mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h

Premises used: Iff.mpr, norm_smul, Left.add_pos_of_nonneg_of_pos, mul_left_eq_self₀, norm_ne_zero_iff, add_eq_right, abs_of_pos, or_iff_left, one_pos, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : (r + 1) • y = x
h₁ : r = 0
hr0₁ : 0 ≤ r
⊢ (r + 1) • y = x

Tactic:
rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),
      mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h

Premises used: Iff.mpr, norm_smul, Left.add_pos_of_nonneg_of_pos, mul_left_eq_self₀, norm_ne_zero_iff, add_eq_right, abs_of_pos, or_iff_left, one_pos, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : r = 0
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ y = x

Tactic:
rw [h, zero_add, one_smul] at hr

Premises used: zero_add, one_smul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : r = 0
hr0 : 0 ≤ r
hr : y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
False.elim (hn hr.symm)

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : r = 0
hr0 : 0 ≤ r
hr : y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
exact False.elim (hn hr.symm)

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
hs
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : |(o.oangle (y - x) y).toReal| < π / 2
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
exact hs
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ |(o.oangle x (x - y)).toReal| < π / 2

Tactic:
(o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h).symm ▸ o.abs_oangle_sub_left_toReal_lt_pi_div_two h

Premises used: Eq.rec, Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq, Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
pos :
  ∀ (hy : y = 0),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
neg :
  ∀ (hy : ¬y = 0),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : y = 0
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

Tactic:
simp [hy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
pos :
  ∀ (hr : SameRay ℝ x z),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
neg :
  ∀ (hr : ¬SameRay ℝ x z),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

Tactic:
by_cases hr : SameRay ℝ x z

Premises used: Real, SameRay
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : SameRay ℝ x z
pos :
  ∀ (r : ℝ) (hrp : 0 < r) (hz : r • x ≠ 0) (hr : SameRay ℝ x (r • x)),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y (r • x) ↔
      o.oangle x y = o.oangle y (r • x) ∨ SameRay ℝ x (r • x)
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

Tactic:
obtain ⟨r, hrp, rfl⟩ := hr.exists_pos_left hx hz

Premises used: SameRay.exists_pos_left, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : ¬y = 0
r : ℝ
hrp : 0 < r
hz : r • x ≠ 0
hr : SameRay ℝ x (r • x)
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y (r • x) ↔
    o.oangle x y = o.oangle y (r • x) ∨ SameRay ℝ x (r • x)

Tactic:
simp [hr, hrp, InnerProductGeometry.angle_comm]

Premises used: InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
neg : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z

Tactic:
simp only [hr, or_false]

Premises used: or_false
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
pos :
  ∀ (hs : (o.oangle x y).sign = (o.oangle y z).sign),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
neg :
  ∀ (hs : ¬(o.oangle x y).sign = (o.oangle y z).sign),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z

Tactic:
by_cases hs : (o.oangle x y).sign = (o.oangle y z).sign

Premises used: Orientation.oangle, Real.Angle.sign
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : (o.oangle x y).sign = (o.oangle y z).sign
pos pos₁ : o.oangle x y = o.oangle y z ↔ o.oangle x y = o.oangle y z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z

Tactic:
rw [o.angle_eq_iff_oangle_eq_of_sign_eq hx hy hy hz hs]

Premises used: Orientation.angle_eq_iff_oangle_eq_of_sign_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
⊢ o.oangle x y ≠ o.oangle y z

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
⊢ o.oangle x y ≠ o.oangle y z

Tactic:
have hn : o.oangle x y ≠ o.oangle y z := by grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
neg : ¬InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z

Tactic:
simp only [hn, iff_false]

Premises used: iff_false
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
neg : SameRay ℝ x z
⊢ False

Tactic:
apply hr
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
pos : ∀ (hs' : (o.oangle x y).sign = -(o.oangle y z).sign), SameRay ℝ x z
neg : ∀ (hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign), SameRay ℝ x z
⊢ SameRay ℝ x z

Tactic:
by_cases hs' : (o.oangle x y).sign = -(o.oangle y z).sign

Premises used: Orientation.oangle, Real.Angle.sign
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : (o.oangle x y).sign = -(o.oangle y z).sign
⊢ o.oangle x y = -o.oangle y z

Tactic:
rw [o.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg hx hy hy hz hs'] at he

Premises used: Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : (o.oangle x y).sign = -(o.oangle y z).sign
he₁ : o.oangle x y = -o.oangle y z
⊢ (o.oangle x y).sign = -(o.oangle y z).sign

Tactic:
rw [o.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg hx hy hy hz hs'] at he

Premises used: Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg