awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
mp :
  (∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)) →
    (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)) ↔
    (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
have mpr : ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
    ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) →
  ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
⊢ (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
    ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
have mp : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
mp : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
⊢ (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
    ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
have mp₁ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef
have simp_rw : ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
    (Q₁.prod Q₂).Anisotropic ↔
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
Tactic: simp_rw [posDef_iff_nonneg, nonneg_prod_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
have mp : ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
    (Q₁.prod Q₂).Anisotropic →
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
mp :
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic →
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
have mpr : ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic →
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
    (Q₁.prod Q₂).Anisotropic
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (hypothesis)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
have ha₁ : Q₁.Anisotropic
Tactic: obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (hypothesis)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₁ : Q₁.Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
have ha₂ : Q₂.Anisotropic
Tactic: obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₂ : Q₂.Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
    (Q₁.prod Q₂).Anisotropic
have mpr : (Q₁.prod Q₂).Anisotropic
Tactic: refine ⟨⟨hle₁, hle₂⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (hypothesis)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x₁ : P) ((Q₂ : (a : M₂) → P) x₂ : P) = 0
⊢ (x₁, x₂) = 0
have hx₁ : x₁ = 0 ∧ x₂ = 0
Tactic: rw [add_eq_zero_iff_of_nonneg (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ polar (⇑(Q₁.prod Q₂) : (a : M₁ × M₂) → P) x y =
    HAdd.hAdd (α := P) (polar (⇑Q₁ : (a : M₁) → P) x.1 y.1) (polar (⇑Q₂ : (a : M₂) → P) x.2 y.2)
have dsimp : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) (x.1 + y.1) : P) ((Q₂ : (a : M₂) → P) (x.2 + y.2) : P) -
      HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x.1 : P) ((Q₂ : (a : M₂) → P) x.2 : P) -
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) y.1 : P) ((Q₂ : (a : M₂) → P) y.2 : P) =
  HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q₁ : (a : M₁) → P) (x.1 + y.1) : P) ((Q₁ : (a : M₁) → P) x.1 : P))
      ((Q₁ : (a : M₁) → P) y.1 : P) +
    HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q₂ : (a : M₂) → P) (x.2 + y.2) : P) ((Q₂ : (a : M₂) → P) x.2 : P))
      ((Q₂ : (a : M₂) → P) y.2 : P)
Tactic: dsimp [polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((associated (R := R) (M := M₁ × M₂) (N := P) : QuadraticMap R (M₁ × M₂) P →ₗ[R] LinearMap.BilinMap R (M₁ × M₂) P) :
        (a : QuadraticMap R (M₁ × M₂) P) → LinearMap.BilinMap R (M₁ × M₂) P)
      (Q₁.prod Q₂) =
    HAdd.hAdd (α := M₁ × M₂ →ₗ[R] M₁ × M₂ →ₗ[R] P)
      (LinearMap.compl₁₂ ((associated : (a : QuadraticMap R M₁ P) → LinearMap.BilinMap R M₁ P) Q₁)
        (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂))
      (LinearMap.compl₁₂ ((associated : (a : QuadraticMap R M₂ P) → LinearMap.BilinMap R M₂ P) Q₂)
        (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂))
have dsimp : HSMul.hSMul (α := Module.End R P) (β := LinearMap.BilinMap R (M₁ × M₂) P)
    (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
    ((Q₁.prod Q₂).polarBilin (R := R) (M := M₁ × M₂) (N := P) : LinearMap.BilinMap R (M₁ × M₂) P) =
  LinearMap.compl₁₂
      (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) Q₁.polarBilin)
      (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
    LinearMap.compl₁₂
      (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) Q₂.polarBilin)
      (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
Tactic: dsimp [associated, associatedHom]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ HSMul.hSMul (α := Module.End R P) (β := LinearMap.BilinMap R (M₁ × M₂) P)
      (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      ((Q₁.prod Q₂).polarBilin (R := R) (M := M₁ × M₂) (N := P) : LinearMap.BilinMap R (M₁ × M₂) P) =
    LinearMap.compl₁₂
        (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
          Q₁.polarBilin)
        (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂
        (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
          Q₂.polarBilin)
        (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
have rw : HSMul.hSMul (α := Module.End R P) (β := LinearMap.BilinMap R (M₁ × M₂) P)
      (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) :
        M₁ × M₂ →ₗ[R] M₁ × M₂ →ₗ[R] P) +
    HSMul.hSMul (α := Module.End R P) (β := LinearMap.BilinMap R (M₁ × M₂) P)
      (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂) :
        M₁ × M₂ →ₗ[R] M₁ × M₂ →ₗ[R] P) =
  LinearMap.compl₁₂
      (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) Q₁.polarBilin)
      (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
    LinearMap.compl₁₂
      (HSMul.hSMul (α := Module.End R P) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) Q₂.polarBilin)
      (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
Tactic: rw [polarBilin_prod, smul_add]
-- 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 ι
inst_6 : DecidableEq ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ Eq.{u_7 + 1} (α := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) (Pi.single (M := Mᵢ) i m) : P)
    ((Q i : (a : Mᵢ i) → P) m : P)
have rw : ∀ (j : ι) (hj : j ≠ i), Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i m j) : P) (0 : P)
Tactic: rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]
-- 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 ι
inst_6 : DecidableEq ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i m j) : P) (0 : P)
have rw : Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) 0 : P) (0 : P)
Tactic: rw [Pi.single_eq_of_ne hj, 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 ι
inst_6 : DecidableEq ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
rw : 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 m j) : P) (0 : P)
have rw₁ : Eq.{u_7 + 1} (α := P) 0 0
Tactic: rw [Pi.single_eq_of_ne hj, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)
inst_3 : AddCommMonoid P
inst_4 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_5 : (i : ι) → Module.{u_2, u_9} R (Nᵢ i)
inst_6 : Module R P
inst_7 : Fintype ι
inst_8 : DecidableEq ι
i : ι
Q : QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
m : (i : ι) → Mᵢ i
⊢ Eq.{u_7 + 1} (α := P)
    ((Q : (a : Mᵢ i) → P) (AddHom.toFun (LinearMap.toAddHom (R := R) (LinearMap.proj (φ := Mᵢ) i)) m) : P)
    ((pi (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q) :
          (a : (i : ι) → Mᵢ i) → P)
        m :
      P)
have dsimp : Eq.{u_7 + 1} (α := P) ((Q : (a : Mᵢ i) → P) (m i) : P)
  ((pi (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q) :
        (a : (i : ι) → Mᵢ i) → P)
      m :
    P)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)
inst_3 : AddCommMonoid P
inst_4 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_5 : (i : ι) → Module.{u_2, u_9} R (Nᵢ i)
inst_6 : Module R P
inst_7 : Fintype ι
inst_8 : DecidableEq ι
i : ι
Q : QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
m : (i : ι) → Mᵢ i
⊢ Eq.{u_7 + 1} (α := P) ((Q : (a : Mᵢ i) → P) (m i) : P)
    ((pi (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q) :
          (a : (i : ι) → Mᵢ i) → P)
        m :
      P)
have rw : ∀ (j : ι) (hij : j ≠ i),
  Eq.{u_7 + 1} (α := P)
    (((Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q j :
            QuadraticMap.{u_2, u_8, u_7} R (Mᵢ j) P) :
          (a : Mᵢ j) → P)
        (m j) :
      P)
    (0 : P)
Tactic: rw [pi_apply, Fintype.sum_eq_single i (fun j hij => ?_), 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_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)
inst_3 : AddCommMonoid P
inst_4 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_5 : (i : ι) → Module.{u_2, u_9} R (Nᵢ i)
inst_6 : Module R P
inst_7 : Fintype ι
inst_8 : DecidableEq ι
i : ι
Q : QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
m : (i : ι) → Mᵢ i
j : ι
hij : j ≠ i
⊢ Eq.{u_7 + 1} (α := P)
    (((Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q j :
            QuadraticMap.{u_2, u_8, u_7} R (Mᵢ j) P) :
          (a : Mᵢ j) → P)
        (m j) :
      P)
    (0 : P)
have rw : Eq.{u_7 + 1} (α := P) ((0 : (a : Mᵢ j) → P) (m j) : P) (0 : P)
Tactic: rw [Pi.single_eq_of_ne hij, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)
inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)
inst_3 : AddCommMonoid P
inst_4 : (i : ι) → Module.{u_2, u_8} R (Mᵢ i)
inst_5 : (i : ι) → Module.{u_2, u_9} R (Nᵢ i)
inst_6 : Module R P
inst_7 : Fintype ι
inst_8 : DecidableEq ι
i : ι
Q : QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
m : (i : ι) → Mᵢ i
j : ι
hij : j ≠ i
rw : Eq.{u_7 + 1} (α := P) ((0 : (a : Mᵢ j) → P) (m j) : P) (0 : P)
⊢ Eq.{u_7 + 1} (α := P)
    (((Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q j :
            QuadraticMap.{u_2, u_8, u_7} R (Mᵢ j) P) :
          (a : Mᵢ j) → P)
        (m j) :
      P)
    (0 : P)
have rw₁ : Eq.{u_7 + 1} (α := P) 0 0
Tactic: rw [Pi.single_eq_of_ne hij, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (hypothesis)
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 : (pi (Mᵢ := Mᵢ) Q).Anisotropic
⊢ ∀ (i : ι), (Q i).Anisotropic
have 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
Tactic: simp_rw [Anisotropic, pi_apply, funext_iff, Pi.zero_apply] at h
Cleared hypotheses: h
-- 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_2 : ∀ (this : Pi.single (M := Mᵢ) i x i = 0), x = 0
Tactic: have := h (Pi.single i x) ?_ 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)
refine_2 : ∀ (this : Pi.single (M := Mᵢ) i x i = 0), x = 0
⊢ 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: have := h (Pi.single i x) ?_ 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)
⊢ Eq.{u_7 + 1} (α := P) (∑ i_1 : ι, (Q i_1 : (a : Mᵢ i_1) → P) (Pi.single (M := Mᵢ) i x i_1)) 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: apply Finset.sum_eq_zero