α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
⊢ Surjective (map f)
intro s
case empty
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s
induction' s using Multiset.induction_on with x s ih
no goals
case empty
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0
exact ⟨0, map_zero _⟩
case cons.intro
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ a, map f a = s
y : α
⊢ ∃ a, map f a = f y ::ₘ s
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s
obtain ⟨y, rfl⟩ := hf x
case cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t
case cons.intro
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ a, map f a = s
y : α
⊢ ∃ a, map f a = f y ::ₘ s
obtain ⟨t, rfl⟩ := ih
no goals
case cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.129073
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t
exact ⟨y ::ₘ t, map_cons _ _ _⟩