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
hx : ¬x = 0
pos : ∀ (hy : y = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
neg : ∀ (hy : ¬y = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

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
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

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
neg : (o.oangle x y + (↑π : Real.Angle)).sign = -(o.oangle x y).sign
neg₁ neg₂ : -(o.oangle x y).sign = -(o.oangle x y).sign
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi]

Premises used: Orientation.oangle_neg_left, Real.Angle.sign_add_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
pos : ∀ (hx : x = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
neg : ∀ (hx : ¬x = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

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
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

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), (o.oangle x (-y)).sign = -(o.oangle x y).sign
neg : ∀ (hy : ¬y = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

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
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

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
neg : (o.oangle x y + (↑π : Real.Angle)).sign = -(o.oangle x y).sign
neg₁ neg₂ : -(o.oangle x y).sign = -(o.oangle x y).sign
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

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

Premises used: Orientation.oangle_neg_right, Real.Angle.sign_add_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
r : ℝ
inl :
  ∀ (h : r < 0),
    (o.oangle (r • x) y).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
inr :
  ∀ (h : r = 0),
    (o.oangle (r • x) y).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
inr₁ :
  ∀ (h : 0 < r),
    (o.oangle (r • x) y).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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

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 y : V
r : ℝ
h : r < 0
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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 : ℝ
h : r = 0
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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 : ℝ
h : 0 < r
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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 : ℝ
inl :
  ∀ (h : r < 0),
    (o.oangle x (r • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
inr :
  ∀ (h : r = 0),
    (o.oangle x (r • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
inr₁ :
  ∀ (h : 0 < r),
    (o.oangle x (r • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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

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 y : V
r : ℝ
h : r < 0
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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 : ℝ
h : r = 0
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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 : ℝ
h : 0 < r
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign

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 : ℝ
simp_rw :
  (∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = (↑π : Real.Angle) ↔
    o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)

Tactic:
simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Fintype.not_linearIndependent_iff,
    Fin.sum_univ_two, Fin.exists_fin_two]

Premises used: Fin.exists_fin_two, Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Fintype.not_linearIndependent_iff, Fin.sum_univ_two
-- 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 : ℝ
⊢ (∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

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
r : ℝ
refine_1 :
  ∀
    (h :
      ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)),
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
refine_2 :
  ∀ (h : ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)),
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ (∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

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
r : ℝ
h : ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
refine_1 :
  ∀ (m : Fin (Nat.succ 0).succ → ℝ) (h : m 0 • ![x, r • x + y] 0 + m 1 • ![x, r • x + y] 1 = 0)
    (hm : m 0 ≠ 0 ∨ m 1 ≠ 0),
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
rcases h with ⟨m, h, hm⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
h : m 0 • ![x, r • x + y] 0 + m 1 • ![x, r • x + y] 1 = 0
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
⊢ m 0 • x + m 1 • (r • x + y) = 0

Tactic:
change m 0 • x + m 1 • (r • x + y) = 0 at h

Premises used: HAdd.hAdd, HSMul.hSMul, 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
⟨![m 0 + m 1 * r, m 1], ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, Exists.intro, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 0
refine_1 :
  ![m 0 + m 1 * r, m 1] 0 • ![x, y] 0 + ![m 0 + m 1 * r, m 1] 1 • ![x, y] 1 = 0 ∧
    (![m 0 + m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 + m 1 * r, m 1] 1 ≠ 0)
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
refine ⟨![m 0 + m 1 * r, m 1], ?_⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 0
refine_1 : (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)
⊢ ![m 0 + m 1 * r, m 1] 0 • ![x, y] 0 + ![m 0 + m 1 * r, m 1] 1 • ![x, y] 1 = 0 ∧
    (![m 0 + m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 + m 1 * r, m 1] 1 ≠ 0)

Tactic:
change (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Premises used: HMul.hMul, Ne, HAdd.hAdd, Or, 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 0
⊢ (m 0 + m 1 * r) • x + m 1 • y = 0

Tactic:
rw [smul_add, smul_smul, ← add_assoc, ← add_smul] at h

Premises used: add_assoc, smul_smul, add_smul, smul_add
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
⊢ (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Tactic:
⟨h, not_and_or.1 fun h0 => ?_⟩

Premises used: And.intro, not_and_or, Iff.mp
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
refine_1 : ∀ (h0 : m 0 + m 1 * r = 0 ∧ m 1 = 0), False
⊢ (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Tactic:
refine ⟨h, not_and_or.1 fun h0 => ?_⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0 ∧ m 1 = 0
⊢ m 0 + m 1 * r = 0

Tactic:
obtain ⟨h0, h1⟩ := h0
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0 ∧ m 1 = 0
h0₁ : m 0 + m 1 * r = 0
⊢ m 1 = 0

Tactic:
obtain ⟨h0, h1⟩ := h0
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0
h1 : m 1 = 0
⊢ m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0

Tactic:
rw [h1] at h0 hm
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
⊢ (m 0 + m 1 * r) • x + m 1 • y = 0

Tactic:
rw [h1] at h0 hm
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h₁ : (m 0 + m 1 * r) • x + m 1 • y = 0
⊢ m 0 + 0 * r = 0

Tactic:
rw [h1] at h0 hm
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h₁ : (m 0 + m 1 * r) • x + m 1 • y = 0
h0₁ : m 0 + 0 * r = 0
⊢ m 1 = 0

Tactic:
rw [h1] at h0 hm
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + 0 * r = 0
h1 : m 1 = 0
⊢ m 0 = 0

Tactic:
rw [zero_mul, add_zero] at h0

Premises used: MulZeroClass.zero_mul, add_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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + 0 * r = 0
h1 : m 1 = 0
h0₁ : m 0 = 0
⊢ m 1 = 0

Tactic:
rw [zero_mul, add_zero] at h0

Premises used: MulZeroClass.zero_mul, add_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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 = 0
h1 : m 1 = 0
⊢ False

Tactic:
simp [h0] at hm
-- 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 : ℝ
h : ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
refine_2 :
  ∀ (m : Fin (Nat.succ 0).succ → ℝ) (h : m 0 • ![x, y] 0 + m 1 • ![x, y] 1 = 0) (hm : m 0 ≠ 0 ∨ m 1 ≠ 0),
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
rcases h with ⟨m, h, hm⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
h : m 0 • ![x, y] 0 + m 1 • ![x, y] 1 = 0
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
⊢ m 0 • x + m 1 • y = 0

Tactic:
change m 0 • x + m 1 • y = 0 at h

Premises used: 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
⟨![m 0 - m 1 * r, m 1], ?_⟩

Premises used: HMul.hMul, HSub.hSub, Exists.intro, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
refine_2 :
  ![m 0 - m 1 * r, m 1] 0 • ![x, r • x + y] 0 + ![m 0 - m 1 * r, m 1] 1 • ![x, r • x + y] 1 = 0 ∧
    (![m 0 - m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 - m 1 * r, m 1] 1 ≠ 0)
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
refine ⟨![m 0 - m 1 * r, m 1], ?_⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
refine_2 : (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
⊢ ![m 0 - m 1 * r, m 1] 0 • ![x, r • x + y] 0 + ![m 0 - m 1 * r, m 1] 1 • ![x, r • x + y] 1 = 0 ∧
    (![m 0 - m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 - m 1 * r, m 1] 1 ≠ 0)

Tactic:
change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Premises used: HMul.hMul, HSub.hSub, Ne, HAdd.hAdd, HSMul.hSMul, Or, 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
refine_2 : m 0 • x + m 1 • y = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
⊢ (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Tactic:
rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_add_cancel]

Premises used: add_assoc, sub_smul, smul_smul, sub_add_cancel, smul_add
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ m 0 • x + m 1 • y = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Tactic:
⟨h, not_and_or.1 fun h0 => ?_⟩

Premises used: And.intro, not_and_or, Iff.mp
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
refine_2 : ∀ (h0 : m 0 - m 1 * r = 0 ∧ m 1 = 0), False
⊢ m 0 • x + m 1 • y = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Tactic:
refine ⟨h, not_and_or.1 fun h0 => ?_⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0 ∧ m 1 = 0
⊢ m 0 - m 1 * r = 0

Tactic:
obtain ⟨h0, h1⟩ := h0
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0 ∧ m 1 = 0
h0₁ : m 0 - m 1 * r = 0
⊢ m 1 = 0

Tactic:
obtain ⟨h0, h1⟩ := h0
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0
h1 : m 1 = 0
⊢ m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0

Tactic:
rw [h1] at h0 hm
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
⊢ m 0 • x + m 1 • y = 0

Tactic:
rw [h1] at h0 hm
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h₁ : m 0 • x + m 1 • y = 0
⊢ m 0 - 0 * r = 0

Tactic:
rw [h1] at h0 hm