awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (hypothesis)
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)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have h₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
Tactic: replace h : algebraMap R _ x = r := Subtype.val_injective h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have 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)
Tactic: rw [← h, lTensorOne'_tmul, ← TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have rw₁ : Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (x • n) : ↥⊥ ⊗[R] ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
Tactic: rw [← h, lTensorOne'_tmul, ← TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have rw₂ : Eq (α := ↥⊥ ⊗[R] ↥N) (HSMul.hSMul (β := ↥⊥) x 1 ⊗ₜ[R] n) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n)
Tactic: rw [← h, lTensorOne'_tmul, ← TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have rw₃ : Eq (α := ↥⊥ ⊗[R] ↥N) (HMul.hMul (α := ↥⊥) (β := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥⊥) (1 : ↥⊥) ⊗ₜ[R] n)
  ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n)
Tactic: rw [← h, lTensorOne'_tmul, ← TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have rw₄ : Eq (α := ↥⊥ ⊗[R] ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
  ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
Tactic: rw [← h, lTensorOne'_tmul, ← TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
⊢ 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
have rw : LinearMap.range (M := ↥M ⊗[R] ↥1) (M.mulMap 1) = M
Tactic: rw [Algebra.toSubmodule_bot, mulMap_range, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ 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
have rw₁ : M * 1 = M
Tactic: rw [Algebra.toSubmodule_bot, mulMap_range, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ 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
have rw₂ : M = M
Tactic: rw [Algebra.toSubmodule_bot, mulMap_range, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)) : S) = (↑(y • m) : S)
have 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)
Tactic: simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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] ↥⊥) =
    y • (↑m : S)
have 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)
Tactic: rw [Algebra.smul_def, Algebra.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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.rTensorOne' ∘ₗ
      (↑(TensorProduct.comm R ↥⊥ ↥M) : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥⊥) ∘ₗ
        (TensorProduct.mk R ↥⊥ ↥M : (a : ↥⊥) → ↥M →ₗ[R] ↥⊥ ⊗[R] ↥M) 1 =
    LinearMap.id
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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 : ↥⊥
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have 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] ↥⊥)
Tactic: obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (hypothesis)
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)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have h₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
Tactic: replace h : algebraMap R _ x = r := Subtype.val_injective h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have 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] ↥⊥)
Tactic: rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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] ↥⊥)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have rw₁ : Eq (α := ↥M ⊗[R] ↥⊥) ((x • n) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
Tactic: rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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] ↥⊥)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have rw₂ : Eq (α := ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] HSMul.hSMul (β := ↥⊥) x 1) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x)
Tactic: rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have rw₃ : Eq (α := ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] HMul.hMul (α := ↥⊥) (β := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥⊥) (1 : ↥⊥))
  (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x)
Tactic: rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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)
⊢ Eq (α := ↥M ⊗[R] ↥⊥) ((M.rTensorOne' : (a : ↥M ⊗[R] ↥⊥) → ↥M) (n ⊗ₜ[R] r) ⊗ₜ[R] 1 : ↥M ⊗[R] ↥⊥)
    (n ⊗ₜ[R] r : ↥M ⊗[R] ↥⊥)
have rw₄ : Eq (α := ↥M ⊗[R] ↥⊥) (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
  (n ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x : ↥M ⊗[R] ↥⊥)
Tactic: rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
have 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)
Tactic: refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun m r ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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 : ↥⊥
⊢ 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)
have 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)
Tactic: obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (hypothesis)
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)
⊢ 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)
have h₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
Tactic: replace h : algebraMap R _ x = r := Subtype.val_injective h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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] r) : ↥M)
    (((↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M) : (a : ↥M ⊗[R] ↥⊥) → ↥M) (m ⊗ₜ[R] r) : ↥M)
have 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)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
have 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)
Tactic: refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun r m ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (hypothesis)
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)
⊢ 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)
have h₁ : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x = r
Tactic: replace h : algebraMap R _ x = r := Subtype.val_injective h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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) (r ⊗ₜ[R] m) : ↥M)
    (((↑M.lTensorOne : ↥⊥ ⊗[R] ↥M →ₗ[R] ↥M) : (a : ↥⊥ ⊗[R] ↥M) → ↥M) (r ⊗ₜ[R] m) : ↥M)
have 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)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ mulLeftMap N m =
    M.mulMap N ∘ₗ
      LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.finsuppScalarLeft R (↥N) ι)) : (ι →₀ ↥N) →ₗ[R] (ι →₀ R) ⊗[R] ↥N)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
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
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (f₁ + f₂) g =
    HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (map f₁ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)
      (map f₂ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)
have a : ∀ (x : M) (x_1 : N),
  Eq (α := P ⊗[R] Q)
    (((((curry (map (f₁ + f₂) g) : M →ₗ[A] N →ₗ[R] P ⊗[R] Q) : (a : M) → N →ₗ[R] P ⊗[R] Q) x : N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    (((((curry
                    (HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q)
                      (map f₁ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q) (map f₂ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                  M →ₗ[A] N →ₗ[R] P ⊗[R] Q) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
Tactic: ext