case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α ⊕ β
⊢ Sum.elim (update f i c) g x = update (Sum.elim f g) (inl i) c x
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
⊢ Sum.elim (update f i c) g = update (Sum.elim f g) (inl i) c
ext x
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : β
⊢ Sum.elim (update f i c) g (inr x) = update (Sum.elim f g) (inl i) c (inr x)
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α ⊕ β
⊢ Sum.elim (update f i c) g x = update (Sum.elim f g) (inl i) c x
rcases x with x | x
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

case neg
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : ¬x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
by_cases h : x = i
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : α
⊢ Sum.elim (update f x c) g (inl x) = update (Sum.elim f g) (inl x) c (inl x)
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
subst h
no goals
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : α
⊢ Sum.elim (update f x c) g (inl x) = update (Sum.elim f g) (inl x) c (inl x)
simp
no goals
case neg
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : ¬x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
simp [h]
no goals
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.36815
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : β
⊢ Sum.elim (update f i c) g (inr x) = update (Sum.elim f g) (inl i) c (inr x)
simp