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

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

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

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

State before:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if a = b then c else f a) = c then d else g (if a = b then c else f a)) = if a = b then d else (g ∘ f) a
Tactic:
simp only [c1]
State after:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if True then c else f b) = c then d else g (if True then c else f b)) = if True then d else (g ∘ f) b

State before:
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if True then c else f b) = c then d else g (if True then c else f b)) = if True then d else (g ∘ f) b
Tactic:
simp
State after:
no goals

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

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

State before:
case neg
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : ¬a = b
⊢ f a = c → d = g (f a)
Tactic:
exact h1
State after:
no goals