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

State before:
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ f y ∈ image (Function.updateITE f x x) S
Tactic:
simp only [Finset.mem_image]
State after:
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ ∃ a ∈ S, Function.updateITE f x x a = f y

State before:
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ ∃ a ∈ S, Function.updateITE f x x a = f y
Tactic:
apply Exists.intro y
State after:
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ y ∈ S ∧ Function.updateITE f x x y = f y

State before:
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ y ∈ S ∧ Function.updateITE f x x y = f y
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ y ∈ S

case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ Function.updateITE f x x y = f y

State before:
case left
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ y ∈ S
Tactic:
exact h2
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ Function.updateITE f x x y = f y
Tactic:
simp only [Function.updateITE]
State after:
case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ (if y = x then x else f y) = f y

State before:
case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ (if y = x then x else f y) = f y
Tactic:
simp only [if_neg h1]
State after:
no goals