awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ #sᶜ < Fintype.card α ↔ s.Nonempty

Tactic:
sᶜ.card_lt_iff_ne_univ.trans s.compl_ne_univ_iff_nonempty

Premises used: Compl.compl, Finset.compl_ne_univ_iff_nonempty, Finset.card_lt_iff_ne_univ, Iff.trans
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ #(univ \ s) = Fintype.card α - #s

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ #sᶜ = Fintype.card α - #s

Tactic:
Finset.card_univ_diff s

Premises used: Finset.card_univ_diff
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
rw : #s + (Fintype.card α - #s) = Fintype.card α
rw₁ : #s + Fintype.card α - #s = Fintype.card α
rw₂ rw₃ : Fintype.card α = Fintype.card α
⊢ #s + #sᶜ = Fintype.card α

Tactic:
rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]

Premises used: Finset.card_compl, Nat.add_sub_assoc, Nat.add_sub_cancel_left, Finset.card_le_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
rw : #s + #sᶜ = Fintype.card α
rw₁ rw₂ : Fintype.card α = Fintype.card α
⊢ #sᶜ + #s = Fintype.card α

Tactic:
rw [Nat.add_comm, card_add_card_compl]

Premises used: Finset.card_add_card_compl, Nat.add_comm
-- Module: Mathlib.Data.Fintype.Card
Goal:
ι : Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = card.{u_4} (α := ι) univ
rwa rwa₁ rwa₂ rwa₃ : Disjoint S₁ S₂
⊢ S₂ ⊆ S₁ᶜ

Tactic:
rwa [Finset.subset_compl_iff_disjoint_left]

Premises used: Finset.subset_compl_iff_disjoint_left
-- Module: Mathlib.Data.Fintype.Card
Goal:
ι : Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = card.{u_4} (α := ι) univ
⊢ #S₁ᶜ ≤ #S₂

Tactic:
simp [← Nat.add_le_add_iff_left (n := S₁.card), h']

Premises used: Nat.add_le_add_iff_left
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
rw : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
rw₁ : #sᶜ.toFinset = card α - #s.toFinset
rw₂ : #sᶜ.toFinset = #s.toFinsetᶜ
rw₃ rw₄ : #s.toFinsetᶜ = #s.toFinsetᶜ
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)

Tactic:
rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

Premises used: Set.toFinset_compl, Finset.card_compl, Set.toFinset_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
classical : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
classical₁ : #sᶜ.toFinset = card α - #s.toFinset
classical₂ : #sᶜ.toFinset = #s.toFinsetᶜ
classical₃ classical₄ : #s.toFinsetᶜ = #s.toFinsetᶜ
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)

Tactic:
classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

Premises used: Set.toFinset_compl, Finset.card_compl, Set.toFinset_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
y : α
inst : Fintype { x : α // x = y }
⊢ card.{u_1} { x : α // x = y } = 1

Tactic:
Fintype.card_unique

Premises used: Fintype.card_unique
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
y : α
inst : Fintype { x : α // y = x }
⊢ card.{u_1} { x : α // y = x } = 1

Tactic:
Fintype.card_unique

Premises used: Fintype.card_unique
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ card Empty = 0

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ card PEmpty.{u_4 + 1} = 0

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ card Unit = 1

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ card PUnit.{u_4 + 1} = 1

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ card Bool = 2

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
⊢ card (ULift.{u_5, u_4} α) = card α

Tactic:
Fintype.ofEquiv_card _

Premises used: Fintype.ofEquiv_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
⊢ card.{u_4 + 1} (PLift α) = card α

Tactic:
Fintype.ofEquiv_card _

Premises used: Fintype.ofEquiv_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
⊢ card.{u_4} αᵒᵈ = card α

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
⊢ card.{u_4} (Lex α) = card α

Tactic:
rfl

Premises used: Lex, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
h : Fintype (↑Set.univ : Type u_1)
H : ∀ (x : α), Membership.mem (γ := Finset α) univ x ↔ Membership.mem (γ := Set α) Set.univ x
⊢ card.{u_1} (↑Set.univ : Type u_1) = card α

Tactic:
apply Fintype.card_of_finset'

Premises used: Fintype.card_of_finset'
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
h : Fintype (↑Set.univ : Type u_1)
⊢ ∀ (x : α), Membership.mem (γ := Finset α) univ x ↔ Membership.mem (γ := Set α) Set.univ x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
h : Fintype { _a : α // True }
H : ∀ (x : α), Membership.mem (γ := Finset α) univ x ↔ True
⊢ card.{u_1} { _a : α // True } = card α

Tactic:
apply Fintype.card_of_subtype

Premises used: Fintype.card_of_subtype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
h : Fintype { _a : α // True }
⊢ ∀ (x : α), Membership.mem (γ := Finset α) univ x ↔ True

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Finite α
intro : ∀ (val : Fintype α), ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
⊢ ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
intro : ∀ (l : List α) (e : ⟦l⟧ = Finset.val univ), ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
⊢ ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1

Premises used: Finset.univ, Finset.val, Quotient.exists_rep
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
l : List α
e : ⟦l⟧ = Finset.val univ
⊢ Multiset.Nodup.{u_4} (α := α) (Finset.val univ) ∧ ∀ (x : α), Membership.mem (γ := Multiset α) (Finset.val univ) x

Tactic:
have := And.intro (@univ α _).2 (@mem_univ_val α _)
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
l : List α
e : ⟦l⟧ = Finset.val univ
this : Multiset.Nodup.{u_4} (α := α) (Finset.val univ) ∧ ∀ (x : α), Membership.mem (γ := Multiset α) (Finset.val univ) x
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Multiset.Nodup ⟦l⟧ ∧ ∀ (x : α), x ∈ ⟦l⟧), l.Nodup ∧ ∀ (x : α), x ∈ l
⊢ l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
rwa [← e] at this
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
l : List α
e : ⟦l⟧ = Finset.val univ
this : Multiset.Nodup.{u_4} (α := α) (Finset.val univ) ∧ ∀ (x : α), Membership.mem (γ := Multiset α) (Finset.val univ) x
⊢ ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
exact ⟨_, by rwa [← e] at this⟩
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

Premises used: Eq.rec, List.toFinset, Finset.card_le_univ, List.toFinset_card_of_nodup
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
hf : Injective f
⊢ card α ≤ card β

Tactic:
Finset.card_le_card_of_injOn f (fun _ _ => Finset.mem_univ _) fun _ _ _ _ h => hf h

Premises used: Finset.mem_univ, Finset.card_le_card_of_injOn, Fintype.card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : card β < card α
⊢ ¬Injective f

Tactic:
Nat.not_le_of_lt h ∘ card_le_of_injective f

Premises used: Fintype.card_le_of_injective, Nat.not_le_of_lt, Function.comp, Not
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α ↪ β
⊢ card α ≤ card β

Tactic:
card_le_of_injective f f.2

Premises used: Fintype.card_le_of_injective, Function.Embedding.inj', DFunLike.coe
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
rwa : b ∉ (↑(map { toFun := f, inj' := h : α ↪ β } univ) : Set β)
rwa₁ : b ∉ (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) '' (↑univ : Set α)
rwa₂ : b ∉ Set.image.{u_1, u_2} (α := α) (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) Set.univ
rwa₃ rwa₄ rwa₅ rwa₆ : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β)
⊢ b ∉ map { toFun := f, inj' := h : α ↪ β } univ

Tactic:
rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_map, Finset.mem_coe
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Injective f
h' : ¬Surjective f
⊢ card α < card β

Tactic:
let ⟨_y, hy⟩ := not_forall.1 h'
  card_lt_of_injective_of_notMem f h hy

Premises used: _private.0.Fintype.card_lt_of_injective_not_surjective.match_1, Fintype.card, Fintype.card_lt_of_injective_of_notMem, LT.lt, Iff.mp, Classical.not_forall
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Surjective f
⊢ card β ≤ card α

Tactic:
card_le_of_injective _ (Function.injective_surjInv h)

Premises used: Fintype.card_le_of_injective, Function.injective_surjInv
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
β : Type u_5
f : α → β
inst : Fintype α
inst_1 : Fintype (↑(Set.range f) : Type u_5)
a : α
⊢ f a ∈ Set.range f

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
β : Type u_5
f : α → β
inst : Fintype α
inst_1 : Fintype (↑(Set.range f) : Type u_5)
x : (↑(Set.range f) : Type u_5)
val : β
a : α
ha : f a = val
⊢ Eq (α := (↑(Set.range f) : Type u_5)) ((fun (a : α) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) (f a) ⋯) a)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) val ⋯)

Tactic:
simpa using ha
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
β : Type u_5
F : Type u_6
inst : FunLike F α β
inst_1 : EmbeddingLike F α β
f : F
inst_2 : Fintype α
inst_3 : Fintype (↑(Set.range.{u_5, u_4 + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_5)
⊢ card.{u_5} (↑(Set.range.{u_5, u_4 + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_5) = card α

Tactic:
Eq.symm <| Fintype.card_congr <| Equiv.ofInjective _ <| EmbeddingLike.injective f

Premises used: Fintype.card_congr, Equiv.ofInjective, EmbeddingLike.injective, Eq.symm
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
rw : Finset.card.{u_1} (α := α) univ = 0 ↔ IsEmpty α
rw₁ : Eq.{u_1 + 1} (α := Finset α) univ ∅ ↔ IsEmpty α
rw₂ rw₃ : IsEmpty α ↔ IsEmpty α
⊢ card α = 0 ↔ IsEmpty α

Tactic:
rw [card, Finset.card_eq_zero, univ_eq_empty_iff]

Premises used: Fintype.card, Finset.card_eq_zero, Finset.univ_eq_empty_iff
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
inst_1 : IsEmpty α
⊢ card α = 0

Tactic:
card_eq_zero_iff.2 ‹_›

Premises used: Iff.mpr, Fintype.card_eq_zero_iff
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
⊢ 0 < card α ↔ Nonempty α

Tactic:
Nat.pos_iff_ne_zero.trans <| not_iff_comm.mp <| not_nonempty_iff.trans card_eq_zero_iff.symm

Premises used: Nat.pos_iff_ne_zero, not_nonempty_iff, Fintype.card_eq_zero_iff, Iff.mp, Iff.trans, Iff.symm, not_iff_comm
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
h : Nonempty α
⊢ 0 < card α

Tactic:
card_pos_iff.mpr h

Premises used: Iff.mpr, Fintype.card_pos_iff
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
⊢ card α ≠ 0

Tactic:
_root_.ne_of_gt card_pos

Premises used: ne_of_gt, Fintype.card_pos
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
inst_1 : Fintype β
inst_2 : Nonempty α
⊢ NeZero (card α)

Tactic:
⟨card_ne_zero⟩

Premises used: NeZero.mk, Fintype.card_ne_zero
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
rw : (∃! a : α, p a) ↔ ∃ (a : α), Eq (α := Finset α) {x : α | p x} {a}
⊢ (∃! a : α, p a) ↔ Finset.card.{u_4} (α := α) {x : α | p x} = 1

Tactic:
rw [Finset.card_eq_one]

Premises used: Finset.card_eq_one
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
⊢ (∃! a : α, p a) ↔ ∃ (a : α), Eq (α := Finset α) {x : α | p x} {a}

Tactic:
exists_congr fun x => ?_

Premises used: exists_congr, ExistsUnique
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
refine :
  ∀ (x : α), ((fun (a : α) ↦ p a) x ∧ ∀ (y : α), (fun (a : α) ↦ p a) y → y = x) ↔ Eq (α := Finset α) {x : α | p x} {x}
⊢ (∃! a : α, p a) ↔ ∃ (a : α), Eq (α := Finset α) {x : α | p x} {a}

Tactic:
refine exists_congr fun x => ?_

Premises used: exists_congr
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
x : α
⊢ ((fun (a : α) ↦ p a) x ∧ ∀ (y : α), (fun (a : α) ↦ p a) y → y = x) ↔ Eq (α := Finset α) {x : α | p x} {x}

Tactic:
simp only [Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff, and_comm,
    mem_filter_univ]

Premises used: Finset.mem_filter_univ, Finset.Subset.antisymm_iff, Finset.singleton_subset_iff, and_comm, Finset.subset_singleton_iff'
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
simp_rw : 2 < Finset.card.{u_1} (α := α) univ ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₁ :
  (∃ (a : α) (b : α) (c : α),
      Membership.mem (γ := Finset α) univ a ∧
        Membership.mem (γ := Finset α) univ b ∧ Membership.mem (γ := Finset α) univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
    ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₂ :
  (∃ (a : α) (b : α) (c : α), True ∧ True ∧ True ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
    ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 2 < card α ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]

Premises used: Finset.mem_univ, Finset.card_univ, Fintype.two_lt_card_iff, true_and
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
hf : Bijective f
⊢ card α = card β

Tactic:
card_congr (Equiv.ofBijective f hf)

Premises used: Fintype.card_congr, Equiv.ofBijective
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
have : ∀ (this : (a : Prop) → Decidable a), ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = x

Tactic:
have := Classical.propDecidable
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
intro : ∀ (val : Fintype α), ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = x

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
⊢ image f univ = univ

Tactic:
have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _)
      ((card_image_of_injective univ hinj).symm ▸ le_rfl)
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
h₁ : image f univ = univ
⊢ x ∈ image f univ

Tactic:
have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
intro : ∀ (y : α) (h : Membership.mem (γ := Finset α) univ y ∧ f y = x), ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = x

Tactic:
obtain ⟨y, h⟩ := mem_image.1 h₂

Premises used: Finset.mem_image, Iff.mp
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : Membership.mem (γ := Finset α) univ y ∧ f y = x
⊢ ∃ (a : α), f a = x

Tactic:
⟨y, h.2⟩

Premises used: And.right, Exists.intro
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : Membership.mem (γ := Finset α) univ y ∧ f y = x
⊢ ∃ (a : α), f a = x

Tactic:
exact ⟨y, h.2⟩
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
⊢ Injective f ↔ Surjective f

Tactic:
⟨surjective_of_injective, fun hsurj =>
    HasLeftInverse.injective ⟨surjInv hsurj, leftInverse_of_surjective_of_rightInverse
      (surjective_of_injective (injective_surjInv _))
      (rightInverse_surjInv _)⟩⟩

Premises used: Function.HasLeftInverse.injective, Function.surjInv, Iff.intro, Exists.intro, Function.rightInverse_surjInv, Finite.surjective_of_injective, Function.leftInverse_of_surjective_of_rightInverse, Function.injective_surjInv
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
⊢ Injective f ↔ Bijective f

Tactic:
simp [Bijective, injective_iff_surjective]

Premises used: Function.Bijective, Finite.injective_iff_surjective
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
f : α → α
⊢ Surjective f ↔ Bijective f

Tactic:
simp [Bijective, injective_iff_surjective]

Premises used: Function.Bijective, Finite.injective_iff_surjective
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
e : α ≃ β
this : Injective (β := α) ((⇑e.symm : (a : β) → α) ∘ f) ↔ Surjective (β := α) ((⇑e.symm : (a : β) → α) ∘ f)
hinj : Injective f
⊢ Surjective f

Tactic:
simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj))

Premises used: Function.comp, Function.Injective.comp, Iff.mp, Function.Surjective.comp, Equiv.injective, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
e : α ≃ β
this : Injective (β := α) ((⇑e.symm : (a : β) → α) ∘ f) ↔ Surjective (β := α) ((⇑e.symm : (a : β) → α) ∘ f)
hsurj : Surjective f
⊢ Injective f

Tactic:
simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))

Premises used: Iff.mpr, Function.comp, Function.Injective.comp, Function.Surjective.comp, Equiv.injective, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
s : Finset α
inst : Fintype ↥s
⊢ card.{u_1} ↥s = #s

Tactic:
@Fintype.card_of_finset' _ _ _ (fun _ => Iff.rfl) (id _)

Premises used: Iff.rfl, Fintype.card_of_finset'
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
n : ℕ
s : Finset α
hsn : #s ≤ n
hnα : n ≤ Fintype.card α
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n

Tactic:
simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα

Premises used: Finset.exists_subsuperset_card_eq, Finset.subset_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ card Prop = 2

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
⊢ Fintype.card.{u_1} (↑s : Type u_1) ≤ Fintype.card α

Tactic:
Fintype.card_le_of_embedding (Function.Embedding.subtype (· ∈ s))

Premises used: Membership.mem, Function.Embedding.subtype, Fintype.card_le_of_embedding
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
rw : #s.toFinset = Fintype.card α ↔ s = Set.univ
rw₁ : s.toFinset = univ ↔ s = Set.univ
rw₂ : s.toFinset = Set.toFinset Set.univ ↔ s = Set.univ
rw₃ rw₄ : s = Set.univ ↔ s = Set.univ
⊢ Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card α ↔ s = Set.univ

Tactic:
rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]

Premises used: Finset.card_eq_iff_eq_univ, Set.toFinset_inj, Set.toFinset_card, Set.toFinset_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
⊢ card.{u_1} { x : α // p x } ≤ card α

Tactic:
Fintype.card_le_of_embedding (Function.Embedding.subtype _)

Premises used: Function.Embedding.subtype, Fintype.card_le_of_embedding
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
x : α
hx : ¬p x
rwa rwa₁ rwa₂ rwa₃ : x ∉ {x : α | p x}
⊢ x ∉ Set.range (ι := { x : α // p x }) (Subtype.val (p := fun (x : α) ↦ p x))

Tactic:
rwa [Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
inst_2 : DecidablePred p
⊢ card.{u_1} { x : α // p x } = Finset.card.{u_1} (α := α) {x : α | p x}

Tactic:
Fintype.card_of_subtype _ ?_

Premises used: Fintype.card_of_subtype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
inst_2 : DecidablePred p
refine : ∀ (x : α), Membership.mem (γ := Finset α) {x : α | p x} x ↔ p x
⊢ card.{u_1} { x : α // p x } = Finset.card.{u_1} (α := α) {x : α | p x}

Tactic:
refine Fintype.card_of_subtype _ ?_

Premises used: Fintype.card_of_subtype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
inst_2 : DecidablePred p
⊢ ∀ (x : α), Membership.mem (γ := Finset α) {x : α | p x} x ↔ p x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }

Tactic:
rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype]

Premises used: Set.toFinset_compl, Compl.compl, Finset.card_compl, setOf, Set.toFinset, Fintype.card_of_subtype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
x : α
⊢ Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x

Tactic:
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]

Premises used: Set.mem_setOf, Set.mem_toFinset, Set.mem_compl_iff
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
x : α
⊢ Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x

Tactic:
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]

Premises used: Set.mem_setOf, Set.mem_toFinset, Set.mem_compl_iff