-- 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'
a : S
b : R'
tmul :
  (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')
tmul₁ :
  ∀ (x y : S ⊗[R] R'),
    (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') →
      (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')
tmul₂ :
  ∀ (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')
⊢ (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')

Tactic:
induction y with
      | zero => simp
      | add x y _ _ => simp [*, mul_add]
      | tmul x y => simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, IsBaseChange.equiv_tmul, Algebra.smul_def, mul_add, TensorProduct.tmul