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 :
  0 ≤
        ((↑⟪x, y⟫ : ℂ) +
            HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) I).re ∧
      ((↑⟪x, y⟫ : ℂ) +
            HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) I).im =
        0 ↔
    SameRay ℝ x y
⊢ o.oangle x y = 0 ↔ SameRay ℝ x y

Tactic:
rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero,
    Complex.arg_eq_zero_iff]

Premises used: Orientation.oangle, Complex.arg_coe_angle_eq_iff_eq_toReal, Complex.arg_eq_zero_iff, Orientation.kahler_apply_apply, Real.Angle.toReal_zero
-- 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
⊢ 0 ≤
        ((↑⟪x, y⟫ : ℂ) +
            HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) I).re ∧
      ((↑⟪x, y⟫ : ℂ) +
            HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) I).im =
        0 ↔
    SameRay ℝ x y

Tactic:
simpa using o.nonneg_inner_and_areaForm_eq_zero_iff_sameRay x y

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

Tactic:
rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_coe_pi]

Premises used: neg_eq_iff_eq_neg, Real.Angle.neg_coe_pi, 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 = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)

Tactic:
rw [← o.oangle_eq_zero_iff_sameRay]

Premises used: Orientation.oangle_eq_zero_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
mp : o.oangle x y = (↑π : Real.Angle) → x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
mpr : x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0 → o.oangle x y = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
constructor
-- 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 : o.oangle x y = (↑π : Real.Angle)
pos : ∀ (hx : x = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
neg : ∀ (hx : ¬x = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 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 y : V
h : o.oangle x y = (↑π : Real.Angle)
hx : x = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
simp [hx, Real.Angle.pi_ne_zero.symm] at h

Premises used: Ne.symm, Real.Angle.pi_ne_zero
-- 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 : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
pos : ∀ (hy : y = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
neg : ∀ (hy : ¬y = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : y = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
simp [hy, Real.Angle.pi_ne_zero.symm] at h

Premises used: Ne.symm, Real.Angle.pi_ne_zero
-- 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 : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
⟨hx, hy, ?_⟩

Premises used: And.intro
-- 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 : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
neg : o.oangle x (-y) = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
refine ⟨hx, 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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
neg : o.oangle x y + (↑π : Real.Angle) = 0
neg₁ : (↑π : Real.Angle) + (↑π : Real.Angle) = 0
neg₂ neg₃ : Eq (α := Real.Angle) 0 0
⊢ o.oangle x (-y) = 0

Tactic:
rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_pi]

Premises used: Orientation.oangle_neg_right, Real.Angle.coe_pi_add_coe_pi
-- 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
h : o.oangle x (-y) = 0
mpr : ∀ (h : o.oangle x y + (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
mpr₁ : ∀ (h : o.oangle x y - (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
mpr₂ mpr₃ mpr₄ mpr₅ : ∀ (h : o.oangle x y = (↑π : Real.Angle)), o.oangle x y = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle)

Tactic:
rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h

Premises used: Orientation.oangle_neg_right, sub_eq_zero, Real.Angle.sub_coe_pi_eq_add_coe_pi
-- 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 : SameRay ℝ x y ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
rw₁ : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ ¬LinearIndependent ℝ ![x, y]
rw₂ rw₃ : ¬LinearIndependent ℝ ![x, y] ↔ ¬LinearIndependent ℝ ![x, y]
⊢ o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]

Tactic:
rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg,
    sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent]

Premises used: sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent, Orientation.oangle_eq_zero_iff_sameRay, 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
rw : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg]

Premises used: Orientation.oangle_eq_zero_iff_sameRay, 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
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (h : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)), x = 0 ∨ ∃ (r : ℝ), y = r • x
refine_2 : ∀ (h : x = 0 ∨ ∃ (r : ℝ), y = r • x), SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
refine ⟨fun h => ?_, fun 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
h : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
refine_1 : ∀ (h : SameRay ℝ x y), x = 0 ∨ ∃ (r : ℝ), y = r • x
refine_1₁ : ∀ (h : SameRay ℝ x (-y)), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
rcases h with (h | ⟨-, -, 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
h : SameRay ℝ x y
pos : ∀ (hx : x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
neg : ∀ (hx : ¬x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

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
h : SameRay ℝ x y
hx : x = 0
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

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
h : SameRay ℝ x y
hx : ¬x = 0
neg : ∀ (r : ℝ) (h : SameRay ℝ x (r • x)), x = 0 ∨ ∃ (r_1 : ℝ), r • x = r_1 • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
obtain ⟨r, -, rfl⟩ := h.exists_nonneg_left hx

Premises used: SameRay.exists_nonneg_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 : V
hx : ¬x = 0
r : ℝ
h : SameRay ℝ x (r • x)
⊢ x = 0 ∨ ∃ (r_1 : ℝ), r • x = r_1 • x

Tactic:
Or.inr ⟨r, rfl⟩

Premises used: Exists.intro, Or.inr, 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 : V
hx : ¬x = 0
r : ℝ
h : SameRay ℝ x (r • x)
⊢ x = 0 ∨ ∃ (r_1 : ℝ), r • x = r_1 • x

Tactic:
exact Or.inr ⟨r, rfl⟩

Premises used: Or.inr
-- 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 : SameRay ℝ x (-y)
pos : ∀ (hx : x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
neg : ∀ (hx : ¬x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

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
h : SameRay ℝ x (-y)
hx : x = 0
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

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
h : SameRay ℝ x (-y)
hx : ¬x = 0
neg : ∀ (r : ℝ) (hy : r • x = -y), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
obtain ⟨r, -, hy⟩ := h.exists_nonneg_left hx

Premises used: SameRay.exists_nonneg_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
h : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
Or.inr ⟨-r, ?_⟩

Premises used: Exists.intro, Neg.neg, Or.inr
-- 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 : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
neg : y = -r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x

Tactic:
refine Or.inr ⟨-r, ?_⟩

Premises used: Or.inr
-- 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 : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ y = -r • x

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
h : x = 0 ∨ ∃ (r : ℝ), y = r • x
refine_2 : SameRay ℝ 0 y ∨ Ne.{u_1 + 1} (α := V) 0 0 ∧ y ≠ 0 ∧ SameRay ℝ 0 (-y)
refine_2₁ : ∀ (r : ℝ), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)

Tactic:
rcases h with (rfl | ⟨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)
y : V
⊢ SameRay ℝ 0 y ∨ Ne.{u_1 + 1} (α := V) 0 0 ∧ y ≠ 0 ∧ SameRay ℝ 0 (-y)

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 : V
r : ℝ
pos : ∀ (hx : x = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
neg : ∀ (hx : ¬x = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

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
r : ℝ
hx : x = 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

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
r : ℝ
hx : ¬x = 0
neg : ∀ (hr : r < 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
neg₁ : ∀ (hr : r = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
neg₂ : ∀ (hr : 0 < r), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
rcases lt_trichotomy r 0 with (hr | hr | hr)

Premises used: OfNat.ofNat, lt_trichotomy
-- 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 : ℝ
hx : ¬x = 0
hr : r < 0
neg : SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-r • x)
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
rw [← neg_smul]

Premises used: neg_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 : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-r • x)

Tactic:
Or.inr ⟨hx, smul_ne_zero hr.ne hx,
        SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩

Premises used: Iff.mpr, smul_ne_zero, Left.neg_pos_iff, And.intro, SameRay.sameRay_pos_smul_right, Or.inr, LT.lt.ne
-- 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 : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-r • x)

Tactic:
exact Or.inr ⟨hx, smul_ne_zero hr.ne hx,
        SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩

Premises used: Or.inr
-- 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 : ℝ
hx : ¬x = 0
hr : r = 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
simp [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 : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
Or.inl (SameRay.sameRay_pos_smul_right x hr)

Premises used: Or.inl, SameRay.sameRay_pos_smul_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
r : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
exact Or.inl (SameRay.sameRay_pos_smul_right x hr)

Premises used: Or.inl, SameRay.sameRay_pos_smul_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
contrapose! : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
⊢ o.oangle x y ≠ 0 ∧ o.oangle x y ≠ (↑π : Real.Angle) ↔ LinearIndependent ℝ ![x, y]

Tactic:
contrapose! +distrib
-- 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 = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]

Tactic:
oangle_eq_zero_or_eq_pi_iff_not_linearIndependent o

Premises used: Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent
-- 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 = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]

Tactic:
exact oangle_eq_zero_or_eq_pi_iff_not_linearIndependent o

Premises used: Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent
-- 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 : x = y ↔ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
⊢ x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0

Tactic:
rw [oangle_eq_zero_iff_sameRay]

Premises used: Orientation.oangle_eq_zero_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
mp : x = y → ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
mpr : ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y
⊢ x = y ↔ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y

Tactic:
constructor
-- 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
mp : SameRay ℝ x x
⊢ ‖x‖ = ‖x‖ ∧ SameRay ℝ x x

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 : V
⊢ SameRay ℝ x x

Tactic:
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
mpr : ‖x‖ = norm.{u_1} (E := V) 0 ∧ SameRay ℝ x 0 → x = 0
mpr₁ : ∀ (hy : y ≠ 0), ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y
⊢ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, 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 : V
⊢ ‖x‖ = norm.{u_1} (E := V) 0 ∧ SameRay ℝ x 0 → x = 0

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
hy : y ≠ 0
h₁ : ‖x‖ = ‖y‖
h₂ : SameRay ℝ x y
mpr : ∀ (r : ℝ) (hr : 0 ≤ r) (h₁ : ‖r • y‖ = ‖y‖) (h₂ : SameRay ℝ (r • y) y), r • y = y
⊢ x = y

Tactic:
obtain ⟨r, hr, rfl⟩ := h₂.exists_nonneg_right hy

Premises used: SameRay.exists_nonneg_right, 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
⊢ ‖y‖ ≠ 0

Tactic:
simpa using 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
⊢ ‖y‖ ≠ 0

Tactic:
have : ‖y‖ ≠ 0 := by simpa using 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
apply : r * ‖y‖ = 1 * ‖y‖
⊢ r = 1

Tactic:
apply mul_right_cancel₀ this

Premises used: mul_right_cancel₀
-- 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
⊢ r * ‖y‖ = 1 * ‖y‖

Tactic:
simpa [norm_smul, abs_of_nonneg hr] using h₁

Premises used: norm_smul, abs_of_nonneg
-- 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
mpr :
  ∀ (hr : LE.le (α := ℝ) 0 1) (h₁ : ‖HSMul.hSMul (α := ℝ) 1 y‖ = ‖y‖) (h₂ : SameRay ℝ (HSMul.hSMul (α := ℝ) 1 y) y),
    HSMul.hSMul (α := ℝ) 1 y = y
⊢ r • y = y

Tactic:
obtain rfl : r = 1 := by
      apply mul_right_cancel₀ this
      simpa [norm_smul, abs_of_nonneg hr] using h₁

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)
y : V
hy : y ≠ 0
this : ‖y‖ ≠ 0
hr : LE.le (α := ℝ) 0 1
h₁ : ‖HSMul.hSMul (α := ℝ) 1 y‖ = ‖y‖
h₂ : SameRay ℝ (HSMul.hSMul (α := ℝ) 1 y) y
⊢ HSMul.hSMul (α := ℝ) 1 y = y

Tactic:
simp