awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
a b : A
f g : End R M
h :
  ∀ (x : A ⊗[R] M),
    Eq (α := A ⊗[R] M)
      ((((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) ((a * b) ⊗ₜ[R] (f * g)) : End A (A ⊗[R] M)) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          x :
        A ⊗[R] M)
      ((HMul.hMul (α := End A (A ⊗[R] M)) (β := End A (A ⊗[R] M))
              ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (a ⊗ₜ[R] f) : End A (A ⊗[R] M))
              ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (b ⊗ₜ[R] g) : End A (A ⊗[R] M)) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          x :
        A ⊗[R] M)
⊢ (tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) ((a * b) ⊗ₜ[R] (f * g)) =
    HMul.hMul (α := End A (A ⊗[R] M)) (β := End A (A ⊗[R] M))
      ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (a ⊗ₜ[R] f) : End A (A ⊗[R] M))
      ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (b ⊗ₜ[R] g) : End A (A ⊗[R] M))

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
a b : A
f g : End R M
x : A ⊗[R] M
⊢ Eq (α := A ⊗[R] M)
    ((((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) ((a * b) ⊗ₜ[R] (f * g)) : End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((HMul.hMul (α := End A (A ⊗[R] M)) (β := End A (A ⊗[R] M))
            ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (a ⊗ₜ[R] f) : End A (A ⊗[R] M))
            ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (b ⊗ₜ[R] g) : End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        x :
      A ⊗[R] M)

Tactic:
simp only [tensorProduct, mul_comm a b, Module.End.mul_eq_comp,
        TensorProduct.AlgebraTensorModule.lift_apply, TensorProduct.lift.tmul, coe_restrictScalars,
        coe_mk, AddHom.coe_mk, mul_smul, smul_apply, baseChangeHom_apply, baseChange_comp,
        comp_apply, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]

Premises used: LinearMap.coe_mk, Algebra.mul_smul_comm, LinearMap.baseChange_comp, Module.End.mul_eq_comp, LinearMap.smul_apply, LinearMap.coe_restrictScalars, LinearMap.comp_apply, TensorProduct.lift.tmul, TensorProduct.AlgebraTensorModule.lift_apply, Algebra.smul_mul_assoc, mul_comm, AddHom.coe_mk, SemigroupAction.mul_smul, LinearMap.baseChangeHom_apply, LinearMap.tensorProduct
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
h :
  ∀ (x : A ⊗[R] M),
    Eq (α := A ⊗[R] M)
      ((((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] 1) : End A (A ⊗[R] M)) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          x :
        A ⊗[R] M)
      ((1 : (a : A ⊗[R] M) → A ⊗[R] M) x : A ⊗[R] M)
⊢ Eq (α := End A (A ⊗[R] M))
    ((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] 1) : End A (A ⊗[R] M))
    (1 : End A (A ⊗[R] M))

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
x : A ⊗[R] M
⊢ Eq (α := A ⊗[R] M)
    ((((tensorProduct R A M M : (a : A ⊗[R] End R M) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] 1) : End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((1 : (a : A ⊗[R] M) → A ⊗[R] M) x : A ⊗[R] M)

Tactic:
simp only [tensorProduct, TensorProduct.AlgebraTensorModule.lift_apply,
        TensorProduct.lift.tmul, coe_restrictScalars, coe_mk, AddHom.coe_mk, one_smul,
        baseChangeHom_apply, baseChange_eq_ltensor, Module.End.one_eq_id,
        lTensor_id, LinearMap.id_apply]

Premises used: LinearMap.baseChange_eq_ltensor, LinearMap.coe_mk, Module.End.one_eq_id, LinearMap.id_apply, LinearMap.coe_restrictScalars, TensorProduct.lift.tmul, LinearMap.lTensor_id, one_smul, TensorProduct.AlgebraTensorModule.lift_apply, AddHom.coe_mk, LinearMap.baseChangeHom_apply, LinearMap.tensorProduct
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Bijective (α := A ⊗[R] A) (β := A) (⇑(mul' R A) : (a : A ⊗[R] A) → A)

Tactic:
have : TensorProduct.CompatibleSMul R A A A := .of_algebraMap_surjective _ _ h
  (Algebra.TensorProduct.lmulEquiv R A).bijective

Premises used: TensorProduct.CompatibleSMul.of_algebraMap_surjective, Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.lmulEquiv, TensorProduct, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Algebra R S
inst_6 : Algebra S A
inst_7 : Algebra R A
inst_8 : Module R M
inst_9 : Module S M
inst_10 : Module A M
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower S A M
inst_14 : IsScalarTower R S M
f : End A M
g : End R N
⊢ Eq (α := End A (M ⊗[R] N))
    (((endTensorEndAlgHom : TensorProduct.{u_1, u_4, u_5} R (End A M) (End R N) →ₐ[S] End A (M ⊗[R] N)) :
          (a : End A M ⊗[R] End R N) → End A (M ⊗[R] N))
        (f ⊗ₜ[R] g) :
      End A (M ⊗[R] N))
    (AlgebraTensorModule.map f g : M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
C : Subalgebra R A
x : A
hx : x ∈ C
b : B
⊢ Membership.mem (γ := Subalgebra B (B ⊗[R] A)) (baseChange B C) (b ⊗ₜ[R] x)

Tactic:
⟨(b ⊗ₜ[R] ⟨x, hx⟩), rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, TensorProduct.tmul, Set.range, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
a : A
b : B
⊢ Eq (α := ULift.{u_9, u_6} A ⊗[ULift.{u_10, u_4} R] ULift.{u_8, u_7} B)
    (((uliftEquiv R S A B :
            ULift.{u_11, max u_7 u_6} (A ⊗[R] B) ≃ₐ[S] ULift.{u_9, u_6} A ⊗[ULift.{u_10, u_4} R] ULift.{u_8, u_7} B) :
          (a : ULift.{u_11, max u_7 u_6} (A ⊗[R] B)) → ULift.{u_9, u_6} A ⊗[ULift.{u_10, u_4} R] ULift.{u_8, u_7} B)
        { down := a ⊗ₜ[R] b } :
      ULift.{u_9, u_6} A ⊗[ULift.{u_10, u_4} R] ULift.{u_8, u_7} B)
    ({ down := a } ⊗ₜ[ULift.{u_10, u_4} R] { down := b } : ULift.{u_9, u_6} A ⊗[ULift.{u_10, u_4} R] ULift.{u_8, u_7} B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
a : ULift.{u_8, u_6} A
b : ULift.{u_9, u_7} B
⊢ Eq (α := A ⊗[R] B)
    (ULift.down
      (((AlgEquiv.symm (uliftEquiv R S A B) :
            ULift.{u_8, u_6} A ⊗[ULift.{u_11, u_4} R] ULift.{u_9, u_7} B ≃ₐ[S] ULift.{u_10, max u_7 u_6} (A ⊗[R] B)) :
          (a : ULift.{u_8, u_6} A ⊗[ULift.{u_11, u_4} R] ULift.{u_9, u_7} B) → ULift.{u_10, max u_7 u_6} (A ⊗[R] B))
        (a ⊗ₜ[ULift.{u_11, u_4} R] b)))
    (a.down ⊗ₜ[R] b.down)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
a : ULift.{u_8, u_6} A
b : ULift.{u_9, u_7} B
⊢ Eq (α := ULift.{u_10, max u_7 u_6} (A ⊗[R] B))
    (((AlgEquiv.symm (uliftEquiv R S A B) :
            ULift.{u_8, u_6} A ⊗[ULift.{u_11, u_4} R] ULift.{u_9, u_7} B ≃ₐ[S] ULift.{u_10, max u_7 u_6} (A ⊗[R] B)) :
          (a : ULift.{u_8, u_6} A ⊗[ULift.{u_11, u_4} R] ULift.{u_9, u_7} B) → ULift.{u_10, max u_7 u_6} (A ⊗[R] B))
        (a ⊗ₜ[ULift.{u_11, u_4} R] b) :
      ULift.{u_10, max u_7 u_6} (A ⊗[R] B))
    ({ down := a.down ⊗ₜ[R] b.down } : ULift.{u_10, max u_6 u_7} (A ⊗[R] B))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ha :
  ∀ (x : ULift.{u₂, u_5} S),
    Eq.{u_5 + 1} (α := S)
      (ULift.down.{u₂, u_5}
        ((AlgHom.comp (lmul' (ULift.{u₁, u_4} R)) includeLeft : (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S) x))
      (ULift.down.{u₂, u_5}
        ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
              (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
                (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                  ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                    ULift.{u_8, u_5} (S ⊗[R] S)))
              includeLeft :
            (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
          x))
hb :
  ∀ (x : ULift.{u₂, u_5} S),
    Eq.{u_5 + 1} (α := S)
      (ULift.down.{u₂, u_5}
        ((AlgHom.comp (AlgHom.restrictScalars (ULift.{u₁, u_4} R) (S := ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R)))
              includeRight :
            (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
          x))
      (ULift.down.{u₂, u_5}
        ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
              (AlgHom.restrictScalars (ULift.{u₁, u_4} R)
                (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
                  (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                    ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                      ULift.{u_8, u_5} (S ⊗[R] S))))
              includeRight :
            (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
          x))
⊢ Eq (α := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
    (lmul' (ULift.{u₁, u_4} R))
    (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
      (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
        ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R] ULift.{u_8, u_5} (S ⊗[R] S)))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : ULift.{u₂, u_5} S
⊢ Eq.{u_5 + 1} (α := S)
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (lmul' (ULift.{u₁, u_4} R)) includeLeft : (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S) x))
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
            (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
              (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                  ULift.{u_8, u_5} (S ⊗[R] S)))
            includeLeft :
          (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
        x))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : ULift.{u₂, u_5} S
⊢ Eq.{u_5 + 1} (α := S)
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (AlgHom.restrictScalars (ULift.{u₁, u_4} R) (S := ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R)))
            includeRight :
          (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
        x))
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
            (AlgHom.restrictScalars (ULift.{u₁, u_4} R)
              (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
                (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                  ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                    ULift.{u_8, u_5} (S ⊗[R] S))))
            includeRight :
          (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
        x))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
a : A
m : M
b : B
⊢ Eq (α := A ⊗[R] AddMonoidAlgebra B M)
    ((AddMonoidAlgebra.tensorEquiv.invFun : (a : AddMonoidAlgebra (A ⊗[R] B) M) → A ⊗[R] AddMonoidAlgebra B M)
        (single m (a ⊗ₜ[R] b)) :
      A ⊗[R] AddMonoidAlgebra B M)
    (a ⊗ₜ[R] single m b : A ⊗[R] B[M])

Tactic:
simp [AddMonoidAlgebra.tensorEquiv.invFun]

Premises used: AddMonoidAlgebra.tensorEquiv.invFun
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CommMonoid M
a : A
m : M
b : B
⊢ Eq (α := A ⊗[R] B[M]) ((invFun : (a : (A ⊗[R] B)[M]) → A ⊗[R] B[M]) (single m (a ⊗ₜ[R] b)) : A ⊗[R] B[M])
    (a ⊗ₜ[R] single m b : A ⊗[R] B[M])

Tactic:
simp [tensorEquiv.invFun]

Premises used: MonoidAlgebra.tensorEquiv.invFun
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_1 :
  Eq (α := (A ⊗[R] B)[M] →ₐ[A] (A ⊗[R] B)[M])
    (AlgHom.comp
      (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯ :
        A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
      (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M]))
    (AlgHom.id A (A ⊗[R] B)[M])
refine_2 :
  Eq (α := A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
    (AlgHom.comp tensorEquiv.invFun
        (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯) :
      A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
    (AlgHom.id A (A ⊗[R] B[M]) : A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
⊢ A ⊗[R] B[M] ≃ₐ[A] (A ⊗[R] B)[M]

Tactic:
refine .ofAlgHom
    (Algebra.TensorProduct.lift
      ((IsScalarTower.toAlgHom A (A ⊗[R] B) _).comp Algebra.TensorProduct.includeLeft)
      (mapAlgHom _ Algebra.TensorProduct.includeRight) fun p n ↦ .all ..)
      tensorEquiv.invFun ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_1 :
  Eq (α := (A ⊗[R] B)[M] →ₗ[A] (A ⊗[R] B)[M])
    (AlgHom.toLinearMap
      (AlgHom.comp
        (Algebra.TensorProduct.lift
            (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
            (mapAlgHom M includeRight) ⋯ :
          A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
        (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])))
    (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]))
⊢ Eq (α := (A ⊗[R] B)[M] →ₐ[A] (A ⊗[R] B)[M])
    (AlgHom.comp
      (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯ :
        A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
      (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M]))
    (AlgHom.id A (A ⊗[R] B)[M])

Tactic:
apply AlgHom.toLinearMap_injective

Premises used: AlgHom.toLinearMap_injective
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_1 :
  ∀ (x : M) (x_1 : B) (m : M),
    Eq (α := A ⊗[R] B)
      ((((((AlgebraTensorModule.curry
                          (AlgHom.toLinearMap
                              (AlgHom.comp
                                (Algebra.TensorProduct.lift
                                    (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M])
                                      includeLeft)
                                    (mapAlgHom M includeRight) ⋯ :
                                  A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
                                (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])) ∘ₗ
                            lsingle x) :
                        A →ₗ[A] B →ₗ[R] (A ⊗[R] B)[M]) :
                      (a : A) → B →ₗ[R] (A ⊗[R] B)[M])
                    1 :
                  (a : B) → (A ⊗[R] B)[M])
                x_1 :
              (A ⊗[R] B)[M]) :
            (a : M) → A ⊗[R] B)
          m :
        A ⊗[R] B)
      ((((((AlgebraTensorModule.curry (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]) ∘ₗ lsingle x) :
                        A →ₗ[A] B →ₗ[R] (A ⊗[R] B)[M]) :
                      (a : A) → B →ₗ[R] (A ⊗[R] B)[M])
                    1 :
                  (a : B) → (A ⊗[R] B)[M])
                x_1 :
              (A ⊗[R] B)[M]) :
            (a : M) → A ⊗[R] B)
          m :
        A ⊗[R] B)
⊢ Eq (α := (A ⊗[R] B)[M] →ₗ[A] (A ⊗[R] B)[M])
    (AlgHom.toLinearMap
      (AlgHom.comp
        (Algebra.TensorProduct.lift
            (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
            (mapAlgHom M includeRight) ⋯ :
          A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
        (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])))
    (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
x : M
x_1 : B
m : M
⊢ Eq (α := A ⊗[R] B)
    ((((((AlgebraTensorModule.curry
                        (AlgHom.toLinearMap
                            (AlgHom.comp
                              (Algebra.TensorProduct.lift
                                  (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M])
                                    includeLeft)
                                  (mapAlgHom M includeRight) ⋯ :
                                A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
                              (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])) ∘ₗ
                          lsingle x) :
                      A →ₗ[A] B →ₗ[R] (A ⊗[R] B)[M]) :
                    (a : A) → B →ₗ[R] (A ⊗[R] B)[M])
                  1 :
                (a : B) → (A ⊗[R] B)[M])
              x_1 :
            (A ⊗[R] B)[M]) :
          (a : M) → A ⊗[R] B)
        m :
      A ⊗[R] B)
    ((((((AlgebraTensorModule.curry (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]) ∘ₗ lsingle x) :
                      A →ₗ[A] B →ₗ[R] (A ⊗[R] B)[M]) :
                    (a : A) → B →ₗ[R] (A ⊗[R] B)[M])
                  1 :
                (a : B) → (A ⊗[R] B)[M])
              x_1 :
            (A ⊗[R] B)[M]) :
          (a : M) → A ⊗[R] B)
        m :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_2 :
  Eq (α := B[M] →ₐ[R] A ⊗[R] B[M])
    (AlgHom.comp (B := A ⊗[R] B[M])
      (AlgHom.restrictScalars R
        (AlgHom.comp tensorEquiv.invFun
            (Algebra.TensorProduct.lift
              (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
              (mapAlgHom M includeRight) ⋯) :
          A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
      includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight)
⊢ Eq (α := A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
    (AlgHom.comp tensorEquiv.invFun
        (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯) :
      A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
    (AlgHom.id A (A ⊗[R] B[M]) : A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_2 :
  Eq (α := B[M] →ₗ[R] A ⊗[R] B[M])
    (AlgHom.toLinearMap
      (AlgHom.comp (B := A ⊗[R] B[M])
        (AlgHom.restrictScalars R
          (AlgHom.comp tensorEquiv.invFun
              (Algebra.TensorProduct.lift
                (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
                (mapAlgHom M includeRight) ⋯) :
            A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
        includeRight))
    (AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight))
⊢ Eq (α := B[M] →ₐ[R] A ⊗[R] B[M])
    (AlgHom.comp (B := A ⊗[R] B[M])
      (AlgHom.restrictScalars R
        (AlgHom.comp tensorEquiv.invFun
            (Algebra.TensorProduct.lift
              (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
              (mapAlgHom M includeRight) ⋯) :
          A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
      includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight)

Tactic:
apply AlgHom.toLinearMap_injective

Premises used: AlgHom.toLinearMap_injective