α : Type u_1
β : Type u_2
γ : Type ?u.304567
ι : Sort u_3
ι' : Sort ?u.304573
ι₂ : Sort ?u.304576
κ : ι → Sort ?u.304581
κ₁ : ι → Sort ?u.304586
κ₂ : ι → Sort ?u.304591
κ' : ι' → Sort ?u.304596
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ (⨆ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a) = ⨆ (j : α) (i : ι) (_ : j ∈ s i), f j
α : Type u_1
β : Type u_2
γ : Type ?u.304567
ι : Sort u_3
ι' : Sort ?u.304573
ι₂ : Sort ?u.304576
κ : ι → Sort ?u.304581
κ₁ : ι → Sort ?u.304586
κ₂ : ι → Sort ?u.304591
κ' : ι' → Sort ?u.304596
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ (⨆ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a) = ⨆ (i : ι) (a : α) (_ : a ∈ s i), f a
rw [iSup_comm]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.304567
ι : Sort u_3
ι' : Sort ?u.304573
ι₂ : Sort ?u.304576
κ : ι → Sort ?u.304581
κ₁ : ι → Sort ?u.304586
κ₂ : ι → Sort ?u.304591
κ' : ι' → Sort ?u.304596
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ (⨆ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a) = ⨆ (j : α) (i : ι) (_ : j ∈ s i), f j
simp_rw [mem_iUnion, iSup_exists]