awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
rw :
  Eq (α := S ⊗[R] T)
    (((Submodule.mulMap (LinearMap.range (AlgHom.toLinearMap includeLeft))
              (LinearMap.range (AlgHom.toLinearMap includeRight)) :
            ↥(LinearMap.range (AlgHom.toLinearMap includeLeft)) ⊗[R]
                ↥(LinearMap.range (AlgHom.toLinearMap includeRight)) →ₗ[R]
              S ⊗[R] T) :
          (a : ↥includeLeft.range ⊗[R] ↥includeRight.range) → S ⊗[R] T)
        (((LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft) :
                S →ₗ[R] ↥(LinearMap.range (AlgHom.toLinearMap includeLeft))) :
              (a : S) → ↥includeLeft.range)
            x ⊗ₜ[R]
          ((LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight) :
                T →ₗ[R] ↥(LinearMap.range (AlgHom.toLinearMap includeRight))) :
              (a : T) → ↥includeRight.range)
            y) :
      S ⊗[R] T)
    (x ⊗ₜ[R] y : S ⊗[R] T)
⊢ Eq (α := S ⊗[R] T)
    (((Submodule.mulMap (LinearMap.range (AlgHom.toLinearMap includeLeft))
                (LinearMap.range (AlgHom.toLinearMap includeRight)) :
              ↥(LinearMap.range (AlgHom.toLinearMap includeLeft)) ⊗[R]
                  ↥(LinearMap.range (AlgHom.toLinearMap includeRight)) →ₗ[R]
                S ⊗[R] T) ∘ₗ
            _root_.TensorProduct.map (LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft))
              (LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight)) :
          (a : S ⊗[R] T) → S ⊗[R] T)
        (x ⊗ₜ[R] y) :
      S ⊗[R] T)
    ((LinearMap.id : (a : S ⊗[R] T) → S ⊗[R] T) (x ⊗ₜ[R] y) : S ⊗[R] T)

Tactic:
rw [LinearMap.comp_apply, LinearMap.id_apply, _root_.TensorProduct.map_tmul]

Premises used: LinearMap.id_apply, LinearMap.comp_apply, TensorProduct.map_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
rw : Eq (α := S ⊗[R] T) ((x * 1) ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
rw₁ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] (1 * y)) (x ⊗ₜ[R] y)
rw₂ rw₃ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] y) (x ⊗ₜ[R] y)
⊢ HMul.hMul (α := S ⊗[R] T) (x ⊗ₜ[R] 1) (1 ⊗ₜ[R] y) = x ⊗ₜ[R] y

Tactic:
rw [tmul_mul_tmul, mul_one, one_mul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
⊢ Eq (α := S ⊗[R] T →ₗ[R] ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    (↑(linearEquivIncludeRange R S T) : S ⊗[R] T →ₗ[R] ↥includeLeft.range ⊗[R] ↥includeRight.range)
    (_root_.TensorProduct.map (LinearMap.rangeRestrict (AlgHom.toLinearMap includeLeft))
      (LinearMap.rangeRestrict (AlgHom.toLinearMap includeRight)))

Tactic:
rfl

Premises used: Set.Mem, LinearMap.range, TensorProduct.map, TensorProduct.tmul, Subsemiring.copy, TensorProduct.lift, AddCon.toQuotient, AlgHom.range, rfl, Submodule.copy, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
⊢ Eq (α := ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight) →ₗ[R] S ⊗[R] T)
    (↑(LinearEquiv.symm (linearEquivIncludeRange R S T)) : ↥includeLeft.range ⊗[R] ↥includeRight.range →ₗ[R] S ⊗[R] T)
    (Submodule.mulMap (LinearMap.range (AlgHom.toLinearMap includeLeft))
      (LinearMap.range (AlgHom.toLinearMap includeRight)))

Tactic:
rfl

Premises used: Submodule.mulMap, Quotient.liftOn', Set.Mem, AddCon.liftOn, LinearMap.range, TensorProduct, TensorProduct.tmul, Subsemiring.copy, TensorProduct.lift, AddCon.toQuotient, AlgHom.range, rfl, Submodule.copy, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
⊢ Eq (α := ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    ((linearEquivIncludeRange R S T : (a : S ⊗[R] T) → ↥includeLeft.range ⊗[R] ↥includeRight.range) (x ⊗ₜ[R] y) :
      ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    ((AlgHom.rangeRestrict includeLeft : (a : S) → ↥includeLeft.range) x ⊗ₜ[R]
        (AlgHom.rangeRestrict includeRight : (a : T) → ↥includeRight.range) y :
      ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : ↥(AlgHom.range includeLeft)
y : ↥(AlgHom.range includeRight)
⊢ (LinearEquiv.symm (linearEquivIncludeRange R S T) : (a : ↥includeLeft.range ⊗[R] ↥includeRight.range) → S ⊗[R] T)
      (x ⊗ₜ[R] y) =
    (↑x : S ⊗[R] T) * (↑y : S ⊗[R] T)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
⊢ ∀ (a₁ a₂ : S) (b₁ b₂ : T),
    (linearEquivIncludeRange R S T : (a : S ⊗[R] T) → ↥includeLeft.range ⊗[R] ↥includeRight.range)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight)) (β :=
        ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
        ((linearEquivIncludeRange R S T : (a : S ⊗[R] T) → ↥includeLeft.range ⊗[R] ↥includeRight.range) (a₁ ⊗ₜ[R] b₁) :
          ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
        ((linearEquivIncludeRange R S T : (a : S ⊗[R] T) → ↥includeLeft.range ⊗[R] ↥includeRight.range) (a₂ ⊗ₜ[R] b₂) :
          ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
⊢ Eq (α := S ⊗[R] T →ₐ[R] ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    (↑(algEquivIncludeRange R S T) : S ⊗[R] T →ₐ[R] ↥includeLeft.range ⊗[R] ↥includeRight.range)
    (map (AlgHom.rangeRestrict includeLeft) (AlgHom.rangeRestrict includeRight))

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, AlgEquiv.toAlgHom, Set.Mem, Algebra.TensorProduct.map, AlgHom.ofLinearMap, TensorProduct.tmul, Subsemiring.copy, AddCon.toQuotient, AlgHom.range, rfl, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : S
y : T
⊢ Eq (α := ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    ((algEquivIncludeRange R S T : (a : S ⊗[R] T) → ↥includeLeft.range ⊗[R] ↥includeRight.range) (x ⊗ₜ[R] y) :
      ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))
    ((AlgHom.rangeRestrict includeLeft : (a : S) → ↥includeLeft.range) x ⊗ₜ[R]
        (AlgHom.rangeRestrict includeRight : (a : T) → ↥includeRight.range) y :
      ↥(AlgHom.range includeLeft) ⊗[R] ↥(AlgHom.range includeRight))

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
x : ↥(AlgHom.range includeLeft)
y : ↥(AlgHom.range includeRight)
⊢ (AlgEquiv.symm (algEquivIncludeRange R S T) : (a : ↥includeLeft.range ⊗[R] ↥includeRight.range) → S ⊗[R] T)
      (x ⊗ₜ[R] y) =
    (↑x : S ⊗[R] T) * (↑y : S ⊗[R] T)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, AlgEquiv.toAlgHom, Set.Mem, AlgHom.ofLinearMap, Algebra.TensorProduct.lift, LinearMap.range, Subalgebra.mulMap, Algebra.TensorProduct.productMap, TensorProduct.tmul, Subsemiring.copy, AddCon.toQuotient, AlgHom.range, rfl, Submodule.copy, RingHom.rangeS
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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 : ↥A
b : ↥B
⊢ (A.mulMap B : (a : ↥A ⊗[R] ↥B) → S) (a ⊗ₜ[R] b) = (↑a : S) * (↑b : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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)
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
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)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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).toLinearMap =
    Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
      ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Submodule.mulMap, Quotient.liftOn', Set.Mem, AddCon.liftOn, TensorProduct, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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)
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)
⊢ B.mulMap A = (A.mulMap B).comp (↑(Algebra.TensorProduct.comm R ↥B ↥A) : ↥B ⊗[R] ↥A →ₐ[R] ↥A ⊗[R] ↥B)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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
simp_rw₁ : A.val.range ⊔ B.val.range = A ⊔ B
⊢ (A.mulMap B).range = A ⊔ B

Tactic:
simp_rw [mulMap, Algebra.TensorProduct.productMap_range, Subalgebra.range_val]

Premises used: Subalgebra.range_val, Subalgebra.mulMap, Algebra.TensorProduct.productMap_range
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ mulMap ⊥ A = A.val.comp (↑A.lTensorBot : ↥⊥ ⊗[R] ↥A →ₐ[R] ↥A)

Tactic:
AlgHom.toLinearMap_injective (toSubmodule A).mulMap_one_left_eq

Premises used: AlgHom.toLinearMap_injective, Submodule.mulMap_one_left_eq, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ A.mulMap ⊥ = A.val.comp (↑A.rTensorBot : ↥A ⊗[R] ↥⊥ →ₐ[R] ↥A)

Tactic:
AlgHom.toLinearMap_injective (toSubmodule A).mulMap_one_right_eq

Premises used: Submodule.mulMap_one_right_eq, AlgHom.toLinearMap_injective, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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 : ↥A
b : ↥B
⊢ (↑((A.mulMap' B : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B)) (a ⊗ₜ[R] b)) : S) = (↑a : S) * (↑b : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
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))
simp_rw₃ :
  Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A.mulMap B).range)
    (⇑(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))

Tactic:
simp_rw [mulMap', AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]

Premises used: AlgHom.rangeRestrict_surjective, Subalgebra.mulMap', AlgHom.coe_comp, AlgEquiv.coe_algHom, EquivLike.comp_surjective
-- 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) → S) (m ⊗ₜ[R] n) = (↑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
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
x : ↥M
x_1 : ↥N
⊢ HMul.hMul (α := T)
      (↑((LinearMap.submoduleMap
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M :
              (a : ↥M) →
                ↥(map
                    (↑f :
                      [inst_5 : FunLike (S →ₐ[R] T) S T] →
                        [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                    M))
            x) :
        T)
      (↑((LinearMap.submoduleMap
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                N :
              (a : ↥N) →
                ↥(map
                    (↑f :
                      [inst_5 : FunLike (S →ₐ[R] T) S T] →
                        [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                    N))
            x_1) :
        T) =
    HMul.hMul (α := T) (β := T) ((f : (a : S) → T) (↑x : S) : T) ((f : (a : S) → T) (↑x_1 : S) : T)

Tactic:
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
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
⊢ Eq (α := ↥M ⊗[R] ↥N → T)
    (Function.comp (β :=
      ↥(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) ⊗[R]
        ↥(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))
      (⇑(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)) :
        (a :
            ↥(map
                  (↑f :
                    [inst_5 : FunLike (S →ₐ[R] T) S T] →
                      [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                  M) ⊗[R]
              ↥(map
                  (↑f :
                    [inst_5 : FunLike (S →ₐ[R] T) S T] →
                      [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                  N)) →
          T)
      (⇑(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)) :
        (a : ↥M ⊗[R] ↥N) →
          ↥(map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M) ⊗[R]
            ↥(map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                N)))
    (Function.comp (β := S) (⇑f : (a : S) → T) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S))

Tactic:
congr(⇑($(mulMap_map_comp_eq M N f)))

Premises used: congrArg, id, Submodule.mulMap_map_comp_eq, DFunLike.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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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
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)

Tactic:
TensorProduct.ext' fun n m ↦ ?_

Premises used: 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 N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
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)
⊢ N.mulMap M = M.mulMap N ∘ₗ (↑(TensorProduct.comm R ↥N ↥M) : ↥N ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥N)

Tactic:
refine TensorProduct.ext' fun n m ↦ ?_

Premises used: TensorProduct.ext'