Theorem: Finset.image_sdiff_singleton_updateITE (FOL/Finset.lean)

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ image (Function.updateITE f x x') (S \ {x}) = image f (S \ {x})
Tactic:
apply Finset.image_congr
State after:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ Set.EqOn (Function.updateITE f x x') f ↑(S \ {x})

State before:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ Set.EqOn (Function.updateITE f x x') f ↑(S \ {x})
Tactic:
simp only [Set.EqOn]
State after:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ ∀ ⦃x_1 : α⦄, x_1 ∈ ↑(S \ {x}) → Function.updateITE f x x' x_1 = f x_1

State before:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ ∀ ⦃x_1 : α⦄, x_1 ∈ ↑(S \ {x}) → Function.updateITE f x x' x_1 = f x_1
Tactic:
intro a a1
State after:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ ↑(S \ {x})
⊢ Function.updateITE f x x' a = f a

State before:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ ↑(S \ {x})
⊢ Function.updateITE f x x' a = f a
Tactic:
simp at a1
State after:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ S ∧ ¬a = x
⊢ Function.updateITE f x x' a = f a

State before:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ S ∧ ¬a = x
⊢ Function.updateITE f x x' a = f a
Tactic:
simp only [Function.updateITE]
State after:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ S ∧ ¬a = x
⊢ (if a = x then x' else f a) = f a

State before:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ S ∧ ¬a = x
⊢ (if a = x then x' else f a) = f a
Tactic:
cases a1
State after:
case h.intro
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
left✝ : a ∈ S
right✝ : ¬a = x
⊢ (if a = x then x' else f a) = f a

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1_left : a ∈ S
a1_right : ¬a = x
⊢ (if a = x then x' else f a) = f a
Tactic:
case _ a1_left a1_right =>
  simp only [if_neg a1_right]
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1_left : a ∈ S
a1_right : ¬a = x
⊢ (if a = x then x' else f a) = f a
Tactic:
simp only [if_neg a1_right]
State after:
no goals