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

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
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

case neg.mpr
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
⊢ SameRay ℝ x y → 0 ≤ inner x y ∧ (o.areaForm x) y = 0

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
hx' : 0 < ‖x‖
ha' : 0 ≤ a
hb' : b = 0
⊢ SameRay ℝ x (b • o.rightAngleRotation x)

Tactic:
simp [hb']

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
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
⊢ 0 < ‖x‖ ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case neg.mpr.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ inner x (r • x) ∧ (o.areaForm x) (r • x) = 0

Tactic:
simp only [inner_smul_right, real_inner_self_eq_norm_sq, LinearMap.map_smulₛₗ,
  areaForm_apply_self, Algebra.id.smul_eq_mul, mul_zero, eq_self_iff_true, and_true]

Result:
case neg.mpr.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ r * ‖x‖ ^ 2

Proof state:
case neg.mpr
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
h : SameRay ℝ x y
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0

Tactic:
obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx

Result:
case neg.mpr.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ inner x (r • x) ∧ (o.areaForm x) (r • x) = 0

Proof state:
case neg.mpr.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ r * ‖x‖ ^ 2

Tactic:
positivity

Result:
no goals

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 ≤ inner x y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
suffices ↑0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x) by
  rw [← (o.basisRightAngleRotation x hx).sum_repr y]
  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]
  exact this

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
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
⊢ 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • 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
hx' : 0 < ‖x‖
ha' : 0 ≤ a
hb' : b = 0
⊢ SameRay ℝ x (a • x + b • o.rightAngleRotation x)

Tactic:
exact (SameRay.sameRay_nonneg_smul_right x ha').add_right <| by simp [hb']

Result:
no goals

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

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg.mpr
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
⊢ SameRay ℝ x y → 0 ≤ inner x y ∧ (o.areaForm x) y = 0

Tactic:
intro h

Result:
case neg.mpr
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
h : SameRay ℝ x y
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0

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
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
let b : ℝ := (o.basisRightAngleRotation x hx).repr y 1

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
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
⊢ 0 ≤ inner x y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

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 y ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
rw [← (o.basisRightAngleRotation x hx).sum_repr y]

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 ≤ 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)