A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ↑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : comp h f = g
⊢ h = ↑(liftOfRightInverse f f_inv hf) { val := comp h f, property := (_ : (fun g => ker f ≤ ker g) (comp h f)) }
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ↑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : comp h f = g
⊢ h = ↑(liftOfRightInverse f f_inv hf) { val := g, property := hg }
simp_rw [← hh]
no goals
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ↑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : comp h f = g
⊢ h = ↑(liftOfRightInverse f f_inv hf) { val := comp h f, property := (_ : (fun g => ker f ≤ ker g) (comp h f)) }
exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm