awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : AddCommGroup N₁
inst_5 : AddCommGroup N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : IsScalarTower R A N₁
inst_14 : Module R M₂
inst_15 : Module R N₂
inst_16 : Invertible (α := R) 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
m₁ : M₁
m₂ : M₂
⊢ Eq (α := N₁ ⊗[R] N₂)
    (((((tensorDistrib R A :
                  QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
                (a : QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂) → QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
              (Q₁ ⊗ₜ[R] Q₂) :
            QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        (m₁ ⊗ₜ[R] m₂) :
      N₁ ⊗[R] N₂)
    ((Q₁ : (a : M₁) → N₁) m₁ ⊗ₜ[R] (Q₂ : (a : M₂) → N₂) m₂ : N₁ ⊗[R] N₂)

Tactic:
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
  (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _
    (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)

Premises used: QuadraticMap.associated_eq_self_apply, Quotient.liftOn', AddCon.liftOn, Prod.mk, List.foldl, Prod.fst, QuadraticMap.associated, LinearMap.BilinMap.tensorDistrib_tmul, TensorProduct.tmul, Prod.snd, DFunLike.coe, AddCon.toQuotient, FreeAddMonoid.sumAux, Eq.trans, congr_arg₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : AddCommGroup N₁
inst_5 : AddCommGroup N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : IsScalarTower R A N₁
inst_14 : Module R M₂
inst_15 : Module R N₂
inst_16 : Invertible (α := R) 2
inst_17 : Invertible (α := A) 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
⊢ Subsingleton.{uA + 1} (Invertible (α := A) 2)

Tactic:
have : Subsingleton (Invertible (2 : A)) := inferInstance
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : AddCommGroup N₁
inst_5 : AddCommGroup N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : IsScalarTower R A N₁
inst_14 : Module R M₂
inst_15 : Module R N₂
inst_16 : Invertible (α := R) 2
inst_17 : Invertible (α := A) 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Subsingleton.{uA + 1} (Invertible (α := A) 2)
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
    (((associatedHom A : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
          (a : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) → BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
        (BilinMap.toQuadraticMap
          (BilinMap.tmul
            (((associatedHom A : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁) :
                (a : QuadraticMap A M₁ N₁) → BilinMap A M₁ N₁)
              Q₁)
            (((associatedHom R : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) :
                (a : QuadraticMap R M₂ N₂) → BilinMap R M₂ N₂)
              Q₂))) :
      BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
    (BilinMap.tmul
        (((associatedHom A : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁) :
            (a : QuadraticMap A M₁ N₁) → BilinMap A M₁ N₁)
          Q₁)
        (((associatedHom R : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂) :
            (a : QuadraticMap R M₂ N₂) → BilinMap R M₂ N₂)
          Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))

Tactic:
associated_left_inverse A
      (LinearMap.BilinMap.tmul_isSymm (QuadraticMap.associated_isSymm A Q₁)
        (QuadraticMap.associated_isSymm R Q₂))

Premises used: LinearMap.BilinMap.tmul_isSymm, QuadraticMap.associated_left_inverse, QuadraticMap.associated_isSymm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : AddCommGroup N₁
inst_5 : AddCommGroup N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : IsScalarTower R A N₁
inst_14 : Module R M₂
inst_15 : Module R N₂
inst_16 : Invertible (α := R) 2
inst_17 : Invertible (α := A) 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Subsingleton.{uA + 1} (Invertible (α := A) 2)
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
    ((associated : (a : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) → BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
        (((tensorDistrib R A :
              QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
            (a : QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂) → QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
          (Q₁ ⊗ₜ[R] Q₂)) :
      BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
    (((BilinMap.tensorDistrib R A : BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂ →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
          (a : BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂) → BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
        ((associated : (a : QuadraticMap A M₁ N₁) → BilinMap A M₁ N₁) Q₁ ⊗ₜ[R]
          (associated : (a : QuadraticMap R M₂ N₂) → BilinMap R M₂ N₂) Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))

Tactic:
convert!
    associated_left_inverse A
      (LinearMap.BilinMap.tmul_isSymm (QuadraticMap.associated_isSymm A Q₁)
        (QuadraticMap.associated_isSymm R Q₂))

Premises used: LinearMap.BilinMap.tmul_isSymm, QuadraticMap.associated_left_inverse, QuadraticMap.associated_isSymm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
inst_10 : Invertible (α := R) 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (((tensorDistrib R A : (a : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) → QuadraticForm A (M₁ ⊗[R] M₂))
            (Q₁ ⊗ₜ[R] Q₂) :
          QuadraticForm A (M₁ ⊗[R] M₂)) :
        (a : M₁ ⊗[R] M₂) → A)
      (m₁ ⊗ₜ[R] m₂) =
    HSMul.hSMul.{uR, uA, uA} (α := R) (β := A) ((Q₂ : (a : M₂) → R) m₂ : R) ((Q₁ : (a : M₁) → A) m₁ : A)

Tactic:
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
  (LinearMap.BilinForm.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <| congr_arg₂ _
    (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)

Premises used: QuadraticMap.associated_eq_self_apply, Quotient.liftOn', AddCon.liftOn, LinearMap.BilinForm.tensorDistrib_tmul, Prod.mk, List.foldl, Prod.fst, QuadraticMap.associated, HSMul.hSMul, Prod.snd, DFunLike.coe, FreeAddMonoid.sumAux, Eq.trans, congr_arg₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
inst_10 : Invertible (α := R) 2
inst_11 : Invertible (α := A) 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
rw :
  Eq (α := BilinMap A (M₁ ⊗[R] M₂) A)
    (((associated (R := A) (M := M₁ ⊗[R] M₂) (N := A) : QuadraticMap A (M₁ ⊗[R] M₂) A →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          (a : QuadraticMap A (M₁ ⊗[R] M₂) A) → BilinMap A (M₁ ⊗[R] M₂) A)
        (Q₁.tmul Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) A)
    ((((↑(LinearEquiv.congrRight₂ (AlgebraTensorModule.rid R A A)) :
              BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
            BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          (a : BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R)) → BilinForm A (M₁ ⊗[R] M₂))
        ((associated : (a : QuadraticMap A (M₁ ⊗[R] M₂) (A ⊗[R] R)) → BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R))
          (QuadraticMap.tmul.{uR, uA, uM₁, uM₂, uA, uR} (R := R) (A := A) (M₁ := M₁) (M₂ := M₂) (N₁ := A) (N₂ := R) Q₁
            Q₂)) :
      BilinForm A (M₁ ⊗[R] M₂))
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) A)
    (((associated (R := A) (M := M₁ ⊗[R] M₂) (N := A) : QuadraticMap A (M₁ ⊗[R] M₂) A →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          (a : QuadraticMap A (M₁ ⊗[R] M₂) A) → BilinMap A (M₁ ⊗[R] M₂) A)
        (Q₁.tmul Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) A)
    (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) A)

Tactic:
rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul,
    ← QuadraticMap.associated_tmul Q₁ Q₂]

Premises used: LinearMap.BilinMap.tmul, LinearMap.comp_apply, QuadraticMap.associated_tmul, LinearMap.BilinForm.tensorDistrib, LinearMap.BilinForm.tmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
inst_10 : Invertible (α := R) 2
inst_11 : Invertible (α := A) 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) A)
    (((associated (R := A) (M := M₁ ⊗[R] M₂) (N := A) : QuadraticMap A (M₁ ⊗[R] M₂) A →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          (a : QuadraticMap A (M₁ ⊗[R] M₂) A) → BilinMap A (M₁ ⊗[R] M₂) A)
        (Q₁.tmul Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) A)
    ((((↑(LinearEquiv.congrRight₂ (AlgebraTensorModule.rid R A A)) :
              BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
            BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          (a : BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R)) → BilinForm A (M₁ ⊗[R] M₂))
        ((associated : (a : QuadraticMap A (M₁ ⊗[R] M₂) (A ⊗[R] R)) → BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R))
          (QuadraticMap.tmul.{uR, uA, uM₁, uM₂, uA, uR} (R := R) (A := A) (M₁ := M₁) (M₂ := M₂) (N₁ := A) (N₂ := R) Q₁
            Q₂)) :
      BilinForm A (M₁ ⊗[R] M₂))

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
inst_10 : Invertible (α := R) 2
inst_11 : Invertible (α := A) 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
simp_rw :
  HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂)) =
    HSMul.hSMul (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
          ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
              (((associatedHom.{uA, uA, uM₁, uA} A (R := A) (M := M₁) (N := A) :
                      QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
                    (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
                  Q₁ ⊗ₜ[R]
                ((associatedHom.{uR, uR, uM₂, uR} R (R := R) (M := M₂) (N := R) :
                      QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
                    (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
                  Q₂) :
            BilinForm A (M₁ ⊗[R] M₂))))
⊢ polarBilin (R := A) (M := M₁ ⊗[R] M₂) (N := A) (Q₁.tmul Q₂) =
    HSMul.hSMul (α := A) (β := BilinMap A (M₁ ⊗[R] M₂) A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (BilinForm.tmul (polarBilin.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) Q₁)
        (polarBilin.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) Q₂))

Tactic:
simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul,
    ← smul_tmul', map_nsmul, associated_tmul]

Premises used: TensorProduct.tmul_smul, QuadraticMap.two_nsmul_associated, TensorProduct.smul_tmul', LinearMap.BilinForm.tmul, QuadraticForm.associated_tmul, map_nsmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R M₂
a : A
m₂ : M₂
⊢ (QuadraticForm.baseChange A Q : (a : A ⊗[R] M₂) → A) (a ⊗ₜ[R] m₂) =
    HSMul.hSMul.{uR, uA, uA} (α := R) ((Q : (a : M₂) → R) m₂ : R) (a * a)

Tactic:
tensorDistrib_tmul _ _ _ _

Premises used: QuadraticForm.tensorDistrib_tmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
inst_6 : Invertible (α := A) 2
Q : QuadraticForm R M₂
dsimp :
  Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (((associated (R := A) (M := A ⊗[R] M₂) (N := A) : QuadraticMap A (A ⊗[R] M₂) A →ₗ[A] BilinMap A (A ⊗[R] M₂) A) :
          (a : QuadraticMap A (A ⊗[R] M₂) A) → BilinMap A (A ⊗[R] M₂) A)
        (QuadraticForm.tmul.{uR, uA, uA, uM₂} (A := A) (M₁ := A) QuadraticMap.sq Q) :
      BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.baseChange A
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q) :
      BilinForm A (A ⊗[R] M₂))
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (((associated (R := A) (M := A ⊗[R] M₂) (N := A) : QuadraticMap A (A ⊗[R] M₂) A →ₗ[A] BilinMap A (A ⊗[R] M₂) A) :
          (a : QuadraticMap A (A ⊗[R] M₂) A) → BilinMap A (A ⊗[R] M₂) A)
        (QuadraticForm.baseChange A Q) :
      BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.baseChange A
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q) :
      BilinForm A (A ⊗[R] M₂))

Tactic:
dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]

Premises used: LinearMap.baseChange, QuadraticForm.baseChange
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
inst_6 : Invertible (α := A) 2
Q : QuadraticForm R M₂
rw :
  Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.tmul (LinearMap.mul A A)
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q))
    (BilinForm.baseChange A
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q))
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (((associated (R := A) (M := A ⊗[R] M₂) (N := A) : QuadraticMap A (A ⊗[R] M₂) A →ₗ[A] BilinMap A (A ⊗[R] M₂) A) :
          (a : QuadraticMap A (A ⊗[R] M₂) A) → BilinMap A (A ⊗[R] M₂) A)
        (QuadraticForm.tmul.{uR, uA, uA, uM₂} (A := A) (M₁ := A) QuadraticMap.sq Q) :
      BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.baseChange A
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q) :
      BilinForm A (A ⊗[R] M₂))

Tactic:
rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]

Premises used: QuadraticMap.sq, QuadraticMap.associated_sq, QuadraticForm.associated_tmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
inst_6 : Invertible (α := A) 2
Q : QuadraticForm R M₂
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.tmul (LinearMap.mul A A)
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q))
    (BilinForm.baseChange A
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q))

Tactic:
rfl

Premises used: LinearMap.BilinForm.baseChange, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
inst_6 : Invertible (α := A) 2
Q : QuadraticForm R M₂
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.tmul (LinearMap.mul A A)
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q))
    (BilinForm.baseChange A
      (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
          (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
        Q))

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
rw :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
rw₁ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
rw₂ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
rw₃ :
  HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
    (Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m))
rw₄ :
  HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
    HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
rw₅ rw₆ :
  HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
    HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)

Tactic:
rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]

Premises used: QuadraticMap.map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
⊢ ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)

Tactic:
replace h (a m) : Q₁ (a ⊗ₜ m) = Q₂ (a ⊗ₜ m) := by
    rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
H : ∀ (x : A ⊗[R] M₂), Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
⊢ Q₁ = Q₂

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x : A
y : M₂
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x ⊗ₜ[R] y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x ⊗ₜ[R] y) : N₁)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) 0 : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) 0 : N₁)

Tactic:
simp