awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s.val = 0 ↔ s = ∅

Tactic:
@val_inj _ s ∅

Premises used: Finset.val_inj
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s ⊆ ∅ ↔ s = ∅

Tactic:
subset_zero.trans val_eq_zero

Premises used: Set.Mem, setOf, Finset.val_eq_zero, Multiset.Mem, Multiset.subset_zero, Iff.trans, Multiset.Subset
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ ¬s ⊂ ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
h : s ≠ ∅
⊢ s.Nonempty

Tactic:
exists_mem_of_ne_zero (mt val_eq_zero.1 h)

Premises used: Set.Mem, setOf, Finset.val_eq_zero, mt, Multiset.Mem, Iff.mp, Finset.Nonempty, Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s.Nonempty ↔ s ≠ ∅

Tactic:
⟨Nonempty.ne_empty, nonempty_of_ne_empty⟩

Premises used: Finset.Nonempty.ne_empty, Iff.intro, Finset.nonempty_of_ne_empty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ ¬s.Nonempty ↔ s = ∅

Tactic:
nonempty_iff_ne_empty.not.trans not_not

Premises used: Classical.not_not, Iff.not, Finset.nonempty_iff_ne_empty, Iff.trans
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s = ∅ ∨ s.Nonempty

Tactic:
by_cases Or.inl fun h => Or.inr (nonempty_of_ne_empty h)

Premises used: by_cases, Or.inl, Or.inr, Finset.nonempty_of_ne_empty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
⊢ (↑∅ : Set α) = ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α) = ∅ ↔ s = ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ IsEmpty.{u_1 + 1} ↥s ↔ s = ∅

Tactic:
simpa using @Set.isEmpty_coe_sort α s

Premises used: Set.isEmpty_coe_sort
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ IsEmpty.{u_1 + 1} ↥∅

Tactic:
isEmpty_coe_sort.2 rfl

Premises used: Iff.mpr, Finset.isEmpty_coe_sort, rfl
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
inst : IsEmpty α
s : Finset α
⊢ s = ∅

Tactic:
Finset.eq_empty_of_forall_notMem isEmptyElim

Premises used: isEmptyElim, Finset.eq_empty_of_forall_notMem
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α) ⊥ ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ ∅ ⊂ s ↔ s.Nonempty

Tactic:
(@bot_lt_iff_ne_bot (Finset α) _ _ _).trans nonempty_iff_ne_empty.symm

Premises used: Set.Mem, setOf, bot_lt_iff_ne_bot, Finset.nonempty_iff_ne_empty, Set.Subset, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
p : α → Prop
⊢ (∃ (x : α), Membership.mem (γ := Finset α) ∅ x ∧ p x) ↔ False

Tactic:
grind
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
p : α → Prop
⊢ (∀ (x : α), Membership.mem (γ := Finset α) ∅ x → p x) ↔ True

Tactic:
grind
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ (s.erase a).val = s.val.erase a

Tactic:
rfl

Premises used: Multiset.erase, rfl
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Finset α
⊢ a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s

Tactic:
s.2.mem_erase_iff

Premises used: Set.Mem, setOf, Finset.nodup, Multiset.Mem, Multiset.Nodup.mem_erase_iff, Multiset.erase
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ ¬a ∈ s.erase a

Tactic:
s.2.notMem_erase

Premises used: Set.Mem, setOf, Finset.nodup, Multiset.Mem, Multiset.erase, Multiset.Nodup.notMem_erase
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ b ∈ s.erase a → b ≠ a

Tactic:
fun h => (mem_erase.1 h).1

Premises used: Finset.mem_erase, And.left, Iff.mp
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ b ∈ s.erase a → b ∈ s

Tactic:
Multiset.mem_of_mem_erase

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.erase, Multiset.mem_of_mem_erase
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
simp : a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
⊢ a ≠ b → a ∈ s → a ∈ s.erase b

Tactic:
simp only [mem_erase]

Premises used: Finset.mem_erase
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s

Tactic:
And.intro

Premises used: And.intro
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s

Tactic:
exact And.intro

Premises used: And.intro
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hs : b ∈ s
hsa : ¬b ∈ s.erase a
⊢ b = a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ s.erase a = s

Tactic:
eq_of_veq <| erase_of_notMem h

Premises used: Finset.eq_of_veq, Multiset.erase_of_notMem
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s.erase a = s ↔ ¬a ∈ s

Tactic:
⟨fun h => h ▸ notMem_erase _ _, erase_eq_of_notMem⟩

Premises used: Eq.rec, Iff.intro, Finset.notMem_erase, Finset.erase_eq_of_notMem
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ≠ s ↔ a ∈ s

Tactic:
erase_eq_self.not_left

Premises used: Iff.not_left, Finset.erase_eq_self
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
h : s ⊆ t
⊢ s.erase a ⊆ t.erase a

Tactic:
val_le_iff.1 <| erase_le_erase _ <| val_le_iff.2 h

Premises used: Iff.mpr, Multiset.erase_le_erase, Iff.mp, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ s.erase a ⊆ s

Tactic:
Multiset.erase_subset _ _

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.erase, Multiset.erase_subset, Multiset.Subset
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ s ⊆ t.erase a ↔ s ⊆ t ∧ ¬a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (↑(s.erase a) : Set α) = (↑s : Set α) \ {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (s.erase a).erase a = s.erase a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Finset α
⊢ (s.erase a).erase b = (s.erase b).erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
⊢ s.erase x = s.erase y ↔ x = y

Tactic:
grind [eq_of_mem_of_notMem_erase]

Premises used: Finset.eq_of_mem_of_notMem_erase
-- Module: Mathlib.Data.Finset.Erase
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ Set.InjOn s.erase (↑s : Set α)

Tactic:
fun _ _ _ _ => (erase_inj s ‹_›).mp

Premises used: Finset.erase_inj, Iff.mp, Set.InjOn
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ (filter p s).val = Multiset.filter p s.val

Tactic:
rfl

Premises used: rfl, Multiset.filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ filter p s ⊆ s

Tactic:
Multiset.filter_subset _ _

Premises used: Multiset.filter_subset, Set.Mem, setOf, Multiset.Mem, Multiset.Subset, Multiset.filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
a : α
⊢ a ∈ filter p s ↔ a ∈ s ∧ p a

Tactic:
Multiset.mem_filter

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_filter, Multiset.filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
x : α
h : x ∈ filter p s
⊢ x ∈ s

Tactic:
Multiset.mem_of_mem_filter h

Premises used: Set.Mem, setOf, Multiset.mem_of_mem_filter, Multiset.Mem
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ filter p s ⊂ s ↔ ∃ (x : α), x ∈ s ∧ ¬p x

Tactic:
grind
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s : Finset α
⊢ filter q (filter p s) = filter (fun (a : α) ↦ p a ∧ q a) s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s : Finset α
⊢ filter q (filter p s) = filter p (filter q s)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
s : Finset α
p : α → Prop
h inst : DecidablePred p
⊢ filter p s = filter p s

Tactic:
congr
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
h : DecidablePred fun (x : α) ↦ True
s : Finset α
h₁ : ∀ (a : α), a ∈ filter (fun (x : α) ↦ True) s ↔ a ∈ s
⊢ filter (fun (x : α) ↦ True) s = s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
h : DecidablePred fun (x : α) ↦ True
s : Finset α
a : α
⊢ a ∈ filter (fun (x : α) ↦ True) s ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
h : DecidablePred fun (x : α) ↦ False
s : Finset α
h₁ : ∀ (a : α), a ∈ filter (fun (x : α) ↦ False) s ↔ Membership.mem (γ := Finset α) ∅ a
⊢ filter (fun (x : α) ↦ False) s = ∅

Tactic:
ext
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
h : DecidablePred fun (x : α) ↦ False
s : Finset α
a : α
⊢ a ∈ filter (fun (x : α) ↦ False) s ↔ Membership.mem (γ := Finset α) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ filter p s = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ (filter p s).Nonempty ↔ ∃ (a : α), a ∈ s ∧ p a

Tactic:
simp only [nonempty_iff_ne_empty, Ne, filter_eq_empty_iff, Classical.not_not, not_forall,
    exists_prop]

Premises used: Classical.not_not, Ne, Finset.nonempty_iff_ne_empty, exists_prop, Finset.filter_eq_empty_iff, Classical.not_forall
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
h : ∀ (x : α), x ∈ s → p x
⊢ filter p s = s

Tactic:
filter_eq_self.2 h

Premises used: Iff.mpr, Finset.filter_eq_self
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
h : ∀ (x : α), x ∈ s → ¬p x
⊢ filter p s = ∅

Tactic:
filter_eq_empty_iff.2 h

Premises used: Iff.mpr, Finset.filter_eq_empty_iff
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Finset α
pos : p → filter (fun (_a : α) ↦ p) s = s
neg : ¬p → filter (fun (_a : α) ↦ p) s = ∅
⊢ filter (fun (_a : α) ↦ p) s = if p then s else ∅

Tactic:
split_ifs
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Finset α
h : p
⊢ filter (fun (_a : α) ↦ p) s = s

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Finset α
h : ¬p
⊢ filter (fun (_a : α) ↦ p) s = ∅

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s : Finset α
H : ∀ (x : α), x ∈ s → (p x ↔ q x)
⊢ filter p s = filter q s

Tactic:
eq_of_veq <| Multiset.filter_congr H

Premises used: Finset.eq_of_veq, Multiset.filter_congr
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ filter p ∅ = ∅

Tactic:
subset_empty.1 <| filter_subset _ _

Premises used: Finset.subset_empty, Finset.filter_subset, Iff.mp
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Finset α
h : s ⊆ t
⊢ filter p s ⊆ filter p t

Tactic:
fun _a ha =>
  mem_filter.2 ⟨h (mem_filter.1 ha).1, (mem_filter.1 ha).2⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ Monotone (filter p)

Tactic:
fun _ _ => filter_subset_filter p

Premises used: Finset.filter_subset_filter, Monotone
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
s : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∀ (a : α), a ∈ s → p a → q a
⊢ filter p s ⊆ filter q s

Tactic:
simp +contextual [subset_iff, h]

Premises used: Finset.subset_iff
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ (↑(filter p s) : Set α) = {x : α | x ∈ s ∧ p x}

Tactic:
Set.ext fun _ => mem_filter

Premises used: Set.ext, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
t : Set α
h₁ : t ⊆ (↑s : Set α)
h₂ : ∀ (x : α), x ∈ t → p x
⊢ t ⊆ (↑(filter p s) : Set α)

Tactic:
fun x hx => (s.coe_filter p).symm ▸ ⟨h₁ hx, h₂ x hx⟩

Premises used: Finset.coe_filter, Eq.rec, Set.Subset, And.intro, Eq.symm
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
s t : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ Disjoint s t → Disjoint (filter p s) (filter q t)

Tactic:
Disjoint.mono (filter_subset _ _) (filter_subset _ _)

Premises used: Finset.filter_subset, Disjoint.mono
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) i
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ t ∧ f x = i

Tactic:
simpa using hi hx
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) i
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ f x ≠ j

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx

Premises used: rfl
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) i
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h₁ : f x ≠ j
⊢ u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx

Premises used: rfl
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)
⊢ x ∈ t ∧ f x = j

Tactic:
simpa using hj hx
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)
⊢ u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx

Premises used: rfl
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi hj₁ : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)
⊢ f x ≠ f x

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx

Premises used: rfl
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set β
t u : Finset α
x : α
hx : x ∈ u
hi hj : u ≤ (fun (x : β) ↦ filter (fun (x_1 : α) ↦ f x_1 = x) t) (f x)
h : f x ≠ f x
⊢ Membership.mem (γ := Finset α) ⊥ x

Tactic:
contradiction
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s x : Finset α
htp : x ≤ filter (fun (x : α) ↦ p x ∧ ¬q x) s
htq : x ≤ filter (fun (x : α) ↦ q x ∧ ¬p x) s
simp : x = ∅
⊢ x ≤ ⊥

Tactic:
simp only [bot_eq_empty, le_eq_subset, subset_empty]

Premises used: Finset.bot_eq_empty, Finset.subset_empty, Finset.le_eq_subset
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s x : Finset α
htp : x ≤ filter (fun (x : α) ↦ p x ∧ ¬q x) s
htq : x ≤ filter (fun (x : α) ↦ q x ∧ ¬p x) s
by_contra! : ∀ (w : α) (hx : w ∈ x), False
⊢ x = ∅

Tactic:
by_contra! ⟨_, hx⟩
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s x : Finset α
htp : x ≤ filter (fun (x : α) ↦ p x ∧ ¬q x) s
htq : x ≤ filter (fun (x : α) ↦ q x ∧ ¬p x) s
w : α
hx : w ∈ x
⊢ False

Tactic:
(mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1

Premises used: And.right, And.left, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s x : Finset α
htp : x ≤ filter (fun (x : α) ↦ p x ∧ ¬q x) s
htq : x ≤ filter (fun (x : α) ↦ q x ∧ ¬p x) s
w : α
hx : w ∈ x
⊢ False

Tactic:
exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1

Premises used: And.right, And.left, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Finset α
⊢ filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s : Finset α
⊢ filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Filter
Goal:
α : Type u_1
s t : Finset α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hst : s ⊆ t
⊢ filter (fun (x : α) ↦ x ∈ s) t = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
a : Fin n
⊢ a ∈ s.attachFin h ↔ (↑a : ℕ) ∈ s

Tactic:
⟨fun h ↦
    let ⟨_, hb₁, hb₂⟩ := Multiset.mem_pmap.1 h
    hb₂ ▸ hb₁,
    fun h ↦ Multiset.mem_pmap.2 ⟨a, h, Fin.eta _ _⟩⟩

Premises used: Iff.mpr, Membership.mem, Eq.rec, Fin.eta, _private.0.Finset.mem_attachFin.match_1, Fin.val, Iff.intro, Exists.intro, Iff.mp, Multiset.mem_pmap
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
h₁ :
  ∀ (x : Fin n), x ∈ (↑(s.attachFin h) : Set (Fin n)) ↔ Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' (↑s : Set ℕ)) x
⊢ (↑(s.attachFin h) : Set (Fin n)) = Fin.val ⁻¹' (↑s : Set ℕ)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
x : Fin n
⊢ x ∈ (↑(s.attachFin h) : Set (Fin n)) ↔ Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' (↑s : Set ℕ)) x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ #(s.attachFin h) = #s

Tactic:
Multiset.card_pmap _ _ _

Premises used: Multiset.card_pmap, Multiset.pmap, Finset.card
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
a : (↑(image Fin.val (s.attachFin h)) : Set ℕ) = (↑s : Set ℕ)
⊢ image Fin.val (s.attachFin h) = s

Tactic:
apply coe_injective

Premises used: Finset.coe_injective
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
a : (↑s : Set ℕ) ⊆ Set.range (ι := Fin n) Fin.val
⊢ (↑(image Fin.val (s.attachFin h)) : Set ℕ) = (↑s : Set ℕ)

Tactic:
rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]

Premises used: Finset.coe_attachFin, Finset.coe_image, Set.image_preimage_eq_iff
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ (↑s : Set ℕ) ⊆ Set.range (ι := Fin n) Fin.val

Tactic:
fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩

Premises used: Set.Mem, setOf, Fin.mk, Set.Subset, Exists.intro, Set.range, rfl
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ (↑s : Set ℕ) ⊆ Set.range (ι := Fin n) Fin.val

Tactic:
exact fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ map Fin.valEmbedding (s.attachFin h) = s

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t

Tactic:
simp [← map_subset_map (f := Fin.valEmbedding)]

Premises used: Finset.map_subset_map
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s t : Finset ℕ
hst : s ⊆ t
ht : ∀ m ∈ t, m < n
⊢ s.attachFin ⋯ ⊆ t.attachFin ht

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t

Tactic:
simp [← map_ssubset_map (f := Fin.valEmbedding)]

Premises used: Finset.map_ssubset_map
-- Module: Mathlib.Data.Finset.Fin
Goal:
n : ℕ
s t : Finset ℕ
hst : s ⊂ t
ht : ∀ m ∈ t, m < n
⊢ s.attachFin ⋯ ⊂ t.attachFin ht

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)

Tactic:
mem_map.trans ⟨?_, ?_⟩

Premises used: Set.Mem, setOf, Iff.intro, Iff.trans, Finset.mem_map
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
refine_1 :
  (∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f) →
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)
refine_2 :
  (f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)) →
    ∃ a ∈ s.pi (β := fun (a : ι) ↦ α) t,
      ({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) a = f
⊢ Membership.mem (γ := Finset (ι →₀ α)) (s.finsupp t) f ↔
    f.support ⊆ s ∧ ∀ i ∈ s, Membership.mem (α := α) (t i) ((f : (a : ι) → α) i : α)

Tactic:
refine mem_map.trans ⟨?_, ?_⟩

Premises used: Iff.intro, Iff.trans, Finset.mem_map
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
⊢ support.{u_1, u_2} (M := α) (({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f) ⊆ s ∧
    ∀ i ∈ s,
      Membership.mem (α := α) (t i)
        (((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)

Tactic:
⟨support_indicator_subset _ _, fun i hi => ?_⟩

Premises used: And.intro, Finsupp.support_indicator_subset
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
refine_1 :
  ∀ (i : ι) (hi : i ∈ s),
    Membership.mem (α := α) (t i)
      (((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)
⊢ support.{u_1, u_2} (M := α) (({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f) ⊆ s ∧
    ∀ i ∈ s,
      Membership.mem (α := α) (t i)
        (((({ toFun := indicator s, inj' := ⋯ } : (a : (i : ι) → i ∈ s → α) → ι →₀ α) f : ι →₀ α) : (a : ι) → α) i : α)

Tactic:
refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩
-- Module: Mathlib.Data.Finset.Finsupp
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi (β := fun (a : ι) ↦ α) t
i : ι
hi : i ∈ s
⊢ f i hi ∈ t i

Tactic:
mem_pi.1 hf i hi

Premises used: Finset.mem_pi, Iff.mp