-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x y : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    x
hy :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    y
hxx :
  ∀ (a : A),
    Eq.{u_3 + 1} (α := A')
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
            (a : Derivation R A' A') → Derivation R A A')
          x.1))
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
            (a : Derivation R A A) → Derivation R A A')
          x.2))
hyy :
  ∀ (a : A),
    Eq.{u_3 + 1} (α := A')
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
            (a : Derivation R A' A') → Derivation R A A')
          y.1))
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
            (a : Derivation R A A) → Derivation R A A')
          y.2))
⊢ Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    ⁅x, y⁆
have H : ∀ (z : A),
  Eq.{u_3 + 1} (α := A')
    (((((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                (a : Derivation R A' A') → Derivation R A A')
              ⁅x, y⁆.1 :
            Derivation R A A') :
          (a : A) → A')
        z :
      A')
    (((((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                (a : Derivation R A A) → Derivation R A A')
              ⁅x, y⁆.2 :
            Derivation R A A') :
          (a : A) → A')
        z :
      A')
Tactic: ext z