α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ (Antitone fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) ∧
    (⨅ (i : ℕ), 𝓟 (s i)) = ⨅ (i : ℕ), 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ ∃ t, Antitone t ∧ (⨅ (i : ℕ), 𝓟 (s i)) = ⨅ (i : ℕ), 𝓟 (t i)
use fun n => ⋂ m ≤ n, s m
case left
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ Antitone fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m

case right
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ (⨅ (i : ℕ), 𝓟 (s i)) = ⨅ (i : ℕ), 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ (Antitone fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) ∧
    (⨅ (i : ℕ), 𝓟 (s i)) = ⨅ (i : ℕ), 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)
constructor
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ (⨅ (i : ℕ), 𝓟 (s i)) ≤ 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)

case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ (⨅ (i : ℕ), 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)) ≤ 𝓟 (s i)
case right
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ (⨅ (i : ℕ), 𝓟 (s i)) = ⨅ (i : ℕ), 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)
apply le_antisymm <;> rw [le_iInf_iff] <;> intro i
no goals
case left
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
⊢ Antitone fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m
exact fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ (fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i ∈ ⨅ (i : ℕ), 𝓟 (s i)
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ (⨅ (i : ℕ), 𝓟 (s i)) ≤ 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)
rw [le_principal_iff]
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i j : ℕ
x✝ : j ∈ {i_1 | i_1 ≤ i}
⊢ s j ∈ ⨅ (i : ℕ), 𝓟 (s i)
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ (fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i ∈ ⨅ (i : ℕ), 𝓟 (s i)
refine' (biInter_mem (finite_le_nat _)).2 fun j _ => _
no goals
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i j : ℕ
x✝ : j ∈ {i_1 | i_1 ≤ i}
⊢ s j ∈ ⨅ (i : ℕ), 𝓟 (s i)
exact mem_iInf_of_mem j (mem_principal_self _)
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ i ≤ i
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ (⨅ (i : ℕ), 𝓟 ((fun n => ⋂ (m : ℕ) (_ : m ≤ n), s m) i)) ≤ 𝓟 (s i)
refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)
no goals
case right.a
α : Type u_1
β : Type ?u.93399
γ : Type ?u.93402
ι : Type ?u.93405
ι' : Sort ?u.93408
s : ℕ → Set α
i : ℕ
⊢ i ≤ i
rfl