no goals
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (i : ι), s i) = ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i
classical
  refine le_antisymm ?_ ?_
  exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
  exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
case refine_1
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (i : ι), s i) ≤ ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i

case refine_2
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) ≤ ⨆ (i : ι), s i
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (i : ι), s i) = ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i
refine le_antisymm ?_ ?_
case refine_2
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) ≤ ⨆ (i : ι), s i
case refine_1
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (i : ι), s i) ≤ ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i

case refine_2
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) ≤ ⨆ (i : ι), s i
exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
no goals
case refine_2
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
⊢ (⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) ≤ ⨆ (i : ι), s i
exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
no goals
F : Type ?u.418480
α : Type u_1
β : Type ?u.418486
γ : Type ?u.418489
ι : Type u_2
κ : Type ?u.418495
ι' : Sort ?u.418498
inst✝ : CompleteLattice α
s : ι → α
b : ι
⊢ b ∈ {b}
simp