G : Type ?u.666706
G' : Type ?u.666709
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.666718
inst✝³ : AddGroup A
G₁ : Type u_1
G₂ : Type u_2
G₃ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : Function.RightInverse f_inv ↑f
g : G₁ →* G₃
hg : ker f ≤ ker g
h : G₂ →* G₃
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)) }
G : Type ?u.666706
G' : Type ?u.666709
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.666718
inst✝³ : AddGroup A
G₁ : Type u_1
G₂ : Type u_2
G₃ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : Function.RightInverse f_inv ↑f
g : G₁ →* G₃
hg : ker f ≤ ker g
h : G₂ →* G₃
hh : comp h f = g
⊢ h = ↑(liftOfRightInverse f f_inv hf) { val := g, property := hg }
simp_rw [← hh]
no goals
G : Type ?u.666706
G' : Type ?u.666709
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.666718
inst✝³ : AddGroup A
G₁ : Type u_1
G₂ : Type u_2
G₃ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : Function.RightInverse f_inv ↑f
g : G₁ →* G₃
hg : ker f ≤ ker g
h : G₂ →* G₃
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