-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_pi_iff_sameRay_neg {x y : V} :
    o.oangle x y = π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)

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 = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)

Tactic:
rw [← o.oangle_eq_zero_iff_sameRay]

Result:
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 = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

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

Tactic:
refine ⟨hx, hy, ?_⟩

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

Proof state:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0 → o.oangle x y = ↑π

Tactic:
rintro ⟨hx, hy, h⟩

Result:
case mpr.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
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x (-y) = 0
⊢ o.oangle x y = ↑π

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

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

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

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

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

Proof state:
case mpr.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
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x (-y) = 0
⊢ o.oangle x y = ↑π

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

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

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

Result:
no goals

Proof state:
case mp
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 = ↑π → x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
intro h

Result:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑π
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Proof state:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑π
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

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

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

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 : o.oangle x y = ↑π
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

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 = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

Tactic:
constructor

Result:
case mp
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 = ↑π → x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0

case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0 → o.oangle x y = ↑π