-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two {x y : V} :
    ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ r : ℝ, r • o.rotation (π / 2 : ℝ) 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
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

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 : x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

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, r • (o.rotation ↑(π / 2)) x = y
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)

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 : ℝ
⊢ x = 0 ∨
    r • (o.rotation ↑(π / 2)) x = 0 ∨
      o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2) ∨ o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(-π / 2)

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
⊢ x = 0 ∨
    r • (o.rotation ↑(π / 2)) x = 0 ∨
      o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2) ∨ o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(-π / 2)

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
⊢ x = 0 ∨
    r • (o.rotation ↑(π / 2)) x = 0 ∨
      o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2) ∨ o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(-π / 2)

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
⊢ o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(-π / 2)

Tactic:
rw [o.oangle_smul_right_of_neg _ _ hr, o.neg_rotation_pi_div_two,
  o.oangle_rotation_self_right hx]

Result:
no goals

Proof state:
case refine_1.inr.inr.inr
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 = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

Tactic:
obtain ⟨r, _, rfl⟩ :=
  (o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero
    (o.left_ne_zero_of_oangle_eq_neg_pi_div_two h)
    (o.right_ne_zero_of_oangle_eq_neg_pi_div_two h) _).1 h

Result:
case refine_1.inr.inr.inr.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
left✝ : 0 < r
h : o.oangle x (r • (o.rotation ↑(-π / 2)) x) = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r_1, r_1 • (o.rotation ↑(π / 2)) x = r • (o.rotation ↑(-π / 2)) 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 : x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

Tactic:
rcases h with (rfl | rfl | 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)
y : V
⊢ 0 = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) 0 = y

case refine_1.inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = 0

case refine_1.inr.inr.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 : o.oangle x y = ↑(π / 2)
⊢ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

case refine_1.inr.inr.inr
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 = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

Proof state:
case refine_1.inr.inr.inr.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
left✝ : 0 < r
h : o.oangle x (r • (o.rotation ↑(-π / 2)) x) = ↑(-π / 2)
⊢ -r • (o.rotation ↑(π / 2)) x = r • (o.rotation ↑(-π / 2)) x

Tactic:
rw [neg_smul, ← smul_neg, o.neg_rotation_pi_div_two]

Result:
no goals

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
hx : ¬x = 0
⊢ x = 0 ∨
    0 • (o.rotation ↑(π / 2)) x = 0 ∨
      o.oangle x (0 • (o.rotation ↑(π / 2)) x) = ↑(π / 2) ∨ o.oangle x (0 • (o.rotation ↑(π / 2)) x) = ↑(-π / 2)

Tactic:
exact Or.inr (Or.inl (zero_smul _ _))

Result:
no goals