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 = ⊤

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) = ⊤
α : 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 = ⊤
constructor
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 = ⊤
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 = ⊤
rintro ⟨s, hps, hs⟩
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) = ⊤
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 = ⊤
refine' ⟨range s, countable_range s, forall_range_iff.2 hps, _⟩
no goals
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) = ⊤
rwa [sSup_range]
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) = ⊤
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) = ⊤
rintro ⟨S, hSc, hps, hS⟩
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) = ⊤

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) = ⊤
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) = ⊤
rcases eq_empty_or_nonempty S with (rfl | hne)
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) = ⊤
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) = ⊤
rw [sSup_empty] at hS
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) = ⊤
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) = ⊤
haveI := subsingleton_of_bot_eq_top hS
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) = ⊤
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) = ⊤
rcases h with ⟨x, hx⟩
no goals
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) = ⊤
exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
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) = ⊤
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) = ⊤
rcases(Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
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) = ⊤
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) = ⊤
refine' ⟨fun n => s n, fun n => hps _ (s n).coe_prop, _⟩
no goals
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) = ⊤
rwa [hs.iSup_comp, ← sSup_eq_iSup']