awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₁ : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})ᶜ = card α - card.{u_1} { x : α // p x }
H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₂ : card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) = card α - card.{u_1} { x : α // p x }
H₂ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₃ :
  card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) =
    card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})
s : Finset α
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
rw₄ :
  card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) =
    card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})
s₁ : Finset α
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
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
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
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
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:
classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]

Premises used: Set.toFinset_compl, Finset.card_compl, Set.mem_setOf, Set.mem_toFinset, Fintype.card_of_subtype, Set.mem_compl_iff
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p q : α → Prop
h : p ≤ q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
⊢ card.{u_1} { x : α // p x } ≤ card.{u_1} { x : α // q x }

Tactic:
Fintype.card_le_of_embedding (Subtype.impEmbedding _ _ h)

Premises used: Subtype.impEmbedding, Fintype.card_le_of_embedding
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
p q : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
inst_3 : Fintype { x : α // q x }
inst_4 : Fintype { x : α // ¬q x }
h : card.{u_1} { x : α // p x } = card.{u_1} { x : α // q x }
intro : ∀ (val : Fintype α), card.{u_1} { x : α // ¬p x } = card.{u_1} { x : α // ¬q x }
⊢ card.{u_1} { x : α // ¬p x } = card.{u_1} { x : α // ¬q x }

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
p q : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
inst_3 : Fintype { x : α // q x }
inst_4 : Fintype { x : α // ¬q x }
h : card.{u_1} { x : α // p x } = card.{u_1} { x : α // q x }
val : Fintype α
⊢ card.{u_1} { x : α // ¬p x } = card.{u_1} { x : α // ¬q x }

Tactic:
simp only [Fintype.card_subtype_compl, h]

Premises used: Fintype.card_subtype_compl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Setoid α
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
⊢ card.{u_1} (Quotient s) ≤ card α

Tactic:
Fintype.card_le_of_surjective _ Quotient.mk'_surjective

Premises used: Quotient.mk'_surjective, Fintype.card_le_of_surjective
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
x : α
h : Fintype.card α = 1
symm : Eq (α := Finset α) {x} univ
⊢ Eq (α := Finset α) univ {x}

Tactic:
symm
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
x : α
h : Fintype.card α = 1
apply : card.{u_4} (α := α) univ ≤ card (α := α) {x}
⊢ Eq (α := Finset α) {x} univ

Tactic:
apply eq_of_subset_of_card_le (subset_univ {x})

Premises used: Finset.eq_of_subset_of_card_le, Singleton.singleton, Finset.subset_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
inst : Fintype α
x : α
h : Fintype.card α = 1
⊢ card.{u_4} (α := α) univ ≤ card (α := α) {x}

Tactic:
simp [h]
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
intro : ∀ (val : Fintype α), WellFounded r
⊢ WellFounded r

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
x y : α
hxy : r x y
simp_rw : (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
⊢ SSubset.{u_1} (α := Finset α) {z : α | r z x} {z : α | r z y}

Tactic:
simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]

Premises used: lt_iff_le_not_ge, Finset.mem_filter_univ, Finset.subset_iff, Finset.le_iff_subset, Finset.lt_iff_ssubset, Iff.symm
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x

Tactic:
⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩

Premises used: Iff.mpr, trans, irrefl, not_forall_of_exists_not, Classical.not_imp, And.intro, Exists.intro
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x

Tactic:
exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
⊢ ∀ (x y : α) (hxy : r x y), card.{u_1} (α := α) {z : α | r z x} < card.{u_1} (α := α) {z : α | r z y}

Tactic:
have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
this : ∀ (x y : α) (hxy : r x y), card.{u_1} (α := α) {z : α | r z x} < card.{u_1} (α := α) {z : α | r z y}
⊢ WellFounded r

Tactic:
Subrelation.wf (this _ _) (measure _).wf

Premises used: Subrelation.wf, WellFoundedRelation.wf
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
this : ∀ (x y : α) (hxy : r x y), card.{u_1} (α := α) {z : α | r z x} < card.{u_1} (α := α) {z : α | r z y}
⊢ WellFounded r

Tactic:
exact Subrelation.wf (this _ _) (measure _).wf

Premises used: Subrelation.wf, WellFoundedRelation.wf
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
intro : ∀ (val : Fintype α), WellFounded r
intro₁ :
  ∀ (val : Fintype α)
    (this : ∀ (x y : α) (hxy : r x y), card.{u_1} (α := α) {z : α | r z x} < card.{u_1} (α := α) {z : α | r z y}),
    WellFounded r
⊢ WellFounded r

Tactic:
classical
  cases nonempty_fintype α
  have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  exact Subrelation.wf (this _ _) (measure _).wf

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Finite α
inst_1 : Preorder α
⊢ WellFoundedLT α

Tactic:
⟨wellFounded_of_trans_of_irrefl _⟩

Premises used: IsWellFounded.mk, Finite.wellFounded_of_trans_of_irrefl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ WellFoundedLT Bool

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ WellFoundedGT Bool

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ WellFoundedLT Prop

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ WellFoundedGT Prop

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
⊢ ∃ (n : ℕ), card α = n

Tactic:
⟨Fintype.card α, rfl⟩

Premises used: Fintype.card, Exists.intro, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
obtain : ∀ (n : ℕ) (hn : card α = n), P α
⊢ P α

Tactic:
obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩

Premises used: Fintype.card
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
h :
  ∀ (n : ℕ) (ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α) (α : Type u_4) [inst : Fintype α]
    (hn : card α = n), P α
⊢ P α

Tactic:
induction n using Nat.strong_induction_on generalizing α with | _ n ih
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
h : ∀ (hsing : Subsingleton α), P α
h₁ : ∀ (hnontriv : Nontrivial α), P α
⊢ P α

Tactic:
rcases subsingleton_or_nontrivial α with hsing | hnontriv

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hsing : Subsingleton α
⊢ P α

Tactic:
apply hbase
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
h : ∀ (β : Type u_4) [inst_1 : Fintype β], card β < card α → P β
⊢ P α

Tactic:
apply hstep
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
h : ∀ [inst_1 : Fintype β], card β < card α → P β
⊢ ∀ [inst_1 : Fintype β], card β < card α → P β

Tactic:
_
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_3 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst_1 : Fintype β
hlt : card β < card α
⊢ card β < n

Tactic:
rw [hn] at hlt
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_3 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst_1 : Fintype β
hlt : card β < n
⊢ P β

Tactic:
ih (Fintype.card β) hlt _ rfl

Premises used: Fintype.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_3 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst_1 : Fintype β
hlt : card β < n
⊢ P β

Tactic:
exact ih (Fintype.card β) hlt _ rfl

Premises used: Fintype.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
n : ℕ
⊢ card (Fin n) = n

Tactic:
List.length_finRange

Premises used: Fintype.card, List.length_finRange, Finset.card, Multiset.card
-- Module: Mathlib.Data.Fintype.Card
Goal:
m n : ℕ
h : m ≤ n
rw : card (Fin m)
| m

Tactic:
rw [← Fintype.card_fin m]

Premises used: Fintype.card_fin
-- Module: Mathlib.Data.Fintype.Card
Goal:
m n : ℕ
h : m ≤ n
conv_rhs : card { i : Fin n // (↑i : ℕ) < m } = card (Fin m)
⊢ card { i : Fin n // (↑i : ℕ) < m } = m

Tactic:
conv_rhs => rw [← Fintype.card_fin m]

Premises used: Fintype.card_fin
-- Module: Mathlib.Data.Fintype.Card
Goal:
m n : ℕ
h : m ≤ n
f : { i : Fin n // (↑i : ℕ) < m } ≃ Fin m
⊢ card { i : Fin n // (↑i : ℕ) < m } = card (Fin m)

Tactic:
apply Fintype.card_congr

Premises used: Fintype.card_congr
-- Module: Mathlib.Data.Fintype.Card
Goal:
m n : ℕ
h : m ≤ n
⊢ { i : Fin n // (↑i : ℕ) < m } ≃ Fin m

Tactic:
exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
          invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩ }
-- Module: Mathlib.Data.Fintype.Card
Goal:
n : ℕ
⊢ card (α := Fin n) univ = n

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Card
Goal:
⊢ Injective Fin

Tactic:
fun m n h =>
  (Fintype.card_fin m).symm.trans <| (Fintype.card_congr <| Equiv.cast h).trans (Fintype.card_fin n)

Premises used: Fintype.card_congr, Fintype.card_fin, Equiv.cast, Function.Injective, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Fintype.Card
Goal:
k l : ℕ
i : Fin k
j : Fin l
h : i ≍ j
⊢ (↑i : ℕ) = (↑j : ℕ)

Tactic:
(Fin.heq_ext_iff (fin_injective (type_eq_of_heq h))).1 h

Premises used: fin_injective, type_eq_of_heq, Fin.heq_ext_iff, Iff.mp
-- Module: Mathlib.Data.Fintype.Card
Goal:
n m : ℕ
h : Fin n = Fin m
refl : ∀ (h : Fin n = Fin n), cast h = Fin.cast ⋯
⊢ cast h = Fin.cast ⋯

Tactic:
cases fin_injective h

Premises used: fin_injective
-- Module: Mathlib.Data.Fintype.Card
Goal:
n : ℕ
h : Fin n = Fin n
⊢ cast h = Fin.cast ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
n : ℕ
s : Finset (Fin n)
⊢ #s ≤ n

Tactic:
simpa only [Fintype.card_fin] using s.card_le_univ

Premises used: Fintype.card_fin, Finset.card_le_univ
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
inst_1 : Fintype β
inst_2 : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖

Tactic:
card_congr Equiv.uniqueEmbeddingEquivResult

Premises used: Fintype.card_congr, Equiv.uniqueEmbeddingEquivResult
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
rw : ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
rw [Subsingleton.elim emb Embedding.fintype]

Premises used: Function.Embedding.fintype, Subsingleton.elim
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α

Premises used: Fintype.induction_empty_option
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
refine_1 :
  ∀ (α₁ α₂ : Type u_1) (h₂ : Fintype α₂) (e : α₁ ≃ α₂)
    (ih : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₁),
    (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₂
refine_2 : ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖
refine_3 :
  ∀ (γ : Type u_1) (h : Fintype γ) (ih : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) γ),
    (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) (Option γ)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α

Premises used: Fintype.induction_empty_option
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ e.symm
refine_1 : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
refine_1₁ : ‖β‖.descFactorial ‖α₁‖ = ‖β‖.descFactorial ‖α₂‖
refine_1₂ refine_1₃ : ‖β‖.descFactorial ‖α₂‖ = ‖β‖.descFactorial ‖α₂‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

Tactic:
rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]

Premises used: Fintype.card_congr, Equiv.embeddingCongr, Equiv.refl
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
refine_2 : ∃ (x : PEmpty.{u_1 + 1} ↪ β), ∀ (y : PEmpty.{u_1 + 1} ↪ β), y = x
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

Tactic:
rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]

Premises used: Fintype.card_pempty, Nat.descFactorial_zero, Fintype.card_eq_one_iff
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
⊢ ∃ (x : PEmpty.{u_1 + 1} ↪ β), ∀ (y : PEmpty.{u_1 + 1} ↪ β), y = x

Tactic:
⟨Embedding.ofIsEmpty, fun x ↦ DFunLike.ext _ _ isEmptyElim⟩

Premises used: Function.Embedding.ofIsEmpty, isEmptyElim, DFunLike.ext, Exists.intro
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
⊢ ∃ (x : PEmpty.{u_1 + 1} ↪ β), ∀ (y : PEmpty.{u_1 + 1} ↪ β), y = x

Tactic:
exact ⟨Embedding.ofIsEmpty, fun x ↦ DFunLike.ext _ _ isEmptyElim⟩
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
refine_3 :
  ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))

Tactic:
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]

Premises used: Fintype.card_congr, Fintype.card_sigma, Fintype.card_option, Nat.descFactorial_succ, Function.Embedding.optionEmbeddingEquiv
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖

Tactic:
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]

Premises used: Finset.card_univ, Fintype.card_range, Nat.nsmul_eq_mul, mul_comm, Fintype.card_compl_set, Finset.sum_const
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
refine_3 : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (‖γ‖ + 1)
refine_3₁ : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
refine_3₂ :
  ‖(f : γ ↪ β) × (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑f : (a : γ) → β))ᶜ : Type u_2)‖ =
    (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
refine_3₃ :
  ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) =
    (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
refine_3₄ refine_3₅ refine_3₆ :
  ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))

Tactic:
classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]

Premises used: Finset.card_univ, Fintype.card_range, Nat.nsmul_eq_mul, Fintype.card_sigma, Fintype.card_option, Nat.descFactorial_succ, mul_comm, Fintype.card_compl_set, Finset.sum_const
-- Module: Mathlib.Data.Fintype.CardEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
inst_2 : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = 0

Tactic:
card_eq_zero

Premises used: Fintype.card_eq_zero
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).Nodup ↔ Set.InjOn f (↑s : Set α)

Tactic:
simp [Multiset.nodup_map_iff_inj_on s.nodup, Set.InjOn]

Premises used: Finset.nodup, Multiset.nodup_map_iff_inj_on, Set.InjOn
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
x : α
⊢ Membership.mem (γ := Finset α) univ x

Tactic:
Fintype.complete x

Premises used: Set.Mem, setOf, Fintype.complete
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
⊢ ∀ (x : α), Membership.mem (γ := Multiset α) (val univ) x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ s = univ ↔ ∀ (x : α), x ∈ s

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ (∀ (x : α), x ∈ s) → s = univ

Tactic:
eq_univ_iff_forall.2

Premises used: Iff.mpr, Finset.eq_univ_iff_forall
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
h : ∀ (x : α), x ∈ (↑univ : Set α) ↔ Membership.mem (γ := Set α) Set.univ x
⊢ (↑univ : Set α) = Set.univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
x : α
⊢ x ∈ (↑univ : Set α) ↔ Membership.mem (γ := Set α) Set.univ x

Tactic:
simp