F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
⊢ (s ⊔ ⨆ (x_1 : α) (_ : x_1 ∈ t), update f x s x_1) = s ⊔ ⨆ (i : α) (_ : i ∈ t), f i
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
⊢ (⨆ (i : α) (_ : i ∈ insert x t), update f x s i) = s ⊔ ⨆ (i : α) (_ : i ∈ t), f i
simp only [Finset.iSup_insert, update_same]
case e_a.e_s.h.e_s.h
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
i : α
hi : i ∈ t
⊢ update f x s i = f i
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
⊢ (s ⊔ ⨆ (x_1 : α) (_ : x_1 ∈ t), update f x s x_1) = s ⊔ ⨆ (i : α) (_ : i ∈ t), f i
rcongr (i hi)
case e_a.e_s.h.e_s.h.h
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
i : α
hi : i ∈ t
⊢ i ≠ x
case e_a.e_s.h.e_s.h
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
i : α
hi : i ∈ t
⊢ update f x s i = f i
apply update_noteq
case e_a.e_s.h.e_s.h.h
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
t : Finset α
f : α → β
s : β
i : α
hi : i ∈ t
hx : ¬i ∈ t
⊢ False
case e_a.e_s.h.e_s.h.h
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
i : α
hi : i ∈ t
⊢ i ≠ x
rintro rfl
no goals
case e_a.e_s.h.e_s.h.h
F : Type ?u.452327
α : Type u_1
β : Type u_2
γ : Type ?u.452336
ι : Type ?u.452339
κ : Type ?u.452342
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
t : Finset α
f : α → β
s : β
i : α
hi : i ∈ t
hx : ¬i ∈ t
⊢ False
exact hx hi