[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
[PROOFSTEP]
letI := h.toEncodable
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
this : Encodable ↑s := Countable.toEncodable h
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
[PROOFSTEP]
simp [enumerateCountable, Encodable.encodek]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
⊢ ∃ f, s ⊆ range f
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
inhabited_h : Inhabited α
⊢ ∃ f, s ⊆ range f
[PROOFSTEP]
exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
⊢ ∃ f, s = range f
[PROOFSTEP]
rcases hc.exists_surjective hs with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f
[PROOFSTEP]
refine' ⟨(↑) ∘ f, _⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)
[PROOFSTEP]
rw [hf.range_comp, Subtype.range_coe]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (f '' s)
[PROOFSTEP]
rw [image_eq_range]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (range fun x => f ↑x)
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
this : Countable ↑s
⊢ Set.Countable (range fun x => f ↑x)
[PROOFSTEP]
apply countable_range
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤) ↔ ∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤) → ∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤
[PROOFSTEP]
rintro ⟨s, hps, hs⟩
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ (n : ℕ), s n = ⊤
⊢ ∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤
[PROOFSTEP]
refine' ⟨range s, countable_range s, forall_range_iff.2 hps, _⟩
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ (n : ℕ), s n = ⊤
⊢ sSup (range s) = ⊤
[PROOFSTEP]
rwa [sSup_range]
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rintro ⟨S, hSc, hps, hS⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rcases eq_empty_or_nonempty S with (rfl | hne)
[GOAL]
case mpr.intro.intro.intro.inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : sSup ∅ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rw [sSup_empty] at hS 
[GOAL]
case mpr.intro.intro.intro.inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : ⊥ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
haveI := subsingleton_of_bot_eq_top hS
[GOAL]
case mpr.intro.intro.intro.inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : ⊥ = ⊤
this : Subsingleton α
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rcases h with ⟨x, hx⟩
[GOAL]
case mpr.intro.intro.intro.inl.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : ⊥ = ⊤
this : Subsingleton α
x : α
hx : p x
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
[GOAL]
case mpr.intro.intro.intro.inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
hne : Set.Nonempty S
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rcases(Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
[GOAL]
case mpr.intro.intro.intro.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
hne : Set.Nonempty S
s : ℕ → ↑S
hs : Surjective s
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
refine' ⟨fun n => s n, fun n => hps _ (s n).coe_prop, _⟩
[GOAL]
case mpr.intro.intro.intro.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
hne : Set.Nonempty S
s : ℕ → ↑S
hs : Surjective s
⊢ ⨆ (n : ℕ), (fun n => ↑(s n)) n = ⊤
[PROOFSTEP]
rwa [hs.iSup_comp, ← sSup_eq_iSup']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
⊢ Set.Countable (⋃ (i : ι), t i)
[PROOFSTEP]
haveI := fun a => (ht a).to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (⋃ (i : ι), t i)
[PROOFSTEP]
rw [iUnion_eq_range_psigma]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (range fun a => ↑a.snd)
[PROOFSTEP]
apply countable_range
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
[PROOFSTEP]
rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set (Set α)
hs : Set.Countable s
⊢ Set.Countable (⋃₀ s) ↔ ∀ (a : Set α), a ∈ s → Set.Countable a
[PROOFSTEP]
rw [sUnion_eq_biUnion, hs.biUnion_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s t : Set α
⊢ Set.Countable (s ∪ t) ↔ Set.Countable s ∧ Set.Countable t
[PROOFSTEP]
simp [union_eq_iUnion, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
a : α
⊢ Set.Countable (insert a s) ↔ Set.Countable s
[PROOFSTEP]
simp only [insert_eq, countable_union, countable_singleton, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
[PROOFSTEP]
refine' Countable.mono _ (countable_range fun t : Finset s => Subtype.val '' (t : Set s))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ {t | Set.Finite t ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
rintro t ⟨ht, hts⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set α
ht : Set.Finite t
hts : t ⊆ s
⊢ t ∈ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
lift t to Set s using hts
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val t)
⊢ (fun x x_1 => x '' x_1) Subtype.val t ∈ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
lift t to Finset s using ht.of_finite_image (Subtype.val_injective.injOn _)
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Finset ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val ↑t)
⊢ (fun x x_1 => x '' x_1) Subtype.val ↑t ∈ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
exact mem_range_self _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), Set.Countable (s a)
⊢ Set.Countable {f | ∀ (a : α), f a ∈ s a}
[PROOFSTEP]
simpa only [← mem_univ_pi] using countable_univ_pi hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
⊢ Set.Countable (s ×ˢ t)
[PROOFSTEP]
haveI : Countable s := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
this : Countable ↑s
⊢ Set.Countable (s ×ˢ t)
[PROOFSTEP]
haveI : Countable t := ht.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
this✝ : Countable ↑s
this : Countable ↑t
⊢ Set.Countable (s ×ˢ t)
[PROOFSTEP]
exact (Countable.of_equiv _ <| (Equiv.Set.prod _ _).symm).to_set
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable (Set.image2 f s t)
[PROOFSTEP]
rw [← image_prod]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable ((fun x => f x.fst x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).image _
