awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y x_1 x_2 : N
ha :
  Eq (α := N)
    ((IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) : (a : N) → N) x_1 : N)
    (((↑R :
              {S : Type v₃} →
                {M M₂ : Type v₂} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
          (a : N) → N)
        x_1 :
      N)
hb :
  Eq (α := N)
    ((IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) : (a : N) → N) x_2 : N)
    (((↑R :
              {S : Type v₃} →
                {M M₂ : Type v₂} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
          (a : N) → N)
        x_2 :
      N)
⊢ Eq (α := N)
    ((IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x) : (a : N) → N)
        (x_1 + x_2) :
      N)
    (((↑R :
              {S : Type v₃} →
                {M M₂ : Type v₂} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x)) :
          (a : N) → N)
        (x_1 + x_2) :
      N)

Tactic:
simp [ha, hb]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
x y : S ⊗[R] R'
dsimp :
  (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (x * y) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') x : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y : S')
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
      (x * y) =
    HMul.hMul (α := S')
      (AddHom.toFun
        (LinearMap.toAddHom (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
        x)
      (AddHom.toFun
        (LinearMap.toAddHom (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
        y)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
y : S ⊗[R] R'
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (0 * y) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') 0 : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y : S')

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
y_1 x y : S ⊗[R] R'
h_2 :
  (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (x * y_1) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') x : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y_1 : S')
h_3 :
  (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (y * y_1) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y_1 : S')
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') ((x + y) * y_1) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (x + y) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y_1 : S')

Tactic:
simp [*, add_mul]

Premises used: add_mul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
a : S
b : R'
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S')
      (HMul.hMul (α := S ⊗[R] R') (a ⊗ₜ[R] b) 0) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') 0 : S')

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
a : S
b : R'
x y : S ⊗[R] R'
h_2 :
  (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b * x) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') x : S')
h_3 :
  (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b * y) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') y : S')
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b * (x + y)) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (x + y) : S')

Tactic:
simp [*, mul_add]

Premises used: mul_add
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
a : S
b : R'
x : S
y : R'
⊢ (IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S')
      (HMul.hMul (α := S ⊗[R] R') (a ⊗ₜ[R] b) (x ⊗ₜ[R] y)) =
    HMul.hMul (α := S') (β := S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) : S')
      ((IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯ : (a : S ⊗[R] R') → S') (x ⊗ₜ[R] y) : S')

Tactic:
simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, IsBaseChange.equiv_tmul, Algebra.smul_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h_1 : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
h : IsPushout R S R' S'
⊢ ∀ (r : S),
    Eq.{u_7 + 1} (α := S')
      (AddHom.toFun (M := S ⊗[R] R')
          (LinearMap.toAddHom
            (↑(IsBaseChange.equiv (f := AlgHom.toLinearMap (toAlgHom R R' S')) ⋯) : S ⊗[R] R' →ₗ[S] S'))
          ((algebraMap S (S ⊗[R] R') : (a : S) → S ⊗[R] R') r) :
        S')
      ((algebraMap S S' : (a : S) → S') r : S')

Tactic:
simp [IsBaseChange.equiv_tmul, Algebra.smul_def]

Premises used: IsBaseChange.equiv_tmul, Algebra.smul_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsPushout R S R' S'
a : S
b : R'
⊢ (equiv R S R' S' : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] b) =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap R' S' : (a : R') → S') b : S')

Tactic:
(h.out.equiv_tmul _ _).trans (Algebra.smul_def _ _)

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Algebra.IsPushout.out, IsBaseChange.equiv_tmul, Algebra.smul_def, FreeAddMonoid.sumAux, Eq.trans
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
a : S
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (a ⊗ₜ[R] 1) : S')
rw₁ :
  (algebraMap S S' : (a : S) → S') a =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap R' S' : (a : R') → S') 1 : S')
rw₂ :
  (algebraMap S S' : (a : S) → S') a = HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') a : S') (1 : S')
rw₃ rw₄ : Eq.{u_7 + 1} (α := S') ((algebraMap S S' : (a : S) → S') a : S') ((algebraMap S S' : (a : S) → S') a : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap S S' : (a : S) → S') a) : S ⊗[R] R')
    (a ⊗ₜ[R] 1 : S ⊗[R] R')

Tactic:
rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]

Premises used: AlgEquiv.symm_apply_eq, Algebra.IsPushout.equiv, Algebra.IsPushout.equiv_tmul, map_one, mul_one
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
a : R'
rw :
  Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S')
    ((equiv R S R' S' : (a : S ⊗[R] R') → S') (1 ⊗ₜ[R] a) : S')
rw₁ :
  (algebraMap R' S' : (a : R') → S') a =
    HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') 1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
rw₂ :
  (algebraMap R' S' : (a : R') → S') a =
    HMul.hMul (α := S') (β := S') (1 : S') ((algebraMap R' S' : (a : R') → S') a : S')
rw₃ rw₄ : Eq.{u_7 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') a : S') ((algebraMap R' S' : (a : R') → S') a : S')
⊢ Eq (α := S ⊗[R] R')
    ((AlgEquiv.symm (equiv R S R' S') : (a : S') → S ⊗[R] R') ((algebraMap R' S' : (a : R') → S') a) : S ⊗[R] R')
    (1 ⊗ₜ[R] a : S ⊗[R] R')

Tactic:
rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]

Premises used: AlgEquiv.symm_apply_eq, Algebra.IsPushout.equiv, Algebra.IsPushout.equiv_tmul, map_one, one_mul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsPushout R S R' S'
x_1 : R'
x : R' ⊗[R] S
⊢ Equiv.toFun
      (AddEquiv.toEquiv
        (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S)) (AlgEquiv.toAddEquiv (equiv R S R' S'))))
      (HSMul.hSMul (β := R' ⊗[R] S) x_1 0) =
    HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x_1 : R')
      (Equiv.toFun (α := R' ⊗[R] S)
        (AddEquiv.toEquiv
          (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S)) (AlgEquiv.toAddEquiv (equiv R S R' S'))))
        0)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsPushout R S R' S'
x_1 : R'
x : R' ⊗[R] S
x_2 : R'
x_3 : S
⊢ Equiv.toFun
      (AddEquiv.toEquiv
        (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S)) (AlgEquiv.toAddEquiv (equiv R S R' S'))))
      (HSMul.hSMul (β := R' ⊗[R] S) x_1 (x_2 ⊗ₜ[R] x_3)) =
    HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x_1 : R')
      (Equiv.toFun (α := R' ⊗[R] S)
        (AddEquiv.toEquiv
          (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S)) (AlgEquiv.toAddEquiv (equiv R S R' S'))))
        (x_2 ⊗ₜ[R] x_3))

Tactic:
simp [equiv_tmul, Algebra.smul_def, mul_left_comm]

Premises used: mul_left_comm, Algebra.IsPushout.equiv_tmul, Algebra.smul_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsPushout R S R' S'
x_1 : R'
x : R' ⊗[R] S
⊢ ∀ (x y : R' ⊗[R] S),
    Equiv.toFun
          (AddEquiv.toEquiv
            (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S)) (AlgEquiv.toAddEquiv (equiv R S R' S'))))
          (x_1 • x) =
        HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x_1 : R')
          (Equiv.toFun
            (AddEquiv.toEquiv
              (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S))
                (AlgEquiv.toAddEquiv (equiv R S R' S'))))
            x) →
      Equiv.toFun
            (AddEquiv.toEquiv
              (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S))
                (AlgEquiv.toAddEquiv (equiv R S R' S'))))
            (x_1 • y) =
          HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x_1 : R')
            (Equiv.toFun
              (AddEquiv.toEquiv
                (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S))
                  (AlgEquiv.toAddEquiv (equiv R S R' S'))))
              y) →
        Equiv.toFun
            (AddEquiv.toEquiv
              (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S))
                (AlgEquiv.toAddEquiv (equiv R S R' S'))))
            (x_1 • (x + y)) =
          HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x_1 : R')
            (Equiv.toFun
              (AddEquiv.toEquiv
                (AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S))
                  (AlgEquiv.toAddEquiv (equiv R S R' S'))))
              (x + y))

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h : IsPushout R S R' S'
x : S
⊢ Eq.{u_7 + 1} (α := S')
    ((let __spread.0 : R' ⊗[R] S ≃+ S' :=
            AddEquiv.trans (AlgEquiv.toAddEquiv (TensorProduct.comm R R' S)) (AlgEquiv.toAddEquiv (equiv R S R' S'));
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ } :
          (a : R' ⊗[R] S) → S')
        (1 ⊗ₜ[R] x) :
      S')
    ((AlgHom.toLinearMap (toAlgHom R S S') : (a : S) → S') x : S')

Tactic:
simp [equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul