α : Type u_3
β : Type u_1
β₂ : Type ?u.166426
γ : Type u_2
ι : Sort ?u.166432
ι' : Sort ?u.166435
κ : ι → Sort ?u.166440
κ' : ι' → Sort ?u.166445
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β × γ → α
s : Set β
t : Set γ
⊢ (⨆ (i : β) (j : γ) (_ : i ∈ s) (_ : j ∈ t), f (i, j)) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)
α : Type u_3
β : Type u_1
β₂ : Type ?u.166426
γ : Type u_2
ι : Sort ?u.166432
ι' : Sort ?u.166435
κ : ι → Sort ?u.166440
κ' : ι' → Sort ?u.166445
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β × γ → α
s : Set β
t : Set γ
⊢ (⨆ (x : β × γ) (_ : x ∈ s ×ˢ t), f x) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)
simp_rw [iSup_prod, mem_prod, iSup_and]
no goals
α : Type u_3
β : Type u_1
β₂ : Type ?u.166426
γ : Type u_2
ι : Sort ?u.166432
ι' : Sort ?u.166435
κ : ι → Sort ?u.166440
κ' : ι' → Sort ?u.166445
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β × γ → α
s : Set β
t : Set γ
⊢ (⨆ (i : β) (j : γ) (_ : i ∈ s) (_ : j ∈ t), f (i, j)) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)
exact iSup_congr fun _ => iSup_comm