α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
h : ncard s = 1
⊢ ∃ a, s = {a}
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
⊢ ncard s = 1 ↔ ∃ a, s = {a}
refine' ⟨fun h ↦ _, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
h : ncard s = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
h : ncard s = 1
⊢ ∃ a, s = {a}
have hft := (Finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
⊢ ∃ a, s = {a}
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
h : ncard s = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}
simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h
α : Type u_1
β : Type ?u.138753
s t : Set α
a✝ b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : toFinset s = {a}
⊢ s = {a}
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
⊢ ∃ a, s = {a}
refine' h.imp fun a ha ↦ _
α : Type u_1
β : Type ?u.138753
s t : Set α
a✝ b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : toFinset s = {a}
⊢ ∀ (x : α), x ∈ s ↔ x = a
α : Type u_1
β : Type ?u.138753
s t : Set α
a✝ b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : toFinset s = {a}
⊢ s = {a}
simp_rw [Set.ext_iff, mem_singleton_iff]
α : Type u_1
β : Type ?u.138753
s t : Set α
a✝ b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a
α : Type u_1
β : Type ?u.138753
s t : Set α
a✝ b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : toFinset s = {a}
⊢ ∀ (x : α), x ∈ s ↔ x = a
simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha
no goals
α : Type u_1
β : Type ?u.138753
s t : Set α
a✝ b x y : α
f : α → β
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a
exact ha
case intro
α : Type u_1
β : Type ?u.138753
t : Set α
a✝ b x y : α
f : α → β
a : α
⊢ ncard {a} = 1
α : Type u_1
β : Type ?u.138753
s t : Set α
a b x y : α
f : α → β
⊢ (∃ a, s = {a}) → ncard s = 1
rintro ⟨a, rfl⟩
no goals
case intro
α : Type u_1
β : Type ?u.138753
t : Set α
a✝ b x y : α
f : α → β
a : α
⊢ ncard {a} = 1
rw [ncard_singleton]