-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
g : A ⊗[R] Dual R V
zero :
  AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (HSMul.hSMul (β := A ⊗[R] Dual R V) a 0) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun (M := A ⊗[R] Dual R V)
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        0)
add :
  ∀ (x y : A ⊗[R] Dual R V)
    (hx :
      AddHom.toFun
          (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
            (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
          (a • x) =
        HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
          (AddHom.toFun
            (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
              (TensorProduct.lift
                { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ :
                  A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
            x))
    (hy :
      AddHom.toFun
          (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
            (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
          (a • y) =
        HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
          (AddHom.toFun
            (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
              (TensorProduct.lift
                { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ :
                  A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
            y)),
    AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
        (a • (x + y)) =
      HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
        (AddHom.toFun
          (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
            (TensorProduct.lift
              { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ :
                A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
          (x + y))
tmul :
  ∀ (b : A) (f : Dual R V),
    AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
        (HSMul.hSMul (β := A ⊗[R] Dual R V) a (b ⊗ₜ[R] f)) =
      HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
        (AddHom.toFun (M := A ⊗[R] Dual R V)
          (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
            (TensorProduct.lift
              { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ :
                A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
          (b ⊗ₜ[R] f))
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (a • g) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        g)

Tactic:
induction g using TensorProduct.induction_on with
    | zero => simp
    | add x y hx hy => aesop
    | tmul b f => simp [TensorProduct.smul_tmul', mul_smul]

Premises used: TensorProduct.smul_tmul', TensorProduct.tmul, SemigroupAction.mul_smul