Theorem: quotient_mk_eq_ofRel (DividedPowers/DPAlgebra/Misc.lean)

State before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ (Ideal.Quotient.mk (ofRel r)) a = (Ideal.Quotient.mk (ofRel r)) b
Tactic:
suffices hinj : Function.Injective (RingQuot.ringQuotEquivIdealQuotient r).invFun by
  apply hinj; exact mkRingHom_rel h
State after:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.Injective (ringQuotEquivIdealQuotient r).invFun

State before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.Injective (ringQuotEquivIdealQuotient r).invFun
Tactic:
rw [Function.injective_iff_hasLeftInverse]
State after:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.HasLeftInverse (ringQuotEquivIdealQuotient r).invFun

State before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
⊢ Function.HasLeftInverse (ringQuotEquivIdealQuotient r).invFun
Tactic:
exact ⟨(ringQuotEquivIdealQuotient r).toFun, (ringQuotEquivIdealQuotient r).right_inv⟩
State after:
no goals

State before:
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
hinj : Function.Injective (ringQuotEquivIdealQuotient r).invFun
⊢ (Ideal.Quotient.mk (ofRel r)) a = (Ideal.Quotient.mk (ofRel r)) b
Tactic:
apply hinj
State after:
case a
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
hinj : Function.Injective (ringQuotEquivIdealQuotient r).invFun
⊢ (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) a) =
    (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) b)

State before:
case a
A : Type u_1
inst✝ : CommRing A
r : A → A → Prop
a b : A
h : r a b
hinj : Function.Injective (ringQuotEquivIdealQuotient r).invFun
⊢ (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) a) =
    (ringQuotEquivIdealQuotient r).invFun ((Ideal.Quotient.mk (ofRel r)) b)
Tactic:
exact mkRingHom_rel h
State after:
no goals