case mp
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b
constructor
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a} ∧ f a = b
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b
intro h
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ a, s = {a} ∧ f a = b
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a} ∧ f a = b
obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ a, s = {a} ∧ f a = b
refine' ⟨a, ha, _⟩
no goals
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b
rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a}
rw [← card_eq_one, ← card_map, h, card_singleton]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
a : α
⊢ map f {a} = {f a}
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}
rintro ⟨a, rfl, rfl⟩
no goals
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.121890
f : α → β
a : α
⊢ map f {a} = {f a}
simp