awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
rw : s = t ↔ (↑s : Finset α) = (↑t : Finset α)
rw₁ rw₂ : (↑s : Finset α) = (↑t : Finset α) ↔ (↑s : Finset α) = (↑t : Finset α)
⊢ s = t ↔ (↑s : Finset α) ⊆ (↑t : Finset α)

Tactic:
rw [Finset.subset_iff_eq_of_card_le (t.prop.trans_le s.prop.ge), Subtype.ext_iff]

Premises used: Eq.ge, Eq.trans_le, Subtype.ext_iff, Finset.subset_iff_eq_of_card_le, Subtype.prop
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
rwa : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b} + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
rwa₁ : ∀ (hα : (↑n : ℕ∞) < 1 + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
rwa₂ : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b}ᶜ + 1) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hα : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ

Tactic:
rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα

Premises used: ENat.lt_add_one_iff', Set.encard_univ, add_comm, ENat.coe_ne_top, Set.encard_add_encard_compl, Singleton.singleton, Set.encard_singleton, Eq.trans
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
⊢ (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ

Tactic:
have ha' : n ≤ Set.encard {b}ᶜ := by
    rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ Subset (α := Set α) {a} {b}ᶜ

Tactic:
simp [Ne.symm hab]

Premises used: Ne.symm
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ encard (α := α) {a} ≤ (↑n : ℕ∞)

Tactic:
simpa
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
obtain :
  ∀ (s : Set α) (has : {a} ⊆ s) (has' : s ⊆ {b}ᶜ) (hs : s.encard = (↑n : ℕ∞)),
    ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s
⊢ ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s

Tactic:
obtain ⟨s, has, has', hs⟩ :=
    Set.exists_superset_subset_encard_eq (s := {a}) (by simp [Ne.symm hab]) (by simpa) ha'

Premises used: Set.exists_superset_subset_encard_eq
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
⊢ s.Finite

Tactic:
have : Set.Finite s := Set.finite_of_encard_eq_coe hs
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
this : s.Finite
rwa : #(this.toFinset (s := s)) = n
rwa₁ : Eq (α := ℕ∞) (↑(#(this.toFinset (s := s))) : ℕ∞) (↑n : ℕ∞)
rwa₂ rwa₃ rwa₄ rwa₅ : s.encard = (↑n : ℕ∞)
⊢ this.toFinset (s := s) ∈ powersetCard α n

Tactic:
rwa [mem_iff, ← ENat.coe_inj, ← this.encard_eq_coe_toFinset_card]

Premises used: ENat.coe_inj, Set.powersetCard.mem_iff, Set.Finite.encard_eq_coe_toFinset_card
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
this : s.Finite
⊢ Membership.mem (γ := (↑(powersetCard α n) : Type u_1))
    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) (this.toFinset (s := s)) ⋯) a

Tactic:
simpa using has
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
this : s.Finite
⊢ b ∉ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) (this.toFinset (s := s)) ⋯

Tactic:
simpa using has'
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
this : s.Finite
⊢ ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s

Tactic:
exact ⟨⟨Set.Finite.toFinset this, by
    rwa [mem_iff, ← ENat.coe_inj, ← this.encard_eq_coe_toFinset_card]⟩,
      by simpa using has, by simpa using has'⟩
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
contrapose! : s = t ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t
⊢ s ≠ t ↔ ∃ a ∈ s, a ∉ t

Tactic:
contrapose!
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
rw : (↑s : Finset α) ⊆ (↑t : Finset α) ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t
⊢ s = t ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t

Tactic:
rw [eq_iff_subset]

Premises used: Set.powersetCard.eq_iff_subset
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
⊢ (↑s : Finset α) ⊆ (↑t : Finset α) ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t

Tactic:
rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
rw : #(Finset.map f (↑s : Finset α)) = n
rw₁ : #(↑s : Finset α) = n
rw₂ rw₃ : n = n
⊢ Finset.map f (↑s : Finset α) ∈ powersetCard β n

Tactic:
rw [mem_iff, card_map, s.prop]

Premises used: Finset.card_map, Set.powersetCard.mem_iff, Subtype.prop
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
b : β
simp : (∃ a ∈ (↑s : Finset α), (f : (a : α) → β) a = b) ↔ ∃ x ∈ s, (f : (a : α) → β) x = b
⊢ b ∈ map n f s ↔ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑s : Set α)) b

Tactic:
simp [map]

Premises used: Set.powersetCard.map
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
b : β
⊢ (∃ a ∈ (↑s : Finset α), (f : (a : α) → β) a = b) ↔ ∃ x ∈ s, (f : (a : α) → β) x = b

Tactic:
rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
h : ∀ (x : β), x ∈ (↑(map n f s) : Set β) ↔ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑s : Set α)) x
⊢ (↑(map n f s) : Set β) = (⇑f : (a : α) → β) '' (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
x : β
⊢ x ∈ (↑(map n f s) : Set β) ↔ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑s : Set α)) x

Tactic:
simp [mem_map_iff_mem_range]

Premises used: Set.powersetCard.mem_map_iff_mem_range
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑(map n f s) : Finset β) = Finset.map f (↑s : Finset α)

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : Finset α
s_card : #s = n
⊢ (↑(ofCard s_card) : Finset α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
h : #(↑s : Finset α) = n
⊢ ofCard h = s

Tactic:
rfl

Premises used: Set.powersetCard.ofCard, rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
a : α
⊢ (fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a}))
      ((fun (a : α) ↦
          (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ :
            { x : Finset α // x ∈ powersetCard α 1 }))
        a) =
    a

Tactic:
simp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α 1) : Type u_1)
rw :
  (↑((fun (a : α) ↦
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ :
              { x : Finset α // x ∈ powersetCard α 1 }))
          ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s)) :
      Finset α) =
    (↑s : Finset α)
rw₁ rw₂ :
  Eq (α := Finset α)
    (↑((fun (a : α) ↦
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ :
              { x : Finset α // x ∈ powersetCard α 1 }))
          ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s)) :
      Finset α)
    {⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})}
⊢ (fun (a : α) ↦
        (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ : { x : Finset α // x ∈ powersetCard α 1 }))
      ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s) =
    s

Tactic:
rw [← Subtype.val_inj, (Finset.card_eq_one.mp s.prop).choose_spec]

Premises used: Exists.choose_spec, Finset.card_eq_one, Subtype.val_inj, Subtype.prop, Iff.mp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : Fin n ↪ β
rw : card (α := Fin n) Finset.univ = n
rw₁ : Fintype.card (Fin n) = n
rw₂ rw₃ : n = n
⊢ Membership.mem (γ := Set (Finset (Fin n))) (powersetCard (Fin n) n) Finset.univ

Tactic:
rw [mem_iff, Finset.card_univ, Fintype.card_fin]

Premises used: Finset.card_univ, Fintype.card_fin, Set.powersetCard.mem_iff
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
f : Fin n ↪ β
b : β
⊢ b ∈ ofFinEmb n β f ↔ Membership.mem (γ := Set β) (range (ι := Fin n) (⇑f : (a : Fin n) → β)) b

Tactic:
simp [ofFinEmb, mem_map_iff_mem_range]

Premises used: Set.powersetCard.ofFinEmb, Set.powersetCard.mem_map_iff_mem_range
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
f : Fin n ↪ β
h :
  ∀ (x : β), x ∈ (↑(ofFinEmb n β f) : Set β) ↔ Membership.mem (γ := Set β) (range (ι := Fin n) (⇑f : (a : Fin n) → β)) x
⊢ (↑(ofFinEmb n β f) : Set β) = range (ι := Fin n) (⇑f : (a : Fin n) → β)

Tactic:
ext
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
f : Fin n ↪ β
x : β
⊢ x ∈ (↑(ofFinEmb n β f) : Set β) ↔ Membership.mem (γ := Set β) (range (ι := Fin n) (⇑f : (a : Fin n) → β)) x

Tactic:
simp [mem_ofFinEmb_iff_mem_range]

Premises used: Set.powersetCard.mem_ofFinEmb_iff_mem_range
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ (↑(ofFinEmb n β f) : Finset β) = Finset.map f Finset.univ

Tactic:
simp [← coe_inj, coe_ofFinEmb]

Premises used: Finset.coe_inj, Set.powersetCard.coe_ofFinEmb
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
rw : Fintype.card (Fin n) = n
rw₁ : n = n
rw₂ : ℕ
rw₃ : n = n
rw₄ : ℕ
⊢ Fintype.card (Fin n) = #s

Tactic:
rw [hs, Fintype.card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
obtain :
  ∀ (f : Fin n ↪ β) (hf : Finset.map f Finset.univ = s),
    ∃ (a : Fin n ↪ β), ofFinEmb n β a = Subtype.mk (p := fun (x : Finset β) ↦ x ∈ powersetCard β n) s hs
⊢ ∃ (a : Fin n ↪ β), ofFinEmb n β a = Subtype.mk (p := fun (x : Finset β) ↦ x ∈ powersetCard β n) s hs

Tactic:
obtain ⟨f : Fin n ↪ β, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])

Premises used: Function.Embedding.exists_of_card_eq_finset, Fin
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
f : Fin n ↪ β
hf : Finset.map f Finset.univ = s
⊢ ∃ (a : Fin n ↪ β), ofFinEmb n β a = Subtype.mk (p := fun (x : Finset β) ↦ x ∈ powersetCard β n) s hs

Tactic:
⟨f, Subtype.ext hf⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
f : Fin n ↪ β
hf : Finset.map f Finset.univ = s
⊢ ∃ (a : Fin n ↪ β), ofFinEmb n β a = Subtype.mk (p := fun (x : Finset β) ↦ x ∈ powersetCard β n) s hs

Tactic:
exact ⟨f, Subtype.ext hf⟩
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_1)
simp : Fintype.card α - n = m
⊢ (↑s : Finset α)ᶜ ∈ powersetCard α m

Tactic:
simp [Finset.card_compl, mem_iff.mp s.2]

Premises used: Finset.card_compl, Set.powersetCard.mem_iff, Iff.mp, Subtype.property
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_1)
⊢ Fintype.card α - n = m

Tactic:
omega
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : (↑(powersetCard α m) : Type u_1)
simp : Fintype.card α - m = n
⊢ (↑t : Finset α)ᶜ ∈ powersetCard α n

Tactic:
simp [Finset.card_compl, mem_iff.mp t.2]

Premises used: Finset.card_compl, Set.powersetCard.mem_iff, Iff.mp, Subtype.property
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : (↑(powersetCard α m) : Type u_1)
⊢ Fintype.card α - m = n

Tactic:
omega
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_1)
⊢ (fun (t : (↑(powersetCard α m) : Type u_1)) ↦
        Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) (↑t : Finset α)ᶜ ⋯)
      ((fun (s : (↑(powersetCard α n) : Type u_1)) ↦
          Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α m) (↑s : Finset α)ᶜ ⋯)
        s) =
    s

Tactic:
simp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : (↑(powersetCard α m) : Type u_1)
⊢ (fun (s : (↑(powersetCard α n) : Type u_1)) ↦
        Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α m) (↑s : Finset α)ᶜ ⋯)
      ((fun (t : (↑(powersetCard α m) : Type u_1)) ↦
          Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) (↑t : Finset α)ᶜ ⋯)
        t) =
    t

Tactic:
simp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑((compl hm : (a : (↑(powersetCard α n) : Type u_1)) → (↑(powersetCard α m) : Type u_1)) s) : Finset α) =
    (↑s : Finset α)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_1)
a : α
⊢ Membership.mem (γ := (↑(powersetCard α m) : Type u_1))
      ((compl hm : (a : (↑(powersetCard α n) : Type u_1)) → (↑(powersetCard α m) : Type u_1)) s :
        (↑(powersetCard α m) : Type u_1))
      a ↔
    a ∉ s

Tactic:
Finset.mem_compl

Premises used: Set.Mem, setOf, Finset.mem_compl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ (compl hm).symm = compl ⋯

Tactic:
rfl

Premises used: Set.powersetCard.compl, Equiv.symm, rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
rw : #((↑s : Finset α).disjUnion (↑t : Finset α) hst) = m + n
rw₁ : #(↑s : Finset α) + #(↑t : Finset α) = m + n
rw₂ : m + #(↑t : Finset α) = m + n
rw₃ rw₄ : m + n = m + n
⊢ (↑s : Finset α).disjUnion (↑t : Finset α) hst ∈ powersetCard α (m + n)

Tactic:
rw [mem_iff, Finset.card_disjUnion, card_eq s, card_eq t]

Premises used: Set.powersetCard.card_eq, Set.powersetCard.mem_iff, Finset.card_disjUnion
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
⊢ (↑(disjUnion hst) : Finset α) = (↑s : Finset α).disjUnion (↑t : Finset α) hst

Tactic:
rfl

Premises used: Finset.disjUnion, rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
a : α
⊢ a ∈ disjUnion hst ↔ a ∈ s ∨ a ∈ t

Tactic:
Finset.mem_disjUnion (h := hst)

Premises used: Set.Mem, setOf, Finset.mem_disjUnion
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Fintype α
h : ∀ (x : Finset α), x ∈ powersetCard α n ↔ x ∈ (↑(Finset.powersetCard n Finset.univ) : Set (Finset α))
⊢ powersetCard α n = (↑(Finset.powersetCard n Finset.univ) : Set (Finset α))

Tactic:
ext
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Fintype α
x : Finset α
⊢ x ∈ powersetCard α n ↔ x ∈ (↑(Finset.powersetCard n Finset.univ) : Set (Finset α))

Tactic:
simp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Fintype α
rw : Fintype (↑(↑(Finset.powersetCard n Finset.univ) : Set (Finset α)) : Type u_1)
⊢ Fintype (↑(powersetCard α n) : Type u_1)

Tactic:
rw [coe_finset]

Premises used: Set.powersetCard.coe_finset
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Fintype α
⊢ Fintype (↑(↑(Finset.powersetCard n Finset.univ) : Set (Finset α)) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Finite α
have : ∀ (this : Fintype α), Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
⊢ Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)

Tactic:
have : Fintype α := Fintype.ofFinite α
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Finite α
this : Fintype α
⊢ Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)

Tactic:
simpa [coe_finset] using Subtype.finite

Premises used: Subtype.finite, Set.powersetCard.coe_finset
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
⊢ 1 ≤ n

Tactic:
h

Premises used: Nat.lt
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
⊢ 1 ≤ n

Tactic:
exact h
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
obtain : ∀ (s : Finset α) (a_mem : {a} ⊆ s) (s_card : #s = n), ∃ s ∈ powersetCard α n, a ∈ s
⊢ ∃ s ∈ powersetCard α n, a ∈ s

Tactic:
obtain ⟨s, a_mem, s_card⟩ := Infinite.exists_superset_card_eq ({a} : Finset α) n
    (by rw [Finset.card_singleton]; exact h)

Premises used: Infinite.exists_superset_card_eq, Singleton.singleton
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
h₁ : s ∈ powersetCard α n ∧ a ∈ s
⊢ ∃ s ∈ powersetCard α n, a ∈ s

Tactic:
use ↑s
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ a ∈ s

Tactic:
simpa using a_mem
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ s ∈ powersetCard α n ∧ a ∈ s

Tactic:
exact ⟨mem_iff.mp s_card, by simpa using a_mem⟩
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
rw : ¬Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
⊢ Infinite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)

Tactic:
rw [← not_finite_iff_infinite]

Premises used: not_finite_iff_infinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
by_contra : ∀ (finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)), False
⊢ ¬Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)

Tactic:
by_contra finite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
apply : Finite α
⊢ False

Tactic:
apply Finite.false (α := α)

Premises used: Finite.false
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
rw : (⋃₀ (SetLike.coe '' powersetCard α n)).Finite
⊢ Finite α

Tactic:
rw [← Set.finite_univ_iff, ← this]

Premises used: Set.finite_univ_iff
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
apply : ∀ t ∈ SetLike.coe '' powersetCard α n, t.Finite
⊢ (⋃₀ (SetLike.coe '' powersetCard α n)).Finite

Tactic:
apply Set.Finite.sUnion (Finite.image SetLike.coe finite)

Premises used: Set.Finite.sUnion, Set.Finite.image, SetLike.coe
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ ∀ t ∈ SetLike.coe '' powersetCard α n, t.Finite

Tactic:
aesop
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
suffices : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ False

Tactic:
suffices ⋃₀ (SetLike.coe '' powersetCard α n) = Set.univ by
    apply Finite.false (α := α)
    rw [← Set.finite_univ_iff, ← this]
    apply Set.Finite.sUnion (Finite.image SetLike.coe finite)
    aesop
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
rw : ∀ (a : α), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
⊢ ⋃₀ (SetLike.coe '' powersetCard α n) = univ

Tactic:
rw [sUnion_eq_univ_iff]

Premises used: Set.sUnion_eq_univ_iff
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
a : α
obtain : ∀ (s : Finset α) (s_mem : s ∈ powersetCard α n) (mem_s : a ∈ s), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
⊢ ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b

Tactic:
obtain ⟨s, s_mem, mem_s⟩ := exist_mem_powersetCard_of_inf α n (Nat.pos_of_neZero n) a

Premises used: Set.powersetCard.exist_mem_powersetCard_of_inf, Nat.pos_of_neZero
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
a : α
s : Finset α
s_mem : s ∈ powersetCard α n
mem_s : a ∈ s
⊢ ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b

Tactic:
⟨↑s, mem_image_of_mem SetLike.coe s_mem, mem_coe.mpr mem_s⟩

Premises used: Iff.mpr, SetLike.coe, Set.mem_image_of_mem, And.intro, Exists.intro, Finset.mem_coe
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
a : α
s : Finset α
s_mem : s ∈ powersetCard α n
mem_s : a ∈ s
⊢ ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b

Tactic:
exact ⟨↑s, mem_image_of_mem SetLike.coe s_mem, mem_coe.mpr mem_s⟩
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inl : ∀ (val : Fintype α), Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
inr : Infinite α → Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n

Tactic:
cases fintypeOrInfinite α

Premises used: fintypeOrInfinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
val : Fintype α
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n

Tactic:
simp [coe_finset]

Premises used: Set.powersetCard.coe_finset