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

State before:
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
⊢ f ∘ updateITE g a b = updateITE (f ∘ g) a (f b)
Tactic:
funext x
State after:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ (f ∘ updateITE g a b) x = updateITE (f ∘ g) a (f b) x

State before:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ (f ∘ updateITE g a b) x = updateITE (f ∘ g) a (f b) x
Tactic:
simp
State after:
case h
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
⊢ f (updateITE g a b x) = updateITE (f ∘ g) a (f b) x

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

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

case neg
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : ¬x = a
⊢ f (g x) = (f ∘ g) x

State before:
case pos
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : x = a
⊢ f b = f b
Tactic:
rfl
State after:
no goals

State before:
case neg
α β γ : Type
inst✝ : DecidableEq α
f : β → γ
g : α → β
a : α
b : β
x : α
h✝ : ¬x = a
⊢ f (g x) = (f ∘ g) x
Tactic:
rfl
State after:
no goals