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

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

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

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

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

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
h✝¹ : ¬x = b
h✝ : ¬x = a
⊢ f x = f x
Tactic:
case _ | _ | _ =>
  rfl
State after:
no goals

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

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

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