awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard
have rw : (s \ t).encard + (s ∩ t).encard = t.encard ↔ (s \ t).encard = (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_right_inj h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard = t.encard ↔ (s \ t).encard = (t \ s).encard
⊢ s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard
have rw₁ : (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard = (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_right_inj h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard = t.encard ↔ (s \ t).encard = (t \ s).encard
rw₁ : (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard = (t \ s).encard
⊢ s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard
have rw₂ : (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard = (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_right_inj h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard = t.encard ↔ (s \ t).encard = (t \ s).encard
rw₁ : (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard = (t \ s).encard
rw₂ : (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard = (t \ s).encard
⊢ s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard
have rw₃ : (s \ t).encard = (t \ s).encard ↔ (s \ t).encard = (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_right_inj h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
have rw : (s \ t).encard + (s ∩ t).encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_le_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
⊢ s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
have rw₁ : (s \ t).encard + (s ∩ t).encard ≤ (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard ≤ (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_le_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
rw₁ : (s \ t).encard + (s ∩ t).encard ≤ (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard ≤ (t \ s).encard
⊢ s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
have rw₂ : (s \ t).encard + (s ∩ t).encard ≤ (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard ≤ (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_le_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
rw₁ : (s \ t).encard + (s ∩ t).encard ≤ (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard ≤ (t \ s).encard
rw₂ : (s \ t).encard + (s ∩ t).encard ≤ (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard ≤ (t \ s).encard
⊢ s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
have rw₃ : (s \ t).encard ≤ (t \ s).encard ↔ (s \ t).encard ≤ (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_le_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard
have rw : (s \ t).encard + (s ∩ t).encard < t.encard ↔ (s \ t).encard < (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_lt_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard < t.encard ↔ (s \ t).encard < (t \ s).encard
⊢ s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard
have rw₁ : (s \ t).encard + (s ∩ t).encard < (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard < (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_lt_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard < t.encard ↔ (s \ t).encard < (t \ s).encard
rw₁ : (s \ t).encard + (s ∩ t).encard < (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard < (t \ s).encard
⊢ s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard
have rw₂ : (s \ t).encard + (s ∩ t).encard < (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard < (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_lt_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
rw : (s \ t).encard + (s ∩ t).encard < t.encard ↔ (s \ t).encard < (t \ s).encard
rw₁ : (s \ t).encard + (s ∩ t).encard < (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard < (t \ s).encard
rw₂ : (s \ t).encard + (s ∩ t).encard < (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard < (t \ s).encard
⊢ s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard
have rw₃ : (s \ t).encard < (t \ s).encard ↔ (s \ t).encard < (t \ s).encard
Tactic: rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_lt_add_iff_right h.encard_lt_top.ne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ s.encard + t.encard
have rw : (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
Tactic: rw [← encard_union_add_encard_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.Finite ↔ t.Finite
have rw : s.encard < ⊤ ↔ t.Finite
Tactic: rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
rw : s.encard < ⊤ ↔ t.Finite
⊢ s.Finite ↔ t.Finite
have rw₁ : s.encard < ⊤ ↔ t.encard < ⊤
Tactic: rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
rw : s.encard < ⊤ ↔ t.Finite
rw₁ : s.encard < ⊤ ↔ t.encard < ⊤
⊢ s.Finite ↔ t.Finite
have rw₂ : t.encard < ⊤ ↔ t.encard < ⊤
Tactic: rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.Infinite ↔ t.Infinite
have rw : s.encard = ⊤ ↔ t.Infinite
Tactic: rw [← encard_eq_top_iff, h, encard_eq_top_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
rw : s.encard = ⊤ ↔ t.Infinite
⊢ s.Infinite ↔ t.Infinite
have rw₁ : t.encard = ⊤ ↔ t.Infinite
Tactic: rw [← encard_eq_top_iff, h, encard_eq_top_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
rw : s.encard = ⊤ ↔ t.Infinite
rw₁ : t.encard = ⊤ ↔ t.Infinite
⊢ s.Infinite ↔ t.Infinite
have rw₂ : t.Infinite ↔ t.Infinite
Tactic: rw [← encard_eq_top_iff, h, encard_eq_top_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : t.encard ≤ s.encard
⊢ s = t
have hts₁ : (t \ s).encard + s.encard ≤ 0 + s.encard
Tactic: rw [← zero_add (a := encard s), ← encard_diff_add_encard_of_subset hst] at hts
Cleared hypotheses: hts
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t
have hdiff : (t \ s).encard ≤ 0
Tactic: have hdiff := WithTop.le_of_add_le_add_right (ht.subset hst).encard_lt_top.ne hts
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : (t \ s).encard ≤ 0
⊢ s = t
have hdiff₁ : t ⊆ s
Tactic: rw [nonpos_iff_eq_zero, encard_eq_zero, diff_eq_empty] at hdiff
Cleared hypotheses: hdiff
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ (s \ t).encard + t.encard = (s ∪ t).encard
have rw : (s \ t ∪ t).encard = (s ∪ t).encard
Tactic: rw [← encard_union_eq disjoint_sdiff_left, diff_union_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
rw : (s \ t ∪ t).encard = (s ∪ t).encard
⊢ (s \ t).encard + t.encard = (s ∪ t).encard
have rw₁ : (s ∪ t).encard = (s ∪ t).encard
Tactic: rw [← encard_union_eq disjoint_sdiff_left, diff_union_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ s.encard - t.encard ≤ (s \ t).encard
have rw : s.encard ≤ (s \ t).encard + t.encard
Tactic: rw [tsub_le_iff_left, add_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard + sᶜ.encard = encard.{u_1} (α := α) univ
have rw : (s ∪ sᶜ).encard = encard.{u_1} (α := α) univ
Tactic: rw [← encard_union_eq disjoint_compl_right, union_compl_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : (s ∪ sᶜ).encard = encard.{u_1} (α := α) univ
⊢ s.encard + sᶜ.encard = encard.{u_1} (α := α) univ
have rw₁ : encard.{u_1} (α := α) univ = encard.{u_1} (α := α) univ
Tactic: rw [← encard_union_eq disjoint_compl_right, union_compl_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
⊢ (insert x s).encard ≤ s.encard + 1
have rw : (s ∪ {x}).encard ≤ s.encard + encard (α := α) {x}
Tactic: rw [← union_singleton, ← encard_singleton x]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
⊢ ({x} ∩ s).encard ≤ 1
have grw : ({x} ∩ s).encard ≤ encard (α := α) {x}
Tactic: grw [← encard_singleton x, inter_subset_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
grw : ({x} ∩ s).encard ≤ encard (α := α) {x}
⊢ ({x} ∩ s).encard ≤ 1
have grw₁ : encard (α := α) {x} ≤ encard (α := α) {x}
Tactic: grw [← encard_singleton x, inter_subset_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard + 1 = s.encard
have rw : (insert a (s \ {a})).encard = s.encard
Tactic: rw [← encard_insert_of_notMem (fun h ↦ h.2 rfl), insert_diff_singleton, insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
rw : (insert a (s \ {a})).encard = s.encard
⊢ (s \ {a}).encard + 1 = s.encard
have rw₁ : (insert a s).encard = s.encard
Tactic: rw [← encard_insert_of_notMem (fun h ↦ h.2 rfl), insert_diff_singleton, insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
rw : (insert a (s \ {a})).encard = s.encard
rw₁ : (insert a s).encard = s.encard
⊢ (s \ {a}).encard + 1 = s.encard
have rw₂ : s.encard = s.encard
Tactic: rw [← encard_insert_of_notMem (fun h ↦ h.2 rfl), insert_diff_singleton, insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = s.encard - 1
have rw : (s \ {a}).encard = (s \ {a}).encard + 1 - 1
Tactic: rw [← encard_diff_singleton_add_one h, ← WithTop.add_right_inj WithTop.one_ne_top,
    tsub_add_cancel_of_le (self_le_add_left _ _)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
rw : (s \ {a}).encard = (s \ {a}).encard + 1 - 1
⊢ (s \ {a}).encard = s.encard - 1
have rw₁ : (s \ {a}).encard + 1 = (s \ {a}).encard + 1 - 1 + 1
Tactic: rw [← encard_diff_singleton_add_one h, ← WithTop.add_right_inj WithTop.one_ne_top,
    tsub_add_cancel_of_le (self_le_add_left _ _)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
rw : (s \ {a}).encard = (s \ {a}).encard + 1 - 1
rw₁ : (s \ {a}).encard + 1 = (s \ {a}).encard + 1 - 1 + 1
⊢ (s \ {a}).encard = s.encard - 1
have rw₂ : (s \ {a}).encard + 1 = (s \ {a}).encard + 1
Tactic: rw [← encard_diff_singleton_add_one h, ← WithTop.add_right_inj WithTop.one_ne_top,
    tsub_add_cancel_of_le (self_le_add_left _ _)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
⊢ s.encard - 1 ≤ (s \ {x}).encard
have rw : s.encard - encard (α := α) {x} ≤ (s \ {x}).encard
Tactic: rw [← encard_singleton x]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).encard = s.encard
have rw : a ∉ s \ {b}
Tactic: rw [encard_insert_of_notMem, encard_diff_singleton_add_one hb]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).encard = s.encard
have rw : (insert a (s \ {b})).encard = s.encard
Tactic: rw [← insert_diff_singleton_comm (by rintro rfl; exact ha hb), encard_exchange ha hb]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
rw : (insert a (s \ {b})).encard = s.encard
⊢ (insert a s \ {b}).encard = s.encard
have rw₁ : s.encard = s.encard
Tactic: rw [← insert_diff_singleton_comm (by rintro rfl; exact ha hb), encard_exchange ha hb]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
⊢ s.encard = k + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
have refine_1 : ∀ (h : s.encard = k + 1), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
refine_1 : ∀ (h : s.encard = k + 1), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
⊢ s.encard = k + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
have refine_2 : (∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k) → s.encard = k + 1
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
have refine_1 : ∀ (a : α) (ha : a ∈ s), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
Tactic: obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s
have rwa : insert a s = s
Tactic: rwa [insert_diff_singleton, insert_eq_of_mem]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
rwa : insert a s = s
⊢ insert a (s \ {a}) = s
have rwa₁ : s = s
Tactic: rwa [insert_diff_singleton, insert_eq_of_mem]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
have refine_1 : (s \ {a}).encard = k
Tactic: refine ⟨a, s \ {a}, fun h ↦ h.2 rfl, by rwa [insert_diff_singleton, insert_eq_of_mem], ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ (s \ {a}).encard = k
have refine_1 : (s \ {a}).encard + 1 = k + 1
Tactic: rw [← WithTop.add_right_inj WithTop.one_ne_top, ← h,
      encard_diff_singleton_add_one ha]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
refine_1 : (s \ {a}).encard + 1 = k + 1
⊢ (s \ {a}).encard = k
have refine_1₁ : (s \ {a}).encard + 1 = s.encard
Tactic: rw [← WithTop.add_right_inj WithTop.one_ne_top, ← h,
      encard_diff_singleton_add_one ha]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
refine_1 : (s \ {a}).encard + 1 = k + 1
refine_1₁ : (s \ {a}).encard + 1 = s.encard
⊢ (s \ {a}).encard = k
have refine_1₂ : s.encard = s.encard
Tactic: rw [← WithTop.add_right_inj WithTop.one_ne_top, ← h,
      encard_diff_singleton_add_one ha]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ (insert a t).encard = t.encard + 1
have refine_2 : t.encard + 1 = t.encard + 1
Tactic: rw [encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard
have refine : s.Nonempty → ∀ (a : α) (ha : a ∈ s) (hfin : s.Finite), (s \ {a}).encard < s.encard
Tactic: refine s.eq_empty_or_nonempty.elim Or.inl (Or.inr ∘ fun ⟨a,ha⟩ ↦
    (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, ?_⟩) (Or.inl ∘ Infinite.encard_eq)))
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < s.encard
have rw : (s \ {a}).encard < (s \ {a}).encard + 1
Tactic: rw [← encard_diff_singleton_add_one ha]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1
have nth_rw : (s \ {a}).encard + 0 < (s \ {a}).encard + 1
Tactic: nth_rw 1 [← add_zero (encard _)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
x y : α
hne : x ≠ y
⊢ encard (α := α) {x, y} = 2
have rw : encard (α := α) {y} + 1 = 2
Tactic: rw [encard_insert_of_notMem (by simpa), ← one_add_one_eq_two,
    WithTop.add_right_inj WithTop.one_ne_top, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
x y : α
hne : x ≠ y
rw : encard (α := α) {y} + 1 = 2
⊢ encard (α := α) {x, y} = 2
have rw₁ : encard (α := α) {y} + 1 = HAdd.hAdd (α := ℕ∞) 1 1
Tactic: rw [encard_insert_of_notMem (by simpa), ← one_add_one_eq_two,
    WithTop.add_right_inj WithTop.one_ne_top, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
x y : α
hne : x ≠ y
rw : encard (α := α) {y} + 1 = 2
rw₁ : encard (α := α) {y} + 1 = HAdd.hAdd (α := ℕ∞) 1 1
⊢ encard (α := α) {x, y} = 2
have rw₂ : encard (α := α) {y} = 1
Tactic: rw [encard_insert_of_notMem (by simpa), ← one_add_one_eq_two,
    WithTop.add_right_inj WithTop.one_ne_top, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
x y : α
hne : x ≠ y
rw : encard (α := α) {y} + 1 = 2
rw₁ : encard (α := α) {y} + 1 = HAdd.hAdd (α := ℕ∞) 1 1
rw₂ : encard (α := α) {y} = 1
⊢ encard (α := α) {x, y} = 2
have rw₃ : Eq (α := WithTop ℕ) 1 1
Tactic: rw [encard_insert_of_notMem (by simpa), ← one_add_one_eq_two,
    WithTop.add_right_inj WithTop.one_ne_top, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α), s = {x}
x : α
hx : s = {x}
⊢ s.encard = 1
have rw : encard (α := α) {x} = 1
Tactic: rw [hx, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α), s = {x}
x : α
hx : s = {x}
rw : encard (α := α) {x} = 1
⊢ s.encard = 1
have rw₁ : Eq (α := ℕ∞) 1 1
Tactic: rw [hx, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard = 1 ↔ ∃ (x : α), s = {x}
have refine : ∀ (h : s.encard = 1), ∃ (x : α), s = {x}
Tactic: refine ⟨fun h ↦ ?_, fun ⟨x, hx⟩ ↦ by rw [hx, encard_singleton]⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ s.encard ≠ 0
have rw : Ne (α := ℕ∞) 1 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ ∃ (x : α), s = {x}
have obtain : ∀ (x : α) (hx : x ∈ s), ∃ (x : α), s = {x}
Tactic: obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
have rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
Tactic: rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
have rw₁ : ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
Tactic: rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₁ : ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
have rw₂ : ¬s.encard ≠ 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
Tactic: rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₁ : ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₂ : ¬s.encard ≠ 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
have rw₃ : s.encard = 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
Tactic: rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₁ : ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₂ : ¬s.encard ≠ 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₃ : s.encard = 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
have rw₄ : s = ∅ ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
Tactic: rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₁ : ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₂ : ¬s.encard ≠ 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₃ : s.encard = 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₄ : s = ∅ ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
have rw₅ : (s = ∅ ∨ ∃ (x : α), s = {x}) ↔ s = ∅ ∨ ∃ (x : α), s = {x}
Tactic: rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
have rw : (s.Nonempty → ∃ (x : α), s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
Tactic: rw [encard_le_one_iff_eq, or_iff_not_imp_left, ← Ne, ← nonempty_iff_ne_empty]