-- Lean 4 proof step from Mathlib.Algebra.Lie.EngelSubalgebra (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H :=
  {
    toFun := fun (n : ℕ) ↦
      LinearMap.ker (HPow.hPow (α := Module.End R ↥H) ((ad R ↥H : (a : ↥H) → Module.End R ↥H) x : Module.End R ↥H) n),
    monotone' := ⋯ }
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H)
        ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H)
y : ↥H
m : ℕ
hm :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) m : (a : L) → L)
        (↑y : L) :
      L)
    (0 : L)
hmn : n ≤ m
this :
  ∀ (k : ℕ),
    Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
              (a : L) → L)
            (↑y : L) :
          L)
        (0 : L) ↔
      Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y
h :
  ∀ (hm : Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) m : Submodule R ↥H) y) (hmn : n ≤ m)
    (this :
      ∀ (k : ℕ),
        Eq (α := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
                  (a : L) → L)
                (↑y : L) :
              L)
            (0 : L) ↔
          Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
h₁ :
  ∀ (hm : Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) n : Submodule R ↥H) y) (hmn : n ≤ m)
    (this :
      ∀ (k : ℕ),
        Eq (α := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
                  (a : L) → L)
                (↑y : L) :
              L)
            (0 : L) ↔
          Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
have h₂ : ∀
  (hm :
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
          (↑y : L) :
        L)
      (0 : L))
  (hmn : n ≤ m)
  (this :
    ∀ (k : ℕ),
      Eq (α := L)
          ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) k :
                (a : L) → L)
              (↑y : L) :
            L)
          (0 : L) ↔
        Membership.mem (γ := Submodule R ↥H) ((K : (a : ℕ) → Submodule R ↥H) k : Submodule R ↥H) y),
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n : (a : L) → L)
        (↑y : L) :
      L)
    ((↑((0 : (a : ↥H) → ↥H) y) : L) : L)
Tactic: rwa [this, ← hn m hmn, ← this] at hm
Cleared hypotheses: hm, hmn, this