Theorem: Tutorial.GroupHom.rangeKerLift_surjective (Tutorial/Advanced/Algebra/Lecture5.lean)

State before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ Function.Surjective ⇑(rangeKerLift f)
Tactic:
intro ⟨y, hy⟩
State after:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
hy : y ∈ range f
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := hy }

State before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
hy : y ∈ range f
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := hy }
Tactic:
sorry
State after:
no goals