-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} :
    o.oangle x y = 0 ∨ o.oangle x y = π ↔ x = 0 ∨ ∃ r : ℝ, y = r • x

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

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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:
obtain ⟨r, -, rfl⟩ := h.exists_nonneg_left hx

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

Proof state:
case refine_2.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
⊢ SameRay ℝ 0 y ∨ 0 ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ 0 (-y)

Tactic:
simp

Result:
no goals

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

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

Result:
case neg.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
h : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ y = -r • x

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

Result:
no goals

Proof state:
case neg.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
h : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ y = -r • x

Tactic:
simp [hy]

Result:
no goals

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

Result:
no goals

Proof state:
case refine_1.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : SameRay ℝ x y
⊢ x = 0 ∨ ∃ r, y = r • x

Tactic:
by_cases hx : x = 0

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

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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

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

Tactic:
rcases h with (h | ⟨-, -, h⟩)

Result:
case refine_1.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : SameRay ℝ x y
⊢ x = 0 ∨ ∃ r, y = r • x

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

Proof state:
case refine_2.inr.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
by_cases hx : x = 0

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

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

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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:
obtain ⟨r, -, hy⟩ := h.exists_nonneg_left hx

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

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

Result:
no goals

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

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ x = 0 ∨ ∃ r, y = r • x

Tactic:
rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg]

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

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

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : 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:
refine ⟨fun h => ?_, fun h => ?_⟩

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

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

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

Result:
no goals