Theorem: Function.updateITE_idem (FOL/FunctionUpdateITE.lean)

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
⊢ updateITE (updateITE f a b) a c = updateITE f a c
Tactic:
funext x
State after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ updateITE (updateITE f a b) a c x = updateITE f a c x

State before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ updateITE (updateITE f a b) a c x = updateITE f a c x
Tactic:
simp only [Function.updateITE]
State after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ (if x = a then c else if x = a then b else f x) = if x = a then c else f x

State before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ (if x = a then c else if x = a then b else f x) = if x = a then c else f x
Tactic:
split_ifs
State after:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : x = a
⊢ c = c

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : ¬x = a
⊢ f x = f x

State before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : x = a
⊢ c = c
Tactic:
rfl
State after:
no goals

State before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : ¬x = a
⊢ f x = f x
Tactic:
rfl
State after:
no goals