case inl
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, (⨅ (t : ι) (_ : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)

case inr
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : Set.Nonempty B
⊢ ∃ x, (⨅ (t : ι) (_ : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
⊢ ∃ x, (⨅ (t : ι) (_ : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)
cases' B.eq_empty_or_nonempty with hB Bnonempty
case inl
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⊤ = ⨅ (i : ℕ), f (x i)
case inl
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, (⨅ (t : ι) (_ : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)
rw [hB, iInf_emptyset]
case inl
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ⊤ = ⨅ (i : ℕ), f ((fun x => i₀) i)
case inl
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⊤ = ⨅ (i : ℕ), f (x i)
use fun _ => i₀
no goals
case inl
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ⊤ = ⨅ (i : ℕ), f ((fun x => i₀) i)
simp [h]
no goals
case inr
α : Type u_1
β : Type ?u.94654
γ : Type ?u.94657
ι : Type u_2
ι' : Sort ?u.94663
inst✝ : CompleteLattice α
B : Set ι
Bcbl : Set.Countable B
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : Set.Nonempty B
⊢ ∃ x, (⨅ (t : ι) (_ : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)
exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f