-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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
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)) ⋯))
                ((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)) ⋯)))
              (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)))
⊢ 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))))

Tactic:
ext b