-- 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
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)
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)
a₃ :
  ∀ (x y : W)
    (hx :
      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) x : 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)
            x :
          A))
    (hy :
      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) y : 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)
            y :
          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) (x + y) :
        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)
          (x + y) :
        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)

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]

Premises used: IsBaseChange.basis_repr_comp_apply, map_add, map_sum, LinearEquiv.baseChange, TensorProduct.tmul, _private.0.IsBaseChange.toDualBaseChangeAux_tmul, one_mul