awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid 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₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ Eq.{uA + 1} (α := A)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (B₁.tmul B₂) : M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                            x₁ :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                      x₂) :
                  M₁ →ₗ[A] M₂ →ₗ[R] A) :
                (a : M₁) → M₂ →ₗ[R] A)
              y₁ :
            M₂ →ₗ[R] A) :
          (a : M₂) → A)
        y₂ :
      A)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂)) :
                                M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                            x₁ :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                      x₂) :
                  M₁ →ₗ[A] M₂ →ₗ[R] A) :
                (a : M₁) → M₂ →ₗ[R] A)
              y₁ :
            M₂ →ₗ[R] A) :
          (a : M₂) → A)
        y₂ :
      A)

Tactic:
congr_arg₂ (HSMul.hSMul) (hB₂.eq x₂ y₂) (hB₁.eq x₁ y₁)

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, LinearMap.IsSymm.eq, HSMul.hSMul, FreeAddMonoid.sumAux, congr_arg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid 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₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ Eq.{uA + 1} (α := A)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (B₁.tmul B₂) : M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                            x₁ :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                      x₂) :
                  M₁ →ₗ[A] M₂ →ₗ[R] A) :
                (a : M₁) → M₂ →ₗ[R] A)
              y₁ :
            M₂ →ₗ[R] A) :
          (a : M₂) → A)
        y₂ :
      A)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂)) :
                                M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                            x₁ :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                      x₂) :
                  M₁ →ₗ[A] M₂ →ₗ[R] A) :
                (a : M₁) → M₂ →ₗ[R] A)
              y₁ :
            M₂ →ₗ[R] A) :
          (a : M₂) → A)
        y₂ :
      A)

Tactic:
exact congr_arg₂ (HSMul.hSMul) (hB₂.eq x₂ y₂) (hB₁.eq x₁ y₁)

Premises used: LinearMap.IsSymm.eq, HSMul.hSMul, congr_arg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
B₂ : BilinForm R M₂
a : A
m₂ : M₂
a' : A
m₂' : M₂
⊢ (((BilinForm.baseChange A B₂ : (a : A ⊗[R] M₂) → A ⊗[R] M₂ →ₗ[A] A) (a ⊗ₜ[R] m₂) : A ⊗[R] M₂ →ₗ[A] A) :
        (a : A ⊗[R] M₂) → A)
      (a' ⊗ₜ[R] m₂') =
    HSMul.hSMul.{uR, uA, uA} (α := R) ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) m₂ : M₂ →ₗ[R] R) : (a : M₂) → R) m₂' : R) (a * a')

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
a :
  ∀ (x x_1 : M₂),
    Eq.{uA + 1} (α := A)
      ((((AlgebraTensorModule.curry
                    ((((AlgebraTensorModule.curry (BilinForm.baseChange A 0) : A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A) :
                            (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A)
                          1 :
                        (a : M₂) → A ⊗[R] M₂ →ₗ[A] A)
                      x) :
                  A →ₗ[A] M₂ →ₗ[R] A) :
                (a : A) → M₂ →ₗ[R] A)
              1 :
            (a : M₂) → A)
          x_1 :
        A)
      ((((AlgebraTensorModule.curry
                    ((((AlgebraTensorModule.curry 0 : A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A) :
                            (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A)
                          1 :
                        (a : M₂) → A ⊗[R] M₂ →ₗ[A] A)
                      x) :
                  A →ₗ[A] M₂ →ₗ[R] A) :
                (a : A) → M₂ →ₗ[R] A)
              1 :
            (a : M₂) → A)
          x_1 :
        A)
⊢ Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
x x_1 : M₂
⊢ Eq.{uA + 1} (α := A)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (BilinForm.baseChange A 0) : A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] A)
                    x) :
                A →ₗ[A] M₂ →ₗ[R] A) :
              (a : A) → M₂ →ₗ[R] A)
            1 :
          (a : M₂) → A)
        x_1 :
      A)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry 0 : A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] A)
                    x) :
                A →ₗ[A] M₂ →ₗ[R] A) :
              (a : A) → M₂ →ₗ[R] A)
            1 :
          (a : M₂) → A)
        x_1 :
      A)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : FaithfulSMul R A
B : BilinForm R M₂
h : B = 0
⊢ Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : FaithfulSMul R A
B : BilinForm R M₂
refine : ∀ (h : Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0), B = 0
⊢ Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0 ↔ B = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : FaithfulSMul R A
B : BilinForm R M₂
h : Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0
H :
  ∀ (m m' : M₂),
    Eq.{uR + 1} (α := R) ((((B : (a : M₂) → M₂ →ₗ[R] R) m : M₂ →ₗ[R] R) : (a : M₂) → R) m' : R)
      ((((0 : (a : M₂) → M₂ →ₗ[R] R) m : M₂ →ₗ[R] R) : (a : M₂) → R) m' : R)
⊢ B = 0

Tactic:
ext m m'
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : FaithfulSMul R A
B : BilinForm R M₂
h : Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0
m m' : M₂
⊢ Eq.{uR + 1} (α := R) ((((B : (a : M₂) → M₂ →ₗ[R] R) m : M₂ →ₗ[R] R) : (a : M₂) → R) m' : R)
    ((((0 : (a : M₂) → M₂ →ₗ[R] R) m : M₂ →ₗ[R] R) : (a : M₂) → R) m' : R)

Tactic:
simpa [← Algebra.algebraMap_eq_smul_one] using LinearMap.congr_fun₂ h (1 ⊗ₜ[R] m) (1 ⊗ₜ[R] m')

Premises used: Algebra.algebraMap_eq_smul_one, LinearMap.congr_fun₂, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
B₂ : BilinForm R M₂
hB₂ : IsSymm B₂
⊢ IsSymm (M := A ⊗[R] M₂) (BilinForm.baseChange A B₂)

Tactic:
IsSymm.tmul ⟨mul_comm⟩ hB₂

Premises used: LinearMap.BilinForm.baseChange, LinearMap.IsSymm.tmul, LinearMap.IsSymm.mk, mul_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ (((((tensorDistribEquiv R : (a : BilinForm R M₁ ⊗[R] BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂)) (B₁ ⊗ₜ[R] B₂) :
                BilinForm R (M₁ ⊗[R] M₂)) :
              (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
            (m₁ ⊗ₜ[R] m₂) :
          M₁ ⊗[R] M₂ →ₗ[R] R) :
        (a : M₁ ⊗[R] M₂) → R)
      (m₁' ⊗ₜ[R] m₂') =
    HMul.hMul (α := R) (β := R) ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) m₁ : M₁ →ₗ[R] R) : (a : M₁) → R) m₁' : R)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) m₂ : M₂ →ₗ[R] R) : (a : M₂) → R) m₂' : R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
a :
  ∀ (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂),
    Eq (α := BilinForm R (M₁ ⊗[R] M₂))
      (((((AlgebraTensorModule.curry
                      (↑(tensorDistribEquiv R) : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                    BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                  (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                B₁ :
              BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
            (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
          B₂ :
        BilinForm R (M₁ ⊗[R] M₂))
      (((((AlgebraTensorModule.curry (tensorDistrib R R) :
                    BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                  (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                B₁ :
              BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
            (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
          B₂ :
        BilinForm R (M₁ ⊗[R] M₂))
⊢ Eq (α := BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
    (↑(tensorDistribEquiv R) : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) (tensorDistrib R R)

Tactic:
ext B₁ B₂ : 3
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x : M₁
x_1 : M₂
x_2 : M₁
x_3 : M₂
⊢ Eq.{uR + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (((((AlgebraTensorModule.curry
                                                (↑(tensorDistribEquiv R) :
                                                  BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                              BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                            (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                                          B₁ :
                                        BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                      (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
                                    B₂) :
                                M₁ →ₗ[R] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R)
                            x :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
                      x_1) :
                  M₁ →ₗ[R] M₂ →ₗ[R] R) :
                (a : M₁) → M₂ →ₗ[R] R)
              x_2 :
            M₂ →ₗ[R] R) :
          (a : M₂) → R)
        x_3 :
      R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (((((AlgebraTensorModule.curry (tensorDistrib R R) :
                                              BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                            (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                                          B₁ :
                                        BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                      (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
                                    B₂) :
                                M₁ →ₗ[R] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R)
                            x :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
                      x_1) :
                  M₁ →ₗ[R] M₂ →ₗ[R] R) :
                (a : M₁) → M₂ →ₗ[R] R)
              x_2 :
            M₂ →ₗ[R] R) :
          (a : M₂) → R)
        x_3 :
      R)

Tactic:
mul_comm _ _

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, mul_comm, FreeAddMonoid.sumAux
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x : M₁
x_1 : M₂
x_2 : M₁
x_3 : M₂
⊢ Eq.{uR + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (((((AlgebraTensorModule.curry
                                                (↑(tensorDistribEquiv R) :
                                                  BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                              BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                            (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                                          B₁ :
                                        BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                      (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
                                    B₂) :
                                M₁ →ₗ[R] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R)
                            x :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
                      x_1) :
                  M₁ →ₗ[R] M₂ →ₗ[R] R) :
                (a : M₁) → M₂ →ₗ[R] R)
              x_2 :
            M₂ →ₗ[R] R) :
          (a : M₂) → R)
        x_3 :
      R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (((((AlgebraTensorModule.curry (tensorDistrib R R) :
                                              BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                            (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
                                          B₁ :
                                        BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                                      (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
                                    B₂) :
                                M₁ →ₗ[R] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R)
                            x :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[R] R) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
                      x_1) :
                  M₁ →ₗ[R] M₂ →ₗ[R] R) :
                (a : M₁) → M₂ →ₗ[R] R)
              x_2 :
            M₂ →ₗ[R] R) :
          (a : M₂) → R)
        x_3 :
      R)

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
B : BilinForm R M₁ ⊗[R] BilinForm R M₂
⊢ Eq (α := BilinForm R (M₁ ⊗[R] M₂))
    ((tensorDistribEquiv R : (a : BilinForm R M₁ ⊗[R] BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂)) B :
      BilinForm R (M₁ ⊗[R] M₂))
    ((tensorDistrib R R : (a : BilinForm R M₁ ⊗[R] BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂)) B :
      BilinForm R (M₁ ⊗[R] M₂))

Tactic:
DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B

Premises used: DFunLike.congr_fun, LinearMap.BilinForm.tensorDistribEquiv_toLinearMap
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M → N → P
H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n
H2 :
  ∀ (c : R) (m : M) (n : N), f (c • m) n = HSMul.hSMul.{u_2, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) c : R₂) (f m n)
H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂
H4 :
  ∀ (c : S) (m : M) (n : N), f m (c • n) = HSMul.hSMul.{u_4, u_9, u_9} (α := S₂) ((σ₁₂ : (a : S) → S₂) c : S₂) (f m n)
m : M
n : N
⊢ (((mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n = f m n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
M : Type u_5
N : Type u_7
Pₗ : Type u_11
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R M
inst_6 : Module S N
inst_7 : Module R Pₗ
inst_8 : Module S Pₗ
inst_9 : SMulCommClass S R Pₗ
f : M → N → Pₗ
H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n
H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = c • f m n
H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂
H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = c • f m n
m : M
n : N
⊢ (((mk₂' R S f H1 H2 H3 H4 : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) n = f m n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H :
  ∀ (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)
      ((((g : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)
⊢ f = g

Tactic:
LinearMap.ext fun m => LinearMap.ext fun n => H m n

Premises used: LinearMap.ext
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
h : f = g
x : M
y : N
⊢ Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)
    ((((g : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)

Tactic:
LinearMap.congr_fun (LinearMap.congr_fun h x) y

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
⊢ f = g ↔
    ∀ (m : M) (n : N),
      Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)
        ((((g : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)

Tactic:
⟨congr_fun₂, ext₂⟩

Premises used: LinearMap.congr_fun₂, LinearMap.ext₂, Iff.intro
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid P
inst_9 : AddCommMonoid P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R M
inst_12 : Module R M₂
inst_13 : Module S N
inst_14 : Module S N₂
inst_15 : Module R₂ P
inst_16 : Module S₂ P
inst_17 : Module R P₂
inst_18 : Module S₂ P₂
inst_19 : Module R Pₗ
inst_20 : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst_21 : AddCommGroup M'
inst_22 : AddCommGroup P'
inst_23 : Module R M'
inst_24 : Module R₂ P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂ P
inst_27 : SMulCommClass S R Pₗ
inst_28 : SMulCommClass S₂ R₂ P'
inst_29 : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
n : N
m₁ m₂ : M
⊢ (fun (n : N) (m : M) ↦ ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)) n (m₁ + m₂) =
    HAdd.hAdd (α := P)
      ((fun (n : N) (m : M) ↦ ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)) n m₁)
      ((fun (n : N) (m : M) ↦ ((((f : (a : M) → N →ₛₗ[σ₁₂] P) m : N →ₛₗ[σ₁₂] P) : (a : N) → P) n : P)) n m₂)

Tactic:
simp only [map_add, add_apply]

Premises used: LinearMap.add_apply, map_add