-- Module: Mathlib.Algebra.RingQuot
Goal:
B : Type uR
inst : CommRing B
r : B → B → Prop
x : B
simp_rw :
  Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    (((({
                  toFun :=
                    fun
                      (f :
                        { f : B →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r) //
                          ∀ ⦃x y : B⦄,
                            r x y →
                              Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
                                ((f : (a : B) → B ⧸ Ideal.ofRel r) x :
                                  HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
                                ((f : (a : B) → B ⧸ Ideal.ofRel r) y :
                                  HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)) }) ↦
                    {
                      toFun := fun (x : RingQuot r) ↦
                        Quot.lift (r := Rel r) (⇑(↑f : B →+* B ⧸ Ideal.ofRel r) : (a : B) → B ⧸ Ideal.ofRel r) ⋯
                          (x.toQuot (r := r)),
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
                  invFun := fun (F : RingQuot r →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)) ↦
                    Subtype.mk (p := fun (f : B →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)) ↦
                      ∀ ⦃x y : B⦄,
                        r x y →
                          Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
                            ((f : (a : B) → B ⧸ Ideal.ofRel r) x :
                              HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
                            ((f : (a : B) → B ⧸ Ideal.ofRel r) y :
                              HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)))
                      (F.comp
                        { toFun := fun (x : B) ↦ mk (r := r) (Quot.mk (Rel r) x), map_one' := ⋯, map_mul' := ⋯,
                          map_zero' := ⋯, map_add' := ⋯ })
                      ⋯,
                  left_inv := ⋯, right_inv := ⋯ } :
                (a :
                    { f : B →+* B ⧸ Ideal.ofRel r //
                      ∀ ⦃x y : B⦄,
                        r x y → (f : (a : B) → B ⧸ Ideal.ofRel r) x = (f : (a : B) → B ⧸ Ideal.ofRel r) y }) →
                  RingQuot r →+* B ⧸ Ideal.ofRel r)
              (Subtype.mk (p := fun (f : B →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)) ↦
                ∀ ⦃x y : B⦄,
                  r x y →
                    Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
                      ((f : (a : B) → B ⧸ Ideal.ofRel r) x : HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
                      ((f : (a : B) → B ⧸ Ideal.ofRel r) y : HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)))
                (Ideal.Quotient.mk (Ideal.ofRel r)) ⋯) :
            RingQuot r →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)) :
          (a : RingQuot r) → B ⧸ Ideal.ofRel r)
        (({ toFun := fun (x : B) ↦ mk (r := r) (Quot.mk (Rel r) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
              map_add' := ⋯ } :
            (a : B) → RingQuot r)
          x) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    ((Ideal.Quotient.mk (Ideal.ofRel r) : (a : B) → B ⧸ Ideal.ofRel r) x :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
⊢ Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    ((ringQuotToIdealQuotient r : (a : RingQuot r) → B ⧸ Ideal.ofRel r) ((mkRingHom r : (a : B) → RingQuot r) x) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    ((Ideal.Quotient.mk (Ideal.ofRel r) : (a : B) → B ⧸ Ideal.ofRel r) x :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))

Tactic:
simp_rw [ringQuotToIdealQuotient, lift_def, preLift_def, mkRingHom_def]

Premises used: RingQuot.preLift_def, RingQuot.mkRingHom_def, RingQuot.lift_def, RingQuot.ringQuotToIdealQuotient