-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : Pre R X
H :
  ∀ (a : X),
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          (Quot.mk (Rel R X) (Pre.of a)) :
        A)
      ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of a)) : A)
H₁ :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          (Quot.mk (Rel R X) (Pre.ofScalar x)) :
        A)
      ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.ofScalar x)) : A)
H₂ :
  ∀ (a b : Pre R X)
    (ha :
      Eq.{u_3 + 1} (α := A)
        ((liftAux R
                ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                    (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                  F) :
              (a : FreeAlgebra R X) → A)
            (Quot.mk (Rel R X) a) :
          A)
        ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) a) : A))
    (hb :
      Eq.{u_3 + 1} (α := A)
        ((liftAux R
                ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                    (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                  F) :
              (a : FreeAlgebra R X) → A)
            (Quot.mk (Rel R X) b) :
          A)
        ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) b) : A)),
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          (Quot.mk (Rel R X) (a.add b)) :
        A)
      ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (a.add b)) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) x) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) x) : A)
have H₃ : ∀ (a b : Pre R X)
  (ha :
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          (Quot.mk (Rel R X) a) :
        A)
      ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) a) : A))
  (hb :
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          (Quot.mk (Rel R X) b) :
        A)
      ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) b) : A)),
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) (a.mul b)) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (a.mul b)) : A)
Tactic: induction x with
      | of =>
        change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
        simp only [Function.comp_apply, ι_def]
      | ofScalar x =>
        change algebraMap _ _ x = F (algebraMap _ _ x)
        rw [AlgHom.commutes F _]
      | add a b ha hb =>
        -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
        -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
        grind
      | mul a b ha hb =>
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        grind
Cleared hypotheses: x