awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ ENat.card.{u_1} (↑(s ∪ t) : Type u_1) = ENat.card.{u_1} (↑s : Type u_1) + ENat.card.{u_1} (↑t : Type u_1)

Tactic:
simp [ENat.card_congr (Equiv.Set.union h)]

Premises used: ENat.card_congr, Equiv.Set.union
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
⊢ a ∉ {x : α | x ≠ a}

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
⊢ Disjoint (α := Set α) {x : α | x ≠ a} {a}

Tactic:
have : Disjoint {x | x ≠ a} {a} := disjoint_singleton_right.mpr <| by simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
this : Disjoint (α := Set α) {x : α | x ≠ a} {a}
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})

Tactic:
replace this := (Set.encard_union_eq this).symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
h : ∀ (x : α), Membership.mem (γ := Set α) ({x : α | x ≠ a} ∪ {a}) x ↔ Membership.mem (γ := Set α) univ x
⊢ Eq (α := Set α) ({x : α | x ≠ a} ∪ {a}) univ

Tactic:
ext x
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
this : encard.{u_1} (α := α) {x : α | x ≠ a} + encard (α := α) {a} = encard (α := α) ({x : α | x ≠ a} ∪ {a})
x : α
⊢ Membership.mem (γ := Set α) ({x : α | x ≠ a} ∪ {a}) x ↔ Membership.mem (γ := Set α) univ x

Tactic:
simp [eq_or_ne x a]

Premises used: eq_or_ne
-- Module: Mathlib.Data.Set.Card
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

Tactic:
have aux : {x | x ≠ a} ∪ {a} = univ := by ext x; simp [eq_or_ne x a]
-- Module: Mathlib.Data.Set.Card
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 α
rwa₂ rwa₃ rwa₄ 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 α
⊢ encard.{u_1} (α := α) {x : α | x ≠ a} + 1 = ENat.card α

Tactic:
rwa [encard_singleton, aux, encard_univ] at this

Premises used: Set.encard_univ, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ Disjoint s {a}

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
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
rw₂ rw₃ : s.encard + 1 = s.encard + 1
⊢ (insert a s).encard = s.encard + 1

Tactic:
rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]

Premises used: Set.encard_union_eq, Set.union_singleton, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ encard.{u_1} (α := α) ∅ < ⊤

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
s_1 : Set α
hat : a ∉ s_1
hs : s_1.Finite
ht' : s_1.encard < ⊤
insert : s_1.encard + 1 < ⊤
⊢ (Insert.insert a s_1).encard < ⊤

Tactic:
rw [encard_insert_of_notMem hat]

Premises used: Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
s_1 : Set α
hat : a ∉ s_1
hs : s_1.Finite
ht' : s_1.encard < ⊤
⊢ s_1.encard + 1 < ⊤

Tactic:
lt_tsub_iff_right.1 ht'

Premises used: lt_tsub_iff_right, Iff.mp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
s_1 : Set α
hat : a ∉ s_1
hs : s_1.Finite
ht' : s_1.encard < ⊤
⊢ s_1.encard + 1 < ⊤

Tactic:
exact lt_tsub_iff_right.1 ht'

Premises used: lt_tsub_iff_right, Iff.mp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Finite
empty : encard.{u_1} (α := α) ∅ < ⊤
insert : ∀ {a : α} {s : Set α} (hat : a ∉ s), s.Finite → ∀ (ht' : s.encard < ⊤), (Insert.insert a s).encard < ⊤
⊢ 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'

Premises used: Insert.insert
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard = (↑s.encard.toNat : ℕ∞)

Tactic:
(ENat.coe_toNat h.encard_lt_top.ne).symm

Premises used: Set.Finite.encard_lt_top, ENat.coe_toNat, Eq.symm, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Finite
⊢ ∃ (n : ℕ), s.encard = (↑n : ℕ∞)

Tactic:
⟨_, h.encard_eq_coe⟩

Premises used: Set.Finite.encard_eq_coe, Exists.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard < ⊤ ↔ s.Finite

Tactic:
⟨fun h ↦ by_contra fun h' ↦ h.ne (Infinite.encard_eq h'), Finite.encard_lt_top⟩

Premises used: Set.Finite.encard_lt_top, Set.Infinite.encard_eq, Iff.intro, by_contra, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
contrapose! : s.encard ≠ ⊤ ↔ s.Finite
⊢ s.encard = ⊤ ↔ s.Infinite

Tactic:
contrapose!
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : s.encard < ⊤ ↔ s.Finite
rw₁ rw₂ : s.Finite ↔ s.Finite
⊢ s.encard ≠ ⊤ ↔ s.Finite

Tactic:
rw [← lt_top_iff_ne_top, encard_lt_top_iff]

Premises used: Set.encard_lt_top_iff, lt_top_iff_ne_top
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≠ ⊤ ↔ s.Finite

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ (↑k : ℕ∞)
rw : s.encard < ⊤
⊢ s.Finite

Tactic:
rw [← encard_lt_top_iff]

Premises used: Set.encard_lt_top_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ (↑k : ℕ∞)
⊢ s.encard < ⊤

Tactic:
h.trans_lt (WithTop.coe_lt_top _)

Premises used: WithTop.coe_lt_top, LE.le.trans_lt
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ (↑k : ℕ∞)
⊢ s.encard < ⊤

Tactic:
exact h.trans_lt (WithTop.coe_lt_top _)

Premises used: WithTop.coe_lt_top, LE.le.trans_lt
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard = (↑k : ℕ∞)
⊢ s.Finite

Tactic:
finite_of_encard_le_coe h.le

Premises used: Eq.le, Set.finite_of_encard_le_coe
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ (↑k : ℕ∞)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k), ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k
⊢ ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k

Tactic:
rwa [ENat.le_coe_iff] at h

Premises used: ENat.le_coe_iff
-- Module: Mathlib.Data.Set.Card
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
rwa : LE.le (α := ℕ∞) (↑n₀ : ℕ∞) (↑k : ℕ∞)
rwa₁ rwa₂ rwa₃ rwa₄ : n₀ ≤ k
⊢ s.encard ≤ (↑k : ℕ∞)

Tactic:
rwa [hs, Nat.cast_le]

Premises used: Nat.cast_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ENat.card (↑(s ×ˢ t) : Type (max u_1 u_2)) = ENat.card.{u_1} (↑s : Type u_1) * ENat.card.{u_2} (↑t : Type u_2)

Tactic:
simp [ENat.card_congr (Equiv.Set.prod ..)]

Premises used: ENat.card_congr, Equiv.Set.prod
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
h : Fintype α
ι : α → Type u_3
s : (i : α) → Set (ι i)
⊢ Eq (α := ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{max u_1 u_3}) → ℕ∞) (Cardinal.mk (↑(pi (α := ι) univ s) : Type (max u_1 u_3))) :
      ℕ∞)
    (∏ i : α, (Cardinal.toENat : (a : Cardinal.{u_3}) → ℕ∞) (Cardinal.mk (↑(s i) : Type u_3)) : ℕ∞)

Tactic:
simp [Cardinal.mk_congr (Equiv.Set.univPi s), Cardinal.prod_eq_of_fintype]

Premises used: Equiv.Set.univPi, Cardinal.prod_eq_of_fintype, Cardinal.mk_congr
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
rw : s.encard ≤ s.encard + (t \ s).encard
⊢ s.encard ≤ t.encard

Tactic:
rw [← union_diff_cancel h, encard_union_eq disjoint_sdiff_right]

Premises used: Set.encard_union_eq, Set.union_diff_cancel, Set.disjoint_sdiff_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ ENat.card α

Tactic:
encard_univ _ ▸ encard_le_encard s.subset_univ

Premises used: Set.subset_univ, Eq.rec, Set.encard_univ, Set.encard_le_encard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
⊢ Monotone.{u_3, 0} (α := Set α) encard

Tactic:
fun _ _ ↦ encard_le_encard

Premises used: Monotone, Set.encard_le_encard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
rw : (t \ s ∪ s).encard = t.encard
rw₁ rw₂ : t.encard = t.encard
⊢ (t \ s).encard + s.encard = t.encard

Tactic:
rw [← encard_union_eq disjoint_sdiff_left, diff_union_of_subset h]

Premises used: Set.encard_union_eq, Set.disjoint_sdiff_left, Set.diff_union_of_subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
rw : (t \ s).encard = (t \ s).encard + s.encard - s.encard
⊢ (t \ s).encard = t.encard - s.encard

Tactic:
rw [← @Set.encard_diff_add_encard_of_subset _ s t h]

Premises used: Set.encard_diff_add_encard_of_subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = (t \ s).encard + s.encard - s.encard

Tactic:
(ENat.addLECancellable_of_ne_top <| encard_ne_top_iff.mpr hs).eq_tsub_of_add_eq rfl

Premises used: Iff.mpr, AddLECancellable.eq_tsub_of_add_eq, ENat.addLECancellable_of_ne_top, Set.encard_ne_top_iff, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = (t \ s).encard + s.encard - s.encard

Tactic:
exact (ENat.addLECancellable_of_ne_top <| encard_ne_top_iff.mpr hs).eq_tsub_of_add_eq rfl

Premises used: Iff.mpr, AddLECancellable.eq_tsub_of_add_eq, ENat.addLECancellable_of_ne_top, Set.encard_ne_top_iff, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : 1 ≤ s.encard ↔ s ≠ ∅
rw₁ : 1 ≤ s.encard ↔ ¬s = ∅
rw₂ : 1 ≤ s.encard ↔ ¬s.encard = 0
rw₃ rw₄ : s.encard ≠ 0 ↔ ¬s.encard = 0
⊢ 1 ≤ s.encard ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]

Premises used: Set.encard_eq_zero, Ne, Set.nonempty_iff_ne_empty, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard < 1 ↔ s = ∅

Tactic:
simp [← not_le, not_nonempty_iff_eq_empty]

Premises used: not_le, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
rw : (s \ t ∪ s ∩ t).encard = s.encard
rw₁ rw₂ : s.encard = s.encard
⊢ (s \ t).encard + (s ∩ t).encard = s.encard

Tactic:
rw [← encard_union_eq disjoint_sdiff_inter, diff_union_inter]

Premises used: Set.encard_union_eq, Set.disjoint_sdiff_inter, Set.diff_union_inter
-- Module: Mathlib.Data.Set.Card
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
rw₃ rw₄ : s.encard + t.encard = s.encard + t.encard
⊢ (s ∪ 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]

Premises used: Set.encard_union_eq, Set.diff_union_self, add_right_comm, Set.disjoint_sdiff_left, Set.encard_diff_add_encard_inter
-- Module: Mathlib.Data.Set.Card
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
rw₃ rw₄ : (s \ t).encard = (t \ s).encard ↔ (s \ t).encard = (t \ s).encard
⊢ s.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]

Premises used: Set.Finite.encard_lt_top, WithTop.add_right_inj, Set.inter_comm, Set.encard_diff_add_encard_inter, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
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
rw₃ rw₄ : (s \ t).encard ≤ (t \ s).encard ↔ (s \ t).encard ≤ (t \ s).encard
⊢ s.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]

Premises used: Set.Finite.encard_lt_top, Set.inter_comm, Set.encard_diff_add_encard_inter, LT.lt.ne, WithTop.add_le_add_iff_right
-- Module: Mathlib.Data.Set.Card
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
rw₃ rw₄ : (s \ t).encard < (t \ s).encard ↔ (s \ t).encard < (t \ s).encard
⊢ s.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]

Premises used: Set.Finite.encard_lt_top, Set.inter_comm, WithTop.add_lt_add_iff_right, Set.encard_diff_add_encard_inter, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
rw : (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
rw [← encard_union_add_encard_inter]

Premises used: Set.encard_union_add_encard_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
rw : s.encard < ⊤ ↔ t.Finite
rw₁ : s.encard < ⊤ ↔ t.encard < ⊤
rw₂ rw₃ : t.encard < ⊤ ↔ t.encard < ⊤
⊢ s.Finite ↔ t.Finite

Tactic:
rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]

Premises used: Set.encard_lt_top_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.encard = t.encard
rw : s.encard = ⊤ ↔ t.Infinite
rw₁ : t.encard = ⊤ ↔ t.Infinite
rw₂ rw₃ : t.Infinite ↔ t.Infinite
⊢ s.Infinite ↔ t.Infinite

Tactic:
rw [← encard_eq_top_iff, h, encard_eq_top_iff]

Premises used: Set.encard_eq_top_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
h : t.encard ≤ s.encard
⊢ t.Finite

Tactic:
encard_lt_top_iff.1 (h.trans_lt hs.encard_lt_top)

Premises used: Set.Finite.encard_lt_top, Set.encard_lt_top_iff, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : t.encard ≤ s.encard
⊢ (t \ s).encard + s.encard ≤ 0 + s.encard

Tactic:
rw [← zero_add (a := encard s), ← encard_diff_add_encard_of_subset hst] at hts

Premises used: Set.encard, Set.encard_diff_add_encard_of_subset, zero_add
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ (t \ s).encard ≤ 0

Tactic:
have hdiff := WithTop.le_of_add_le_add_right (ht.subset hst).encard_lt_top.ne hts
-- Module: Mathlib.Data.Set.Card
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
⊢ t ⊆ s

Tactic:
rw [nonpos_iff_eq_zero, encard_eq_zero, diff_eq_empty] at hdiff

Premises used: Set.encard_eq_zero, Set.diff_eq_empty, nonpos_iff_eq_zero
-- Module: Mathlib.Data.Set.Card
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
⊢ s = t

Tactic:
hst.antisymm hdiff

Premises used: HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Set.Card
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
⊢ s = t

Tactic:
exact hst.antisymm hdiff

Premises used: HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hst : s ⊆ t
hts : t.encard ≤ s.encard
⊢ s = t

Tactic:
(hs.finite_of_encard_le hts).eq_of_subset_of_encard_le' hst hts

Premises used: Set.Finite.eq_of_subset_of_encard_le', Set.Finite.finite_of_encard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊂ t
⊢ s.encard < t.encard

Tactic:
(encard_mono h.subset).lt_of_ne fun he ↦ h.ne (hs.eq_of_subset_of_encard_le h.subset he.symm.le)

Premises used: Eq.le, HasSSubset.SSubset.subset, LE.le.lt_of_ne, Set.encard_mono, HasSSubset.SSubset.ne, Eq.symm, Set.Finite.eq_of_subset_of_encard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
⊢ StrictMono.{u_1, 0} (α := Set α) encard

Tactic:
fun _ _ h ↦ (toFinite _).encard_lt_encard h

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

Tactic:
fun _ hs _ _ hlt ↦ hs.encard_lt_encard hlt.ssubset

Premises used: Set.Finite.encard_lt_encard, LT.lt.ssubset, StrictMonoOn
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hfin : s.Finite
hne : s ≠ univ
⊢ s.encard < ENat.card α

Tactic:
encard_univ α ▸ hfin.encard_lt_encard (ssubset_univ_iff.mpr hne)

Premises used: Iff.mpr, Eq.rec, Set.Finite.encard_lt_encard, Set.encard_univ, Set.ssubset_univ_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
rw : (s \ t ∪ t).encard = (s ∪ t).encard
rw₁ rw₂ : (s ∪ t).encard = (s ∪ t).encard
⊢ (s \ t).encard + t.encard = (s ∪ t).encard

Tactic:
rw [← encard_union_eq disjoint_sdiff_left, diff_union_self]

Premises used: Set.encard_union_eq, Set.diff_union_self, Set.disjoint_sdiff_left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
⊢ s.encard ≤ (s \ t).encard + t.encard

Tactic:
(encard_mono subset_union_left).trans_eq (encard_diff_add_encard _ _).symm

Premises used: Set.encard_diff_add_encard, LE.le.trans_eq, Set.subset_union_left, Set.encard_mono, Eq.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
rw : s.encard ≤ (s \ t).encard + t.encard
⊢ s.encard - t.encard ≤ (s \ t).encard

Tactic:
rw [tsub_le_iff_left, add_comm]

Premises used: tsub_le_iff_left, add_comm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
⊢ s.encard ≤ (s \ t).encard + t.encard

Tactic:
apply encard_le_encard_diff_add_encard

Premises used: Set.encard_le_encard_diff_add_encard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : (s ∪ sᶜ).encard = encard.{u_1} (α := α) univ
rw₁ rw₂ : encard.{u_1} (α := α) univ = encard.{u_1} (α := α) univ
⊢ s.encard + sᶜ.encard = encard.{u_1} (α := α) univ

Tactic:
rw [← encard_union_eq disjoint_compl_right, union_compl_self]

Premises used: Set.encard_union_eq, Set.union_compl_self, disjoint_compl_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
rw : (s ∪ {x}).encard ≤ s.encard + encard (α := α) {x}
⊢ (insert x s).encard ≤ s.encard + 1

Tactic:
rw [← union_singleton, ← encard_singleton x]

Premises used: Set.union_singleton, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + encard (α := α) {x}

Tactic:
apply encard_union_le

Premises used: Set.encard_union_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
s : Set α
⊢ 1 ≤ (insert a s).encard

Tactic:
ENat.one_le_iff_ne_zero.mpr <| encard_ne_zero_of_mem (mem_insert a s)

Premises used: Iff.mpr, Set.encard_ne_zero_of_mem, Set.mem_insert, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
grw : ({x} ∩ s).encard ≤ encard (α := α) {x}
grw₁ grw₂ : encard (α := α) {x} ≤ encard (α := α) {x}
⊢ ({x} ∩ s).encard ≤ 1

Tactic:
grw [← encard_singleton x, inter_subset_left]

Premises used: Set.inter_subset_left, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
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
rw₂ rw₃ : s.encard = s.encard
⊢ (s \ {a}).encard + 1 = s.encard

Tactic:
rw [← encard_insert_of_notMem (fun h ↦ h.2 rfl), insert_diff_singleton, insert_eq_of_mem h]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
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
rw₂ rw₃ : (s \ {a}).encard + 1 = (s \ {a}).encard + 1
⊢ (s \ {a}).encard = s.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 _ _)]

Premises used: WithTop.one_ne_top, self_le_add_left, tsub_add_cancel_of_le, WithTop.add_right_inj, Set.encard_diff_singleton_add_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
rw : s.encard - encard (α := α) {x} ≤ (s \ {x}).encard
⊢ s.encard - 1 ≤ (s \ {x}).encard

Tactic:
rw [← encard_singleton x]

Premises used: Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
⊢ s.encard - encard (α := α) {x} ≤ (s \ {x}).encard

Tactic:
apply tsub_encard_le_encard_diff

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

Tactic:
rw [encard_insert_of_notMem, encard_diff_singleton_add_one hb]

Premises used: Set.encard_diff_singleton_add_one, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ∉ s \ {b}

Tactic:
simp_all only [mem_diff, mem_singleton_iff, false_and, not_false_eq_true]

Premises used: false_and, Set.mem_singleton_iff, Set.mem_diff, not_false_eq_true
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False

Tactic:
ha hb
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False

Tactic:
exact ha hb
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
rw : (insert a (s \ {b})).encard = s.encard
rw₁ rw₂ : s.encard = s.encard
⊢ (insert a s \ {b}).encard = s.encard

Tactic:
rw [← insert_diff_singleton_comm (by rintro rfl; exact ha hb), encard_exchange ha hb]

Premises used: Set.encard_exchange, Set.insert_diff_singleton_comm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
⊢ s.encard = k + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Card
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
refine_2 : (∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k) → s.encard = k + 1
⊢ s.encard = k + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ s.encard ≠ 0

Tactic:
simp [h]