Theorem: Ideal.quotient_mk_eq_ringQuot_apply (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
r : A → A → Prop
a : A
⊢ (Quotient.mk (ofRel r)) a = (ringQuotToIdealQuotient r) ((mkAlgHom R r) a)
Tactic:
rw [← ringQuotToIdealQuotient_apply r a, ← mkAlgHom_coe R r]
State after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
r : A → A → Prop
a : A
⊢ (ringQuotToIdealQuotient r) (↑(mkAlgHom R r) a) = (ringQuotToIdealQuotient r) ((mkAlgHom R r) a)

State before:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
r : A → A → Prop
a : A
⊢ (ringQuotToIdealQuotient r) (↑(mkAlgHom R r) a) = (ringQuotToIdealQuotient r) ((mkAlgHom R r) a)
Tactic:
rfl
State after:
no goals