awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
n : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
rw :
  Eq (α := ↥M ⊗[R] ↥⊥)
    ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
rw₁ : Eq (α := ↥M ⊗[R] ↥⊥) ((x • n) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
rw₂ : Eq (α := ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] HSMul.hSMul (β := ↥⊥) x 1) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x)
rw₃ :
  Eq (α := ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] HMul.hMul (α := ↥⊥) (β := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥⊥) (1 : ↥⊥))
    (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x)
rw₄ rw₅ :
  Eq (α := ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)

Tactic:
rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]

Premises used: TensorProduct.smul_tmul, Submodule.rTensorOne'_tmul, Algebra.smul_def, mul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.rTensorOne : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y) = y • m

Tactic:
M.rTensorOne'_tmul y m

Premises used: Submodule.rTensorOne'_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
m : ↥M
⊢ (M.rTensorOne : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] 1) = m

Tactic:
M.rTensorOne'_tmul_one m

Premises used: Submodule.rTensorOne'_tmul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
m : ↥M
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne.symm : (a : ↥M) → ↥M ⊗[R] ↥⊥) m : ↥M ⊗[R] ↥⊥) (m ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ M.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) =
    M.subtype ∘ₗ (↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M)

Tactic:
TensorProduct.ext' fun _ _ ↦ rfl

Premises used: TensorProduct.ext', rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne

Tactic:
LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun m r ↦ ?_

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
refine :
  ∀ (m : ↥M) (r : ↥⊥),
    Eq (α := ↥M)
      (((↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) :
        ↥M)
      (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)
⊢ TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne

Tactic:
refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun m r ↦ ?_

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
obtain :
  ∀ (x : R) (h : (algebraMap R S : (a : R) → S) x = (↑r : S)),
    Eq (α := ↥M)
      (((↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) :
        ↥M)
      (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)
⊢ Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)
    (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Premises used: Algebra.mem_bot, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R S : (a : R) → S) x = (↑r : S)
⊢ (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r

Tactic:
replace h : algebraMap R _ x = r := Subtype.val_injective h
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
rw :
  Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M)
        (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x) :
      ↥M)
    (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x) : ↥M)
⊢ Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)
    (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)

Tactic:
rw [← h]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
⊢ Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M)
        (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x) :
      ↥M)
    (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x) : ↥M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne

Tactic:
LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun r m ↦ ?_

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
refine :
  ∀ (r : ↥⊥) (m : ↥M),
    Eq (α := ↥M)
      (((↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) :
        ↥M)
      (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)
⊢ TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne

Tactic:
refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun r m ↦ ?_

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
obtain :
  ∀ (x : R) (h : (algebraMap R S : (a : R) → S) x = (↑r : S)),
    Eq (α := ↥M)
      (((↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) :
        ↥M)
      (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)
⊢ Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)
    (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Premises used: Algebra.mem_bot, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R S : (a : R) → S) x = (↑r : S)
⊢ (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r

Tactic:
replace h : algebraMap R _ x = r := Subtype.val_injective h
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
rw :
  Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M)
        ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] m) :
      ↥M)
    (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] m) : ↥M)
⊢ Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)
    (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)

Tactic:
rw [← h]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
⊢ Eq (α := ↥M)
    (((↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M)
        ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] m) :
      ↥M)
    (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] m) : ↥M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
inst_3 : DecidableEq ι
m : ι → ↥M
h :
  ∀ (a : ι) (x : ↥N),
    Eq (α := S) ((mulLeftMap N m ∘ₗ Finsupp.lsingle a : (a : ↥N) → S) x : S)
      (((M.mulMap N ∘ₗ
                LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ
                  (↑(LinearEquiv.symm (TensorProduct.finsuppScalarLeft R (↥N) ι)) :
                    (ι →₀ ↥N) →ₗ[R] (ι →₀ R) ⊗[R] ↥N)) ∘ₗ
              Finsupp.lsingle a :
            (a : ↥N) → S)
          x :
        S)
⊢ mulLeftMap N m =
    M.mulMap N ∘ₗ
      LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.finsuppScalarLeft R (↥N) ι)) : (ι →₀ ↥N) →ₗ[R] (ι →₀ R) ⊗[R] ↥N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
inst_3 : DecidableEq ι
m : ι → ↥M
a : ι
x : ↥N
⊢ Eq (α := S) ((mulLeftMap N m ∘ₗ Finsupp.lsingle a : (a : ↥N) → S) x : S)
    (((M.mulMap N ∘ₗ
              LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ
                (↑(LinearEquiv.symm (TensorProduct.finsuppScalarLeft R (↥N) ι)) : (ι →₀ ↥N) →ₗ[R] (ι →₀ R) ⊗[R] ↥N)) ∘ₗ
            Finsupp.lsingle a :
          (a : ↥N) → S)
        x :
      S)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
inst_3 : DecidableEq ι
n : ι → ↥N
h :
  ∀ (a : ι) (x : ↥M),
    Eq (α := S) ((M.mulRightMap n ∘ₗ Finsupp.lsingle a : (a : ↥M) → S) x : S)
      (((M.mulMap N ∘ₗ
                LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
                  (↑(LinearEquiv.symm (TensorProduct.finsuppScalarRight R R (↥M) ι)) :
                    (ι →₀ ↥M) →ₗ[R] ↥M ⊗[R] (ι →₀ R))) ∘ₗ
              Finsupp.lsingle a :
            (a : ↥M) → S)
          x :
        S)
⊢ M.mulRightMap n =
    M.mulMap N ∘ₗ
      LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.finsuppScalarRight R R (↥M) ι)) : (ι →₀ ↥M) →ₗ[R] ↥M ⊗[R] (ι →₀ R))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
inst_3 : DecidableEq ι
n : ι → ↥N
a : ι
x : ↥M
⊢ Eq (α := S) ((M.mulRightMap n ∘ₗ Finsupp.lsingle a : (a : ↥M) → S) x : S)
    (((M.mulMap N ∘ₗ
              LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
                (↑(LinearEquiv.symm (TensorProduct.finsuppScalarRight R R (↥M) ι)) :
                  (ι →₀ ↥M) →ₗ[R] ↥M ⊗[R] (ι →₀ R))) ∘ₗ
            Finsupp.lsingle a :
          (a : ↥M) → S)
        x :
      S)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
⊢ N.mulMap M = M.mulMap N ∘ₗ (↑(TensorProduct.comm R ↥N ↥M) : ↥N ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥N)

Tactic:
mulMap_comm_of_commute M N fun _ _ ↦ mul_comm _ _

Premises used: Submodule.mulMap_comm_of_commute, mul_comm, Subtype.val
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
a : A
x : M ⊗[R] N
⊢ a • x = (rTensor N ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) : (a : M ⊗[R] N) → M ⊗[R] N) x

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Quot.map, Quotient.map', TensorProduct, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
f : M ⊗[R] N →ₗ[A] P
⊢ Eq (α := M →ₗ[R] N →ₗ[R] P)
    ((↑R :
        {S : Type uA} →
          {M : Type uM} →
            {M₂ : Type (max uP uN)} →
              [inst : Semiring R] →
                [inst_13 : Semiring S] →
                  [inst_14 : AddCommMonoid M] →
                    [inst_15 : AddCommMonoid M₂] →
                      [inst_16 : Module R M] →
                        [inst_17 : Module R M₂] →
                          [inst_18 : Module S M] →
                            [inst_19 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (curry f : M →ₗ[A] N →ₗ[R] P))
    (TensorProduct.curry
      ((↑R :
          {S : Type uA} →
            {M : Type (max uM uN)} →
              {M₂ : Type uP} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f))

Tactic:
rfl

Premises used: LinearMap.restrictScalars, TensorProduct.curry, LinearMap.compr₂ₛₗ, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
⊢ Function.Injective (α := M ⊗[R] N →ₗ[A] P) (β := M →ₗ[A] N →ₗ[R] P)
    (curry : (f : M ⊗[R] N →ₗ[A] P) → M →ₗ[A] N →ₗ[R] P)

Tactic:
fun _ _ h =>
  LinearMap.restrictScalars_injective R <|
    curry_injective <| (congr_arg (LinearMap.restrictScalars R) h :)

Premises used: LinearMap.restrictScalars, TensorProduct.curry_injective, congr_arg, Function.Injective, LinearMap.restrictScalars_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
g h : M ⊗[R] N →ₗ[A] P
H :
  ∀ (x : M) (y : N),
    Eq.{uP + 1} (α := P) ((g : (a : M ⊗[R] N) → P) (x ⊗ₜ[R] y) : P) ((h : (a : M ⊗[R] N) → P) (x ⊗ₜ[R] y) : P)
⊢ g = h

Tactic:
curry_injective <| LinearMap.ext₂ H

Premises used: LinearMap.ext₂, TensorProduct.AlgebraTensorModule.curry_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : Module A P'
inst_20 : Module B P'
inst_21 : IsScalarTower R A P'
inst_22 : IsScalarTower R B P'
inst_23 : SMulCommClass A B P'
inst_24 : AddCommMonoid Q'
inst_25 : Module R Q'
f : M →ₗ[A] N →ₗ[R] P
c : A
x : M
y : N
⊢ Eq.{uP + 1} (α := P)
    ((TensorProduct.lift
              ((↑R :
                  {S : Type uA} →
                    {M : Type uM} →
                      {M₂ : Type (max uN uP)} →
                        [inst : Semiring R] →
                          [inst_26 : Semiring S] →
                            [inst_27 : AddCommMonoid M] →
                              [inst_28 : AddCommMonoid M₂] →
                                [inst_29 : Module R M] →
                                  [inst_30 : Module R M₂] →
                                    [inst_31 : Module S M] →
                                      [inst_32 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                f) ∘ₗ
            (Algebra.lsmul R R (M ⊗[R] N) : (a : A) → Module.End R (M ⊗[R] N)) c :
          (a : M ⊗[R] N) → P)
        (x ⊗ₜ[R] y) :
      P)
    (((Algebra.lsmul R R P : (a : A) → Module.End R P) c ∘ₗ
            TensorProduct.lift
              ((↑R :
                  {S : Type uA} →
                    {M : Type uM} →
                      {M₂ : Type (max uN uP)} →
                        [inst : Semiring R] →
                          [inst_26 : Semiring S] →
                            [inst_27 : AddCommMonoid M] →
                              [inst_28 : AddCommMonoid M₂] →
                                [inst_29 : Module R M] →
                                  [inst_30 : Module R M₂] →
                                    [inst_31 : Module S M] →
                                      [inst_32 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                f) :
          (a : M ⊗[R] N) → P)
        (x ⊗ₜ[R] y) :
      P)

Tactic:
simp only [comp_apply, Algebra.lsmul_coe, smul_tmul', lift.tmul,
              coe_restrictScalars, f.map_smul, smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.coe_restrictScalars, LinearMap.comp_apply, TensorProduct.lift.tmul, TensorProduct.smul_tmul', LinearMap.map_smul, Algebra.lsmul_coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
f : M →ₗ[A] N →ₗ[R] P
a : M ⊗[R] N
⊢ Eq.{uP + 1} (α := P) (((lift f : M ⊗[R] N →ₗ[A] P) : (a : M ⊗[R] N) → P) a : P)
    ((TensorProduct.lift
            ((↑R :
                {S : Type uA} →
                  {M : Type uM} →
                    {M₂ : Type (max uP uN)} →
                      [inst : Semiring R] →
                        [inst_13 : Semiring S] →
                          [inst_14 : AddCommMonoid M] →
                            [inst_15 : AddCommMonoid M₂] →
                              [inst_16 : Module R M] →
                                [inst_17 : Module R M₂] →
                                  [inst_18 : Module S M] →
                                    [inst_19 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              f) :
          (a : M ⊗[R] N) → P)
        a :
      P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
f : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ Eq.{uP + 1} (α := P) (((lift f : M ⊗[R] N →ₗ[A] P) : (a : M ⊗[R] N) → P) (x ⊗ₜ[R] y) : P)
    ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : Module A P'
inst_20 : Module B P'
inst_21 : IsScalarTower R A P'
inst_22 : IsScalarTower R B P'
inst_23 : SMulCommClass A B P'
inst_24 : AddCommMonoid Q'
inst_25 : Module R Q'
inst_26 : Module B P
inst_27 : IsScalarTower R B P
inst_28 : SMulCommClass A B P
x_1 x_2 : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ Eq.{uP + 1} (α := P) (((lift (x_1 + x_2) : M ⊗[R] N →ₗ[A] P) : (a : M ⊗[R] N) → P) (x ⊗ₜ[R] y) : P)
    ((HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P) (β := M ⊗[R] N →ₗ[A] P) (lift x_1 : M ⊗[R] N →ₗ[A] P)
            (lift x_2 : M ⊗[R] N →ₗ[A] P) :
          (a : M ⊗[R] N) → P)
        (x ⊗ₜ[R] y) :
      P)

Tactic:
simp only [lift_tmul, add_apply]

Premises used: LinearMap.add_apply, TensorProduct.AlgebraTensorModule.lift_tmul