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

State before:
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
⊢ updateITE (updateITE id b c) a a = updateITE id b c
Tactic:
funext x
State after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ updateITE (updateITE id b c) a a x = updateITE id b c x

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

State before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ (if x = a then a else if x = b then c else id x) = if x = b then c else id x
Tactic:
simp
State after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ x = a → a = if x = b then c else x

State before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ x = a → a = if x = b then c else x
Tactic:
intro a1
State after:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
a1 : x = a
⊢ a = if x = b then c else x

State before:
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
a1 : x = a
⊢ a = if x = b then c else x
Tactic:
subst a1
State after:
case h
α : Type
inst✝ : DecidableEq α
b c x : α
h1 : ¬x = b
⊢ x = if x = b then c else x

State before:
case h
α : Type
inst✝ : DecidableEq α
b c x : α
h1 : ¬x = b
⊢ x = if x = b then c else x
Tactic:
simp only [if_neg h1]
State after:
no goals