awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
this : x = 0
⊢ x = 0

Tactic:
exact this
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
refine_1 :
  ∀ (x_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ x_1 →
      Eq.{u_7 + 1} (α := P) ((Q x_1 : (a : Mᵢ x_1) → P) (Pi.single (M := Mᵢ) i x x_1) : P) (0 : P)
⊢ Eq.{u_7 + 1} (α := P) (∑ i_1 : ι, (Q i_1 : (a : Mᵢ i_1) → P) (Pi.single (M := Mᵢ) i x i_1)) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
j : ι
refine_1 :
  Membership.mem (γ := Finset ι) Finset.univ j →
    Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
⊢ Membership.mem (γ := Finset ι) Finset.univ j →
    Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
pos : ∀ (hji : j = i), Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
neg : ∀ (hji : ¬j = i), Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)

Tactic:
by_cases hji : j = i
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
hji : j = i
pos :
  ∀ (x : Mᵢ j) (hx : Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) x : P) (0 : P)),
    Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) j x j) : P) (0 : P)
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)

Tactic:
subst hji
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
x : Mᵢ j
hx : Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) x : P) (0 : P)
pos : Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) x : P) (0 : P)
pos₁ pos₂ : Eq.{u_7 + 1} (α := P) 0 0
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) j x j) : P) (0 : P)

Tactic:
rw [Pi.single_eq_same, hx]

Premises used: Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
hji : ¬j = i
neg : Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) 0 : P) (0 : P)
neg₁ neg₂ : Eq.{u_7 + 1} (α := P) 0 0
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)

Tactic:
rw [Pi.single_eq_of_ne hji, map_zero]

Premises used: map_zero, Pi.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : AddCommMonoid P
inst_3 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_4 : Module R P
inst_5 : Fintype ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), Eq.{u_7 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : Eq.{u_7 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P) (0 : P)
refine_1 : Eq.{u_7 + 1} (α := P) (∑ i_1 : ι, (Q i_1 : (a : Mᵢ i_1) → P) (Pi.single (M := Mᵢ) i x i_1)) 0
refine_2 : ∀ (this : Pi.single (M := Mᵢ) i x i = 0), x = 0
refine_1₁ : Eq.{u_7 + 1} (α := P) (∑ i_1 : ι, (Q i_1 : (a : Mᵢ i_1) → P) (Pi.single (M := Mᵢ) i x i_1)) 0
refine_2₁ refine_2₂ : ∀ (this : Pi.single (M := Mᵢ) i x i = 0), x = 0
refine_1₂ refine_1₃ : Eq.{u_7 + 1} (α := P) (∑ i_1 : ι, (Q i_1 : (a : Mᵢ i_1) → P) (Pi.single (M := Mᵢ) i x i_1)) 0
refine_1₄ refine_1₅ :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
pos :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      ∀ (hji : j = i), Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
neg neg₁ :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      ∀ (hji : ¬j = i), Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
⊢ x = 0

Tactic:
classical
  have := h (Pi.single i x) ?_ i
  · rw [Pi.single_eq_same] at this
    exact this
  apply Finset.sum_eq_zero
  intro j _
  by_cases hji : j = i
  · subst hji; rw [Pi.single_eq_same, hx]
  · rw [Pi.single_eq_of_ne hji, map_zero]

Premises used: Finset.sum_eq_zero, map_zero, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
simp_rw :
  (∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))) ↔
    ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)
⊢ (∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P)) ↔
    ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)

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

Premises used: QuadraticMap.pi, QuadraticMap.sum_apply, LinearMap.proj_apply, QuadraticMap.comp_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
mp :
  (∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))) →
    ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)
mpr :
  (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) →
    ∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))
⊢ (∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))) ↔
    ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))
i : ι
x : Mᵢ i
⊢ LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (Pi.single (M := Mᵢ) i x x_1))

Tactic:
h (Pi.single i x)

Premises used: Pi.single
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))
i : ι
x : Mᵢ i
h₁ :
  Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P)
    (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (Pi.single (M := Mᵢ) i x x_1) : P)
⊢ LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)

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

Premises used: Pi.single
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))
i : ι
x : Mᵢ i
rw :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      ∀ (hji : j ≠ i), Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
⊢ Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P)
    (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (Pi.single (M := Mᵢ) i x x_1) : P)

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

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))
i : ι
x : Mᵢ i
j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
hji : j ≠ i
rw : Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) 0 : P) (0 : P)
rw₁ rw₂ : Eq.{u_10 + 1} (α := P) 0 0
⊢ Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)

Tactic:
rw [Pi.single_eq_of_ne hji, map_zero]

Premises used: map_zero, Pi.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))
i : ι
x : Mᵢ i
h₁ :
  Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) x : P)
    (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (Pi.single (M := Mᵢ) i x x_1) : P)
convert! :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      ∀ (hji : j ≠ i), Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
⊢ LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)

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]

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem, map_zero, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)
x : (i : ι) → Mᵢ i
⊢ LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))

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

Premises used: Finset.sum_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)
x : (i : ι) → Mᵢ i
⊢ LE.le.{u_10} (α := P) 0 (∑ x_1 : ι, (Q x_1 : (a : Mᵢ x_1) → P) (x x_1))

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

Premises used: Finset.sum_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
simp_rw :
  (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (pi (Mᵢ := Mᵢ) Q).Anisotropic ↔
    ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
⊢ (pi (Mᵢ := Mᵢ) Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef

Tactic:
simp_rw [posDef_iff_nonneg, nonneg_pi_iff]

Premises used: QuadraticMap.nonneg_pi_iff, QuadraticMap.posDef_iff_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
mp :
  (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (pi (Mᵢ := Mᵢ) Q).Anisotropic →
    ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
mpr :
  (∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic) →
    (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (pi (Mᵢ := Mᵢ) Q).Anisotropic
⊢ (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (pi (Mᵢ := Mᵢ) Q).Anisotropic ↔
    ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
hle : ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)
ha : (pi (Mᵢ := Mᵢ) Q).Anisotropic
i : ι
⊢ (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic

Tactic:
⟨hle i, anisotropic_of_pi ha i⟩

Premises used: QuadraticMap.anisotropic_of_pi, And.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
hle : ∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)
ha : (pi (Mᵢ := Mᵢ) Q).Anisotropic
i : ι
⊢ (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic

Tactic:
exact ⟨hle i, anisotropic_of_pi ha i⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
⊢ (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (pi (Mᵢ := Mᵢ) Q).Anisotropic

Tactic:
⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ ?_⟩

Premises used: funext, And.right, And.left, And.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
mpr :
  ∀ (x : (i : ι) → Mᵢ i) (hx : Eq.{u_10 + 1} (α := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P) (0 : P))
    (i : ι), Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
⊢ (∀ (i : ι) (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (pi (Mᵢ := Mᵢ) Q).Anisotropic

Tactic:
refine ⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ ?_⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx : Eq.{u_10 + 1} (α := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P) (0 : P)
i : ι
mpr :
  ∀
    (hx :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) Finset.univ i →
          Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P))
    (i : ι), Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
rw :
  ∀ (hx : Eq.{u_10 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0) (i j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j → LE.le.{u_10} (α := P) (0 : P) ((Q j : (a : Mᵢ j) → P) (x j) : P)
⊢ Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)

Tactic:
rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx

Premises used: Finset.sum_eq_zero_iff_of_nonneg, QuadraticMap.pi_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
i : ι
⊢ Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)

Tactic:
hx _ (Finset.mem_univ _)

Premises used: Finset.mem_univ
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)
i : ι
⊢ Eq.{u_10 + 1} (α := P) ((Q i : (a : Mᵢ i) → P) (x i) : P) (0 : P)

Tactic:
exact hx _ (Finset.mem_univ _)

Premises used: Finset.mem_univ
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
P : Type u_10
inst_3 : Fintype ι
inst_4 : AddCommMonoid P
inst_5 : PartialOrder P
inst_6 : IsOrderedAddMonoid P
inst_7 : Module R P
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_10} R (Mᵢ i) P
h : ∀ (i : ι), (∀ (x : Mᵢ i), LE.le.{u_10} (α := P) (0 : P) ((Q i : (a : Mᵢ i) → P) x : P)) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx : Eq.{u_10 + 1} (α := P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i)) 0
i j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
⊢ LE.le.{u_10} (α := P) (0 : P) ((Q j : (a : Mᵢ j) → P) (x j) : P)

Tactic:
(h j).1 _

Premises used: And.left