-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
B : Type uR
inst : CommRing B
r : B → B → Prop
x : B
⊢ 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))
have 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) sorry
                        (x.toQuot (r := r)),
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry },
                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' := sorry, map_mul' := sorry,
                        map_zero' := sorry, map_add' := sorry })
                    sorry,
                left_inv := sorry, right_inv := sorry } :
              (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)) sorry) :
          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' := sorry, map_mul' := sorry, map_zero' := sorry,
            map_add' := sorry } :
          (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]