α : Type u_3
β : Type u_2
β₂ : Type ?u.142989
γ : Type ?u.142992
ι : Sort u_1
ι' : Sort ?u.142998
κ : ι → Sort ?u.143003
κ' : ι' → Sort ?u.143008
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
e : ι → β
he : Injective e
f : ι → α
⊢ ((⨆ (i : β) (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ (i : β) (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i) =
    ⨆ (i : ι), f i
α : Type u_3
β : Type u_2
β₂ : Type ?u.142989
γ : Type ?u.142992
ι : Sort u_1
ι' : Sort ?u.142998
κ : ι → Sort ?u.143003
κ' : ι' → Sort ?u.143008
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ (j : β), extend e f ⊥ j) = ⨆ (i : ι), f i
rw [iSup_split _ fun j => ∃ i, e i = j]
no goals
α : Type u_3
β : Type u_2
β₂ : Type ?u.142989
γ : Type ?u.142992
ι : Sort u_1
ι' : Sort ?u.142998
κ : ι → Sort ?u.143003
κ' : ι' → Sort ?u.143008
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
e : ι → β
he : Injective e
f : ι → α
⊢ ((⨆ (i : β) (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ (i : β) (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i) =
    ⨆ (i : ι), f i
simp (config := { contextual := true }) [he.extend_apply, extend_apply', @iSup_comm _ β ι]