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

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

State before:
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ updateITE (updateITE f a c) b d x = updateITE (updateITE f b d) a c 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 d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

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

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

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

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

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

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

State before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
c d : β
x : α
h1 : ¬x = x
⊢ (if x = x then d else if x = x then c else f x) = if x = x then c else if x = x then d else f x
Tactic:
contradiction
State after:
no goals

State before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
subst c1
State after:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ (if x = b then d else if x = x then c else f x) = if x = x then c else if x = b then d else f x

State before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ (if x = b then d else if x = x then c else f x) = if x = x then c else if x = b then d else f x
Tactic:
simp
State after:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ x = b → d = c

State before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ x = b → d = c
Tactic:
intro a1
State after:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
a1 : x = b
⊢ d = c

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

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

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x

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

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

State before:
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
c d : β
x : α
c1 : ¬x = a
h1 : ¬a = x
⊢ d = if x = a then c else d
Tactic:
simp only [if_neg c1]
State after:
no goals

State before:
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
c1 : ¬x = a
c2 : ¬x = b
⊢ (if x = b then d else if x = a then c else f x) = if x = a then c else if x = b then d else f x
Tactic:
simp only [if_neg c1]
State after:
no goals