-- 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
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
f : Dual R V
w : W
a :
  Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) 0 : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        0 :
      A)
a₁ :
  ∀ (v : V),
    Eq.{u_4 + 1} (α := A)
      ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A)
          ((j : (a : V) → W) v : W) :
        A)
      (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
                ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                  ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                        (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                      (1 ⊗ₜ[R] f) :
                    A ⊗[R] (ι → R))) :
              W →ₗ[A] A) :
            (a : W) → A)
          ((j : (a : V) → W) v : W) :
        A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) w : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        w :
      A)
have a₂ : ∀ (a : A) (w : W)
  (h :
    Eq.{u_4 + 1} (α := A)
      ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) w : A)
      (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
                ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                  ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                        (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                      (1 ⊗ₜ[R] f) :
                    A ⊗[R] (ι → R))) :
              W →ₗ[A] A) :
            (a : W) → A)
          w :
        A)),
  Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) (a • w) : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        (a • w) :
      A)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | tmul v =>
    simp only [toDualBaseChangeAux_tmul, one_mul]
    conv_lhs => rw [← Basis.sum_equivFun b v, map_sum]
    simp [LinearEquiv.baseChange, basis_repr_comp_apply]
  | smul a w h => simp [h]
  | add x y hx hy => simp [map_add, hx, hy]
Cleared hypotheses: w