-- Lean 4 proof step from Mathlib.Algebra.Lie.Free (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
f : X → L
a b : lib R X
h : Rel R X a b
lie_self :
  ∀ (a' : lib R X),
    Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a' * a') : CommutatorRing L)
      ((liftAux R f : (a : lib R X) → CommutatorRing L) 0 : CommutatorRing L)
leibniz_lie :
  ∀ (a' b' c' : lib R X),
    Eq.{w + 1} (α := CommutatorRing L)
      ((liftAux R f : (a : lib R X) → CommutatorRing L) (a' * (b' * c')) : CommutatorRing L)
      ((liftAux R f : (a : lib R X) → CommutatorRing L) (a' * b' * c' + b' * (a' * c')) : CommutatorRing L)
smul :
  ∀ (b' : R) {a b : lib R X},
    Rel R X a b →
      ∀
        (h₂ :
          Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)
            ((liftAux R f : (a : lib R X) → CommutatorRing L) b : CommutatorRing L)),
        Eq.{w + 1} (α := CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • a) : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b' • b) : CommutatorRing L)
add_right :
  ∀ {a b : lib R X} (c' : lib R X),
    Rel R X a b →
      ∀
        (h₂ :
          Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)
            ((liftAux R f : (a : lib R X) → CommutatorRing L) b : CommutatorRing L)),
        Eq.{w + 1} (α := CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (a + c') : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (b + c') : CommutatorRing L)
mul_left :
  ∀ (c' : lib R X) {b c : lib R X},
    Rel R X b c →
      ∀
        (h₂ :
          Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) b : CommutatorRing L)
            ((liftAux R f : (a : lib R X) → CommutatorRing L) c : CommutatorRing L)),
        Eq.{w + 1} (α := CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (c' * b) : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) (c' * c) : CommutatorRing L)
⊢ Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)
    ((liftAux R f : (a : lib R X) → CommutatorRing L) b : CommutatorRing L)
have mul_right : ∀ {a b : lib R X} (c' : lib R X),
  Rel R X a b →
    ∀
      (h₂ :
        Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) a : CommutatorRing L)
          ((liftAux R f : (a : lib R X) → CommutatorRing L) b : CommutatorRing L)),
      Eq.{w + 1} (α := CommutatorRing L) ((liftAux R f : (a : lib R X) → CommutatorRing L) (a * c') : CommutatorRing L)
        ((liftAux R f : (a : lib R X) → CommutatorRing L) (b * c') : CommutatorRing L)
Tactic: induction h with
  | lie_self a' => simp only [liftAux_map_mul, map_zero, lie_self]
  | leibniz_lie a' b' c' =>
    simp only [liftAux_map_mul, liftAux_map_add, sub_add_cancel, lie_lie]
  | smul b' _ h₂ => simp only [liftAux_map_smul, h₂]
  | add_right c' _ h₂ => simp only [liftAux_map_add, h₂]
  | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
  | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
Cleared hypotheses: h