case mp
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} → Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a

case mpr
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ (Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a) → s = {a}
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} ↔ Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a
constructor
case mp
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s : Finset α
a✝ b a : α
⊢ Finset.Nonempty {a} ∧ ∀ (x : α), x ∈ {a} → x = a
case mp
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} → Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a
rintro rfl
no goals
case mp
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s : Finset α
a✝ b a : α
⊢ Finset.Nonempty {a} ∧ ∀ (x : α), x ∈ {a} → x = a
simp
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ s = {a}
case mpr
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ (Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a) → s = {a}
rintro ⟨hne, h_uniq⟩
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ s = {a}
rw [eq_singleton_iff_unique_mem]
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ a ∈ s
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
refine' ⟨_, h_uniq⟩
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ Exists.choose hne ∈ s
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ a ∈ s
rw [← h_uniq hne.choose hne.choose_spec]
no goals
case mpr.intro
α : Type u_1
β : Type ?u.30920
γ : Type ?u.30923
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ Exists.choose hne ∈ s
exact hne.choose_spec