n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this :
  RingHom.comp
      (↑(RingHom.liftOfRightInverse f cast (_ : Function.RightInverse cast ↑f))
        { val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) })
      f =
    ↑{ val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) }
⊢ f = g
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
⊢ f = g
have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this :
  RingHom.comp
      (↑(RingHom.liftOfRightInverse f cast (_ : Function.RightInverse cast ↑f))
        { val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) })
      f =
    g
⊢ f = g
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this :
  RingHom.comp
      (↑(RingHom.liftOfRightInverse f cast (_ : Function.RightInverse cast ↑f))
        { val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) })
      f =
    ↑{ val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) }
⊢ f = g
rw [Subtype.coe_mk] at this
no goals
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this :
  RingHom.comp
      (↑(RingHom.liftOfRightInverse f cast (_ : Function.RightInverse cast ↑f))
        { val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) })
      f =
    g
⊢ f = g
rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]