-- 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:
case refine_1.inr.inr.inl.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

Tactic:
exact Or.inr ⟨r, rfl⟩

Result:
no goals

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

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

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

Proof state:
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

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

Result:
case refine_1.inr.inr.inl.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 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
⊢ 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:
refine Or.inr (Or.inr (Or.inr ?_))

Result:
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)

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

Tactic:
rw [← o.eq_zero_or_oangle_eq_iff_inner_eq_zero]

Result:
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

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
⊢ 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:
exact Or.inl 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 : 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)

Tactic:
rcases lt_trichotomy r 0 with (hr | rfl | hr)

Result:
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
⊢ 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.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)

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

Tactic:
exact Or.inl rfl

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

Tactic:
exact Or.inl rfl

Result:
no goals

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
⊢ 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:
refine Or.inr (Or.inr (Or.inl ?_))

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

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

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

Result:
no goals

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

Tactic:
rcases h with (rfl | ⟨r, rfl⟩)

Result:
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
⊢ 0 = 0 ∨ y = 0 ∨ o.oangle 0 y = ↑(π / 2) ∨ o.oangle 0 y = ↑(-π / 2)

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)

Proof state:
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

Tactic:
exact Or.inr ⟨0, zero_smul _ _⟩

Result:
no goals