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

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
f : α → β
a : α
b : β
h1 : a ∉ S
⊢ Finset.image (updateITE f a b) S = Finset.image f S
Tactic:
induction S using Finset.induction_on
State after:
case empty
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
h1 : a ∉ ∅
⊢ Finset.image (updateITE f a b) ∅ = Finset.image f ∅

case insert
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
a✝² : α
s✝ : Finset α
a✝¹ : a✝² ∉ s✝
a✝ : a ∉ s✝ → Finset.image (updateITE f a b) s✝ = Finset.image f s✝
h1 : a ∉ insert a✝² s✝
⊢ Finset.image (updateITE f a b) (insert a✝² s✝) = Finset.image f (insert a✝² s✝)

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
h1 : a ∉ ∅
⊢ Finset.image (updateITE f a b) ∅ = Finset.image f ∅
Tactic:
case empty =>
  simp
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
h1 : a ∉ ∅
⊢ Finset.image (updateITE f a b) ∅ = Finset.image f ∅
Tactic:
simp
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1 : a ∉ insert S_a S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
simp at h1
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1 : ¬a = S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1 : ¬a = S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
push_neg at h1
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1 : a ≠ S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1 : a ≠ S_a ∧ a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
cases h1
State after:
case intro
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
left✝ : a ≠ S_a
right✝ : a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ Finset.image (updateITE f a b) (insert S_a S_S) = Finset.image f (insert S_a S_S)
Tactic:
simp
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ insert (updateITE f a b S_a) (Finset.image (updateITE f a b) S_S) = insert (f S_a) (Finset.image f S_S)

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ insert (updateITE f a b S_a) (Finset.image (updateITE f a b) S_S) = insert (f S_a) (Finset.image f S_S)
Tactic:
congr! 1
State after:
case h.e'_4
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ updateITE f a b S_a = f S_a

case h.e'_5
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ Finset.image (updateITE f a b) S_S = Finset.image f S_S

State before:
case h.e'_4
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ updateITE f a b S_a = f S_a
Tactic:
simp only [Function.updateITE]
State after:
case h.e'_4
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ (if S_a = a then b else f S_a) = f S_a

State before:
case h.e'_4
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ (if S_a = a then b else f S_a) = f S_a
Tactic:
split_ifs
State after:
case pos
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
h✝ : S_a = a
⊢ b = f S_a

case neg
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
h✝ : ¬S_a = a
⊢ f S_a = f S_a

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : S_a = a
⊢ b = f S_a
Tactic:
case _ c1 =>
  subst c1
  contradiction
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : ¬S_a = a
⊢ f S_a = f S_a
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : S_a = a
⊢ b = f S_a
Tactic:
subst c1
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : S_a ∉ S_S → Finset.image (updateITE f S_a b) S_S = Finset.image f S_S
h1_left : S_a ≠ S_a
h1_right : S_a ∉ S_S
⊢ b = f S_a

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : S_a ∉ S_S → Finset.image (updateITE f S_a b) S_S = Finset.image f S_S
h1_left : S_a ≠ S_a
h1_right : S_a ∉ S_S
⊢ b = f S_a
Tactic:
contradiction
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : ¬S_a = a
⊢ f S_a = f S_a
Tactic:
rfl
State after:
no goals

State before:
case h.e'_5
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
⊢ Finset.image (updateITE f a b) S_S = Finset.image f S_S
Tactic:
exact S_ih h1_right
State after:
no goals