-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem nonneg_pi_iff {P} [Fintype ι] [OrderedAddCommMonoid P] [Module R P]
    {Q : ∀ i, QuadraticMap R (Mᵢ i) P} : (∀ x, 0 ≤ pi Q x) ↔ ∀ i x, 0 ≤ Q i x

Proof state:
case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
⊢ 0 ≤ (Q i) x

Tactic:
classical
convert h (Pi.single i x) using 1
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hji => ?_, Pi.single_eq_same]
rw [Pi.single_eq_of_ne hji, map_zero]

Result:
no goals

Proof state:
case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)) → ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

Tactic:
intro h i x

Result:
case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
⊢ 0 ≤ (Q i) x

Proof state:
case h.e'_4
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
⊢ (Q i) x = ∑ x_1 : ι, (Q x_1) (Pi.single i x x_1)

Tactic:
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hji => ?_, Pi.single_eq_same]

Result:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ (Q j) (Pi.single i x j) = 0

Proof state:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

Tactic:
constructor

Result:
case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)) → ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

case mpr
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x) → ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)

Proof state:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
j : ι
x✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
rw [Pi.single_eq_of_ne hji, map_zero]

Result:
no goals

Proof state:
case mpr
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x) → ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)

Tactic:
rintro h x

Result:
case mpr
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
x : (i : ι) → Mᵢ i
⊢ 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)

Proof state:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ (pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

Tactic:
simp_rw [pi, sum_apply, comp_apply, LinearMap.proj_apply]

Result:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

Proof state:
case mpr
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
x : (i : ι) → Mᵢ i
⊢ 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)

Tactic:
exact Finset.sum_nonneg fun i _ => h i (x i)

Result:
no goals

Proof state:
case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
⊢ 0 ≤ (Q i) x

Tactic:
convert h (Pi.single i x) using 1

Result:
case h.e'_4
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝² : Fintype ι
inst✝¹ : OrderedAddCommMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)
i : ι
x : Mᵢ i
⊢ (Q i) x = ∑ x_1 : ι, (Q x_1) (Pi.single i x x_1)