case pos
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ (⨆ (i : { i // f i ≠ ⊥ }), f ↑i) = ⨆ (i : ι), f i

case neg
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
⊢ (⨆ (i : { i // f i ≠ ⊥ }), f ↑i) = ⨆ (i : ι), f i
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
⊢ (⨆ (i : { i // f i ≠ ⊥ }), f ↑i) = ⨆ (i : ι), f i
by_cases htriv : ∀ i, f i = ⊥
case neg
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'
case neg
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
⊢ (⨆ (i : { i // f i ≠ ⊥ }), f ↑i) = ⨆ (i : ι), f i
refine' (iSup_comp_le f _).antisymm (iSup_mono' fun i => _)
case pos
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

case neg
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
case neg
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'
by_cases hi : f i = ⊥
no goals
case pos
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ (⨆ (i : { i // f i ≠ ⊥ }), f ↑i) = ⨆ (i : ι), f i
simp only [iSup_bot, (funext htriv : f = _)]
case pos
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
case pos
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
rw [hi]
case pos.intro
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : ¬f i₀ = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
case pos
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
obtain ⟨i₀, hi₀⟩ := not_forall.mp htriv
no goals
case pos.intro
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : ¬f i₀ = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
exact ⟨⟨i₀, hi₀⟩, bot_le⟩
no goals
case neg
α : Type u_1
β : Type ?u.174146
β₂ : Type ?u.174149
γ : Type ?u.174152
ι : Sort u_2
ι' : Sort ?u.174158
κ : ι → Sort ?u.174163
κ' : ι' → Sort ?u.174168
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
exact ⟨⟨i, hi⟩, rfl.le⟩