-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
w : W
h :
  Eq.{u_6 + 1} (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) 0 : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        0 :
      W)
h₁ :
  ∀ (x y : W)
    (hx :
      Eq (α := W)
        ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) x : W)
        (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
              (a : W) → W)
            x :
          W))
    (hy :
      Eq (α := W)
        ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) y : W)
        (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
              (a : W) → W)
            y :
          W)),
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (x + y) :
        W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          (x + y) :
        W)
h₂ :
  ∀ (a : A) (w : W)
    (hw :
      Eq (α := W)
        ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
        (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
              (a : W) → W)
            w :
          W)),
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (a • w) :
        W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          (a • w) :
        W)
⊢ Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        w :
      W)
have h₃ : ∀ (x : V),
  Eq.{u_6 + 1} (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W)
        ((ε : (a : V) → W) x : W) :
      W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        ((ε : (a : V) → W) x : W) :
      W)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul a w hw => simp [hw]
  | tmul x => simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]
Cleared hypotheses: w