case mp
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k → ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s

case mpr
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s) → IsCompactElement k
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
constructor
case mp
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
⊢ ∃ t, k ≤ Finset.sup t s
case mp
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k → ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
intro H ι s hs
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
⊢ ∃ t, k ≤ Finset.sup t s
case mp
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
⊢ ∃ t, k ≤ Finset.sup t s
obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
this : ∀ (x : { x // x ∈ t }), ∃ i, s i = ↑x
⊢ ∃ t, k ≤ Finset.sup t s
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
⊢ ∃ t, k ≤ Finset.sup t s
have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ ∃ t, k ≤ Finset.sup t s
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
this : ∀ (x : { x // x ∈ t }), ∃ i, s i = ↑x
⊢ ∃ t, k ≤ Finset.sup t s
choose f hf using this
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ Finset.sup t id ≤ Finset.sup (Finset.image f Finset.univ) s
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ ∃ t, k ≤ Finset.sup t s
refine' ⟨Finset.univ.image f, ht'.trans _⟩
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ ∀ (b : α), b ∈ t → id b ≤ Finset.sup (Finset.image f Finset.univ) s
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ Finset.sup t id ≤ Finset.sup (Finset.image f Finset.univ) s
rw [Finset.sup_le_iff]
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ id b ≤ Finset.sup (Finset.image f Finset.univ) s
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ ∀ (b : α), b ∈ t → id b ≤ Finset.sup (Finset.image f Finset.univ) s
intro b hb
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ s (f { val := b, property := hb }) ≤ Finset.sup (Finset.image f Finset.univ) s
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ id b ≤ Finset.sup (Finset.image f Finset.univ) s
rw [← show s (f ⟨b, hb⟩) = id b from hf _]
no goals
case mp.intro.intro
ι✝ : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ s (f { val := b, property := hb }) ≤ Finset.sup (Finset.image f Finset.univ) s
exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
case mpr
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s) → IsCompactElement k
intro H s hs
case mpr.intro
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
obtain ⟨t, ht⟩ :=
  H s Subtype.val
    (by
      delta iSup
      rwa [Subtype.range_coe])
case mpr.intro
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ Finset.sup t Subtype.val ≤ Finset.sup (Finset.image Subtype.val t) id
case mpr.intro
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
refine' ⟨t.image Subtype.val, by simp, ht.trans _⟩
case mpr.intro
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ∀ (b : ↑s), b ∈ t → ↑b ≤ Finset.sup (Finset.image Subtype.val t) id
case mpr.intro
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ Finset.sup t Subtype.val ≤ Finset.sup (Finset.image Subtype.val t) id
rw [Finset.sup_le_iff]
no goals
case mpr.intro
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ∀ (b : ↑s), b ∈ t → ↑b ≤ Finset.sup (Finset.image Subtype.val t) id
exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ sSup (Set.range Subtype.val)
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ iSup Subtype.val
delta iSup
no goals
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ sSup (Set.range Subtype.val)
rwa [Subtype.range_coe]
no goals
ι : Sort ?u.1219
α✝ : Type ?u.1222
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ↑(Finset.image Subtype.val t) ⊆ s
simp