awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
ha :
  ∀ (x : ↥A),
    Eq.{u_3 + 1} (α := T)
      ((AlgHom.comp
              (AlgHom.comp ((map f A).mulMap (map f B))
                  (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) :
                AlgHom.{u_1, u_2, u_3} R (↥A ⊗[R] ↥B) T)
              (Algebra.TensorProduct.includeLeft : ↥A →ₐ[R] ↥A ⊗[R] ↥B) :
            (a : ↥A) → T)
          x :
        T)
      (((f.comp (A.mulMap B)).comp Algebra.TensorProduct.includeLeft : (a : ↥A) → T) x : T)
⊢ AlgHom.comp ((map f A).mulMap (map f B))
      (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) =
    f.comp (A.mulMap B)
have hb : ∀ (x : ↥B),
  Eq.{u_3 + 1} (α := T)
    ((AlgHom.comp (B := ↥A ⊗[R] ↥B)
            (AlgHom.restrictScalars R
              (AlgHom.comp ((map f A).mulMap (map f B))
                  (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) :
                AlgHom.{u_1, u_2, u_3} R (↥A ⊗[R] ↥B) T))
            Algebra.TensorProduct.includeRight :
          (a : ↥B) → T)
        x :
      T)
    ((AlgHom.comp (AlgHom.restrictScalars R (f.comp (A.mulMap B))) Algebra.TensorProduct.includeRight : (a : ↥B) → T)
        x :
      T)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ B.mulMap A = (A.mulMap B).comp (↑(Algebra.TensorProduct.comm R ↥B ↥A) : ↥B ⊗[R] ↥A →ₐ[R] ↥A ⊗[R] ↥B)
have ha : ∀ (x : ↥B),
  Eq (α := S) (((B.mulMap A).comp Algebra.TensorProduct.includeLeft : (a : ↥B) → S) x : S)
    ((((A.mulMap B).comp (↑(Algebra.TensorProduct.comm R ↥B ↥A) : ↥B ⊗[R] ↥A →ₐ[R] ↥A ⊗[R] ↥B)).comp
            Algebra.TensorProduct.includeLeft :
          (a : ↥B) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
ha :
  ∀ (x : ↥B),
    Eq (α := S) (((B.mulMap A).comp Algebra.TensorProduct.includeLeft : (a : ↥B) → S) x : S)
      ((((A.mulMap B).comp (↑(Algebra.TensorProduct.comm R ↥B ↥A) : ↥B ⊗[R] ↥A →ₐ[R] ↥A ⊗[R] ↥B)).comp
              Algebra.TensorProduct.includeLeft :
            (a : ↥B) → S)
          x :
        S)
⊢ B.mulMap A = (A.mulMap B).comp (↑(Algebra.TensorProduct.comm R ↥B ↥A) : ↥B ⊗[R] ↥A →ₐ[R] ↥A ⊗[R] ↥B)
have hb : ∀ (x : ↥A),
  Eq (α := S)
    ((AlgHom.comp (AlgHom.restrictScalars R (B.mulMap A)) Algebra.TensorProduct.includeRight : (a : ↥A) → S) x : S)
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              ((A.mulMap B).comp (↑(Algebra.TensorProduct.comm R ↥B ↥A) : ↥B ⊗[R] ↥A →ₐ[R] ↥A ⊗[R] ↥B)))
            Algebra.TensorProduct.includeRight :
          (a : ↥A) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ (A.mulMap B).range = A ⊔ B
have simp_rw : (Algebra.TensorProduct.productMap A.val B.val).range = A ⊔ B
Tactic: simp_rw [mulMap, Algebra.TensorProduct.productMap_range, Subalgebra.range_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
simp_rw : (Algebra.TensorProduct.productMap A.val B.val).range = A ⊔ B
⊢ (A.mulMap B).range = A ⊔ B
have simp_rw₁ : A.val.range ⊔ B.val.range = A ⊔ B
Tactic: simp_rw [mulMap, Algebra.TensorProduct.productMap_range, Subalgebra.range_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B) : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
have simp_rw : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
  (⇑((↑((A.mulMap B).range.equivOfEq (A ⊔ B) sorry) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)).comp (A.mulMap B).rangeRestrict) :
    (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
Tactic: simp_rw [mulMap', AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
simp_rw :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
    (⇑((↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)).comp
          (A.mulMap B).rangeRestrict) :
      (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
⊢ Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B) : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
have simp_rw₁ : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
  (Function.comp (β := ↥(A.mulMap B).range)
    (⇑(↑((A.mulMap B).range.equivOfEq (A ⊔ B) sorry) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)) :
      (a : ↥(A.mulMap B).range) → ↥(A ⊔ B))
    (⇑(A.mulMap B).rangeRestrict : (a : ↥A ⊗[R] ↥B) → ↥(A.mulMap B).range))
Tactic: simp_rw [mulMap', AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
simp_rw :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
    (⇑((↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)).comp
          (A.mulMap B).rangeRestrict) :
      (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
simp_rw₁ :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
    (Function.comp (β := ↥(A.mulMap B).range)
      (⇑(↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)) :
        (a : ↥(A.mulMap B).range) → ↥(A ⊔ B))
      (⇑(A.mulMap B).rangeRestrict : (a : ↥A ⊗[R] ↥B) → ↥(A.mulMap B).range))
⊢ Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B) : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
have simp_rw₂ : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
  (Function.comp (β := ↥(A.mulMap B).range)
    (⇑((A.mulMap B).range.equivOfEq (A ⊔ B) sorry) : (a : ↥(A.mulMap B).range) → ↥(A ⊔ B))
    (⇑(A.mulMap B).rangeRestrict : (a : ↥A ⊗[R] ↥B) → ↥(A.mulMap B).range))
Tactic: simp_rw [mulMap', AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
simp_rw :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
    (⇑((↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)).comp
          (A.mulMap B).rangeRestrict) :
      (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
simp_rw₁ :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
    (Function.comp (β := ↥(A.mulMap B).range)
      (⇑(↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯) : ↥(A.mulMap B).range →ₐ[R] ↥(A ⊔ B)) :
        (a : ↥(A.mulMap B).range) → ↥(A ⊔ B))
      (⇑(A.mulMap B).rangeRestrict : (a : ↥A ⊗[R] ↥B) → ↥(A.mulMap B).range))
simp_rw₂ :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B))
    (Function.comp (β := ↥(A.mulMap B).range)
      (⇑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯) : (a : ↥(A.mulMap B).range) → ↥(A ⊔ B))
      (⇑(A.mulMap B).rangeRestrict : (a : ↥A ⊗[R] ↥B) → ↥(A.mulMap B).range))
⊢ Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B) : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
have simp_rw₃ : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A.mulMap B).range)
  (⇑(A.mulMap B).rangeRestrict : (a : ↥A ⊗[R] ↥B) → ↥(A.mulMap B).range)
Tactic: simp_rw [mulMap', AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]
-- 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
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
⊢ Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) (↥M ⊗[R] ↥N) T)
    (mulMap
        (map (σ₁₂ := RingHom.id R)
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) M)
        (map (σ₁₂ := RingHom.id R)
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          N) ∘ₗ
      TensorProduct.map
        (LinearMap.submoduleMap
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) M)
        (LinearMap.submoduleMap
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          N))
    ((↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) ∘ₗ
      M.mulMap N)
have a : ∀ (x : ↥M) (x_1 : ↥N),
  Eq.{w + 1} (α := T)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (mulMap
                        (map (σ₁₂ := RingHom.id R)
                          (↑f :
                            [inst_5 : FunLike (S →ₐ[R] T) S T] →
                              [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                          M)
                        (map (σ₁₂ := RingHom.id R)
                          (↑f :
                            [inst_5 : FunLike (S →ₐ[R] T) S T] →
                              [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                          N) ∘ₗ
                      TensorProduct.map
                        (LinearMap.submoduleMap
                          (↑f :
                            [inst_5 : FunLike (S →ₐ[R] T) S T] →
                              [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                          M)
                        (LinearMap.submoduleMap
                          (↑f :
                            [inst_5 : FunLike (S →ₐ[R] T) S T] →
                              [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                          N)) :
                  ↥M →ₗ[R] LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
                (a : ↥M) → ↥N →ₗ[R] T)
              x :
            LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
          (a : ↥N) → T)
        x_1 :
      T)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑f :
                        [inst_5 : FunLike (S →ₐ[R] T) S T] →
                          [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) ∘ₗ
                      M.mulMap N) :
                  ↥M →ₗ[R] LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
                (a : ↥M) → ↥N →ₗ[R] T)
              x :
            LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
          (a : ↥N) → T)
        x_1 :
      T)
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
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
⊢ N.mulMap M = M.mulMap N ∘ₗ (↑(TensorProduct.comm R ↥N ↥M) : ↥N ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥N)
have refine : ∀ (n : ↥N) (m : ↥M),
  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: refine TensorProduct.ext' fun n 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 N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
n : ↥N
m : ↥M
⊢ 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)
have simp_rw : (↑n : S) * (↑m : S) = (↑m : S) * (↑n : S)
Tactic: simp_rw [LinearMap.comp_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul, mulMap_tmul]
-- 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.mulMap N).range = M * N
have refine : (M.mulMap N).range ≤ M * N
Tactic: refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)
-- 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
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) 0 : S)
have zero : 0 ∈ M * N
Tactic: rw [map_zero]
-- 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
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)
have 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
Tactic: rw [map_add]
-- 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
x : ↥M ⊗[R] ↥N
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S)
have zero : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) 0 : 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
Cleared hypotheses: x
-- 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
x : ↥M ⊗[R] ↥N
zero : Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) 0 : S)
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S)
have tmul : ∀ (a : ↥M) (b : ↥N), Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) (a ⊗ₜ[R] b) : 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
Cleared hypotheses: x
-- 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
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)
⊢ Membership.mem (α := S) (M * N) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S)
have 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)
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
Cleared hypotheses: x
-- 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
⊢ Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N)) (⇑(M.mulMap' N) : (a : ↥M ⊗[R] ↥N) → ↥(M * N))
have simp_rw : Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N))
  (⇑((↑(LinearEquiv.ofEq (M.mulMap N).range (M * N) sorry) : ↥(M.mulMap N).range →ₗ[R] ↥(M * N)) ∘ₗ
        (M.mulMap N).rangeRestrict) :
    (a : ↥M ⊗[R] ↥N) → ↥(M * N))
Tactic: simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]
-- 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
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))
⊢ Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N)) (⇑(M.mulMap' N) : (a : ↥M ⊗[R] ↥N) → ↥(M * N))
have simp_rw₁ : Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N))
  (Function.comp (β := ↥(M.mulMap N).range)
    (⇑(↑(LinearEquiv.ofEq (M.mulMap N).range (M * N) sorry) : ↥(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))
Tactic: simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]
-- 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
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))
⊢ Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N)) (⇑(M.mulMap' N) : (a : ↥M ⊗[R] ↥N) → ↥(M * N))
have simp_rw₂ : Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N))
  (Function.comp (β := ↥(M.mulMap N).range)
    (⇑(LinearEquiv.ofEq (M.mulMap N).range (M * N) sorry) : (a : ↥(M.mulMap N).range) → ↥(M * N))
    (⇑(M.mulMap N).rangeRestrict : (a : ↥M ⊗[R] ↥N) → ↥(M.mulMap N).range))
Tactic: simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]
-- 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
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))
⊢ Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M * N)) (⇑(M.mulMap' N) : (a : ↥M ⊗[R] ↥N) → ↥(M * N))
have simp_rw₃ : Function.Surjective (α := ↥M ⊗[R] ↥N) (β := ↥(M.mulMap N).range)
  (⇑(M.mulMap N).rangeRestrict : (a : ↥M ⊗[R] ↥N) → ↥(M.mulMap N).range)
Tactic: simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
    LinearMap.surjective_rangeRestrict]
-- 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 := ↥((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
have rw : LinearMap.range (M := ↥1 ⊗[R] ↥N) (mulMap 1 N) = N
Tactic: rw [Algebra.toSubmodule_bot, mulMap_range, one_mul]
-- 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 := ↥1 ⊗[R] ↥N) (mulMap 1 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
have rw₁ : 1 * N = N
Tactic: rw [Algebra.toSubmodule_bot, mulMap_range, one_mul]
-- 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 := ↥1 ⊗[R] ↥N) (mulMap 1 N) = N
rw₁ : 1 * 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
have rw₂ : N = N
Tactic: rw [Algebra.toSubmodule_bot, mulMap_range, one_mul]
-- 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
N : Submodule R S
y : R
n : ↥N
⊢ (↑((N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y ⊗ₜ[R] n)) : S) = (↑(y • n) : S)
have 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)
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]
-- 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.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N : (a : ↥⊥) → ↥N →ₗ[R] ↥⊥ ⊗[R] ↥N) 1 = LinearMap.id
have 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)
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
r : ↥⊥
n : ↥N
⊢ Eq (α := ↥⊥ ⊗[R] ↥N) (1 ⊗ₜ[R] (N.lTensorOne' : (a : ↥⊥ ⊗[R] ↥N) → ↥N) (r ⊗ₜ[R] n) : ↥⊥ ⊗[R] ↥N)
    (r ⊗ₜ[R] n : ↥⊥ ⊗[R] ↥N)
have 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)
Tactic: obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2