Theorem: Tutorial.GroupHom.rangeKerLift_surjective (Solution/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:
rcases hy with ⟨x, hxy⟩
State after:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := ⋯ }

State before:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := ⋯ }
Tactic:
exists LeftQuotient.mk x
State after:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ (rangeKerLift f) (LeftQuotient.mk x) = { val := y, property := ⋯ }

State before:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ (rangeKerLift f) (LeftQuotient.mk x) = { val := y, property := ⋯ }
Tactic:
simpa
State after:
no goals