-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M'_1 : Type u_7
M''_1 : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'_1
inst_4 : Module R_1 M'_1
ι : Type u_10
R_2 : Type u_11
M_2 : Type u_12
inst_5 : Semiring R_2
inst_6 : AddCommMonoid M_2
inst_7 : Module R_2 M_2
b_1 : Basis ι R_2 M_2
inst_8 : Module R_2 M'_1
i_1 : ι
M'' : Type u_13
b'_1 : Basis ι' R_2 M'_1
e : ι ≃ ι'
inst_9 : AddCommMonoid M''
inst_10 : Module R_2 M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst_11 : CommSemiring R
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : AddCommMonoid M'
inst_15 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_16 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι'
i' : ι
hi' : (b : (a : ι) → M) i' = g ((b' : (a : ι') → M') i)
rw :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
            ((b' : (a : ι') → M') i : M') :
          M) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₁ :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        ((g ∘ (⇑b' : (a : ι') → M')) i) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₂ :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        (g ((b' : (a : ι') → M') i)) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₃ :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        ((b : (a : ι) → M) i' : M) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₄ : (f ∘ (⇑b : (a : ι) → M)) i' = (LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M')
rw₅ : f ((b : (a : ι) → M) i') = (LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M')
rw₆ : f (g ((b' : (a : ι') → M') i)) = (LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M')
rw₇ :
  Eq.{u_16 + 1} (α := M') ((b' : (a : ι') → M') i : M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
⊢ Eq.{u_16 + 1} (α := M')
    (((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) ∘ₗ
            (b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) :
          (a : M') → M')
        ((b' : (a : ι') → M') i : M') :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
have rw₈ : Eq.{u_16 + 1} (α := M') ((b' : (a : ι') → M') i : M') ((b' : (a : ι') → M') i : M')
Tactic: rw [LinearMap.comp_apply, b'.constr_basis, Function.comp_apply, ← hi', b.constr_basis,
              Function.comp_apply, hi', hfg, LinearMap.id_apply]