-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) :
    0 ≤ ⟪x, y⟫ ∧ ω x y = 0 ↔ SameRay ℝ x y

Proof state:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
ha' : 0 ≤ a
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Tactic:
have hb' : b = 0 := eq_zero_of_ne_zero_of_mul_right_eq_zero (pow_ne_zero 2 hx'.ne') hb

Result:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
ha' : 0 ≤ a
hb' : b = 0
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Proof state:
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
⊢ 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Tactic:
rintro ⟨ha, hb⟩

Result:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

Tactic:
by_cases hx : x = 0

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x = 0
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

Proof state:
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
let a : ℝ := (o.basisRightAngleRotation x hx).repr y 0

Result:
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Proof state:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Tactic:
have ha' : 0 ≤ a := nonneg_of_mul_nonneg_left ha (by positivity)

Result:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
ha' : 0 ≤ a
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
⊢ 0 < ‖x‖

Tactic:
simpa using hx

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • o.rightAngleRotation x)
⊢ 0 ≤ ((o.basisRightAngleRotation x hx).repr y) 0 * ‖x‖ ^ 2 ∧
      ((o.basisRightAngleRotation x hx).repr y) 1 * ‖x‖ ^ 2 = 0 →
    SameRay ℝ x
      (((o.basisRightAngleRotation x hx).repr y) 0 • x +
        ((o.basisRightAngleRotation x hx).repr y) 1 • o.rightAngleRotation x)

Tactic:
exact this

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • o.rightAngleRotation x)
⊢ 0 ≤ inner x (∑ i : Fin 2, ((o.basisRightAngleRotation x hx).repr y) i • (o.basisRightAngleRotation x hx) i) ∧
      (o.areaForm x) (∑ i : Fin 2, ((o.basisRightAngleRotation x hx).repr y) i • (o.basisRightAngleRotation x hx) i) =
        0 →
    SameRay ℝ x (∑ i : Fin 2, ((o.basisRightAngleRotation x hx).repr y) i • (o.basisRightAngleRotation x hx) i)

Tactic:
simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero,
  Fin.succ_zero_eq_one', Finset.univ_eq_empty, Finset.sum_empty, areaForm_apply_self,
  map_smul, map_add, real_inner_smul_right, inner_add_right, Matrix.cons_val_one,
  Matrix.head_cons, Algebra.id.smul_eq_mul, areaForm_rightAngleRotation_right,
  mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right,
  real_inner_self_eq_norm_sq, zero_smul, one_smul]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • o.rightAngleRotation x)
⊢ 0 ≤ ((o.basisRightAngleRotation x hx).repr y) 0 * ‖x‖ ^ 2 ∧
      ((o.basisRightAngleRotation x hx).repr y) 1 * ‖x‖ ^ 2 = 0 →
    SameRay ℝ x
      (((o.basisRightAngleRotation x hx).repr y) 0 • x +
        ((o.basisRightAngleRotation x hx).repr y) 1 • o.rightAngleRotation x)

Proof state:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Tactic:
have hx' : 0 < ‖x‖ := by simpa using hx

Result:
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)