awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
hs : ncard.{u_1} (α := α) ∅ ≠ 0
⊢ False

Tactic:
simp at hs
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
⊢ ncard (α := α) {a} = 1

Tactic:
simp [ncard]

Premises used: Set.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
rw : ({a} ∩ s).encard ≤ 1
⊢ ({a} ∩ s).ncard ≤ 1

Tactic:
rw [← Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one]

Premises used: Set.toFinite, Nat.cast_le, Set.Finite.cast_ncard_eq, Nat.cast_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1

Tactic:
apply encard_singleton_inter

Premises used: Set.encard_singleton_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).ncard = s.ncard * t.ncard

Tactic:
simp [ncard, ENat.toNat_mul]

Premises used: ENat.toNat_mul, Set.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 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
-- Module: Mathlib.Data.Set.Card
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 : 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

Premises used: Set.Finite.powerset, Set.cast_ncard
-- Module: Mathlib.Data.Set.Card
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})
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  ∀ (h : (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard), (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard
⊢ (𝒫 s).ncard = HPow.hPow (α := ℕ) 2 s.ncard

Tactic:
norm_cast at h
-- Module: Mathlib.Data.Set.Card
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
rw₅ rw₆ : s.encard + 1 = s.encard + 1
⊢ (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]

Premises used: Nat.cast_inj, Nat.cast_add, Set.Finite.insert, Set.encard_insert_of_notMem, Set.Finite.cast_ncard_eq, Nat.cast_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
rw rw₁ : s.ncard = s.ncard
⊢ (insert a s).ncard = s.ncard

Tactic:
rw [insert_eq_of_mem h]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
inl : ∀ (hs : s.Finite), (insert a s).ncard ≤ s.ncard + 1
inr : ∀ (hs : s.Infinite), (insert a s).ncard ≤ s.ncard + 1
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
obtain hs | hs := s.finite_or_infinite

Premises used: Set.finite_or_infinite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Finite
inl : (↑(insert a s).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Finite
inl : (insert a s).encard ≤ s.encard + 1
⊢ (↑(insert a s).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) 1

Tactic:
rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]

Premises used: Set.Finite.insert, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1

Tactic:
apply encard_insert_le

Premises used: Set.encard_insert_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Infinite
inr : 0 ≤ s.ncard + 1
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
rw [(hs.mono (subset_insert a s)).ncard]

Premises used: Set.Infinite.mono, Set.Infinite.ncard, Set.subset_insert
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).Finite

Tactic:
simp [hs]
-- Module: Mathlib.Data.Set.Card
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
neg : ∀ (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

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Set.Card
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
pos₁ pos₂ : s.ncard = s.ncard
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
rw [ncard_insert_of_mem h, if_pos h]

Premises used: if_pos, Set.ncard_insert_of_mem
-- Module: Mathlib.Data.Set.Card
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
neg₁ neg₂ : s.ncard + 1 = s.ncard + 1
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
rw [ncard_insert_of_notMem h hs, if_neg h]

Premises used: Set.ncard_insert_of_notMem, if_neg
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Infinite
rw : 0 ≤ (insert a s).ncard
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
rw [h.ncard]

Premises used: Set.Infinite.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
⊢ s.Finite

Tactic:
refine
    s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))

Premises used: Set.finite_or_infinite, Or.elim
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
rw : s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
rw [ncard_insert_eq_ite h]

Premises used: Set.ncard_insert_eq_ite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
pos : a ∈ s → s.ncard ≤ s.ncard
neg : a ∉ s → s.ncard ≤ s.ncard + 1
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Tactic:
split_ifs
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
h_1 : a ∈ s
⊢ s.ncard ≤ s.ncard

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : s.Finite
h_1 : a ∉ s
⊢ s.ncard ≤ s.ncard + 1

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
h : ∀ (h : s.Finite), s.ncard ≤ (insert a s).ncard
h₁ h₂ : ∀ (h : s.Finite), s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
⊢ 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

Premises used: Set.finite_or_infinite, Or.elim
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a b : α
h : a ≠ b
⊢ ncard (α := α) {a, b} = 2

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
to_encard_tac : HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = (↑s.ncard : ℕ∞)
⊢ (s \ {a}).ncard + 1 = s.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
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
rw₂ rw₃ : s.encard = s.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s \ {a}).ncard : ℕ∞) 1 = (↑s.ncard : ℕ∞)

Tactic:
rw [hs.cast_ncard_eq, hs.diff.cast_ncard_eq, encard_diff_singleton_add_one h]

Premises used: Set.Finite.diff, Set.encard_diff_singleton_add_one, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
inl : ∀ (hs : s.Infinite), (s \ {a}).ncard = s.ncard - 1
inr : ∀ (hs : s.Finite), (s \ {a}).ncard = s.ncard - 1
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
rcases s.infinite_or_finite with hs | hs

Premises used: Set.infinite_or_finite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Infinite
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
simp_all [ncard, Infinite.diff hs (finite_singleton a)]

Premises used: Set.ncard, Set.finite_singleton, Set.Infinite.diff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
eq_tsub_of_add_eq (ncard_diff_singleton_add_one h hs)

Premises used: Set.ncard_diff_singleton_add_one, eq_tsub_of_add_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
exact eq_tsub_of_add_eq (ncard_diff_singleton_add_one h hs)

Premises used: Set.ncard_diff_singleton_add_one, eq_tsub_of_add_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
rw : (s \ {a}).ncard < (s \ {a}).ncard + 1
⊢ (s \ {a}).ncard < s.ncard

Tactic:
rw [← ncard_diff_singleton_add_one h hs]

Premises used: Set.ncard_diff_singleton_add_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1

Tactic:
apply lt_add_one

Premises used: lt_add_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
inl : ∀ (hs : s.Finite), (s \ {a}).ncard ≤ s.ncard
inr : ∀ (hs : s.Infinite), (s \ {a}).ncard ≤ s.ncard
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
obtain hs | hs := s.finite_or_infinite

Premises used: Set.finite_or_infinite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
apply ncard_le_ncard diff_subset hs

Premises used: Set.diff_subset, Set.ncard_le_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ 0 ≤ s.ncard

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
hs : s.Infinite
h : (s \ {a}).ncard = 0
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
convert! Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ Set.Finite (α := α) {a}

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard = 0

Tactic:
exact (hs.diff (by simp)).ncard

Premises used: Set.Infinite.ncard, Set.Infinite.diff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
pos : ∀ (h : a ∈ s), s.ncard - 1 ≤ (s \ {a}).ncard
neg : ∀ (h : a ∉ s), s.ncard - 1 ≤ (s \ {a}).ncard
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
pos pos₁ : s.ncard - 1 ≤ s.ncard - 1
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
rw [ncard_diff_singleton_of_mem h]

Premises used: Set.ncard_diff_singleton_of_mem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
neg : s.ncard - 1 ≤ s.ncard
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
rw [diff_singleton_eq_self h]

Premises used: Set.diff_singleton_eq_self
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard

Tactic:
apply Nat.pred_le

Premises used: Nat.pred_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).ncard = s.ncard

Tactic:
congr_arg ENat.toNat <| encard_exchange ha hb

Premises used: Set.encard_exchange, congr_arg, ENat.toNat, Set.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
h : Membership.mem (γ := Set α) {a} b
rwa rwa₁ rwa₂ rwa₃ : b ∈ s
⊢ a ∈ s

Tactic:
rwa [← mem_singleton_iff.mp h]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Data.Set.Card
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
rw₄ rw₅ : ({a} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard
⊢ (insert a s \ {b}).ncard = s.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])]

Premises used: Set.diff_singleton_eq_self, Set.singleton_union, Set.union_diff_distrib, Set.ncard_exchange
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
rw : (Odd s.ncard ↔ Even (α := ℕ) 1) ↔ Even s.ncard
⊢ Odd (insert a s).ncard ↔ Even s.ncard

Tactic:
rw [ncard_insert_of_notMem ha hs, Nat.odd_add]

Premises used: Set.ncard_insert_of_notMem, Nat.odd_add
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ (Odd s.ncard ↔ Even (α := ℕ) 1) ↔ Even s.ncard

Tactic:
simp only [← Nat.not_even_iff_odd, Nat.not_even_one, iff_false, Decidable.not_not]

Premises used: iff_false, Nat.not_even_iff_odd, Nat.not_even_one, Decidable.not_not
-- Module: Mathlib.Data.Set.Card
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
rw₂ rw₃ : Odd s.ncard ↔ Odd s.ncard
⊢ Even (insert a s).ncard ↔ Odd s.ncard

Tactic:
rw [ncard_insert_of_notMem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]

Premises used: Nat.even_add_one, Nat.not_even_iff_odd, Set.ncard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
to_encard_tac : LE.le (α := ℕ∞) (↑(f '' s).ncard : ℕ∞) (↑s.ncard : ℕ∞)
⊢ (f '' s).ncard ≤ s.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
rw : (f '' s).encard ≤ s.encard
⊢ LE.le (α := ℕ∞) (↑(f '' s).ncard : ℕ∞) (↑s.ncard : ℕ∞)

Tactic:
rw [hs.cast_ncard_eq, (hs.image _).cast_ncard_eq]

Premises used: Set.Finite.image, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).encard ≤ s.encard

Tactic:
apply encard_image_le

Premises used: Set.encard_image_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
H : InjOn f s
⊢ (f '' s).ncard = s.ncard

Tactic:
congr_arg ENat.toNat <| H.encard_image

Premises used: congr_arg, Set.InjOn.encard_image, ENat.toNat, Set.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).ncard = s.ncard
hs : s.Finite
⊢ (f '' s).encard = s.encard

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h

Premises used: Set.Finite.image, Nat.cast_inj, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).ncard = s.ncard
hs : s.Finite
h₁ : (f '' s).encard = s.encard
⊢ s.Finite

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h

Premises used: Set.Finite.image, Nat.cast_inj, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s

Tactic:
hs.injOn_of_encard_image_eq h

Premises used: Set.Finite.injOn_of_encard_image_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s

Tactic:
exact hs.injOn_of_encard_image_eq h

Premises used: Set.Finite.injOn_of_encard_image_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).ncard = s.ncard ↔ InjOn f s

Tactic:
⟨fun h ↦ injOn_of_ncard_image_eq h hs, InjOn.ncard_image⟩

Premises used: Set.InjOn.ncard_image, Iff.intro, Set.injOn_of_ncard_image_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Function.Injective f
⊢ (f '' s).ncard = s.ncard

Tactic:
H.injOn.ncard_image

Premises used: Function.Injective.injOn, Set.InjOn.ncard_image
-- Module: Mathlib.Data.Set.Card
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
rw₁ rw₂ : s.ncard = s.ncard
⊢ (f ⁻¹' s).ncard = s.ncard

Tactic:
rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]

Premises used: Iff.mpr, Set.ncard_image_of_injective, Set.image_preimage_eq_iff
-- Module: Mathlib.Data.Set.Card
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

Tactic:
⟨nonempty_of_ncard_ne_zero, ?_⟩

Premises used: Set.nonempty_of_ncard_ne_zero, Iff.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : s.Finite
refine : y ∈ f '' s → ncard.{u_1} (α := α) {x : α | x ∈ s ∧ f x = y} ≠ 0
⊢ ncard.{u_1} (α := α) {x : α | x ∈ s ∧ f x = y} ≠ 0 ↔ y ∈ f '' s

Tactic:
refine ⟨nonempty_of_ncard_ne_zero, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
z : α
hz : z ∈ s
⊢ ncard.{u_1} (α := α) {x : α | x ∈ s ∧ f x = f z} ≠ 0

Tactic:
@ncard_ne_zero_of_mem _ ({ x ∈ s | f x = f z }) z (mem_sep hz rfl)
    (hs.subset (sep_subset _ _))

Premises used: Set.Finite.subset, Set.mem_sep, Set.sep_subset, Set.ncard_ne_zero_of_mem, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
z : α
hz : z ∈ s
⊢ ncard.{u_1} (α := α) {x : α | x ∈ s ∧ f x = f z} ≠ 0

Tactic:
exact @ncard_ne_zero_of_mem _ ({ x ∈ s | f x = f z }) z (mem_sep hz rfl)
    (hs.subset (sep_subset _ _))

Premises used: Set.Finite.subset, Set.mem_sep, Set.sep_subset, Set.ncard_ne_zero_of_mem, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α ↪ β
⊢ ncard.{u_2} (α := β) ((⇑f : (a : α) → β) '' s) = s.ncard

Tactic:
ncard_image_of_injective _ f.inj'

Premises used: Function.Embedding.inj', Set.ncard_image_of_injective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P : α → Prop
s : Set α
⊢ ncard.{u_1} (α := Subtype P) {x : Subtype P | (↑x : α) ∈ s} =
    ncard.{u_1} (α := α) ((fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s})

Tactic:
(ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm

Premises used: Subtype.coe_injective, Set.ncard_image_of_injective, Eq.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P : α → Prop
s : Set α
h : s ∩ setOf P = (fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}
⊢ ncard.{u_1} (α := Subtype P) {x : Subtype P | (↑x : α) ∈ s} = (s ∩ setOf P).ncard

Tactic:
convert! (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm

Premises used: Subtype.coe_injective, Set.ncard_image_of_injective, Eq.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P : α → Prop
s : Set α
h :
  ∀ (x : α),
    x ∈ s ∩ setOf P ↔ Membership.mem (γ := Set α) ((fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}) x
⊢ s ∩ setOf P = (fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}

Tactic:
ext x
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ setOf P ↔ Membership.mem (γ := Set α) ((fun (a : Subtype P) ↦ (↑a : α)) '' {x : Subtype P | (↑x : α) ∈ s}) x

Tactic:
simp [← and_assoc, exists_eq_right]

Premises used: exists_eq_right, and_assoc
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ (s ∩ t).ncard ≤ s.ncard

Tactic:
ncard_le_ncard inter_subset_left hs

Premises used: Set.inter_subset_left, Set.ncard_le_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
⊢ (s ∩ t).ncard ≤ t.ncard

Tactic:
ncard_le_ncard inter_subset_right ht

Premises used: Set.ncard_le_ncard, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Card
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h' : t.encard ≤ s.encard) (ht : t.Finite), t.encard ≤ s.encard
⊢ t.encard ≤ s.encard

Tactic:
rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h'

Premises used: Set.Finite.subset, Nat.cast_le, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : t.ncard ≤ s.ncard
ht : t.Finite
⊢ s ⊆ t ↔ s = t

Tactic:
⟨fun hst ↦ eq_of_subset_of_ncard_le hst h ht, Eq.subset⟩

Premises used: Eq.subset, Iff.intro, Set.eq_of_subset_of_ncard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
f : α ↪ α
h : (⇑f : (a : α) → α) '' s ⊆ s
hs : s.Finite
⊢ (⇑f : (a : α) → α) '' s = s

Tactic:
eq_of_subset_of_ncard_le h (ncard_map _).ge hs

Premises used: Eq.ge, Set.ncard_map, Set.eq_of_subset_of_ncard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
P : α → Prop
h : ncard.{u_1} (α := α) {x : α | x ∈ s ∧ P x} = s.ncard
ha : a ∈ s
hs : s.Finite
⊢ {x : α | x ∈ s ∧ P x} ⊆ s

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
rw : s.encard < t.encard
⊢ s.ncard < t.ncard

Tactic:
rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]

Premises used: HasSSubset.SSubset.subset, Set.Finite.subset, Nat.cast_lt, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.encard < t.encard

Tactic:
(ht.subset h.subset).encard_lt_encard h

Premises used: Set.Finite.encard_lt_encard, HasSSubset.SSubset.subset, Set.Finite.subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.encard < t.encard

Tactic:
exact (ht.subset h.subset).encard_lt_encard h

Premises used: Set.Finite.encard_lt_encard, HasSSubset.SSubset.subset, Set.Finite.subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Finite α
h : s ≠ univ
⊢ s.ncard < Nat.card α

Tactic:
ncard_univ α ▸ ncard_lt_ncard (ssubset_univ_iff.mpr h)

Premises used: Iff.mpr, Eq.rec, Set.ncard_lt_ncard, Set.ssubset_univ_iff, Set.ncard_univ
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
⊢ StrictMono.{u_1, 0} (α := Set α) ncard

Tactic:
fun _ _ h ↦ ncard_lt_ncard h

Premises used: StrictMono, Set.ncard_lt_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
⊢ StrictMonoOn.{u_1, 0} (α := Set α) ncard (setOf Set.Finite)

Tactic:
fun _ _ _ ht hlt ↦ ncard_lt_ncard hlt.ssubset ht

Premises used: LT.lt.ssubset, Set.ncard_lt_ncard, StrictMonoOn
-- Module: Mathlib.Data.Set.Card
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
rw : (f' '' univ).ncard = ncard (α := Fin n) univ
⊢ s.ncard = n

Tactic:
rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]

Premises used: Fintype.card_fin, Set.ncard_univ, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Set.Card
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
⊢ (f' '' univ).ncard = ncard (α := Fin n) univ

Tactic:
InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h

Premises used: Fin.is_lt, Fin.ext, Fin.val, Set.InjOn.ncard_image