awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : α → Prop
inst_2 : DecidablePred p
inst_3 : (x : α) → Decidable ¬p x
⊢ ∀ (a : α), a ∈ (filter p univ)ᶜ ↔ Membership.mem (γ := Finset α) {x : α | ¬p x} a

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ sᶜ ≠ univ ↔ s.Nonempty

Tactic:
simp [eq_univ_iff_forall, Finset.Nonempty]

Premises used: Finset.eq_univ_iff_forall, Finset.Nonempty
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : univ \ {a} = erase univ a
rw₁ rw₂ : erase univ a = erase univ a
⊢ {a}ᶜ = erase univ a

Tactic:
rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]

Premises used: Finset.compl_eq_univ_sdiff, Finset.sdiff_singleton_eq_erase
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw : Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑s : Set α)ᶜ
⊢ Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑sᶜ : Set α)

Tactic:
rw [coe_compl]

Premises used: Finset.coe_compl
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑s : Set α)ᶜ

Tactic:
s.insert_inj_on

Premises used: Finset.insert_inj_on
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑s : Set α)ᶜ

Tactic:
exact s.insert_inj_on

Premises used: Finset.insert_inj_on
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Fintype β
f : β → α
hf : Surjective f
⊢ image f univ = univ

Tactic:
eq_univ_of_forall <| hf.forall.2 fun _ => mem_image_of_mem _ <| mem_univ _

Premises used: Iff.mpr, Finset.mem_univ, Function.Surjective.forall, Finset.eq_univ_of_forall, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Fintype β
f : β ≃ α
⊢ Eq.{u_1 + 1} (α := Finset α) (image.{u_2, u_1} (α := β) (⇑f : (a : β) → α) univ) univ

Tactic:
Finset.image_univ_of_surjective f.surjective

Premises used: Finset.image_univ_of_surjective, Equiv.surjective
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
h : ∀ (a : α), a ∈ univ ∩ s ↔ a ∈ s
⊢ univ ∩ s = s

Tactic:
ext a
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw : univ ∩ s = s
rw₁ rw₂ : s = s
⊢ s ∩ univ = s

Tactic:
rw [inter_comm, univ_inter]

Premises used: Finset.inter_comm, Finset.univ_inter
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ s ∩ t = univ ↔ s = univ ∧ t = univ

Tactic:
inf_eq_top_iff

Premises used: inf_eq_top_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Subsingleton α
a : α
h : ∀ (b : α), Membership.mem (γ := Finset α) {a} b ↔ Membership.mem (γ := Finset α) univ b
⊢ Eq (α := Finset α) {a} univ

Tactic:
ext b
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Subsingleton α
a b : α
⊢ Membership.mem (γ := Finset α) {a} b ↔ Membership.mem (γ := Finset α) univ b

Tactic:
simp [Subsingleton.elim a b]

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : β ↪ α
hf : Surjective.{u_2 + 1, u_1 + 1} (α := β) (β := α) (⇑f : (a : β) → α)
⊢ map f univ = univ

Tactic:
eq_univ_of_forall <| hf.forall.2 fun _ => mem_map_of_mem _ <| mem_univ _

Premises used: Iff.mpr, Finset.mem_univ, Function.Surjective.forall, Finset.eq_univ_of_forall, Finset.mem_map_of_mem
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : β ≃ α
⊢ map f.toEmbedding univ = univ

Tactic:
map_univ_of_surjective f.surjective

Premises used: Finset.map_univ_of_surjective, Equiv.surjective
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : Fintype β
e : α ≃ β
b : β
⊢ (e.toEmbedding : (a : α) → β) ((e.symm : (a : β) → α) b : α) = b

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
inst_1 : Fintype β
inst_2 : DecidablePred fun (y : β) ↦ ∃ (x : α), f x = y
inst_3 : DecidableEq β
h : ∀ (a : β), Membership.mem (γ := Finset β) {y : β | ∃ (x : α), f x = y} a ↔ a ∈ image f univ
⊢ {y : β | ∃ (x : α), f x = y} = image f univ

Tactic:
ext
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
inst_1 : Fintype β
inst_2 : DecidablePred fun (y : β) ↦ ∃ (x : α), f x = y
inst_3 : DecidableEq β
a : β
⊢ Membership.mem (γ := Finset β) {y : β | ∃ (x : α), f x = y} a ↔ a ∈ image f univ

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
inst_1 : Fintype β
inst_2 : DecidablePred fun (y : β) ↦ y ∈ Set.range f
inst_3 : DecidableEq β
⊢ {y : β | y ∈ Set.range f} = image f univ

Tactic:
grind
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
⊢ (↑(filter p univ) : Set α) = {x : α | p x}

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : Fintype { a : α // p a }
⊢ Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
⊢ Finset.subtype p univ = univ

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
rw : map (Embedding.subtype p) univ = map (Embedding.subtype p) (Finset.subtype p univ)
rw₁ rw₂ : map (Embedding.subtype p) univ = map (Embedding.subtype p) univ
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
rw [← subtype_map, subtype_univ]

Premises used: Finset.subtype_map, Finset.subtype_univ
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
apply : (map (Embedding.subtype p) univ).val = (filter p univ).val
⊢ Multiset.map (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (val univ) = (filter p univ).val

Tactic:
apply (map_val (Function.Embedding.subtype p) univ).symm.trans

Premises used: Finset.univ, Finset.map_val, Function.Embedding.subtype, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
h : map (Embedding.subtype p) univ = filter p univ
⊢ (map (Embedding.subtype p) univ).val = (filter p univ).val

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
apply univ_map_subtype

Premises used: Finset.univ_map_subtype
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype { a : α // p a }
rw :
  Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
    Multiset.map f (Multiset.map (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (val univ))
rw₁ :
  Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) =
    Multiset.map (α := { a : α // p a }) (f ∘ Subtype.val (p := fun (a : α) ↦ p a)) (val univ)
rw₂ rw₃ :
  Multiset.map (α := Subtype p) (f ∘ fun (a : Subtype p) ↦ (↑a : α)) (val univ) =
    Multiset.map (α := { a : α // p a }) (f ∘ Subtype.val (p := fun (a : α) ↦ p a)) (val univ)
⊢ Multiset.map (Subtype.restrict (β := fun (x : α) ↦ β) p f) (val univ) = Multiset.map f (filter p univ).val

Tactic:
rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]

Premises used: Finset.univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ {x : α | x ∈ s} = s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s = s.val.card

Tactic:
rfl

Premises used: Finset.card, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ s.val.card = #s

Tactic:
rfl

Premises used: Finset.card, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
m : Multiset α
nodup : m.Nodup
⊢ #{ val := m, nodup := nodup : Finset α } = m.card

Tactic:
rfl

Premises used: Finset.card, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
⊢ card.{u_1} (α := α) ∅ = 0

Tactic:
rfl

Premises used: Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
⊢ s ⊆ t → #s ≤ #t

Tactic:
Multiset.card_le_card ∘ val_le_iff.mpr

Premises used: Iff.mpr, Multiset.card_le_card, Function.comp, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
⊢ Monotone.{u_1, 0} (α := Finset α) card

Tactic:
apply card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s = 0 ↔ s = ∅

Tactic:
Multiset.card_eq_zero.trans val_eq_zero

Premises used: Multiset.card_eq_zero, Finset.val_eq_zero, Finset.card, Iff.trans
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s ≠ 0 ↔ s.Nonempty

Tactic:
card_eq_zero.ne.trans nonempty_iff_ne_empty.symm

Premises used: Finset.nonempty_iff_ne_empty, Finset.card_eq_zero, Iff.ne, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ 0 < #s ↔ s.Nonempty

Tactic:
Nat.pos_iff_ne_zero.trans card_ne_zero

Premises used: Nat.pos_iff_ne_zero, Iff.trans, Finset.card_ne_zero
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ 1 ≤ #s ↔ s.Nonempty

Tactic:
card_pos

Premises used: Finset.card_pos, Nat.lt
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∈ s
⊢ #s ≠ 0

Tactic:
(not_congr card_eq_zero).2 <| ne_empty_of_mem h

Premises used: Iff.mpr, Finset.ne_empty_of_mem, Finset.card_eq_zero, not_congr
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
a : α
⊢ card (α := α) {a} = 1

Tactic:
Multiset.card_singleton _

Premises used: Multiset.card_singleton, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ #({a} ∩ s) ≤ 1

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
⊢ #(cons a s h) = #s + 1

Tactic:
Multiset.card_cons _ _

Premises used: Multiset.cons, Multiset.card_cons, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
h : a ∉ s
⊢ #(insert a s) = #s + 1

Tactic:
grind [=_ cons_eq_insert]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
h : a ∈ s
rw rw₁ : #s = #s
⊢ #(insert a s) = #s

Tactic:
rw [insert_eq_of_mem h]

Premises used: Finset.insert_eq_of_mem
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ #(insert a s) ≤ #s + 1

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
⊢ card (α := α) {a, b} ≤ 2

Tactic:
card_insert_le _ _

Premises used: Finset.card_insert_le, Finset.card, Multiset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
⊢ card (α := α) {a, b, c} ≤ 3

Tactic:
(card_insert_le _ _).trans (Nat.succ_le_succ card_le_two)

Premises used: Finset.card_insert_le, Finset.card_le_two, LE.le.trans, Nat.succ_le_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
a b c d : α
⊢ card (α := α) {a, b, c, d} ≤ 4

Tactic:
(card_insert_le _ _).trans (Nat.succ_le_succ card_le_three)

Premises used: Finset.card_le_three, Finset.card_insert_le, LE.le.trans, Nat.succ_le_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
a b c d e : α
⊢ card (α := α) {a, b, c, d, e} ≤ 5

Tactic:
(card_insert_le _ _).trans (Nat.succ_le_succ card_le_four)

Premises used: Finset.card_le_four, Finset.card_insert_le, LE.le.trans, Nat.succ_le_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
a b c d e f : α
⊢ card (α := α) {a, b, c, d, e, f} ≤ 6

Tactic:
(card_insert_le _ _).trans (Nat.succ_le_succ card_le_five)

Premises used: Finset.card_le_five, Finset.card_insert_le, LE.le.trans, Nat.succ_le_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
a b : α
inst : DecidableEq α
⊢ card (α := α) {a, b} = 1 ∨ card (α := α) {a, b} = 2

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
a b : α
inst : DecidableEq α
⊢ card (α := α) {a, b} = 2 ↔ a ≠ b

Tactic:
aesop (add simp card_insert_eq_ite)

Premises used: Finset.card_insert_eq_ite
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
a b c : α
inst : DecidableEq α
⊢ card (α := α) {a, b, c} = 3 ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
aesop (add simp card_insert_eq_ite)

Premises used: Finset.card_insert_eq_ite
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ a ∈ s → #(s.erase a) = #s - 1

Tactic:
Multiset.card_erase_of_mem

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.card_erase_of_mem, Multiset.erase, Finset.card, Multiset.card, Nat.pred
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ a ∈ s → #(s.erase a) + 1 = #s

Tactic:
Multiset.card_erase_add_one

Premises used: Set.Mem, setOf, Multiset.card_erase_add_one, Multiset.Mem, Multiset.erase, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ a ∈ s → #(s.erase a) < #s

Tactic:
Multiset.card_erase_lt_of_mem

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.erase, Finset.card, Multiset.card_erase_lt_of_mem
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ #(s.erase a) ≤ #s

Tactic:
Multiset.card_erase_le

Premises used: Multiset.card_erase_le, Multiset.erase, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
⊢ #(s.erase a) = if a ∈ s then #s - 1 else #s

Tactic:
Multiset.card_erase_eq_ite

Premises used: Set.Mem, setOf, Multiset.card_erase_eq_ite, Multiset.Mem, Multiset.erase, Finset.card, Multiset.card, Nat.pred
-- Module: Mathlib.Data.Finset.Card
Goal:
n : ℕ
⊢ #(range n) = n

Tactic:
Multiset.card_range n

Premises used: Multiset.card_range, Multiset.ofList, Finset.card, Multiset.range
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s.attach = #s

Tactic:
Multiset.card_attach

Premises used: Set.Mem, setOf, Multiset.card_attach, Multiset.Mem, Multiset.pmap, Finset.card, Multiset.attach
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ #m.toFinset = m.dedup.card

Tactic:
rfl

Premises used: Multiset.dedup, Finset.card, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ #m.toFinset ≤ m.card

Tactic:
card_le_card <| dedup_le _

Premises used: Multiset.card_le_card, Multiset.dedup_le, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
h : m.Nodup
⊢ #m.toFinset = m.card

Tactic:
congr_arg card <| Multiset.dedup_eq_self.mpr h

Premises used: Iff.mpr, Multiset.dedup_eq_self, congr_arg, Finset.card, Multiset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ m.dedup.card = m.card ↔ m.Nodup

Tactic:
.trans ⟨fun h ↦ eq_of_le_of_card_le (dedup_le m) h.ge, congr_arg _⟩ dedup_eq_self

Premises used: Multiset.dedup_eq_self, Eq.ge, congr_arg, Multiset.dedup_le, Iff.intro, Iff.trans, Multiset.eq_of_le_of_card_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ #m.toFinset = m.card ↔ m.Nodup

Tactic:
dedup_card_eq_card_iff_nodup

Premises used: Multiset.dedup_card_eq_card_iff_nodup, Multiset.dedup, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ #l.toFinset = l.dedup.length

Tactic:
rfl

Premises used: Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ #l.toFinset ≤ l.length

Tactic:
Multiset.toFinset_card_le ⟦l⟧

Premises used: Multiset.toFinset_card_le, List.toFinset, Quotient.mk, Multiset.ofList, Multiset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ #l.toFinset = l.length

Tactic:
Multiset.toFinset_card_of_nodup h

Premises used: List.toFinset, Multiset.toFinset_card_of_nodup, Multiset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
rw : s.val.toList.length = #s
rw₁ : (↑s.val.toList : Multiset α).card = #s
rw₂ : s.val.card = #s
rw₃ rw₄ : s.val.card = s.val.card
⊢ s.toList.length = #s

Tactic:
rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]

Premises used: Multiset.coe_toList, Finset.toList, Multiset.coe_card, Finset.card_def
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
⊢ #(image f s) ≤ #s

Tactic:
simpa only [card_map] using (s.1.map f).toFinset_card_le

Premises used: Multiset.map, Multiset.toFinset_card_le, Finset.val, Multiset.card_map
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : Set.InjOn f (↑s : Set α)
⊢ #(image f s) = #s

Tactic:
simp only [card, image_val_of_injOn H, card_map]

Premises used: Finset.image_val_of_injOn, Finset.card, Multiset.card_map
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : #(image f s) = #s
⊢ { val := (Multiset.map f s.val).dedup, nodup := ⋯ : Finset β }.val.card = s.val.card

Tactic:
rw [card_def, card_def, image, toFinset] at H

Premises used: Multiset.toFinset, Finset.card_def, Finset.image
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val

Tactic:
Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_

Premises used: Multiset.dedup_le, Multiset.eq_of_le_of_card_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
refine : (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val

Tactic:
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_

Premises used: Multiset.dedup_le, Multiset.eq_of_le_of_card_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card

Tactic:
simp only [H, Multiset.card_map, le_rfl]

Premises used: le_rfl, Multiset.card_map
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val

Tactic:
have : (s.1.map f).dedup = s.1.map f := by
    refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
    simp only [H, Multiset.card_map, le_rfl]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ (Multiset.map f s.val).Nodup

Tactic:
rw [Multiset.dedup_eq_self] at this

Premises used: Multiset.dedup_eq_self
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).Nodup
⊢ Set.InjOn f (↑s : Set α)

Tactic:
inj_on_of_nodup_map this

Premises used: Set.Mem, setOf, Multiset.inj_on_of_nodup_map, Multiset.Mem, Set.InjOn
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).Nodup
⊢ Set.InjOn f (↑s : Set α)

Tactic:
exact inj_on_of_nodup_map this

Premises used: Multiset.inj_on_of_nodup_map
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
⊢ #(image f s) = #s ↔ Set.InjOn f (↑s : Set α)

Tactic:
⟨injOn_of_card_image_eq, card_image_of_injOn⟩

Premises used: Finset.injOn_of_card_image_eq, Iff.intro, Finset.card_image_of_injOn
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : DecidableEq β
s : Finset α
H : Injective f
⊢ #(image f s) = #s

Tactic:
card_image_of_injOn fun _ _ _ _ h => H h

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst : DecidableEq β
y : β
rw : 0 < #({x ∈ s | f x = y}) ↔ y ∈ image f s
rw₁ : {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s
rw₂ rw₃ : y ∈ image f s ↔ y ∈ image f s
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s

Tactic:
rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]

Premises used: Nat.pos_iff_ne_zero, Finset.fiber_nonempty_iff_mem_image, Finset.card_pos
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
P : α → Prop
inst : DecidablePred P
n : ℕ
H : ∀ s' ≤ s.val, n < s'.card → ∃ a ∈ s', ¬P a
s' : Finset α
hs' : s' ⊆ s
h : n < #s'
⊢ s'.val ≤ s.val

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α ↪ β
⊢ #(map f s) = #s

Tactic:
Multiset.card_map _ _

Premises used: Multiset.map, Finset.card, Multiset.card_map
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ #(Finset.subtype p s) = #(filter p s)

Tactic:
simp [Finset.subtype]

Premises used: Finset.subtype
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
⊢ #(filter p s) ≤ #s

Tactic:
card_le_card <| filter_subset _ _

Premises used: Finset.card_le_card, Finset.filter_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
h : s ⊆ t
h₂ : #t ≤ #s
⊢ s = t

Tactic:
eq_of_veq <| Multiset.eq_of_le_of_card_le (val_le_iff.mpr h) h₂

Premises used: Iff.mpr, Finset.eq_of_veq, Multiset.eq_of_le_of_card_le, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
hst : s ⊆ t
⊢ #t ≤ #s ↔ s = t

Tactic:
⟨eq_of_subset_of_card_le hst, (ge_of_eq <| congr_arg _ ·)⟩

Premises used: ge_of_eq, congr_arg, Iff.intro, Finset.card, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
hst : s ⊆ t
hts : #t ≤ #s
⊢ t = s

Tactic:
(eq_of_subset_of_card_le hst hts).symm

Premises used: Finset.eq_of_subset_of_card_le, Eq.symm