Theorem: Function.updateITE_eq_Function.updateITE' (FOL/FunctionUpdateITE.lean)

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ updateITE f a b = Function.updateITE' f a b
Tactic:
funext x
State after:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ updateITE f a b x = Function.updateITE' f a b x

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

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

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

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : a = x
⊢ b = b
Tactic:
case _ c1 c2 =>
  rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : ¬a = x
⊢ b = f x
Tactic:
case _ c1 c2 =>
  subst c1
  contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : a = x
⊢ f x = b
Tactic:
case _ c1 c2 =>
  subst c2
  contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : ¬a = x
⊢ f x = f x
Tactic:
case _ c1 c2 =>
  rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : a = x
⊢ b = b
Tactic:
rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : x = a
c2 : ¬a = x
⊢ b = f x
Tactic:
subst c1
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
b : β
x : α
c2 : ¬x = x
⊢ b = f x

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
b : β
x : α
c2 : ¬x = x
⊢ b = f x
Tactic:
contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : a = x
⊢ f x = b
Tactic:
subst c2
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
c1 : ¬a = a
⊢ f a = b

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
c1 : ¬a = a
⊢ f a = b
Tactic:
contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
c1 : ¬x = a
c2 : ¬a = x
⊢ f x = f x
Tactic:
rfl
State after:
no goals