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

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

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

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

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
h✝ : ¬x = a
⊢ f x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : x = a
⊢ g a = g x
Tactic:
case _ c1 =>
  subst c1
  rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : ¬x = a
⊢ f x = g x
Tactic:
case _ c1 =>
  exact h1 x c1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : x = a
⊢ g a = g x
Tactic:
subst c1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : ∀ (x_1 : α), ¬x_1 = x → f x_1 = g x_1
⊢ g x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : ∀ (x_1 : α), ¬x_1 = x → f x_1 = g x_1
⊢ g x = g x
Tactic:
rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : ¬x = a
⊢ f x = g x
Tactic:
exact h1 x c1
State after:
no goals