α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ (⨆ (j : β) (i : ℕ) (_ : j ∈ decode₂ β i), f j) = ⨆ (b : β), f b
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ (⨆ (i : ℕ) (b : β) (_ : b ∈ decode₂ β i), f b) = ⨆ (b : β), f b
rw [iSup_comm]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ (⨆ (j : β) (i : ℕ) (_ : j ∈ decode₂ β i), f j) = ⨆ (b : β), f b
simp only [mem_decode₂, iSup_iSup_eq_right]