Theorem: AlgHom.quotientKerEquivRange_mk (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ (↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)) = φ.rangeRestrict
Tactic:
ext s
State after:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑(((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ))) s) = ↑(φ.rangeRestrict s)

State before:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑(((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ))) s) = ↑(φ.rangeRestrict s)
Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, coe_comp, AlgHom.coe_coe,
  Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply, coe_codRestrict]
State after:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑((Ideal.quotientKerEquivRange φ) ((Ideal.Quotient.mk (RingHom.ker φ)) s)) = φ s

State before:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑((Ideal.quotientKerEquivRange φ) ((Ideal.Quotient.mk (RingHom.ker φ)) s)) = φ s
Tactic:
rfl
State after:
no goals