ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
⊢ (⨅ (x : α), 𝓟 (Ici {x})) ≤ atTop
ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
⊢ atTop = ⨅ (x : α), 𝓟 (Ici {x})
refine' le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop {i}) _
ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
s : Finset α
⊢ (⋂ (i : ↑↑s), Ici {↑i}) ⊆ Ici s
ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
⊢ (⨅ (x : α), 𝓟 (Ici {x})) ≤ atTop
refine'
  le_iInf fun s =>
    le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) _
ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
s : Finset α
⊢ ∀ (x : Finset α), (∀ (x_1 : α), x_1 ∈ ↑s → x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
s : Finset α
⊢ (⋂ (i : ↑↑s), Ici {↑i}) ⊆ Ici s
simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset,
  Finset.mem_singleton, Finset.subset_iff, forall_eq]
no goals
ι : Type ?u.267659
ι' : Type ?u.267662
α : Type u_1
β : Type ?u.267668
γ : Type ?u.267671
s : Finset α
⊢ ∀ (x : Finset α), (∀ (x_1 : α), x_1 ∈ ↑s → x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
exact fun t => id