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
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
n : ↥N
m : ↥M
simp_rw : (↑n : S) * (↑m : S) = (↑m : S) * (↑n : S)
⊢ Eq (α := S) ((N.mulMap M : (a : ↥N ⊗[R] ↥M) → S) (n ⊗ₜ[R] m) : S)
    ((M.mulMap N ∘ₗ (↑(TensorProduct.comm R ↥N ↥M) : ↥N ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥N) : (a : ↥N ⊗[R] ↥M) → S) (n ⊗ₜ[R] m) :
      S)

Tactic:
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul, mulMap_tmul]

Premises used: Submodule.mulMap_tmul, LinearMap.comp_apply, TensorProduct.comm_tmul, LinearEquiv.coe_coe
-- 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
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
n : ↥N
m : ↥M
⊢ (↑n : S) * (↑m : S) = (↑m : S) * (↑n : S)

Tactic:
(hc m n).symm

Premises used: SemiconjBy, Commute, Commute.symm
-- 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
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
n : ↥N
m : ↥M
⊢ (↑n : S) * (↑m : S) = (↑m : S) * (↑n : S)

Tactic:
exact (hc m n).symm

Premises used: Commute.symm
-- 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 M' : Submodule R S
hM : M' ≤ M
⊢ M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion hM) = M'.mulMap N

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 N N' : Submodule R S
hN : N' ≤ N
⊢ M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion hN) = M.mulMap N'

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 N M' N' : Submodule R S
hM : M' ≤ M
hN : N' ≤ N
⊢ M.mulMap N ∘ₗ TensorProduct.map (inclusion hM) (inclusion hN) = M'.mulMap N'

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 N : Submodule R S
⊢ M.mulMap N = LinearMap.mul' R S ∘ₗ TensorProduct.mapIncl M N

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 N : Submodule R S
⊢ (M.mulMap N).range = M * N

Tactic:
le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)

Premises used: Iff.mpr, Subtype.mk, le_antisymm, Exists.intro, Submodule.mul_le, TensorProduct.tmul, 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 N : Submodule R S
refine : (M.mulMap N).range ≤ M * N
⊢ (M.mulMap N).range = M * N

Tactic:
refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, 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 N : Submodule R S
zero : 0 ∈ M * N
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) 0 : S)

Tactic:
rw [map_zero]

Premises used: map_zero
-- 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
⊢ 0 ∈ M * N

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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
⊢ 0 ∈ M * N

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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
a : ↥M
b : ↥N
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) (a ⊗ₜ[R] b) : S)

Tactic:
mul_mem_mul a.2 b.2

Premises used: Submodule.mul_mem_mul, Quotient.liftOn', Set.Mem, AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, 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 N : Submodule R S
a : ↥M
b : ↥N
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) (a ⊗ₜ[R] b) : S)

Tactic:
exact mul_mem_mul a.2 b.2

Premises used: Submodule.mul_mem_mul, 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 N : Submodule R S
a b : ↥M ⊗[R] ↥N
ha : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S)
hb : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S)
add :
  HAdd.hAdd (α := S) (β := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S) ∈
    M * N
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) (a + b) : S)

Tactic:
rw [map_add]

Premises used: map_add
-- 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
a b : ↥M ⊗[R] ↥N
ha : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S)
hb : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S)
⊢ HAdd.hAdd (α := S) (β := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S) ∈
    M * N

Tactic:
add_mem ha hb

Premises used: AddMemClass.add_mem
-- 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
a b : ↥M ⊗[R] ↥N
ha : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S)
hb : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S)
⊢ HAdd.hAdd (α := S) (β := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S) ∈
    M * N

Tactic:
exact add_mem ha hb

Premises used: AddMemClass.add_mem
-- 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
x : ↥M ⊗[R] ↥N
zero : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) 0 : S)
tmul : ∀ (a : ↥M) (b : ↥N), Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) (a ⊗ₜ[R] b) : S)
add :
  ∀ (a b : ↥M ⊗[R] ↥N) (ha : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) a : S))
    (hb : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) b : S)),
    Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) (a + b) : S)
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S)

Tactic:
induction x with
  | zero => rw [map_zero]; exact zero_mem _
  | tmul a b => exact mul_mem_mul a.2 b.2
  | add a b ha hb => rw [map_add]; exact add_mem ha hb

Premises used: map_zero, map_add, Submodule.zero, ZeroMemClass.zero_mem, Submodule.add
-- 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
m : ↥M
n : ↥N
⊢ (↑((M.mulMap' N : (a : ↥M ⊗[R] ↥N) → ↥(M * N)) (m ⊗ₜ[R] n)) : S) = (↑m : S) * (↑n : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, 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 N : Submodule R S
simp_rw :
  Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N))
    (⇑((↑(LinearEquiv.ofEq (M.mulMap N).range (M * N) ⋯) : ↥(M.mulMap N).range →ₗ[R] ↥(M * N)) ∘ₗ
          (M.mulMap N).rangeRestrict) :
      (a : ↥M ⊗[R] ↥N) → ↥(M * N))
simp_rw₁ :
  Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N))
    (Function.comp (β := ↥(M.mulMap N).range)
      (⇑(↑(LinearEquiv.ofEq (M.mulMap N).range (M * N) ⋯) : ↥(M.mulMap N).range →ₗ[R] ↥(M * N)) :
        (a : ↥(M.mulMap N).range) → ↥(M * N))
      (⇑(M.mulMap N).rangeRestrict : (a : ↥M ⊗[R] ↥N) → ↥(M.mulMap N).range))
simp_rw₂ :
  Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N))
    (Function.comp (β := ↥(M.mulMap N).range)
      (⇑(LinearEquiv.ofEq (M.mulMap N).range (M * N) ⋯) : (a : ↥(M.mulMap N).range) → ↥(M * N))
      (⇑(M.mulMap N).rangeRestrict : (a : ↥M ⊗[R] ↥N) → ↥(M.mulMap N).range))
simp_rw₃ :
  Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M.mulMap N).range)
    (⇑(M.mulMap N).rangeRestrict : (a : ↥M ⊗[R] ↥N) → ↥(M.mulMap N).range)
⊢ Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N)) (⇑(M.mulMap' N) : (a : ↥M ⊗[R] ↥N) → ↥(M * N))

Tactic:
simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]

Premises used: LinearMap.coe_comp, EquivLike.comp_surjective, LinearMap.surjective_rangeRestrict, Submodule.mulMap', LinearEquiv.coe_coe
-- 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
rw : LinearMap.range (M := ↥1 ⊗[R] ↥N) (mulMap 1 N) = N
rw₁ : 1 * N = N
rw₂ rw₃ : N = N
⊢ LinearMap.range (M := ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N)
      (mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) N) =
    N

Tactic:
rw [Algebra.toSubmodule_bot, mulMap_range, one_mul]

Premises used: Algebra.toSubmodule_bot, Submodule.mulMap_range, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
y : R
n : ↥N
simp_rw :
  ((mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) N :
          ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N →ₗ[R] S) :
        (a : ↥⊥ ⊗[R] ↥N) → S)
      ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑n : S)
⊢ (↑((N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y ⊗ₜ[R] n)) : S) = (↑(y • n) : S)

Tactic:
simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]

Premises used: LinearEquiv.coe_ofEq_apply, LinearMap.coe_comp, SetLike.val_smul, Algebra.smul_def, Function.comp_apply, LinearMap.codRestrict_apply, Submodule.lTensorOne', LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) N :
          ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N →ₗ[R] S) :
        (a : ↥⊥ ⊗[R] ↥N) → S)
      ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑n : S)

Tactic:
mulMap_tmul _ N _ _

Premises used: Submodule.mulMap_tmul, Set.Mem, setOf, Set.range, Subsemiring.copy, AlgHom.range, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) N :
          ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N →ₗ[R] S) :
        (a : ↥⊥ ⊗[R] ↥N) → S)
      ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑n : S)

Tactic:
exact mulMap_tmul _ N _ _

Premises used: Submodule.mulMap_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
N : Submodule R S
n : ↥N
⊢ (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (1 ⊗ₜ[R] n) = n

Tactic:
simpa using lTensorOne'_tmul 1 n

Premises used: Submodule.lTensorOne'_tmul, OfNat.ofNat
-- 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
h :
  ∀ (x : ↥N),
    Eq.{v + 1} (α := S)
      (↑((N.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N : (a : ↥⊥) → ↥N →ₗ[R] ↥⊥ ⊗[R] ↥N) 1 : (a : ↥N) → ↥N) x) : S)
      (↑((LinearMap.id : (a : ↥N) → ↥N) x) : S)
⊢ N.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N : (a : ↥⊥) → ↥N →ₗ[R] ↥⊥ ⊗[R] ↥N) 1 = LinearMap.id

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
x : ↥N
⊢ Eq.{v + 1} (α := S)
    (↑((N.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N : (a : ↥⊥) → ↥N →ₗ[R] ↥⊥ ⊗[R] ↥N) 1 : (a : ↥N) → ↥N) x) : S)
    (↑((LinearMap.id : (a : ↥N) → ↥N) 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
r : ↥⊥
n : ↥N
obtain :
  ∀ (x : R) (h : (algebraMap R S : (a : R) → S) x = (↑r : S)),
    Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
      (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)

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 N : Submodule R S
r : ↥⊥
n : ↥N
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 N : Submodule R S
r : ↥⊥
n : ↥N
x : R
h : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
rw :
  Eq (α := ↥⊥ ⊗[R] ↥N)
    (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
rw₁ : Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (x • n) : ↥⊥ ⊗[R] ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
rw₂ : Eq (α := ↥⊥ ⊗[R] ↥N) (HSMul.hSMul (β := ↥⊥) x 1 ⊗ₜ[R] n) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n)
rw₃ :
  Eq (α := ↥⊥ ⊗[R] ↥N) (HMul.hMul (α := ↥⊥) (β := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥⊥) (1 : ↥⊥) ⊗ₜ[R] n)
    ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n)
rw₄ rw₅ :
  Eq (α := ↥⊥ ⊗[R] ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
    ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)

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

Premises used: TensorProduct.smul_tmul, Submodule.lTensorOne'_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
N : Submodule R S
y : R
n : ↥N
⊢ (N.lTensorOne : (a : ↥⊥ ⊗[R] ↥N) → ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y ⊗ₜ[R] n) = y • n

Tactic:
N.lTensorOne'_tmul y n

Premises used: Submodule.lTensorOne'_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
N : Submodule R S
n : ↥N
⊢ (N.lTensorOne : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (1 ⊗ₜ[R] n) = n

Tactic:
N.lTensorOne'_one_tmul n

Premises used: Submodule.lTensorOne'_one_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
N : Submodule R S
n : ↥N
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) ((N.lTensorOne.symm : (a : ↥N) → ↥⊥ ⊗[R] ↥N) n : ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, 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
N : Submodule R S
⊢ mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) N =
    N.subtype ∘ₗ (↑N.lTensorOne : ↥⊥ ⊗[R] ↥N →ₗ[R] ↥N)

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 N : Submodule R S
rw : LinearMap.range (M := ↥M ⊗[R] ↥1) (M.mulMap 1) = M
rw₁ : M * 1 = M
rw₂ rw₃ : M = M
⊢ LinearMap.range (M := ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S))
      (M.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥)) =
    M

Tactic:
rw [Algebra.toSubmodule_bot, mulMap_range, mul_one]

Premises used: Algebra.toSubmodule_bot, mul_one, Submodule.mulMap_range
-- 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
simp_rw :
  ((M.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) :
          ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) →ₗ[R] S) :
        (a : ↥M ⊗[R] ↥⊥) → S)
      (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y : ↥M ⊗[R] ↥⊥) =
    y • (↑m : S)
⊢ (↑((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y)) : S) = (↑(y • m) : S)

Tactic:
simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]

Premises used: Submodule.rTensorOne', LinearEquiv.coe_ofEq_apply, LinearMap.coe_comp, SetLike.val_smul, Function.comp_apply, LinearMap.codRestrict_apply, LinearEquiv.coe_coe
-- 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
rw :
  ((M.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) :
          ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) →ₗ[R] S) :
        (a : ↥M ⊗[R] ↥⊥) → S)
      (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y : ↥M ⊗[R] ↥⊥) =
    HMul.hMul (β := S) (↑m : S) ((algebraMap R S : (a : R) → S) y : S)
⊢ ((M.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) :
          ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) →ₗ[R] S) :
        (a : ↥M ⊗[R] ↥⊥) → S)
      (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y : ↥M ⊗[R] ↥⊥) =
    y • (↑m : S)

Tactic:
rw [Algebra.smul_def, Algebra.commutes]

Premises used: Algebra.smul_def, Algebra.commutes
-- 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.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) :
          ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) →ₗ[R] S) :
        (a : ↥M ⊗[R] ↥⊥) → S)
      (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y : ↥M ⊗[R] ↥⊥) =
    HMul.hMul (β := S) (↑m : S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
mulMap_tmul M _ _ _

Premises used: Submodule.mulMap_tmul, Set.Mem, setOf, Set.range, Subsemiring.copy, AlgHom.range, RingHom.rangeS
-- 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.mulMap ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) :
          ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) →ₗ[R] S) :
        (a : ↥M ⊗[R] ↥⊥) → S)
      (m ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y : ↥M ⊗[R] ↥⊥) =
    HMul.hMul (β := S) (↑m : S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
exact mulMap_tmul M _ _ _

Premises used: Submodule.mulMap_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:
simpa using rTensorOne'_tmul 1 m

Premises used: Submodule.rTensorOne'_tmul, OfNat.ofNat
-- 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
h :
  ∀ (x : ↥M),
    Eq.{v + 1} (α := S)
      (↑((M.rTensorOne' ∘ₗ
                (↑(TensorProduct.comm R ↥⊥ ↥M) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥⊥) ∘ₗ
                  (TensorProduct.mk R ↥⊥ ↥M : (a : ↥⊥) → ↥M →ₗ[R] ↥⊥ ⊗[R] ↥M) 1 :
              (a : ↥M) → ↥M)
            x) :
        S)
      (↑((LinearMap.id : (a : ↥M) → ↥M) x) : S)
⊢ M.rTensorOne' ∘ₗ
      (↑(TensorProduct.comm R ↥⊥ ↥M) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥⊥) ∘ₗ
        (TensorProduct.mk R ↥⊥ ↥M : (a : ↥⊥) → ↥M →ₗ[R] ↥⊥ ⊗[R] ↥M) 1 =
    LinearMap.id

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
x : ↥M
⊢ Eq.{v + 1} (α := S)
    (↑((M.rTensorOne' ∘ₗ
              (↑(TensorProduct.comm R ↥⊥ ↥M) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥⊥) ∘ₗ
                (TensorProduct.mk R ↥⊥ ↥M : (a : ↥⊥) → ↥M →ₗ[R] ↥⊥ ⊗[R] ↥M) 1 :
            (a : ↥M) → ↥M)
          x) :
      S)
    (↑((LinearMap.id : (a : ↥M) → ↥M) 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
n : ↥M
r : ↥⊥
obtain :
  ∀ (x : R) (h : (algebraMap R S : (a : R) → S) x = (↑r : S)),
    Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
      (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)

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 N : Submodule R S
n : ↥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