-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A_1 : Type u_6
M_1 : Type u_7
N_1 : Type u_8
P : Type u_9
Q : Type u_10
S_1 : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M_1
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S_1
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M_1
inst_21 : Module R'' M_1
inst_22 : Module R M_1
inst_23 : Module R N_1
inst_24 : Module R S_1
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Module R P
inst_36 : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_37 : AddCommMonoid M
inst_38 : AddCommMonoid N
inst_39 : Module R M
inst_40 : Module R N
inst_41 : CommSemiring A
inst_42 : Module A M
inst_43 : Module A N
inst_44 : SMulCommClass R A M
inst_45 : CommSemiring S
inst_46 : Module S M
inst_47 : SMulCommClass R S M
inst_48 : SMulCommClass A S M
inst_49 : CompatibleSMul R A M N
s : S
x : M ⊗[A] N
zero :
  AddHom.toFun
      (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
        (lift
          {
            toFun := fun (m : M) ↦
              let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }))
      (HSMul.hSMul (β := M ⊗[A] N) s 0) =
    HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (M := M ⊗[A] N)
        (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
          (lift
            {
              toFun := fun (m : M) ↦
                let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
        0)
add :
  ∀ (x y : M ⊗[A] N),
    AddHom.toFun
          (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
            (lift
              {
                toFun := fun (m : M) ↦
                  let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ }))
          (s • x) =
        HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
          (AddHom.toFun
            (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
              (lift
                {
                  toFun := fun (m : M) ↦
                    let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                    { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
                  map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
            x) →
      AddHom.toFun
            (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
              (lift
                {
                  toFun := fun (m : M) ↦
                    let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                    { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ }))
            (s • y) =
          HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
            (AddHom.toFun
              (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
                (lift
                  {
                    toFun := fun (m : M) ↦
                      let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
                    map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
              y) →
        AddHom.toFun
            (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
              (lift
                {
                  toFun := fun (m : M) ↦
                    let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                    { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ }))
            (s • (x + y)) =
          HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
            (AddHom.toFun
              (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
                (lift
                  {
                    toFun := fun (m : M) ↦
                      let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
                    map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
              (x + y))
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
        (lift
          {
            toFun := fun (m : M) ↦
              let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }))
      (s • x) =
    HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun
        (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
          (lift
            {
              toFun := fun (m : M) ↦
                let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
        x)
have tmul : ∀ (x : M) (y : N),
  AddHom.toFun
      (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
        (lift
          {
            toFun := fun (m : M) ↦
              let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := sorry },
            map_add' := sorry, map_smul' := sorry }))
      (HSMul.hSMul (β := M ⊗[A] N) s (x ⊗ₜ[A] y)) =
    HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (M := M ⊗[A] N)
        (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
          (lift
            {
              toFun := fun (m : M) ↦
                let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := sorry : N →ₗ[A] M ⊗[R] N },
              map_add' := sorry, map_smul' := sorry : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
        (x ⊗ₜ[A] y))
Tactic: induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y => simp [smul_tmul']
Cleared hypotheses: x