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
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
by_cases hx : x = 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
hx : x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [hx]
-- 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
pos : ∀ (hy : y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
neg : ∀ (hy : ¬y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

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 : V
hx : ¬x = 0
hy : y = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

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 : V
hx : ¬x = 0
hy : ¬y = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [o.oangle_neg_left hx hy]

Premises used: Orientation.oangle_neg_left
-- 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
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
by_cases hx : x = 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
hx : x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [hx]
-- 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
pos : ∀ (hy : y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
neg : ∀ (hy : ¬y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

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 : V
hx : ¬x = 0
hy : y = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

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 : V
hx : ¬x = 0
hy : ¬y = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [o.oangle_neg_right hx hy]

Premises used: Orientation.oangle_neg_right
-- 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
⊢ o.oangle (-x) (-y) = o.oangle x y

Tactic:
simp [oangle]

Premises used: Orientation.oangle
-- 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 (-x) (- -y) = o.oangle x (- - -y)
rw₁ : o.oangle x (-y) = o.oangle x (- - -y)
rw₂ rw₃ : o.oangle x (-y) = o.oangle x (-y)
⊢ o.oangle (-x) y = o.oangle x (-y)

Tactic:
rw [← neg_neg y, oangle_neg_neg, neg_neg]

Premises used: neg_neg, Orientation.oangle_neg_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 : V
hx : x ≠ 0
⊢ o.oangle (-x) x = (↑π : Real.Angle)

Tactic:
simp [oangle_neg_left, hx]

Premises used: Orientation.oangle_neg_left
-- 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 : V
hx : x ≠ 0
⊢ o.oangle x (-x) = (↑π : Real.Angle)

Tactic:
simp [oangle_neg_right, hx]

Premises used: Orientation.oangle_neg_right
-- 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 : V
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0
neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0

Tactic:
by_cases hx : x = 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 : V
hx : x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0

Tactic:
simp [hx]
-- 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 : V
hx : ¬x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0

Tactic:
simp [hx]
-- 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 : V
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0
neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0

Tactic:
by_cases hx : x = 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 : V
hx : x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0

Tactic:
simp [hx]
-- 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 : V
hx : ¬x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0

Tactic:
simp [hx]
-- 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 x (-y) + o.oangle (-y) x = 0
rw₁ : -o.oangle (-y) x + o.oangle (-y) x = 0
rw₂ rw₃ : Eq (α := Real.Angle) 0 0
⊢ o.oangle (-x) y + o.oangle (-y) x = 0

Tactic:
rw [oangle_neg_left_eq_neg_right, oangle_rev, neg_add_cancel]

Premises used: Orientation.oangle_neg_left_eq_neg_right, neg_add_cancel, 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 x (-y) + -o.oangle (-x) y = 0
rw₁ : o.oangle x (-y) + -o.oangle x (-y) = 0
rw₂ rw₃ : Eq (α := Real.Angle) 0 0
⊢ o.oangle x (-y) + o.oangle y (-x) = 0

Tactic:
rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_cancel]

Premises used: add_neg_cancel, Orientation.oangle_neg_left_eq_neg_right, Orientation.oangle_rev, Neg.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 : ℝ
hr : 0 < r
⊢ o.oangle (r • x) y = o.oangle x y

Tactic:
simp [oangle, Complex.arg_real_mul _ hr]

Premises used: Orientation.oangle, Complex.arg_real_mul
-- 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 : ℝ
hr : 0 < r
⊢ o.oangle x (r • y) = o.oangle x y

Tactic:
simp [oangle, Complex.arg_real_mul _ hr]

Premises used: Orientation.oangle, Complex.arg_real_mul
-- 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 : ℝ
hr : r < 0
rw : o.oangle (- -r • x) y = o.oangle (-x) y
rw₁ : o.oangle (-(-r • x)) y = o.oangle (-x) y
rw₂ : o.oangle (-r • -x) y = o.oangle (-x) y
rw₃ rw₄ : o.oangle (-x) y = o.oangle (-x) y
⊢ o.oangle (r • x) y = o.oangle (-x) y

Tactic:
rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg hr)]

Premises used: neg_smul, neg_pos_of_neg, neg_neg, smul_neg, Orientation.oangle_smul_left_of_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
r : ℝ
hr : r < 0
rw : o.oangle x (- -r • y) = o.oangle x (-y)
rw₁ : o.oangle x (-(-r • y)) = o.oangle x (-y)
rw₂ : o.oangle x (-r • -y) = o.oangle x (-y)
rw₃ rw₄ : o.oangle x (-y) = o.oangle x (-y)
⊢ o.oangle x (r • y) = o.oangle x (-y)

Tactic:
rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg hr)]

Premises used: neg_smul, neg_pos_of_neg, neg_neg, smul_neg, Orientation.oangle_smul_right_of_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 : V
r : ℝ
hr : 0 ≤ r
inl : ∀ (h : 0 < r), o.oangle (r • x) x = 0
inr : ∀ (h : 0 = r), o.oangle (r • x) x = 0
⊢ o.oangle (r • x) x = 0

Tactic:
rcases hr.lt_or_eq with (h | h)

Premises used: LE.le.lt_or_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 : V
r : ℝ
hr : 0 ≤ r
h : 0 < r
⊢ o.oangle (r • x) x = 0

Tactic:
simp [h]
-- 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 : V
r : ℝ
hr : 0 ≤ r
h : 0 = r
⊢ o.oangle (r • x) x = 0

Tactic:
simp [h.symm]

Premises used: 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 : V
r : ℝ
hr : 0 ≤ r
inl : ∀ (h : 0 < r), o.oangle x (r • x) = 0
inr : ∀ (h : 0 = r), o.oangle x (r • x) = 0
⊢ o.oangle x (r • x) = 0

Tactic:
rcases hr.lt_or_eq with (h | h)

Premises used: LE.le.lt_or_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 : V
r : ℝ
hr : 0 ≤ r
h : 0 < r
⊢ o.oangle x (r • x) = 0

Tactic:
simp [h]
-- 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 : V
r : ℝ
hr : 0 ≤ r
h : 0 = r
⊢ o.oangle x (r • x) = 0

Tactic:
simp [h.symm]

Premises used: 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 : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
inl : ∀ (h : 0 < r₁), o.oangle (r₁ • x) (r₂ • x) = 0
inr : ∀ (h : 0 = r₁), o.oangle (r₁ • x) (r₂ • x) = 0
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
rcases hr₁.lt_or_eq with (h | h)

Premises used: LE.le.lt_or_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 : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 < r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
simp [h, 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 : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 = r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
simp [h.symm]

Premises used: 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
r : ℝ
hr : r ≠ 0
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
inr : ∀ (h : 0 < r), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
rcases hr.lt_or_gt with (h | h)

Premises used: Ne.lt_or_gt
-- 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 : ℝ
hr : r ≠ 0
h : r < 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [h]
-- 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 : ℝ
hr : r ≠ 0
h : 0 < r
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [h]
-- 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 : ℝ
hr : r ≠ 0
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
inr : ∀ (h : 0 < r), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
rcases hr.lt_or_gt with (h | h)

Premises used: Ne.lt_or_gt
-- 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 : ℝ
hr : r ≠ 0
h : r < 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [h]
-- 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 : ℝ
hr : r ≠ 0
h : 0 < r
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)

Tactic:
simp [h]
-- 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 : V
r : ℝ
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
inr : ∀ (h : 0 ≤ r), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0

Tactic:
rcases lt_or_ge r 0 with (h | h)

Premises used: lt_or_ge, 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 : V
r : ℝ
h : r < 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0

Tactic:
simp [h]
-- 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 : V
r : ℝ
h : 0 ≤ r
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0

Tactic:
simp [h]
-- 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 : V
r : ℝ
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
inr : ∀ (h : 0 ≤ r), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0

Tactic:
rcases lt_or_ge r 0 with (h | h)

Premises used: lt_or_ge, 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 : V
r : ℝ
h : r < 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0

Tactic:
simp [h]
-- 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 : V
r : ℝ
h : 0 ≤ r
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0

Tactic:
simp [h]
-- 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 : V
r₁ r₂ : ℝ
pos : ∀ (h : r₁ = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
neg : ∀ (h : ¬r₁ = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0

Tactic:
by_cases h : 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 : V
r₁ r₂ : ℝ
h : r₁ = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0

Tactic:
simp [h]
-- 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 : V
r₁ r₂ : ℝ
h : ¬r₁ = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0

Tactic:
simp [h]
-- 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
h : Eq (α := Submodule ℝ V) (ℝ ∙ x) (ℝ ∙ y)
⊢ ∃ (z : ℝˣ), z • x = y

Tactic:
rw [Submodule.span_singleton_eq_span_singleton] at h

Premises used: Submodule.span_singleton_eq_span_singleton
-- 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
h : ∃ (z : ℝˣ), z • x = y
rcases : ∀ (r : ℝˣ), HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) z)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle y z)

Tactic:
rcases h with ⟨r, rfl⟩

Premises used: 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 z : V
r : ℝˣ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) z)

Tactic:
(o.two_zsmul_oangle_smul_left_of_ne_zero _ _ (Units.ne_zero _)).symm

Premises used: Orientation.two_zsmul_oangle_smul_left_of_ne_zero, Units.ne_zero, 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 z : V
r : ℝˣ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) z)

Tactic:
exact (o.two_zsmul_oangle_smul_left_of_ne_zero _ _ (Units.ne_zero _)).symm

Premises used: Orientation.two_zsmul_oangle_smul_left_of_ne_zero, Units.ne_zero, 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
h : Eq (α := Submodule ℝ V) (ℝ ∙ y) (ℝ ∙ z)
⊢ ∃ (z_1 : ℝˣ), z_1 • y = z

Tactic:
rw [Submodule.span_singleton_eq_span_singleton] at h

Premises used: Submodule.span_singleton_eq_span_singleton
-- 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
h : ∃ (z_1 : ℝˣ), z_1 • y = z
rcases : ∀ (r : ℝˣ), HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y))
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)

Tactic:
rcases h with ⟨r, rfl⟩

Premises used: 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
r : ℝˣ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y))

Tactic:
(o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm

Premises used: Units.ne_zero, Orientation.two_zsmul_oangle_smul_right_of_ne_zero, 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
r : ℝˣ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y))

Tactic:
exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm

Premises used: Units.ne_zero, Orientation.two_zsmul_oangle_smul_right_of_ne_zero, 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)
w x y z : V
hwx : Eq (α := Submodule ℝ V) (ℝ ∙ w) (ℝ ∙ x)
hyz : Eq (α := Submodule ℝ V) (ℝ ∙ y) (ℝ ∙ z)
rw : HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
rw₁ rw₂ : HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle w y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)

Tactic:
rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz]

Premises used: Orientation.two_zsmul_oangle_left_of_span_eq, Orientation.two_zsmul_oangle_right_of_span_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
rw : -o.oangle y x = 0 ↔ o.oangle y x = 0
rw₁ rw₂ : o.oangle y x = 0 ↔ o.oangle y x = 0
⊢ o.oangle x y = 0 ↔ o.oangle y x = 0

Tactic:
rw [oangle_rev, neg_eq_zero]

Premises used: neg_eq_zero, Orientation.oangle_rev