-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
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))
⊢ 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)
have 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' := sorry, map_smul' := sorry }))
      (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' := sorry, map_smul' := sorry : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        (b ⊗ₜ[R] f))
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]
Cleared hypotheses: g