awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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₁ = 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

Premises used: add_eq_zero_iff_of_nonneg, QuadraticMap.Anisotropic.eq_zero_iff
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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 mpr mpr₁ mpr₂ mpr₃ : x₁ = 0 ∧ x₂ = 0
⊢ (x₁, x₂) = 0

Tactic:
rwa [Prod.mk_eq_zero]

Premises used: Prod.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
h₁ : Q₁.PosDef
h₂ : Q₂.PosDef
⊢ (Q₁.prod Q₂).PosDef

Tactic:
posDef_prod_iff.mpr ⟨h₁, h₂⟩

Premises used: Iff.mpr, QuadraticMap.posDef_prod_iff, And.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
v w : M₁ × M₂
h₁ : Q₁.IsOrtho v.1 w.1
h₂ : Q₂.IsOrtho v.2 w.2
⊢ (Q₁.prod Q₂).IsOrtho v w

Tactic:
(congr_arg₂ HAdd.hAdd h₁ h₂).trans <| add_add_add_comm _ _ _ _

Premises used: HAdd.hAdd, add_add_add_comm, Eq.trans, QuadraticMap.IsOrtho, congr_arg₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ : M₁
m₂ : M₂
⊢ (Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂)

Tactic:
QuadraticMap.IsOrtho.prod (.zero_right _) (.zero_left _)

Premises used: QuadraticMap.IsOrtho.prod, QuadraticMap.IsOrtho.zero_left, QuadraticMap.IsOrtho.zero_right
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ : M₁
m₂ : M₂
⊢ (Q₁.prod Q₂).IsOrtho (0, m₂) (m₁, 0)

Tactic:
(IsOrtho.inl_inr _ _).symm

Premises used: QuadraticMap.IsOrtho.symm, QuadraticMap.IsOrtho.inl_inr
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ m₁' : M₁
⊢ (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'

Tactic:
simp [isOrtho_def]

Premises used: QuadraticMap.isOrtho_def
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₂ m₂' : M₂
⊢ (Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'

Tactic:
simp [isOrtho_def]

Premises used: QuadraticMap.isOrtho_def
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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₂
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)
⊢ 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)

Tactic:
dsimp [polar]

Premises used: QuadraticMap.polar
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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₂
⊢ 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:
abel
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
⊢ (Q₁.prod Q₂).polarBilin (R := R) (M := M₁ × M₂) (N := P) =
    LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)

Tactic:
LinearMap.ext₂ <| polar_prod _ _

Premises used: QuadraticMap.polar_prod, LinearMap.ext₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
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₂)
⊢ ((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₂))

Tactic:
dsimp [associated, associatedHom]

Premises used: QuadraticMap.associated, QuadraticMap.associatedHom
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
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₂)
⊢ 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:
rw [polarBilin_prod, smul_add]

Premises used: QuadraticMap.polarBilin_prod, smul_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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 _)
        (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:
rfl
-- 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
x : (i : ι) → Mᵢ i
⊢ Eq.{u_7 + 1} (α := P) ((pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P) (∑ i : ι, (Q i : (a : Mᵢ i) → P) (x i) : P)

Tactic:
sum_apply _ _ _

Premises used: QuadraticMap.sum_apply
-- 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 ι
inst_6 : DecidableEq ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
i : ι
m : Mᵢ i
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)
⊢ 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)

Tactic:
rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]

Premises used: QuadraticMap.pi_apply, Pi.single_eq_same, Fintype.sum_eq_single
-- 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 ι
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)
rw₁ rw₂ : Eq.{u_7 + 1} (α := P) 0 0
⊢ Eq.{u_7 + 1} (α := P) ((Q j : (a : Mᵢ j) → P) (Pi.single (M := Mᵢ) i m j) : P) (0 : P)

Tactic:
rw [Pi.single_eq_of_ne hj, 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_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 ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
Q' : (i : ι) → QuadraticMap.{u_2, u_9, u_7} R (Nᵢ i) P
e : (i : ι) → (Q i).IsometryEquiv (Q' i)
x : (i : ι) → Mᵢ i
⊢ Eq.{u_7 + 1} (α := P)
    ((QuadraticMap.pi (Mᵢ := Nᵢ) Q' : (a : (i : ι) → Nᵢ i) → P)
        (AddHom.toFun
          (LinearMap.toAddHom
            (↑(LinearEquiv.piCongrRight (φ := Mᵢ) (ψ := Nᵢ) fun (i : ι) ↦ (e i).toLinearEquiv) :
              ((i : ι) → Mᵢ i) →ₗ[R] (i : ι) → Nᵢ i))
          x) :
      P)
    ((QuadraticMap.pi (Mᵢ := Mᵢ) Q : (a : (i : ι) → Mᵢ i) → P) x : P)

Tactic:
simp only [pi_apply, LinearEquiv.piCongrRight,
      IsometryEquiv.coe_toLinearEquiv, IsometryEquiv.map_app]

Premises used: QuadraticMap.IsometryEquiv.map_app, LinearEquiv.piCongrRight, QuadraticMap.pi_apply, QuadraticMap.IsometryEquiv.coe_toLinearEquiv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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
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)
⊢ 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:
rw [pi_apply, Fintype.sum_eq_single i (fun j hij => ?_), Pi.single_eq_same]

Premises used: QuadraticMap.pi_apply, Pi.single_eq_same, Fintype.sum_eq_single
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
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)
rw₁ rw₂ : Eq.{u_7 + 1} (α := P) 0 0
⊢ 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.single_eq_of_ne hij, zero_apply]

Premises used: QuadraticMap.zero_apply, 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 ι
inst_6 : DecidableEq ι
i : ι
Q : QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
⊢ Eq (α := Isometry (M₁ := Mᵢ i) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q i) Q)
    (comp (Q₂ := pi (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q))
      (proj (Mᵢ := Mᵢ) i Q)
      (single (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q) i))
    (ofEq ⋯)

Tactic:
ext fun _ => Pi.single_eq_same _ _

Premises used: QuadraticMap.Isometry.ext, 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 ι
inst_6 : DecidableEq ι
i j : ι
h : i ≠ j
Q : QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
⊢ Eq (α := Isometry (M₁ := Mᵢ j) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q j) Q)
    (comp (Q₂ := pi (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q))
      (proj (Mᵢ := Mᵢ) i Q)
      (single (Mᵢ := Mᵢ) (Pi.single (M := fun (i : ι) ↦ QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P) i Q) j))
    (comp (Q₂ := 0) 0 (ofEq ⋯))

Tactic:
ext fun _ => Pi.single_eq_of_ne h _

Premises used: Pi.single_eq_of_ne, QuadraticMap.Isometry.ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
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 ι
Q : (i : ι) → QuadraticMap.{u_2, u_8, u_7} R (Mᵢ i) P
Q' : (i : ι) → QuadraticMap.{u_2, u_9, u_7} R (Nᵢ i) P
e : ∀ (i : ι), (Q i).Equivalent (Q' i)
⊢ (QuadraticMap.pi (Mᵢ := Mᵢ) Q).Equivalent (QuadraticMap.pi (Mᵢ := Nᵢ) Q')

Tactic:
⟨IsometryEquiv.pi fun i => Classical.choice (e i)⟩

Premises used: QuadraticMap.IsometryEquiv.pi, Classical.choice, Nonempty.intro, QuadraticMap.Equivalent
-- 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 : (pi (Mᵢ := Mᵢ) Q).Anisotropic
⊢ ∀ (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

Premises used: funext_iff, Pi.zero_apply, QuadraticMap.Anisotropic, QuadraticMap.pi_apply
-- 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_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
⊢ x = 0

Tactic:
have := h (Pi.single i x) ?_ 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)
this : Pi.single (M := Mᵢ) i x i = 0
⊢ x = 0

Tactic:
rw [Pi.single_eq_same] at this

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)
this : x = 0
⊢ x = 0

Tactic:
this