-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_add_right_eq_zero_or_eq_pi_iff {x y : V} (r : ℝ) :
    o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = π ↔
    o.oangle x y = 0 ∨ o.oangle x y = π

Proof state:
case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
rcases h with ⟨m, h, hm⟩

Result:
case refine_1.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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
⊢ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Proof state:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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 - 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]

Result:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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)

Proof state:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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 - 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)

Result:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Proof state:
case refine_2.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - 0 * r = 0
h1 : m 1 = 0
⊢ False

Tactic:
rw [zero_mul, sub_zero] at h0

Result:
case refine_2.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 = 0
h1 : m 1 = 0
⊢ False

Proof state:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, 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⟩

Result:
case refine_2.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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
⊢ ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Proof state:
case refine_1.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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
⊢ False

Tactic:
obtain ⟨h0, h1⟩ := h0

Result:
case refine_1.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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
⊢ False

Proof state:
case refine_1.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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, 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], ?_⟩

Result:
case refine_1.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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, 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)

Proof state:
case refine_1.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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
⊢ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

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

Result:
case refine_1.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Proof state:
case refine_2.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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
⊢ False

Tactic:
rw [h1] at h0 hm

Result:
case refine_2.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - 0 * r = 0
h1 : m 1 = 0
⊢ False

Proof state:
case refine_1.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + 0 * r = 0
h1 : m 1 = 0
⊢ False

Tactic:
rw [zero_mul, add_zero] at h0

Result:
case refine_1.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 = 0
h1 : m 1 = 0
⊢ False