-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
⊢ Eq.{v + 1} (α :=
    RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)) →ₐ[R] RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    (AlgHom.comp (B := RingQuot rel)
      ((liftAlgHom R (s := rel) :
          (a :
              { f_1 : A →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)) //
                ∀ ⦃x y : A⦄,
                  rel x y →
                    (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x =
                      (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y }) →
            RingQuot rel →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)))
        (Subtype.mk (p := fun (f_1 : A →ₐ[R] RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))) ↦
          ∀ ⦃x y : A⦄,
            rel x y →
              Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x :
                  RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y :
                  RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
          (AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B)) ⋯))
      ((liftAlgHom R (s := rel on (⇑f.symm : (a : B) → A)) :
          (a :
              { f_1 : B →ₐ[R] RingQuot rel //
                ∀ ⦃x y : B⦄,
                  (rel on (⇑f.symm : (a : B) → A)) x y →
                    (f_1 : (a : B) → RingQuot rel) x = (f_1 : (a : B) → RingQuot rel) y }) →
            RingQuot (rel on (⇑f.symm : (a : B) → A)) →ₐ[R] RingQuot rel)
        (Subtype.mk (p := fun (f_1 : B →ₐ[R] RingQuot rel) ↦
          ∀ ⦃x y : B⦄,
            (rel on (⇑f.symm : (a : B) → A)) x y →
              Eq (α := RingQuot rel) ((f_1 : (a : B) → RingQuot rel) x : RingQuot rel)
                ((f_1 : (a : B) → RingQuot rel) y : RingQuot rel))
          (AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A)) ⋯)))
    (AlgHom.id R (RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
have w : ∀ (b : B),
  Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (B := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
            (AlgHom.comp (B := RingQuot rel)
              ((liftAlgHom R (s := rel) :
                  (a :
                      { f_1 : A →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)) //
                        ∀ ⦃x y : A⦄,
                          rel x y →
                            (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x =
                              (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y }) →
                    RingQuot rel →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)))
                (Subtype.mk (p := fun (f_1 : A →ₐ[R] RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))) ↦
                  ∀ ⦃x y : A⦄,
                    rel x y →
                      Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                        ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x :
                          RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                        ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y :
                          RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
                  (AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B)) sorry))
              ((liftAlgHom R (s := rel on (⇑f.symm : (a : B) → A)) :
                  (a :
                      { f_1 : B →ₐ[R] RingQuot rel //
                        ∀ ⦃x y : B⦄,
                          (rel on (⇑f.symm : (a : B) → A)) x y →
                            (f_1 : (a : B) → RingQuot rel) x = (f_1 : (a : B) → RingQuot rel) y }) →
                    RingQuot (rel on (⇑f.symm : (a : B) → A)) →ₐ[R] RingQuot rel)
                (Subtype.mk (p := fun (f_1 : B →ₐ[R] RingQuot rel) ↦
                  ∀ ⦃x y : B⦄,
                    (rel on (⇑f.symm : (a : B) → A)) x y →
                      Eq (α := RingQuot rel) ((f_1 : (a : B) → RingQuot rel) x : RingQuot rel)
                        ((f_1 : (a : B) → RingQuot rel) y : RingQuot rel))
                  (AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A)) sorry)))
            (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) :
          (a : B) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        b :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (AlgHom.id R (RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
            (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) :
          (a : B) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        b :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
Tactic: ext b