-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x : R
x_1 : L
rw :
  (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (β := M) x
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
          (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
          ⋯) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (x •
          Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
      M)
rw₂ :
  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
      ⋯ =
    x •
      Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯
rw₃ :
  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
      ⋯ =
    Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (x • HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯
rw₄ :
  HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L) =
    x • HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
        (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x • x_1) : E.L) ((s₂ : (a : L) → E.L) (x • x_1) : E.L))
        ⋯) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) x : R)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw₅ : HSub.hSub (β := E.L) (HSMul.hSMul (β := E.L) x ((s₁ : (a : L) → E.L) x_1 : E.L))
    ((s₂ : (a : L) → E.L) (x • x_1) : E.L) =
  x • HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)
Tactic: rw [RingHom.id_apply, ← map_smul, EquivLike.apply_eq_iff_eq, SetLike.mk_smul_of_tower_mk,
      Subtype.mk_eq_mk, LinearMap.map_smul_of_tower, smul_sub, LinearMap.map_smul_of_tower]