awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have 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)
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have 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)
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have 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)
Tactic: subst hji
Cleared hypotheses: i, x, hx, hji
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) j x j) : P) (0 : P)
have pos₁ : Eq.{u_7 + 1} (α := P) 0 0
Tactic: rw [Pi.single_eq_same, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have neg : Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) 0 : P) (0 : P)
Tactic: rw [Pi.single_eq_of_ne hji, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have neg₁ : Eq.{u_7 + 1} (α := P) 0 0
Tactic: rw [Pi.single_eq_of_ne hji, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ x = 0
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ x = 0
have refine_2 : ∀ (this : Pi.single (M := Mᵢ) i x i = 0), 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ x = 0
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ x = 0
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ x = 0
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (∀ (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)
have 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)
Tactic: simp_rw [pi, sum_apply, comp_apply, LinearMap.proj_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ (∀ (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)
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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 : P) ((Q i : (a : Mᵢ i) → P) x : P)
have 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)
Tactic: convert! h (Pi.single i x) using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ 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)
have 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)
Tactic: rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hji => ?_, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have rw : Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) 0 : P) (0 : P)
Tactic: rw [Pi.single_eq_of_ne hji, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ Eq.{u_10 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i x j) : P) (0 : P)
have rw₁ : Eq.{u_10 + 1} (α := P) 0 0
Tactic: rw [Pi.single_eq_of_ne hji, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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 : P) ((Q i : (a : Mᵢ i) → P) x : P)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (pi (Mᵢ := Mᵢ) Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef
have 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
Tactic: simp_rw [posDef_iff_nonneg, nonneg_pi_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
have 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)
Tactic: refine ⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ ?_⟩