α : Type u_1
β : Type ?u.108111
β₂ : Type ?u.108114
γ : Type ?u.108117
ι : Sort u_2
ι' : Sort ?u.108123
κ : ι → Sort ?u.108128
κ' : ι' → Sort ?u.108133
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ (i : ι), if h : p i then f i h else g i h) = ⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
α : Type u_1
β : Type ?u.108111
β₂ : Type ?u.108114
γ : Type ?u.108117
ι : Sort u_2
ι' : Sort ?u.108123
κ : ι → Sort ?u.108128
κ' : ι' → Sort ?u.108133
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ (i : ι), if h : p i then f i h else g i h) = (⨆ (i : ι) (h : p i), f i h) ⊔ ⨆ (i : ι) (h : ¬p i), g i h
rw [← iSup_sup_eq]
case e_s.h
α : Type u_1
β : Type ?u.108111
β₂ : Type ?u.108114
γ : Type ?u.108117
ι : Sort u_2
ι' : Sort ?u.108123
κ : ι → Sort ?u.108128
κ' : ι' → Sort ?u.108133
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
α : Type u_1
β : Type ?u.108111
β₂ : Type ?u.108114
γ : Type ?u.108117
ι : Sort u_2
ι' : Sort ?u.108123
κ : ι → Sort ?u.108128
κ' : ι' → Sort ?u.108133
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ (i : ι), if h : p i then f i h else g i h) = ⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
congr 1 with i
no goals
case e_s.h
α : Type u_1
β : Type ?u.108111
β₂ : Type ?u.108114
γ : Type ?u.108117
ι : Sort u_2
ι' : Sort ?u.108123
κ : ι → Sort ?u.108128
κ' : ι' → Sort ?u.108133
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
split_ifs with h <;> simp [h]