internlm/Lean-Github huggingface dataset:
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ C \ F ⊆ (C ∪ D) \ F
Tactic:
apply Finset.sdiff_subset_sdiff
Proof state after:
case h.hst
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ C ⊆ C ∪ D

case h.hvu
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ F ⊆ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case h.hst
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ C ⊆ C ∪ D
Tactic:
exact Finset.subset_union_left C D
Proof state after:
no goals
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case h.hvu
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ F ⊆ F
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ B ⊆ E ∪ (C ∪ D) \ F
Tactic:
trans E ∪ D \ F
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ B ⊆ E ∪ D \ F

α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ E ∪ D \ F ⊆ E ∪ (C ∪ D) \ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ B ⊆ E ∪ D \ F
Tactic:
exact h2
Proof state after:
no goals
Theorem: Finset.union_subset_left_right_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ E ∪ D \ F ⊆ E ∪ (C ∪ D) \ F
Tactic:
apply Finset.union_subset_union_right
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ D \ F ⊆ (C ∪ D) \ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ D \ F ⊆ (C ∪ D) \ F
Tactic:
apply Finset.sdiff_subset_sdiff
Proof state after:
case h.hst
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ D ⊆ C ∪ D

case h.hvu
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ F ⊆ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case h.hst
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ D ⊆ C ∪ D
Tactic:
exact Finset.subset_union_right C D
Proof state after:
no goals
Theorem: Finset.diff_union_subset
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
⊢ (A ∪ B) \ E ⊆ C ∪ D
Tactic:
have s1 : (A ∪ B) \ E = (A \ E) ∪ (B \ E)
Proof state after:
case s1
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
⊢ (A ∪ B) \ E = A \ E ∪ B \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D
Theorem: Finset.diff_union_subset
Proof state before:
case s1
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
⊢ (A ∪ B) \ E = A \ E ∪ B \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D
Tactic:
exact Finset.union_sdiff_distrib A B E
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D
Theorem: Finset.diff_union_subset
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D
Tactic:
trans (A \ E) ∪ (B \ E)
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ A \ E ∪ B \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ C ∪ D
Theorem: Finset.diff_union_subset
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ A \ E ∪ B \ E
Tactic:
simp only [s1]
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ A \ E ∪ B \ E
Theorem: Finset.diff_union_subset
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ A \ E ∪ B \ E
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.diff_union_subset
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ C ∪ D
Tactic:
exact Finset.union_subset_left_right (A \ E) (B \ E) C D h1 h2
Proof state after:
no goals
Theorem: Finset.union_right_comm_assoc
Proof state before:
α : Type
inst✝ : DecidableEq α
x : α
S T : Finset α
⊢ S ∪ (T ∪ {x}) = S ∪ {x} ∪ T
Tactic:
simp only [Finset.union_right_comm S {x} T]
Proof state after:
α : Type
inst✝ : DecidableEq α
x : α
S T : Finset α
⊢ S ∪ (T ∪ {x}) = S ∪ T ∪ {x}
Theorem: Finset.union_right_comm_assoc
Proof state before:
α : Type
inst✝ : DecidableEq α
x : α
S T : Finset α
⊢ S ∪ (T ∪ {x}) = S ∪ T ∪ {x}
Tactic:
simp only [Finset.union_assoc S T {x}]
Proof state after:
no goals
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof state after:
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
⊢ image f S \ {f x} = image f (S \ {x}) \ {f x}
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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}
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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}
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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)
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof state after:
no goals
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof state after:
no goals
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof state after:
no goals
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton
Proof 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
Proof state after:
no goals
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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
Proof state after:
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ Set.EqOn (Function.updateITE f x x') f ↑(S \ {x})
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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]
Proof 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
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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]
Proof 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
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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
Proof 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
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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]
Proof state after:
no goals
Theorem: Finset.image_sdiff_singleton_updateITE
Proof 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]
Proof state after:
no goals
Theorem: Finset.image_congr_update_ite
Proof 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
Proof 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})
Theorem: Finset.image_congr_update_ite
Proof 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]
Proof 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
Theorem: Finset.image_congr_update_ite
Proof 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
Proof 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
Theorem: Finset.image_congr_update_ite
Proof 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
Proof 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
Theorem: Finset.image_congr_update_ite
Proof 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]
Proof 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
Theorem: Finset.image_congr_update_ite
Proof 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
Proof 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
Theorem: Finset.image_congr_update_ite
Proof 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]
Proof state after:
no goals
Theorem: Finset.image_congr_update_ite
Proof 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]
Proof state after:
no goals
Theorem: Finset.mem_image_update
Proof 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]
Proof 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
Theorem: Finset.mem_image_update
Proof 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
Proof 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
Theorem: Finset.mem_image_update
Proof 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
Proof 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
Theorem: Finset.mem_image_update
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ y ∈ S
Tactic:
exact h2
Proof state after:
no goals
Theorem: Finset.mem_image_update
Proof 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]
Proof 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