awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Tactic: classical
  by_cases! h : ∀ i ∈ t, (s i).Finite
  · have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
    rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
  · obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
    rw [← Set.insert_diff_self_of_mem hi,
      finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]
    simp [hn]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have neg : ∀ (h : ¬∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Tactic: classical
  by_cases! h : ∀ i ∈ t, (s i).Finite
  · have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
    rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
  · obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
    rw [← Set.insert_diff_self_of_mem hi,
      finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]
    simp [hn]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
neg : ∀ (h : ¬∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
pos₁ : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
neg₁ : ∀ (h : ¬∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
pos₂ : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have neg₂ : ∀ (h : ∃ i ∈ t, (s i).Infinite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Tactic: classical
  by_cases! h : ∀ i ∈ t, (s i).Finite
  · have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
    rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
  · obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
    rw [← Set.insert_diff_self_of_mem hi,
      finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]
    simp [hn]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ encard.{u_1} (α := α) (⋃ (i : ι), s i) = ∑ᶠ (i : ι), (s i).encard
have rw : encard.{u_1} (α := α) (⋃ (i : ι), s i) =
  encard.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), s i)
Tactic: rw [← finsum_mem_univ, ← finite_univ.encard_biUnion (fun a _ b _ hab ↦ hs hab)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_3
⊢ encard.{u_3} (α := α) univ = ENat.card α
have rw : ENat.card.{u_3} (↑univ : Type u_3) = ENat.card α
Tactic: rw [encard, ENat.card_congr (Equiv.Set.univ α)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_3
rw : ENat.card.{u_3} (↑univ : Type u_3) = ENat.card α
⊢ encard.{u_3} (α := α) univ = ENat.card α
have rw₁ : ENat.card α = ENat.card α
Tactic: rw [encard, ENat.card_congr (Equiv.Set.univ α)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)
have have : ∀ (this : Fintype (↑s : Type u_1)), s.encard = (↑h.toFinset (s := s).card : ℕ∞)
Tactic: have := h.fintype
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype (↑s : Type u_1)
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)
have rw : ENat.card.{u_1} (↑s : Type u_1) = (↑h.toFinset (s := s).card : ℕ∞)
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype (↑s : Type u_1)
rw : ENat.card.{u_1} (↑s : Type u_1) = (↑h.toFinset (s := s).card : ℕ∞)
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑h.toFinset (s := s).card : ℕ∞)
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype (↑s : Type u_1)
rw : ENat.card.{u_1} (↑s : Type u_1) = (↑h.toFinset (s := s).card : ℕ∞)
rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑h.toFinset (s := s).card : ℕ∞)
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)
have rw₂ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑s.toFinset.card : ℕ∞)
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype (↑s : Type u_1)
rw : ENat.card.{u_1} (↑s : Type u_1) = (↑h.toFinset (s := s).card : ℕ∞)
rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑h.toFinset (s := s).card : ℕ∞)
rw₂ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑s.toFinset.card : ℕ∞)
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)
have rw₃ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞)
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ s.encard = (↑s.toFinset.card : ℕ∞)
have h : s.Finite
Tactic: have h := toFinite s
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
h : s.Finite
⊢ s.encard = (↑s.toFinset.card : ℕ∞)
have rw : Eq (α := ℕ∞) (↑h.toFinset (s := s).card : ℕ∞) (↑s.toFinset.card : ℕ∞)
Tactic: rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
h : s.Finite
rw : Eq (α := ℕ∞) (↑h.toFinset (s := s).card : ℕ∞) (↑s.toFinset.card : ℕ∞)
⊢ s.encard = (↑s.toFinset.card : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑s.toFinset.card : ℕ∞) (↑s.toFinset.card : ℕ∞)
Tactic: rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α).encard = (↑s.card : ℕ∞)
have rw : Eq (α := ℕ∞) (↑sorry.toFinset (s := (↑s : Set α)).card : ℕ∞) (↑s.card : ℕ∞)
Tactic: rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
⊢ s.encard = ⊤
have this : Infinite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := h.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ s.encard = ⊤
have rw : ENat.card.{u_1} (↑s : Type u_1) = ⊤
Tactic: rw [encard, ENat.card_eq_top_of_infinite]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
rw : ENat.card.{u_1} (↑s : Type u_1) = ⊤
⊢ s.encard = ⊤
have rw₁ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [encard, ENat.card_eq_top_of_infinite]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard = 0 ↔ s = ∅
have rw : ENat.card.{u_1} (↑s : Type u_1) = 0 ↔ s = ∅
Tactic: rw [encard, ENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : ENat.card.{u_1} (↑s : Type u_1) = 0 ↔ s = ∅
⊢ s.encard = 0 ↔ s = ∅
have rw₁ : IsEmpty.{u_1 + 1} (↑s : Type u_1) ↔ s = ∅
Tactic: rw [encard, ENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : ENat.card.{u_1} (↑s : Type u_1) = 0 ↔ s = ∅
rw₁ : IsEmpty.{u_1 + 1} (↑s : Type u_1) ↔ s = ∅
⊢ s.encard = 0 ↔ s = ∅
have rw₂ : (∀ (x : α), x ∉ s) ↔ s = ∅
Tactic: rw [encard, ENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : ENat.card.{u_1} (↑s : Type u_1) = 0 ↔ s = ∅
rw₁ : IsEmpty.{u_1 + 1} (↑s : Type u_1) ↔ s = ∅
rw₂ : (∀ (x : α), x ∉ s) ↔ s = ∅
⊢ s.encard = 0 ↔ s = ∅
have rw₃ : (∀ (x : α), x ∉ s) ↔ ∀ (x : α), x ∉ s
Tactic: rw [encard, ENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
⊢ encard.{u_1} (α := α) ∅ = 0
have rw : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ s.Nonempty
have rwa : s ≠ ∅
Tactic: rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard ≠ 0
rwa : s ≠ ∅
⊢ s.Nonempty
have rwa₁ : ¬s = ∅
Tactic: rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard ≠ 0
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
⊢ s.Nonempty
have rwa₂ : ¬s.encard = 0
Tactic: rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≠ 0 ↔ s.Nonempty
have rw : ¬s.encard = 0 ↔ s.Nonempty
Tactic: rw [ne_eq, encard_eq_zero, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : ¬s.encard = 0 ↔ s.Nonempty
⊢ s.encard ≠ 0 ↔ s.Nonempty
have rw₁ : ¬s = ∅ ↔ s.Nonempty
Tactic: rw [ne_eq, encard_eq_zero, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : ¬s.encard = 0 ↔ s.Nonempty
rw₁ : ¬s = ∅ ↔ s.Nonempty
⊢ s.encard ≠ 0 ↔ s.Nonempty
have rw₂ : ¬s = ∅ ↔ s ≠ ∅
Tactic: rw [ne_eq, encard_eq_zero, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ 0 < s.encard ↔ s.Nonempty
have rw : s.encard ≠ 0 ↔ s.Nonempty
Tactic: rw [pos_iff_ne_zero, encard_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard ≠ 0 ↔ s.Nonempty
⊢ 0 < s.encard ↔ s.Nonempty
have rw₁ : s.Nonempty ↔ s.Nonempty
Tactic: rw [pos_iff_ne_zero, encard_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
e : α
⊢ encard (α := α) {e} = 1
have rw : ENat.card.{u_1} (↑{e} : Type u_1) = 1
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
e : α
rw : ENat.card.{u_1} (↑{e} : Type u_1) = 1
⊢ encard (α := α) {e} = 1
have rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑{e} : Type u_1)) : ℕ∞) 1
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
e : α
rw : ENat.card.{u_1} (↑{e} : Type u_1) = 1
rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑{e} : Type u_1)) : ℕ∞) 1
⊢ encard (α := α) {e} = 1
have rw₂ : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
e : α
rw : ENat.card.{u_1} (↑{e} : Type u_1) = 1
rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑{e} : Type u_1)) : ℕ∞) 1
rw₂ : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
⊢ encard (α := α) {e} = 1
have rw₃ : Eq (α := ℕ∞) 1 1
Tactic: rw [encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
a : α
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
have this : Disjoint (α := Set α) {x : α | x ≠ a} {a}
Tactic: have : Disjoint {x | x ≠ a} {a} := disjoint_singleton_right.mpr <| by simp
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
a : α
this : Disjoint (α := Set α) {x : α | x ≠ a} {a}
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
have this₁ : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
Tactic: replace this := (Set.encard_union_eq this).symm
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
⊢ Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ
have h : ∀ (x : α), Membership.mem (γ := Set α) ({x : α | x ≠ a} ∪ {a}) x ↔ Membership.mem (γ := Set α) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
have aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ
Tactic: have aux : {x | x ≠ a} ∪ {a} = univ := by ext x; simp [eq_or_ne x a]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
have rwa : ∀ (this : encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = encard (α := α) ({x : α | x ≠ a} ∪ {a}))
  (aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ), encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
Tactic: rwa [encard_singleton, aux, encard_univ] at this
Cleared hypotheses: this, aux
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ
rwa :
  ∀ (this : encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = encard (α := α) ({x : α | x ≠ a} ∪ {a}))
    (aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ), encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
have rwa₁ : ∀ (this : encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = encard.{u_1} (α := α) univ)
  (aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ), encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
Tactic: rwa [encard_singleton, aux, encard_univ] at this
Cleared hypotheses: this, aux
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ
rwa :
  ∀ (this : encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = encard (α := α) ({x : α | x ≠ a} ∪ {a}))
    (aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ), encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
rwa₁ :
  ∀ (this : encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = encard.{u_1} (α := α) univ)
    (aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ), encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
have rwa₂ : ∀ (this : encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α) (aux : Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ),
  encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α
Tactic: rwa [encard_singleton, aux, encard_univ] at this
Cleared hypotheses: this, aux
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ (insert a s).encard = s.encard + 1
have rw : (s ∪ {a}).encard = s.encard + 1
Tactic: rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
has : a ∉ s
rw : (s ∪ {a}).encard = s.encard + 1
⊢ (insert a s).encard = s.encard + 1
have rw₁ : s.encard + encard (α := α) {a} = s.encard + 1
Tactic: rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
has : a ∉ s
rw : (s ∪ {a}).encard = s.encard + 1
rw₁ : s.encard + encard (α := α) {a} = s.encard + 1
⊢ (insert a s).encard = s.encard + 1
have rw₂ : s.encard + 1 = s.encard + 1
Tactic: rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
s_1 : Set α
hat : a ∉ s_1
hs : s_1.Finite
ht' : s_1.encard < ⊤
⊢ (insert a s_1).encard < ⊤
have insert : s_1.encard + 1 < ⊤
Tactic: rw [encard_insert_of_notMem hat]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard < ⊤
have empty : encard.{u_1} (α := α) ∅ < ⊤
Tactic: induction s, h using Set.Finite.induction_on with
  | empty => simp
  | insert hat _ ht' =>
    rw [encard_insert_of_notMem hat]
    exact lt_tsub_iff_right.1 ht'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Finite
empty : encard.{u_1} (α := α) ∅ < ⊤
⊢ s.encard < ⊤
have insert : ∀ {a : α} {s : Set α} (hat : a ∉ s), s.Finite → ∀ (ht' : s.encard < ⊤), (insert a s).encard < ⊤
Tactic: induction s, h using Set.Finite.induction_on with
  | empty => simp
  | insert hat _ ht' =>
    rw [encard_insert_of_notMem hat]
    exact lt_tsub_iff_right.1 ht'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard = ⊤ ↔ s.Infinite
have contrapose! : s.encard ≠ ⊤ ↔ s.Finite
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≠ ⊤ ↔ s.Finite
have rw : s.encard < ⊤ ↔ s.Finite
Tactic: rw [← lt_top_iff_ne_top, encard_lt_top_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : s.encard < ⊤ ↔ s.Finite
⊢ s.encard ≠ ⊤ ↔ s.Finite
have rw₁ : s.Finite ↔ s.Finite
Tactic: rw [← lt_top_iff_ne_top, encard_lt_top_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ (↑k : ℕ∞)
⊢ s.Finite
have rw : s.encard < ⊤
Tactic: rw [← encard_lt_top_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ (↑k : ℕ∞)
⊢ ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k
have rwa : ∀ (h : ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k), ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k
Tactic: rwa [ENat.le_coe_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.Finite ∧ ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k
left : s.Finite
n₀ : ℕ
hs : s.encard = (↑n₀ : ℕ∞)
hle : n₀ ≤ k
⊢ s.encard ≤ (↑k : ℕ∞)
have rwa : LE.le (α := ℕ∞) (↑n₀ : ℕ∞) (↑k : ℕ∞)
Tactic: rwa [hs, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard
have rw : s.encard ≤ s.encard + (t \ s).encard
Tactic: rw [← union_diff_cancel h, encard_union_eq disjoint_sdiff_right]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s).encard + s.encard = t.encard
have rw : (t \ s ∪ s).encard = t.encard
Tactic: rw [← encard_union_eq disjoint_sdiff_left, diff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
rw : (t \ s ∪ s).encard = t.encard
⊢ (t \ s).encard + s.encard = t.encard
have rw₁ : t.encard = t.encard
Tactic: rw [← encard_union_eq disjoint_sdiff_left, diff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = t.encard - s.encard
have rw : (t \ s).encard = (t \ s).encard + s.encard - s.encard
Tactic: rw [← @Set.encard_diff_add_encard_of_subset _ s t h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ 1 ≤ s.encard ↔ s.Nonempty
have rw : 1 ≤ s.encard ↔ s ≠ ∅
Tactic: rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : 1 ≤ s.encard ↔ s ≠ ∅
⊢ 1 ≤ s.encard ↔ s.Nonempty
have rw₁ : 1 ≤ s.encard ↔ ¬s = ∅
Tactic: rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : 1 ≤ s.encard ↔ s ≠ ∅
rw₁ : 1 ≤ s.encard ↔ ¬s = ∅
⊢ 1 ≤ s.encard ↔ s.Nonempty
have rw₂ : 1 ≤ s.encard ↔ ¬s.encard = 0
Tactic: rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
rw : 1 ≤ s.encard ↔ s ≠ ∅
rw₁ : 1 ≤ s.encard ↔ ¬s = ∅
rw₂ : 1 ≤ s.encard ↔ ¬s.encard = 0
⊢ 1 ≤ s.encard ↔ s.Nonempty
have rw₃ : s.encard ≠ 0 ↔ ¬s.encard = 0
Tactic: rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ (s \ t).encard + (s ∩ t).encard = s.encard
have rw : (s \ t ∪ s ∩ t).encard = s.encard
Tactic: rw [← encard_union_eq disjoint_sdiff_inter, diff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
rw : (s \ t ∪ s ∩ t).encard = s.encard
⊢ (s \ t).encard + (s ∩ t).encard = s.encard
have rw₁ : s.encard = s.encard
Tactic: rw [← encard_union_eq disjoint_sdiff_inter, diff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
have rw : (s \ t ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
Tactic: rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm,
    encard_diff_add_encard_inter]
-- 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.encard + t.encard
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
have rw₁ : (s \ t).encard + t.encard + (s ∩ t).encard = s.encard + t.encard
Tactic: rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm,
    encard_diff_add_encard_inter]
-- 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.encard + t.encard
rw₁ : (s \ t).encard + t.encard + (s ∩ t).encard = s.encard + t.encard
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
have rw₂ : (s \ t).encard + (s ∩ t).encard + t.encard = s.encard + t.encard
Tactic: rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm,
    encard_diff_add_encard_inter]
-- 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.encard + t.encard
rw₁ : (s \ t).encard + t.encard + (s ∩ t).encard = s.encard + t.encard
rw₂ : (s \ t).encard + (s ∩ t).encard + t.encard = s.encard + t.encard
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
have rw₃ : s.encard + t.encard = s.encard + t.encard
Tactic: rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm,
    encard_diff_add_encard_inter]