-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
theorem dotProduct_star_self_pos_iff {v : n → R} :
    0 < dotProduct (star v) v ↔ v ≠ 0

Proof state:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
⊢ 0 < star v i * v i ↔ v i ≠ 0

Tactic:
constructor

Result:
case inr.mp
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
⊢ 0 < star v i * v i → v i ≠ 0

case inr.mpr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
⊢ v i ≠ 0 → 0 < star v i * v i

Proof state:
case inl
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Subsingleton R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
obtain rfl : v = 0 := Subsingleton.elim _ _

Result:
case inl
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ 0 < star 0 ⬝ᵥ 0 ↔ 0 ≠ 0

Proof state:
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Subsingleton R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Proof state:
case inr.mp
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
⊢ 0 < star v i * v i → v i ≠ 0

Tactic:
rintro h hv

Result:
case inr.mp
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
h : 0 < star v i * v i
hv : v i = 0
⊢ False

Proof state:
case inr.mp
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
h : 0 < star v i * v i
hv : v i = 0
⊢ False

Tactic:
simp [hv] at h

Result:
no goals

Proof state:
case inl
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ 0 < star 0 ⬝ᵥ 0 ↔ 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
⊢ ((0 ≤ fun i => star v i * v i) ∧ ∃ i, 0 < star v i * v i) ↔ ∃ a, v a ≠ 0

Tactic:
refine (and_iff_right fun i => star_mul_self_nonneg (v i)).trans <| exists_congr fun i => ?_

Result:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
i : n
⊢ 0 < star v i * v i ↔ v i ≠ 0

Proof state:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
refine (Fintype.sum_pos_iff_of_nonneg fun i => star_mul_self_nonneg _).trans ?_

Result:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
⊢ (0 < fun i => star v i * v i) ↔ v ≠ 0

Proof state:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
⊢ (0 < fun i => star v i * v i) ↔ v ≠ 0

Tactic:
simp_rw [Pi.lt_def, Function.ne_iff, Pi.zero_apply]

Result:
case inr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
h✝ : Nontrivial R
⊢ ((0 ≤ fun i => star v i * v i) ∧ ∃ i, 0 < star v i * v i) ↔ ∃ a, v a ≠ 0