awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : Eq (α := ℕ∞) (↑s.ncard : ℕ∞) (↑0 : ℕ∞) ↔ s = ∅
rw₁ : s.encard = (↑0 : ℕ∞) ↔ s = ∅
⊢ s.ncard = 0 ↔ s = ∅
have rw₂ : s.encard = 0 ↔ s = ∅
Tactic: rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : Eq (α := ℕ∞) (↑s.ncard : ℕ∞) (↑0 : ℕ∞) ↔ s = ∅
rw₁ : s.encard = (↑0 : ℕ∞) ↔ s = ∅
rw₂ : s.encard = 0 ↔ s = ∅
⊢ s.ncard = 0 ↔ s = ∅
have rw₃ : s = ∅ ↔ s = ∅
Tactic: rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α).ncard = s.card
have rw : sorry.toFinset (s := (↑s : Set α)).card = s.card
Tactic: rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ⋯.toFinset (s := (↑s : Set α)).card = s.card
⊢ (↑s : Set α).ncard = s.card
have rw₁ : s.card = s.card
Tactic: rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_3
⊢ ncard.{u_3} (α := α) ∅ = 0
have rw : Eq.{u_3 + 1} (α := Set α) ∅ ∅
Tactic: rw [ncard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 0 < s.ncard ↔ s.Nonempty
have rw : s.ncard ≠ 0 ↔ s.Nonempty
Tactic: rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : s.ncard ≠ 0 ↔ s.Nonempty
⊢ 0 < s.ncard ↔ s.Nonempty
have rw₁ : ¬s.ncard = 0 ↔ s.Nonempty
Tactic: rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : s.ncard ≠ 0 ↔ s.Nonempty
rw₁ : ¬s.ncard = 0 ↔ s.Nonempty
⊢ 0 < s.ncard ↔ s.Nonempty
have rw₂ : ¬s = ∅ ↔ s.Nonempty
Tactic: rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : s.ncard ≠ 0 ↔ s.Nonempty
rw₁ : ¬s.ncard = 0 ↔ s.Nonempty
rw₂ : ¬s = ∅ ↔ s.Nonempty
⊢ 0 < s.ncard ↔ s.Nonempty
have rw₃ : ¬s = ∅ ↔ s ≠ ∅
Tactic: rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s.Nonempty
have rw : s ≠ ∅
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).ncard ≤ 1
have rw : ({a} ∩ s).encard ≤ 1
Tactic: rw [← Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard
have h : Cardinal.mk (↑(𝒫 s) : Type u_1) = HPow.hPow (α := Cardinal.{u_1}) 2 (Cardinal.mk (↑s : Type u_1))
Tactic: have h := Cardinal.mk_powerset s
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
h : Cardinal.mk (↑(𝒫 s) : Type u_1) = HPow.hPow (α := Cardinal.{u_1}) 2 (Cardinal.mk (↑s : Type u_1))
⊢ (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard
have h₁ : (↑(𝒫 s).ncard : Cardinal.{u_1}) = HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 2 (↑s.ncard : Cardinal.{u_1})
Tactic: rw [← cast_ncard hs.powerset, ← cast_ncard hs] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
h :
  (↑(𝒫 s).ncard : Cardinal.{u_1}) = HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 2 (↑s.ncard : Cardinal.{u_1})
⊢ (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard
have norm_cast : ∀ (h : (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard), (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).ncard = s.ncard + 1
have rw : Eq (α := ℕ∞) (↑(insert a s).ncard : ℕ∞) (↑(s.ncard + 1) : ℕ∞)
Tactic: rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
rw : Eq (α := ℕ∞) (↑(insert a s).ncard : ℕ∞) (↑(s.ncard + 1) : ℕ∞)
⊢ (insert a s).ncard = s.ncard + 1
have rw₁ : (insert a s).encard = (↑(s.ncard + 1) : ℕ∞)
Tactic: rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
rw : Eq (α := ℕ∞) (↑(insert a s).ncard : ℕ∞) (↑(s.ncard + 1) : ℕ∞)
rw₁ : (insert a s).encard = (↑(s.ncard + 1) : ℕ∞)
⊢ (insert a s).ncard = s.ncard + 1
have rw₂ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑1 : ℕ∞)
Tactic: rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
rw : Eq (α := ℕ∞) (↑(insert a s).ncard : ℕ∞) (↑(s.ncard + 1) : ℕ∞)
rw₁ : (insert a s).encard = (↑(s.ncard + 1) : ℕ∞)
rw₂ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑1 : ℕ∞)
⊢ (insert a s).ncard = s.ncard + 1
have rw₃ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1
Tactic: rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
rw : Eq (α := ℕ∞) (↑(insert a s).ncard : ℕ∞) (↑(s.ncard + 1) : ℕ∞)
rw₁ : (insert a s).encard = (↑(s.ncard + 1) : ℕ∞)
rw₂ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑1 : ℕ∞)
rw₃ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1
⊢ (insert a s).ncard = s.ncard + 1
have rw₄ : (insert a s).encard = s.encard + 1
Tactic: rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
rw : Eq (α := ℕ∞) (↑(insert a s).ncard : ℕ∞) (↑(s.ncard + 1) : ℕ∞)
rw₁ : (insert a s).encard = (↑(s.ncard + 1) : ℕ∞)
rw₂ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑1 : ℕ∞)
rw₃ : (insert a s).encard = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1
rw₄ : (insert a s).encard = s.encard + 1
⊢ (insert a s).ncard = s.ncard + 1
have rw₅ : s.encard + 1 = s.encard + 1
Tactic: rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a s).ncard = s.ncard
have rw : s.ncard = s.ncard
Tactic: rw [insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
⊢ (insert a s).ncard ≤ s.ncard + 1
have inl : ∀ (hs : s.Finite), (insert a s).ncard ≤ s.ncard + 1
Tactic: obtain hs | hs := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
inl : ∀ (hs : s.Finite), (insert a s).ncard ≤ s.ncard + 1
⊢ (insert a s).ncard ≤ s.ncard + 1
have inr : ∀ (hs : s.Infinite), (insert a s).ncard ≤ s.ncard + 1
Tactic: obtain hs | hs := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).ncard ≤ s.ncard + 1
have inl : (↑(insert a s).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (↑(insert a s).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1
have inl : (insert a s).encard ≤ s.encard + 1
Tactic: rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1
have inr : 0 ≤ s.ncard + 1
Tactic: rw [(hs.mono (subset_insert a s)).ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inst : Decidable (a ∈ s)
hs : s.Finite
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
have pos : ∀ (h : a ∈ s), (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inst : Decidable (a ∈ s)
hs : s.Finite
pos : ∀ (h : a ∈ s), (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
have neg : ∀ (h : a ∉ s), (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inst : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
have pos : s.ncard = if a ∈ s then s.ncard else s.ncard + 1
Tactic: rw [ncard_insert_of_mem h, if_pos h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inst : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
pos : s.ncard = if a ∈ s then s.ncard else s.ncard + 1
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
have pos₁ : s.ncard = s.ncard
Tactic: rw [ncard_insert_of_mem h, if_pos h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inst : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
have neg : s.ncard + 1 = if a ∈ s then s.ncard else s.ncard + 1
Tactic: rw [ncard_insert_of_notMem h hs, if_neg h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inst : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
neg : s.ncard + 1 = if a ∈ s then s.ncard else s.ncard + 1
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
have neg₁ : s.ncard + 1 = s.ncard + 1
Tactic: rw [ncard_insert_of_notMem h hs, if_neg h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ s.ncard ≤ (insert a s).ncard
have rw : 0 ≤ (insert a s).ncard
Tactic: rw [h.ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
a : α
s : Set α
⊢ s.ncard ≤ (insert a s).ncard
have h : s.Finite
Tactic: refine
    s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ (insert a s).ncard
have rw : s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
Tactic: rw [ncard_insert_eq_ite h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
have pos : a ∈ s → s.ncard ≤ s.ncard
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
pos : a ∈ s → s.ncard ≤ s.ncard
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
have neg : a ∉ s → s.ncard ≤ s.ncard + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
⊢ s.ncard ≤ (insert a s).ncard
have h : ∀ (h : s.Finite), s.ncard ≤ (insert a s).ncard
Tactic: classical
  refine
    s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
  rw [ncard_insert_eq_ite h]; split_ifs <;> simp
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
s : Set α
h : ∀ (h : s.Finite), s.ncard ≤ (insert a s).ncard
⊢ s.ncard ≤ (insert a s).ncard
have h₁ : ∀ (h : s.Finite), s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
Tactic: classical
  refine
    s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
  rw [ncard_insert_eq_ite h]; split_ifs <;> simp
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard + 1 = s.ncard
have to_encard_tac : HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = (↑s.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = (↑s.ncard : ℕ∞)
have rw : HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = s.encard
Tactic: rw [hs.cast_ncard_eq, hs.diff.cast_ncard_eq, encard_diff_singleton_add_one h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = s.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = (↑s.ncard : ℕ∞)
have rw₁ : (s \ {a}).encard + 1 = s.encard
Tactic: rw [hs.cast_ncard_eq, hs.diff.cast_ncard_eq, encard_diff_singleton_add_one h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = s.encard
rw₁ : (s \ {a}).encard + 1 = s.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = (↑s.ncard : ℕ∞)
have rw₂ : s.encard = s.encard
Tactic: rw [hs.cast_ncard_eq, hs.diff.cast_ncard_eq, encard_diff_singleton_add_one h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).ncard = s.ncard - 1
have inl : ∀ (hs : s.Infinite), (s \ {a}).ncard = s.ncard - 1
Tactic: rcases s.infinite_or_finite with hs | hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
inl : ∀ (hs : s.Infinite), (s \ {a}).ncard = s.ncard - 1
⊢ (s \ {a}).ncard = s.ncard - 1
have inr : ∀ (hs : s.Finite), (s \ {a}).ncard = s.ncard - 1
Tactic: rcases s.infinite_or_finite with hs | hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard < s.ncard
have rw : (s \ {a}).ncard < (s \ {a}).ncard + 1
Tactic: rw [← ncard_diff_singleton_add_one h hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
⊢ (s \ {a}).ncard ≤ s.ncard
have inl : ∀ (hs : s.Finite), (s \ {a}).ncard ≤ s.ncard
Tactic: obtain hs | hs := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
inl : ∀ (hs : s.Finite), (s \ {a}).ncard ≤ s.ncard
⊢ (s \ {a}).ncard ≤ s.ncard
have inr : ∀ (hs : s.Infinite), (s \ {a}).ncard ≤ s.ncard
Tactic: obtain hs | hs := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard
have h : (s \ {a}).ncard = 0
Tactic: convert! Nat.zero_le _
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
⊢ s.ncard - 1 ≤ (s \ {a}).ncard
have pos : ∀ (h : a ∈ s), s.ncard - 1 ≤ (s \ {a}).ncard
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
pos : ∀ (h : a ∈ s), s.ncard - 1 ≤ (s \ {a}).ncard
⊢ s.ncard - 1 ≤ (s \ {a}).ncard
have neg : ∀ (h : a ∉ s), s.ncard - 1 ≤ (s \ {a}).ncard
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard
have pos : s.ncard - 1 ≤ s.ncard - 1
Tactic: rw [ncard_diff_singleton_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard
have neg : s.ncard - 1 ≤ s.ncard
Tactic: rw [diff_singleton_eq_self h]
-- 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}).ncard = s.ncard
have rw : (insert a s \ {b}).ncard = (insert a (s \ {b})).ncard
Tactic: rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
    diff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
-- 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}).ncard = (insert a (s \ {b})).ncard
⊢ (insert a s \ {b}).ncard = s.ncard
have rw₁ : (({a} ∪ s) \ {b}).ncard = (insert a (s \ {b})).ncard
Tactic: rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
    diff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
-- 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}).ncard = (insert a (s \ {b})).ncard
rw₁ : (({a} ∪ s) \ {b}).ncard = (insert a (s \ {b})).ncard
⊢ (insert a s \ {b}).ncard = s.ncard
have rw₂ : (({a} ∪ s) \ {b}).ncard = ({a} ∪ s \ {b}).ncard
Tactic: rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
    diff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
-- 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}).ncard = (insert a (s \ {b})).ncard
rw₁ : (({a} ∪ s) \ {b}).ncard = (insert a (s \ {b})).ncard
rw₂ : (({a} ∪ s) \ {b}).ncard = ({a} ∪ s \ {b}).ncard
⊢ (insert a s \ {b}).ncard = s.ncard
have rw₃ : ({a} \ {b} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard
Tactic: rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
    diff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
-- 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}).ncard = (insert a (s \ {b})).ncard
rw₁ : (({a} ∪ s) \ {b}).ncard = (insert a (s \ {b})).ncard
rw₂ : (({a} ∪ s) \ {b}).ncard = ({a} ∪ s \ {b}).ncard
rw₃ : ({a} \ {b} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard
⊢ (insert a s \ {b}).ncard = s.ncard
have rw₄ : ({a} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard
Tactic: rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
    diff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd (insert a s).ncard ↔ Even s.ncard
have rw : (Odd s.ncard ↔ Even (α := ℕ) 1) ↔ Even s.ncard
Tactic: rw [ncard_insert_of_notMem ha hs, Nat.odd_add]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Even (insert a s).ncard ↔ Odd s.ncard
have rw : Even (s.ncard + 1) ↔ Odd s.ncard
Tactic: rw [ncard_insert_of_notMem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
rw : Even (s.ncard + 1) ↔ Odd s.ncard
⊢ Even (insert a s).ncard ↔ Odd s.ncard
have rw₁ : ¬Even s.ncard ↔ Odd s.ncard
Tactic: rw [ncard_insert_of_notMem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
rw : Even (s.ncard + 1) ↔ Odd s.ncard
rw₁ : ¬Even s.ncard ↔ Odd s.ncard
⊢ Even (insert a s).ncard ↔ Odd s.ncard
have rw₂ : Odd s.ncard ↔ Odd s.ncard
Tactic: rw [ncard_insert_of_notMem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).ncard ≤ s.ncard
have to_encard_tac : LE.le (α := ℕ∞) (↑(f '' s).ncard : ℕ∞) (↑s.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ LE.le (α := ℕ∞) (↑(f '' s).ncard : ℕ∞) (↑s.ncard : ℕ∞)
have rw : (f '' s).encard ≤ s.encard
Tactic: rw [hs.cast_ncard_eq, (hs.image _).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).ncard = s.ncard
hs : s.Finite
⊢ InjOn f s
have h₁ : (f '' s).encard = s.encard
Tactic: rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ (f ⁻¹' s).ncard = s.ncard
have rw : (f '' f ⁻¹' s).ncard = s.ncard
Tactic: rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
rw : (f '' f ⁻¹' s).ncard = s.ncard
⊢ (f ⁻¹' s).ncard = s.ncard
have rw₁ : s.ncard = s.ncard
Tactic: rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : s.Finite
⊢ ncard.{u_1} (α := α) {x : α | x ∈ s ∧ f x = y} ≠ 0 ↔ y ∈ f '' s
have refine : y ∈ f '' s → ncard.{u_1} (α := α) {x : α | x ∈ s ∧ f x = y} ≠ 0
Tactic: refine ⟨nonempty_of_ncard_ne_zero, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
P : α → Prop
s : Set α
⊢ ncard.{u_1} (α := Subtype P) {x : Subtype P | (↑x : α) ∈ s} = (s ∩ setOf P).ncard
have h : s ∩ setOf P = (fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}
Tactic: convert! (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
P : α → Prop
s : Set α
⊢ s ∩ setOf P = (fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}
have h : ∀ (x : α),
  x ∈ s ∩ setOf P ↔ Membership.mem (γ := Set α) ((fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.ncard ≤ s.ncard
ht : t.Finite
⊢ t.encard ≤ s.encard
have rwa : ∀ (h' : LE.le (α := ℕ∞) (↑t.ncard : ℕ∞) (↑s.ncard : ℕ∞)) (ht : t.Finite), t.encard ≤ s.encard
Tactic: rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h'
Cleared hypotheses: h', ht
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.ncard ≤ s.ncard
ht : t.Finite
rwa : ∀ (h' : LE.le (α := ℕ∞) (↑t.ncard : ℕ∞) (↑s.ncard : ℕ∞)) (ht : t.Finite), t.encard ≤ s.encard
⊢ t.encard ≤ s.encard
have rwa₁ : ∀ (h' : t.encard ≤ (↑s.ncard : ℕ∞)) (ht : t.Finite), t.encard ≤ s.encard
Tactic: rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h'
Cleared hypotheses: h', ht
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.ncard ≤ s.ncard
ht : t.Finite
rwa : ∀ (h' : LE.le (α := ℕ∞) (↑t.ncard : ℕ∞) (↑s.ncard : ℕ∞)) (ht : t.Finite), t.encard ≤ s.encard
rwa₁ : ∀ (h' : t.encard ≤ (↑s.ncard : ℕ∞)) (ht : t.Finite), t.encard ≤ s.encard
⊢ t.encard ≤ s.encard
have rwa₂ : ∀ (h' : t.encard ≤ s.encard) (ht : t.Finite), t.encard ≤ s.encard
Tactic: rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h'
Cleared hypotheses: h', ht
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.ncard < t.ncard
have rw : s.encard < t.encard
Tactic: rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
himage : s = f' '' univ
⊢ s.ncard = n
have rw : (f' '' univ).ncard = ncard (α := Fin n) univ
Tactic: rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]