awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
have have₁ have₂ : ∀ (hu : (s ∪ t).Finite), ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have₃ :
  ∀ (hu : (s ∪ t).Finite) (hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card),
    ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have₄ :
  ∀ (hu : (s ∪ t).Finite) (hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card) (r' : Finset α)
    (hnr' : n < r'.card) (hr' : r' ⊆ ⋯.toFinset (s := s) ∨ r' ⊆ ⋯.toFinset (s := t)),
    ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
classical
  have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
  rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst
  obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
  exact ⟨r', by simpa, by simpa using hr'⟩

Premises used: Finset.exists_subset_or_subset_of_two_mul_lt_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Finset α
hs : (↑s.card : ℕ∞) < ENat.card α
contrapose! : ∀ (hs : ∀ (a : α), a ∈ s), ENat.card α ≤ (↑s.card : ℕ∞)
⊢ ∃ (a : α), a ∉ s

Tactic:
contrapose! hs
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Finset α
hs : ∀ (a : α), a ∈ s
⊢ ENat.card α ≤ (↑s.card : ℕ∞)

Tactic:
simp [← Set.encard_coe_eq_coe_finsetCard, Set.eq_univ_of_forall (α := α) (s := s) hs]

Premises used: Set.eq_univ_of_forall, Set.encard_coe_eq_coe_finsetCard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
rw rw₁ : Eq (α := ℕ) 1 1
⊢ ncard (α := α) {a} = 1

Tactic:
rw [ncard_singleton]

Premises used: Set.ncard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine : ∀ (h : s.ncard = 1), ∃ (a : α), s = {a}
⊢ s.ncard = 1 ↔ ∃ (a : α), s = {a}

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.ncard = 1
have : ∀ (hft : Fintype (↑s : Type u_1)), ∃ (a : α), s = {a}
⊢ ∃ (a : α), s = {a}

Tactic:
have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype (↑s : Type u_1)
⊢ ∃ (a : α), s.toFinset = {a}

Tactic:
simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h

Premises used: Finset.card_eq_one, Set.ncard_eq_toFinset_card'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
⊢ ∃ (a : α), s = {a}

Tactic:
h.imp fun a ha ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
refine : ∀ (a : α) (ha : s.toFinset = {a}), s = {a}
⊢ ∃ (a : α), s = {a}

Tactic:
refine h.imp fun a ha ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
a : α
ha : s.toFinset = {a}
simp_rw : ∀ (x : α), x ∈ s ↔ x = a
⊢ s = {a}

Tactic:
simp_rw [Set.ext_iff, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.ext_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a

Tactic:
simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha

Premises used: Finset.mem_singleton, Finset.ext_iff, Set.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a

Tactic:
ha
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a

Tactic:
exact ha
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
inl : ∀ (ht : t.Finite), (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
inr : ∀ (ht : t.Infinite), (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
rcases t.finite_or_infinite with ht | ht

Premises used: Set.finite_or_infinite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
inl : (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset (s := s), insert a (hs.toFinset (s := s)) = ht.toFinset (s := t)
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
      ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]

Premises used: Set.Finite.toFinset_subset_toFinset, Set.ncard_eq_toFinset_card, Finset.exists_eq_insert_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ s, insert a s = t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
h :
  Eq.{u_1 + 1} (α := α → Prop)
    (fun (a : α) ↦ a ∉ hs.toFinset (s := s) ∧ insert a (hs.toFinset (s := s)) = ht.toFinset (s := t)) fun (a : α) ↦
    a ∉ s ∧ insert a s = t
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset (s := s), insert a (hs.toFinset (s := s)) = ht.toFinset (s := t)

Tactic:
convert! Iff.rfl using 2

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
h :
  Eq.{u_1 + 1} (α := α → Prop) (fun (a : α) ↦ a ∉ s ∧ insert a (hs.toFinset (s := s)) = ht.toFinset (s := t))
    fun (a : α) ↦ a ∉ s ∧ insert a s = t
⊢ Eq.{u_1 + 1} (α := α → Prop)
    (fun (a : α) ↦ a ∉ hs.toFinset (s := s) ∧ insert a (hs.toFinset (s := s)) = ht.toFinset (s := t)) fun (a : α) ↦
    a ∉ s ∧ insert a s = t

Tactic:
simp only [Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
h : ∀ (x : α), x ∉ s ∧ insert x (hs.toFinset (s := s)) = ht.toFinset (s := t) ↔ x ∉ s ∧ insert x s = t
⊢ Eq.{u_1 + 1} (α := α → Prop) (fun (a : α) ↦ a ∉ s ∧ insert a (hs.toFinset (s := s)) = ht.toFinset (s := t))
    fun (a : α) ↦ a ∉ s ∧ insert a s = t

Tactic:
ext x
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
x : α
⊢ x ∉ s ∧ insert x (hs.toFinset (s := s)) = ht.toFinset (s := t) ↔ x ∉ s ∧ insert x s = t

Tactic:
simp [Finset.ext_iff, Set.ext_iff]

Premises used: Finset.ext_iff, Set.ext_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Infinite
inr : ∀ x ∉ s, ¬insert x s = t
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
simp only [ht.ncard, add_eq_zero, and_false, iff_false, not_exists, not_and,
    reduceCtorEq]

Premises used: reduceCtorEq, Set.Infinite.ncard, iff_false, not_exists, and_false, add_eq_zero, not_and
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
ht : (insert x s).Infinite
⊢ False

Tactic:
ht (hs.insert x)

Premises used: Set.Finite.insert
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
ht : (insert x s).Infinite
⊢ False

Tactic:
exact ht (hs.insert x)

Premises used: Set.Finite.insert
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
inl : ∀ (ht : t.Finite), (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
inr inr₁ : ∀ (ht : t.Infinite), (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
inr₂ : ∀ (ht : t.Infinite), ∀ x ∉ s, ¬insert x s = t
inr₃ : ∀ (x : α) (ht : (insert x s).Infinite), False
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
classical
  rcases t.finite_or_infinite with ht | ht
  · rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
      ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]
    convert! Iff.rfl using 2; simp only [Finite.mem_toFinset]
    ext x
    simp [Finset.ext_iff, Set.ext_iff]
  simp only [ht.ncard, add_eq_zero, and_false, iff_false, not_exists, not_and,
    reduceCtorEq]
  rintro x - rfl
  exact ht (hs.insert x)

Premises used: reduceCtorEq, iff_false, Set.finite_or_infinite, Set.Finite.mem_toFinset, Iff.rfl, not_exists, Finset.ext_iff, Set.ext_iff, Set.ncard_eq_toFinset_card, and_false, add_eq_zero, Finset.exists_eq_insert_iff, not_and, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
simp_rw : hs.toFinset (s := s).card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
simp_rw₁ : (∀ a ∈ hs.toFinset (s := s), ∀ b ∈ hs.toFinset (s := s), a = b) ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, Finset.card_le_one, Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.ncard ≤ 1 ↔ s.Subsingleton

Tactic:
ncard_le_one <| inferInstanceAs (Finite s)

Premises used: Set.ncard_le_one, Set.Subsingleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
rw [ncard_le_one hs]

Premises used: Set.ncard_le_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
mp : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
mpr : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
mp₁ mp₂ mp₃ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
mpr₁ mpr₂ mpr₃ : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
mp₄ mp₅ mp₆ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
mpr₄ mpr₅ mpr₆ : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
mp₇ mp₈ mp₉ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
mpr₇ mpr₈ mpr₉ : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
mp₁₀ mp₁₁ mp₁₂ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
mpr₁₀ mpr₁₁ mpr₁₂ : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
mp₁₃ mp₁₄ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
mpr₁₃ mpr₁₄ : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
tauto
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
inl :
  ∀ (hs : Set.Finite.{u_1} (α := α) ∅),
    ncard.{u_1} (α := α) ∅ ≤ 1 ↔ Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (a : α), Eq (α := Set α) ∅ {a}
inr : ∀ (x : α) (hx : x ∈ s), s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
hs : Set.Finite.{u_1} (α := α) ∅
⊢ ncard.{u_1} (α := α) ∅ ≤ 1

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
hs : Set.Finite.{u_1} (α := α) ∅
⊢ ncard.{u_1} (α := α) ∅ ≤ 1 ↔ Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (a : α), Eq (α := Set α) ∅ {a}

Tactic:
exact iff_of_true (by simp) (Or.inl rfl)

Premises used: iff_of_true, Or.inl, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
inr : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ (a : α), s = {a}
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}

Tactic:
rw [ncard_le_one_iff hs]

Premises used: Set.ncard_le_one_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ (a : α), s = {a}

Tactic:
⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Iff.intro, Exists.intro, HasSubset.Subset.antisymm', Or.inr
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
inr : (s = ∅ ∨ ∃ (a : α), s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ (a : α), s = {a}

Tactic:
refine ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ (a : α), s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Nonempty α
hs : s.Finite
simp_rw : hs.toFinset (s := s).card ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
simp_rw₁ : (∃ (x : α), hs.toFinset (s := s) ⊆ {x}) ↔ ∃ (x : α), s ⊆ {x}
simp_rw₂ : (∃ (x : α), s ⊆ (↑{x} : Set α)) ↔ ∃ (x : α), s ⊆ {x}
⊢ s.ncard ≤ 1 ↔ ∃ (x : α), s ⊆ {x}

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
    Finite.toFinset_subset, Finset.coe_singleton]

Premises used: Finset.coe_singleton, Set.Finite.toFinset_subset, Finset.card_le_one_iff_subset_singleton, Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Subsingleton α
s : Set α
rw : ⋯.toFinset (s := s).card ≤ 1
⊢ s.ncard ≤ 1

Tactic:
rw [ncard_eq_toFinset_card]

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Subsingleton α
s : Set α
⊢ ⋯.toFinset (s := s).card ≤ 1

Tactic:
Finset.card_le_one_of_subsingleton _

Premises used: Finset.card_le_one_of_subsingleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Subsingleton α
s : Set α
⊢ ⋯.toFinset (s := s).card ≤ 1

Tactic:
exact Finset.card_le_one_of_subsingleton _

Premises used: Finset.card_le_one_of_subsingleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
rw : 1 < s.ncard ↔ ¬s.Subsingleton
rw₁ : 1 < s.ncard ↔ ¬s.ncard ≤ 1
rw₂ rw₃ : 1 < s.ncard ↔ 1 < s.ncard
⊢ 1 < s.ncard ↔ s.Nontrivial

Tactic:
rw [← not_subsingleton_iff, ← ncard_le_one_iff_subsingleton, not_le]

Premises used: Set.not_subsingleton_iff, not_le, Set.ncard_le_one_iff_subsingleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite

Tactic:
⟨fun hs ↦ ?_, fun ⟨hs_nontrivial, hs_finite⟩ ↦ ?_⟩

Premises used: LT.lt, Iff.intro, Set.ncard, OfNat.ofNat, _private.0.Set.one_lt_ncard_iff_nontrivial_and_finite.match_1
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine_1 : ∀ (hs : 1 < s.ncard), s.Nontrivial ∧ s.Finite
refine_2 : s.Nontrivial ∧ s.Finite → ∀ (hs_nontrivial : s.Nontrivial) (hs_finite : s.Finite), 1 < s.ncard
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite

Tactic:
refine ⟨fun hs ↦ ?_, fun ⟨hs_nontrivial, hs_finite⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
⊢ s.Finite

Tactic:
have := finite_of_ncard_pos (Nat.zero_lt_of_lt hs)
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : s.Finite
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
rw [← Set.finite_coe_iff] at this

Premises used: Set.finite_coe_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.Nontrivial ∧ s.Finite

Tactic:
⟨one_lt_ncard_iff_nontrivial.mp hs, this⟩

Premises used: Set.one_lt_ncard_iff_nontrivial, And.intro, Iff.mp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.Nontrivial ∧ s.Finite

Tactic:
exact ⟨one_lt_ncard_iff_nontrivial.mp hs, this⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : s.Finite
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
rw [← Set.finite_coe_iff] at hs_finite

Premises used: Set.finite_coe_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : Finite.{u_1 + 1} (↑s : Type u_1)
refine_2 refine_2₁ refine_2₂ refine_2₃ : s.Nontrivial
⊢ 1 < s.ncard

Tactic:
rwa [one_lt_ncard_iff_nontrivial]

Premises used: Set.one_lt_ncard_iff_nontrivial
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
simp_rw : 1 < hs.toFinset (s := s).card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
simp_rw₁ : (∃ a ∈ hs.toFinset (s := s), ∃ b ∈ hs.toFinset (s := s), a ≠ b) ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, Set.ncard_eq_toFinset_card, Finset.one_lt_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
⊢ 1 < s.ncard ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
rw [one_lt_ncard hs]

Premises used: Set.one_lt_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
simp only [exists_and_left]

Premises used: exists_and_left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : s.Nonempty
he : Even s.ncard
⊢ 0 < s.ncard

Tactic:
rw [← Set.ncard_pos hs] at hn

Premises used: Set.ncard_pos
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : s.Nonempty
he : Even s.ncard
hn₁ : 0 < s.ncard
⊢ Even s.ncard

Tactic:
rw [← Set.ncard_pos hs] at hn

Premises used: Set.ncard_pos
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
h : s.ncard = 1
⊢ False

Tactic:
simp [h] at he
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
⊢ s.ncard ≠ 1

Tactic:
have : s.ncard ≠ 1 := fun h ↦ by simp [h] at he
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
this : s.ncard ≠ 1
⊢ 1 < s.ncard

Tactic:
lia
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
simp_rw : 2 < hs.toFinset (s := s).card ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₁ :
  (∃ (a : α) (b : α) (c : α),
      a ∈ hs.toFinset (s := s) ∧ b ∈ hs.toFinset (s := s) ∧ c ∈ hs.toFinset (s := s) ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 2 < s.ncard ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.two_lt_card_iff, Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, Set.ncard_eq_toFinset_card, Finset.two_lt_card_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp only [two_lt_ncard_iff hs, exists_and_left]

Premises used: exists_and_left, Set.two_lt_ncard_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
simp_rw :
  3 < hs.toFinset (s := s).card ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
simp_rw₁ :
  (∃ (a : α) (b : α) (c : α) (d : α),
      a ∈ hs.toFinset (s := s) ∧
        b ∈ hs.toFinset (s := s) ∧
          c ∈ hs.toFinset (s := s) ∧ d ∈ hs.toFinset (s := s) ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
⊢ 3 < s.ncard ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.three_lt_card_iff, Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, Finset.three_lt_card_iff, Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp only [three_lt_ncard_iff hs, exists_and_left]

Premises used: Set.three_lt_ncard_iff, exists_and_left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
⊢ s.Finite

Tactic:
have hsf := finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
hsf : s.Finite
⊢ 1 < hsf.toFinset (s := s).card

Tactic:
rw [ncard_eq_toFinset_card _ hsf] at hs

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
hsf : s.Finite
hs : 1 < hsf.toFinset (s := s).card
⊢ ∃ b ∈ s, b ≠ a

Tactic:
simpa only [Finite.mem_toFinset] using Finset.exists_mem_ne hs a

Premises used: Set.Finite.mem_toFinset, Finset.exists_mem_ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ s.Finite

Tactic:
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
hsf : s.Finite
⊢ ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = hsf.toFinset (s := s) ∧ t.card = n

Tactic:
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h

Premises used: Finset.card_eq_succ, Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = hsf.toFinset (s := s) ∧ t.card = n
obtain :
  ∀ (a : α) (t : Finset α) (hat : a ∉ t) (hts : insert a t = hsf.toFinset (s := s)),
    ∃ (a : α) (t_1 : Set α), a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
obtain ⟨a, t, hat, hts, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : insert a t = hsf.toFinset (s := s)
⊢ ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s

Tactic:
simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts

Premises used: Set.Finite.mem_toFinset, Finset.mem_insert, Finset.ext_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ (a : α) (t_1 : Set α), a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Tactic:
⟨a, t, hat, ?_, ?_⟩

Premises used: SetLike.coe, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
refine_1 : insert a (↑t : Set α) = s
refine_2 : (↑t : Set α).ncard = t.card
⊢ ∃ (a : α) (t_1 : Set α), a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Tactic:
refine ⟨a, t, hat, ?_, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a (↑t : Set α) = s

Tactic:
simp [Set.ext_iff, hts]

Premises used: Set.ext_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t : Set α).ncard = t.card

Tactic:
simp