case mk.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, ↑(rangeKerLift φ) a = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ↑(rangeKerLift φ)
rintro ⟨_, g, rfl⟩
case mk.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ↑(rangeKerLift φ) ↑g = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
case mk.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, ↑(rangeKerLift φ) a = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
use mk g
no goals
case mk.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ↑(rangeKerLift φ) ↑g = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
rfl