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

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

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

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

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

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

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

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

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