awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.ncard = 1
⊢ ∃ (a : α), s = {a}
have have : ∀ (hft : Fintype (↑s : Type u_1)), ∃ (a : α), s = {a}
Tactic: have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype (↑s : Type u_1)
⊢ ∃ (a : α), s = {a}
have h₁ : ∃ (a : α), s.toFinset = {a}
Tactic: simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
⊢ ∃ (a : α), s = {a}
have refine : ∀ (a : α) (ha : s.toFinset = {a}), s = {a}
Tactic: refine h.imp fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hft : Fintype (↑s : Type u_1)
h : ∃ (a : α), s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}
have simp_rw : ∀ (x : α), x ∈ s ↔ x = a
Tactic: simp_rw [Set.ext_iff, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inl : ∀ (ht : t.Finite), (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
Tactic: rcases t.finite_or_infinite with ht | ht
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inr : ∀ (ht : t.Infinite), (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
Tactic: rcases t.finite_or_infinite with ht | ht
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inl : (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset (s := s), insert a (hs.toFinset (s := s)) = ht.toFinset (s := t)
Tactic: rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
      ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset (s := s), insert a (hs.toFinset (s := s)) = ht.toFinset (s := t)
have 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
Tactic: convert! Iff.rfl using 2
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ 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
have 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
Tactic: simp only [Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ 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
have h : ∀ (x : α), x ∉ s ∧ insert x (hs.toFinset (s := s)) = ht.toFinset (s := t) ↔ x ∉ s ∧ insert x s = t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Infinite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inr : ∀ x ∉ s, ¬insert x s = t
Tactic: simp only [ht.ncard, add_eq_zero, and_false, iff_false, not_exists, not_and,
    reduceCtorEq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inl : ∀ (ht : t.Finite), (∃ 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)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inr : ∀ (ht : t.Infinite), (∃ 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)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inr₂ : ∀ (ht : t.Infinite), ∀ x ∉ s, ¬insert x s = t
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)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
have inr₃ : ∀ (x : α) (ht : (insert x s).Infinite), False
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)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
have simp_rw : hs.toFinset (s := s).card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
simp_rw : hs.toFinset (s := s).card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
have simp_rw₁ : (∀ a ∈ hs.toFinset (s := s), ∀ b ∈ hs.toFinset (s := s), a = b) ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
have rw : (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Tactic: rw [ncard_le_one hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
have mp : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
mp : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
have mpr : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) → ∀ a ∈ s, ∀ b ∈ s, a = b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}
have inl : ∀ (hs : Set.Finite.{u_1} (α := α) ∅),
  ncard.{u_1} (α := α) ∅ ≤ 1 ↔ Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (a : α), Eq (α := Set α) ∅ {a}
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}
have inr : ∀ (x : α) (hx : x ∈ s), s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}
have inr : (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ (a : α), s = {a}
Tactic: rw [ncard_le_one_iff hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
have inr : (s = ∅ ∨ ∃ (a : α), s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Tactic: refine ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
have simp_rw : hs.toFinset (s := s).card ≤ 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]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Nonempty α
hs : s.Finite
simp_rw : hs.toFinset (s := s).card ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
⊢ s.ncard ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
have simp_rw₁ : (∃ (x : α), hs.toFinset (s := s) ⊆ {x}) ↔ ∃ (x : α), s ⊆ {x}
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
    Finite.toFinset_subset, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ s.ncard ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
have simp_rw₂ : (∃ (x : α), s ⊆ (↑{x} : Set α)) ↔ ∃ (x : α), s ⊆ {x}
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
    Finite.toFinset_subset, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Subsingleton α
s : Set α
⊢ s.ncard ≤ 1
have rw : sorry.toFinset (s := s).card ≤ 1
Tactic: rw [ncard_eq_toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ 1 < s.ncard ↔ s.Nontrivial
have rw : 1 < s.ncard ↔ ¬s.Subsingleton
Tactic: rw [← not_subsingleton_iff, ← ncard_le_one_iff_subsingleton, not_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
rw : 1 < s.ncard ↔ ¬s.Subsingleton
⊢ 1 < s.ncard ↔ s.Nontrivial
have rw₁ : 1 < s.ncard ↔ ¬s.ncard ≤ 1
Tactic: rw [← not_subsingleton_iff, ← ncard_le_one_iff_subsingleton, not_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ 1 < s.ncard ↔ s.Nontrivial
have rw₂ : 1 < s.ncard ↔ 1 < s.ncard
Tactic: rw [← not_subsingleton_iff, ← ncard_le_one_iff_subsingleton, not_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite
have refine_1 : ∀ (hs : 1 < s.ncard), s.Nontrivial ∧ s.Finite
Tactic: refine ⟨fun hs ↦ ?_, fun ⟨hs_nontrivial, hs_finite⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
refine_1 : ∀ (hs : 1 < s.ncard), s.Nontrivial ∧ s.Finite
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite
have refine_2 : s.Nontrivial ∧ s.Finite → ∀ (hs_nontrivial : s.Nontrivial) (hs_finite : s.Finite), 1 < s.ncard
Tactic: refine ⟨fun hs ↦ ?_, fun ⟨hs_nontrivial, hs_finite⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
⊢ s.Nontrivial ∧ s.Finite
have this : s.Finite
Tactic: have := finite_of_ncard_pos (Nat.zero_lt_of_lt hs)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : s.Finite
⊢ s.Nontrivial ∧ s.Finite
have this₁ : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: rw [← Set.finite_coe_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : s.Finite
⊢ 1 < s.ncard
have hs_finite₁ : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: rw [← Set.finite_coe_iff] at hs_finite
Cleared hypotheses: hs_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
have simp_rw : 1 < hs.toFinset (s := s).card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
simp_rw : 1 < hs.toFinset (s := s).card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
have simp_rw₁ : (∃ a ∈ hs.toFinset (s := s), ∃ b ∈ hs.toFinset (s := s), a ≠ b) ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
have rw : (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic: rw [one_lt_ncard hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : s.Nonempty
he : Even s.ncard
⊢ 1 < s.ncard
have hn₁ : 0 < s.ncard
Tactic: rw [← Set.ncard_pos hs] at hn
Cleared hypotheses: hn, he
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
⊢ 1 < s.ncard
have this : s.ncard ≠ 1
Tactic: have : s.ncard ≠ 1 := fun h ↦ by simp [h] at he
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have simp_rw : 2 < hs.toFinset (s := s).card ↔ ∃ (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]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ 2 < s.ncard ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have 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
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.two_lt_card_iff, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 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
have 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
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.three_lt_card_iff, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ 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
have 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
Tactic: simp_rw [ncard_eq_toFinset_card _ hs, Finset.three_lt_card_iff, Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
⊢ ∃ b ∈ s, b ≠ a
have hsf : s.Finite
Tactic: have hsf := finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
hsf : s.Finite
⊢ ∃ b ∈ s, b ≠ a
have hs₁ : 1 < hsf.toFinset (s := s).card
Tactic: rw [ncard_eq_toFinset_card _ hsf] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have hsf : s.Finite
Tactic: have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
hsf : s.Finite
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have 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
Tactic: obtain ⟨a, t, hat, hts, rfl⟩ := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hsf : s.Finite
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
have hts₁ : ∀ (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
Cleared hypotheses: hts
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
have refine_1 : insert a (↑t : Set α) = s
Tactic: refine ⟨a, t, hat, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : α) (t_1 : Set α), a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card
have refine_2 : (↑t : Set α).ncard = t.card
Tactic: refine ⟨a, t, hat, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have have : ∀ (hsf : s.Finite), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
Tactic: classical
  have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
have have₁ have₂ : ∀ (hsf : s.Finite), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have have₃ : ∀ (hsf : s.Finite) (h : ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = hsf.toFinset (s := s) ∧ t.card = n),
  ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
Tactic: classical
  have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
have have₁ have₂ : ∀ (hsf : s.Finite), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have₃ :
  ∀ (hsf : s.Finite) (h : ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = hsf.toFinset (s := s) ∧ t.card = n),
    ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have have₄ : ∀ (hsf : s.Finite) (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
Tactic: classical
  have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
have have₁ have₂ : ∀ (hsf : s.Finite), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have₃ :
  ∀ (hsf : s.Finite) (h : ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = hsf.toFinset (s := s) ∧ t.card = n),
    ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have₄ :
  ∀ (hsf : s.Finite) (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
have have₅ : ∀ (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: classical
  have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp
Cleared hypotheses: n, h