-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq :
  Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯ =
    Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a k) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a l) ⋯
rw :
  ((algebraMap R K : R →+* K) : (a : R) → K)
      (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R)
        ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R)) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    (((algebraMap R K : R →+* K) : (a : R) → K)
        (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R)
          ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R)) :
      K)
    (((algebraMap R K : R →+* K) : (a : R) → K)
        (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R)
          ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R)) :
      K)
rw₂ :
  Eq.{u_6 + 1} (α := K)
    (((algebraMap R K : R →+* K) : (a : R) → K)
        ((f : (a : ↥E) → R)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯ -
              Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) :
          R) :
      K)
    (((algebraMap R K : R →+* K) : (a : R) → K)
        (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R)
          ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R)) :
      K)
⊢ HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R) :
        K) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
have rw₃ : Eq.{u_6 + 1} (α := K)
  (((algebraMap R K : R →+* K) : (a : R) → K)
      ((f : (a : ↥E) → R)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) sorry -
            Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) sorry) :
        R) :
    K)
  (((algebraMap R K : R →+* K) : (a : R) → K)
      ((f : (a : ↥E) → R)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) sorry -
            Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) sorry) :
        R) :
    K)
Tactic: rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]