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

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
h1 : f x = x'
⊢ image f S \ {x'} = image f (S \ {x}) \ {x'}
Tactic:
subst h1
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
⊢ image f S \ {f x} = image f (S \ {x}) \ {f x}

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
⊢ image f S \ {f x} = image f (S \ {x}) \ {f x}
Tactic:
apply Finset.ext
State after:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
⊢ ∀ (a : β), a ∈ image f S \ {f x} ↔ a ∈ image f (S \ {x}) \ {f x}

State before:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
⊢ ∀ (a : β), a ∈ image f S \ {f x} ↔ a ∈ image f (S \ {x}) \ {f x}
Tactic:
intro a
State after:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
⊢ a ∈ image f S \ {f x} ↔ a ∈ image f (S \ {x}) \ {f x}

State before:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
⊢ a ∈ image f S \ {f x} ↔ a ∈ image f (S \ {x}) \ {f x}
Tactic:
simp
State after:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
⊢ ¬a = f x → ((∃ a_2 ∈ S, f a_2 = a) ↔ ∃ a_2, (a_2 ∈ S ∧ ¬a_2 = x) ∧ f a_2 = a)

State before:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
⊢ ¬a = f x → ((∃ a_2 ∈ S, f a_2 = a) ↔ ∃ a_2, (a_2 ∈ S ∧ ¬a_2 = x) ∧ f a_2 = a)
Tactic:
intro a1
State after:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
⊢ (∃ a_1 ∈ S, f a_1 = a) ↔ ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a

State before:
case a
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
⊢ (∃ a_1 ∈ S, f a_1 = a) ↔ ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
Tactic:
constructor
State after:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
⊢ (∃ a_1 ∈ S, f a_1 = a) → ∃ a_2, (a_2 ∈ S ∧ ¬a_2 = x) ∧ f a_2 = a

case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
⊢ (∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a) → ∃ a_2 ∈ S, f a_2 = a

State before:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
⊢ (∃ a_1 ∈ S, f a_1 = a) → ∃ a_2, (a_2 ∈ S ∧ ¬a_2 = x) ∧ f a_2 = a
Tactic:
intro a2
State after:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
⊢ ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a

State before:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
⊢ ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
Tactic:
apply Exists.elim a2
State after:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
⊢ ∀ (a_1 : α), a_1 ∈ S ∧ f a_1 = a → ∃ a_3, (a_3 ∈ S ∧ ¬a_3 = x) ∧ f a_3 = a

State before:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
⊢ ∀ (a_1 : α), a_1 ∈ S ∧ f a_1 = a → ∃ a_3, (a_3 ∈ S ∧ ¬a_3 = x) ∧ f a_3 = a
Tactic:
intro b a3
State after:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
a3 : b ∈ S ∧ f b = a
⊢ ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a

State before:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
a3 : b ∈ S ∧ f b = a
⊢ ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
Tactic:
apply Exists.intro b
State after:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
a3 : b ∈ S ∧ f b = a
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = a

State before:
case a.mp
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
a3 : b ∈ S ∧ f b = a
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = a
Tactic:
cases a3
State after:
case a.mp.intro
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
left✝ : b ∈ S
right✝ : f b = a
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = a

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
a3_left : b ∈ S
a3_right : f b = a
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = a
Tactic:
case _ a3_left a3_right =>
  subst a3_right
  tauto
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1 ∈ S, f a_1 = a
b : α
a3_left : b ∈ S
a3_right : f b = a
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = a
Tactic:
subst a3_right
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
b : α
a3_left : b ∈ S
a1 : ¬f b = f x
a2 : ∃ a ∈ S, f a = f b
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = f b

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
b : α
a3_left : b ∈ S
a1 : ¬f b = f x
a2 : ∃ a ∈ S, f a = f b
⊢ (b ∈ S ∧ ¬b = x) ∧ f b = f b
Tactic:
tauto
State after:
no goals

State before:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
⊢ (∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a) → ∃ a_2 ∈ S, f a_2 = a
Tactic:
intro a2
State after:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
⊢ ∃ a_1 ∈ S, f a_1 = a

State before:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
⊢ ∃ a_1 ∈ S, f a_1 = a
Tactic:
apply Exists.elim a2
State after:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
⊢ ∀ (a_1 : α), (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a → ∃ a_3 ∈ S, f a_3 = a

State before:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
⊢ ∀ (a_1 : α), (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a → ∃ a_3 ∈ S, f a_3 = a
Tactic:
intro b a3
State after:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
a3 : (b ∈ S ∧ ¬b = x) ∧ f b = a
⊢ ∃ a_1 ∈ S, f a_1 = a

State before:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
a3 : (b ∈ S ∧ ¬b = x) ∧ f b = a
⊢ ∃ a_1 ∈ S, f a_1 = a
Tactic:
apply Exists.intro b
State after:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
a3 : (b ∈ S ∧ ¬b = x) ∧ f b = a
⊢ b ∈ S ∧ f b = a

State before:
case a.mpr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
a3 : (b ∈ S ∧ ¬b = x) ∧ f b = a
⊢ b ∈ S ∧ f b = a
Tactic:
cases a3
State after:
case a.mpr.intro
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
left✝ : b ∈ S ∧ ¬b = x
right✝ : f b = a
⊢ b ∈ S ∧ f b = a

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
a3_left : b ∈ S ∧ ¬b = x
a3_right : f b = a
⊢ b ∈ S ∧ f b = a
Tactic:
case _ a3_left a3_right =>
  subst a3_right
  tauto
State after:
no goals

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
a : β
a1 : ¬a = f x
a2 : ∃ a_1, (a_1 ∈ S ∧ ¬a_1 = x) ∧ f a_1 = a
b : α
a3_left : b ∈ S ∧ ¬b = x
a3_right : f b = a
⊢ b ∈ S ∧ f b = a
Tactic:
subst a3_right
State after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
b : α
a3_left : b ∈ S ∧ ¬b = x
a1 : ¬f b = f x
a2 : ∃ a, (a ∈ S ∧ ¬a = x) ∧ f a = f b
⊢ b ∈ S ∧ f b = f b

State before:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
b : α
a3_left : b ∈ S ∧ ¬b = x
a1 : ¬f b = f x
a2 : ∃ a, (a ∈ S ∧ ¬a = x) ∧ f a = f b
⊢ b ∈ S ∧ f b = f b
Tactic:
tauto
State after:
no goals