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

State before:
α : Type
inst✝ : DecidableEq α
a : α
⊢ updateITE id a a = id
Tactic:
funext x
State after:
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ updateITE id a a x = id x

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

State before:
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ (if x = a then a else id x) = id x
Tactic:
split_ifs
State after:
case pos
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : x = a
⊢ a = id x

case neg
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x

State before:
α : Type
inst✝ : DecidableEq α
a x : α
c1 : x = a
⊢ a = id x
Tactic:
case _ c1 =>
  subst c1
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x
Tactic:
case _ =>
  rfl
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
a x : α
c1 : x = a
⊢ a = id x
Tactic:
subst c1
State after:
α : Type
inst✝ : DecidableEq α
x : α
⊢ x = id x

State before:
α : Type
inst✝ : DecidableEq α
x : α
⊢ x = id x
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x
Tactic:
rfl
State after:
no goals