-- 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' = f ((b : (a : ι) → M) i)
rw :
  Eq.{u_15 + 1} (α := M)
    ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → 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') :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
rw₁ :
  Eq.{u_15 + 1} (α := M)
    ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
        ((f ∘ (⇑b : (a : ι) → M)) i) :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
rw₂ :
  Eq.{u_15 + 1} (α := M)
    ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
        (f ((b : (a : ι) → M) i)) :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
rw₃ :
  Eq.{u_15 + 1} (α := 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)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
rw₄ : (g ∘ (⇑b' : (a : ι') → M')) i' = (LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M)
rw₅ : g ((b' : (a : ι') → M') i') = (LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M)
⊢ Eq.{u_15 + 1} (α := M)
    (((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) ∘ₗ
            (b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑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₆ : g (f ((b : (a : ι) → M) i)) = (LinearMap.id : (a : M) → 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', hgf, LinearMap.id_apply]