awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
inl : ∀ (ht : t.Finite), (t \ s).ncard = t.ncard - s.ncard
inr : ∀ (ht : t.Infinite), (t \ s).ncard = t.ncard - s.ncard
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
obtain ht | ht := t.finite_or_infinite

Premises used: Set.finite_or_infinite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Finite
inl : (t \ s).ncard = (t \ s).ncard + s.ncard - s.ncard
inl₁ inl₂ : (t \ s).ncard = (t \ s).ncard
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
rw [← ncard_diff_add_ncard_of_subset hst ht, add_tsub_cancel_right]

Premises used: Set.ncard_diff_add_ncard_of_subset, add_tsub_cancel_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
inr : (t \ s).ncard = 0 - s.ncard
inr₁ : (t \ s).ncard = 0
inr₂ inr₃ : Eq (α := ℕ) 0 0
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
rw [ht.ncard, Nat.zero_sub, (ht.diff hs).ncard]

Premises used: Set.Infinite.ncard, Nat.zero_sub, Set.Infinite.diff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
R : Type u_3
inst : AddGroupWithOne R
hst : s ⊆ t
ht : t.Finite
rw : (↑(t.ncard - s.ncard) : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
rw₁ rw₂ : HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
⊢ (↑(t \ s).ncard : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)

Tactic:
rw [ncard_diff hst (ht.subset hst), Nat.cast_sub (ncard_le_ncard hst ht)]

Premises used: Nat.cast_sub, Set.Finite.subset, Set.ncard_diff, Set.ncard_le_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
inl : ∀ (hs : s.Finite), s.ncard ≤ (s \ t).ncard + t.ncard
inr : ∀ (hs : s.Infinite), s.ncard ≤ (s \ t).ncard + t.ncard
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Tactic:
rcases s.finite_or_infinite with hs | hs

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

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

Tactic:
rw [ht.cast_ncard_eq, hs.cast_ncard_eq, hs.diff.cast_ncard_eq]

Premises used: Set.Finite.diff, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ 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 t : Set α
ht : t.Finite
hs : s.Infinite
⊢ 0 ≤ (s \ t).ncard + t.ncard

Tactic:
Nat.zero_le _

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

Tactic:
convert! Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
h h₁ : Eq (α := ℕ) 0 0
⊢ s.ncard = 0

Tactic:
rw [hs.ncard]

Premises used: Set.Infinite.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
rw : t.ncard ≤ (t \ s).ncard + s.ncard
⊢ t.ncard ≤ s.ncard + (t \ s).ncard

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ (t \ s).ncard + s.ncard

Tactic:
apply ncard_le_ncard_diff_add_ncard _ _ hs

Premises used: Set.ncard_le_ncard_diff_add_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s \ t ∪ t).ncard = (s ∪ t).ncard
rw₁ rw₂ : (s ∪ t).ncard = (s ∪ t).ncard
⊢ (s \ t).ncard + t.ncard = (s ∪ t).ncard

Tactic:
rw [← ncard_union_eq disjoint_sdiff_left hs.diff ht, diff_union_self]

Premises used: Set.ncard_union_eq, Set.diff_union_self, Set.Finite.diff, Set.disjoint_sdiff_left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
rw : ¬t ⊆ s
⊢ (t \ s).Nonempty

Tactic:
rw [Set.nonempty_iff_ne_empty, Ne, diff_eq_empty]

Premises used: Ne, Set.nonempty_iff_ne_empty, Set.diff_eq_empty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t ⊆ s

Tactic:
fun h' ↦ h.not_ge (ncard_le_ncard h' hs)

Premises used: LT.lt.not_ge, Set.ncard_le_ncard, Not
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t ⊆ s

Tactic:
exact fun h' ↦ h.not_ge (ncard_le_ncard h' hs)

Premises used: LT.lt.not_ge, Set.ncard_le_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ∃ e ∈ t, e ∉ s

Tactic:
diff_nonempty_of_ncard_lt_ncard h hs

Premises used: Set.diff_nonempty_of_ncard_lt_ncard, Set.Mem, Set.diff, setOf, Set.Nonempty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
rw : (s ∩ t ∪ s \ t).ncard = s.ncard
rw₁ : (s \ t ∪ s ∩ t).ncard = s.ncard
rw₂ rw₃ : s.ncard = s.ncard
⊢ (s ∩ t).ncard + (s \ t).ncard = s.ncard

Tactic:
rw [← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
    (hs.inter_of_left _) hs.diff, union_comm, diff_union_inter]

Premises used: Set.Finite.inter_of_left, Set.disjoint_of_subset_left, Set.ncard_union_eq, Set.union_comm, Set.Finite.diff, Set.disjoint_sdiff_right, Set.diff_union_inter, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
rw₂ : (t ∩ s).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
rw₃ rw₄ : (s \ t).ncard = (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_right_inj]

Premises used: Set.ncard_inter_add_ncard_diff_eq_ncard, Set.inter_comm, add_right_inj
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
rw₂ : (t ∩ s).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
rw₃ rw₄ : (s \ t).ncard ≤ (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]

Premises used: add_le_add_iff_left, Set.ncard_inter_add_ncard_diff_eq_ncard, Set.inter_comm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
rw₂ : (t ∩ s).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
rw₃ rw₄ : (s \ t).ncard < (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]

Premises used: Set.ncard_inter_add_ncard_diff_eq_ncard, Set.inter_comm, add_lt_add_iff_left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
rw : s.ncard + sᶜ.ncard = ncard.{u_1} (α := α) univ
rw₁ : (s ∪ sᶜ).ncard = ncard.{u_1} (α := α) univ
rw₂ rw₃ : ncard.{u_1} (α := α) univ = ncard.{u_1} (α := α) univ
⊢ s.ncard + sᶜ.ncard = Nat.card α

Tactic:
rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]

Premises used: Set.ncard_union_eq, Set.union_compl_self, disjoint_compl_right, Set.ncard_univ
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
rw : sᶜ.ncard = s.ncard + sᶜ.ncard - s.ncard
rw₁ rw₂ : sᶜ.ncard = sᶜ.ncard
⊢ sᶜ.ncard = Nat.card α - s.ncard

Tactic:
rw [← ncard_add_ncard_compl s hs hsc, Nat.add_sub_cancel_left]

Premises used: Nat.add_sub_cancel_left, Set.ncard_add_ncard_compl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
s : Set α
rw : sᶜ = ∅ ↔ s.ncard = Nat.card α
rw₁ : sᶜ.ncard = 0 ↔ s.ncard = Nat.card α
rw₂ : sᶜ.ncard = 0 ↔ s.ncard = s.ncard + sᶜ.ncard
rw₃ rw₄ : sᶜ.ncard = 0 ↔ sᶜ.ncard = 0
⊢ s = univ ↔ s.ncard = Nat.card α

Tactic:
rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]

Premises used: left_eq_add, Set.ncard_add_ncard_compl, Set.ncard_eq_zero, Set.compl_empty_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
rwa : Even s.ncard ↔ Even sᶜ.ncard
rwa₁ : Even (s.ncard + sᶜ.ncard)
rwa₂ rwa₃ rwa₄ rwa₅ : Even (Nat.card α)
⊢ Even sᶜ.ncard ↔ Even s.ncard

Tactic:
rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]

Premises used: iff_comm, Nat.even_add, Set.ncard_add_ncard_compl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
rw : ¬Even sᶜ.ncard ↔ Odd s.ncard
rw₁ : ¬Even s.ncard ↔ Odd s.ncard
rw₂ rw₃ : Odd s.ncard ↔ Odd s.ncard
⊢ Odd sᶜ.ncard ↔ Odd s.ncard

Tactic:
rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]

Premises used: Set.even_ncard_compl_iff, Nat.not_even_iff_odd
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : Nat.card α < s.ncard + t.ncard
⊢ Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard

Tactic:
rw [← ncard_union_add_ncard_inter s t] at h

Premises used: Set.ncard_union_add_ncard_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard

Tactic:
replace h := (s ∪ t).ncard_le_card.trans_lt h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
rwa : ∀ (h : 0 < (s ∩ t).ncard), (s ∩ t).Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : (s ∩ t).Nonempty), (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty

Tactic:
rwa [lt_add_iff_pos_right, ncard_pos] at h

Premises used: lt_add_iff_pos_right, Set.ncard_pos
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ s.ncard + t.ncard
h : s ∪ t ≠ univ
⊢ Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard

Tactic:
rw [← ncard_union_add_ncard_inter s t] at h'

Premises used: Set.ncard_union_add_ncard_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ s.ncard + t.ncard
h : s ∪ t ≠ univ
h'₁ : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
⊢ s ∪ t ≠ univ

Tactic:
rw [← ncard_union_add_ncard_inter s t] at h'

Premises used: Set.ncard_union_add_ncard_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : s ∪ t ≠ univ
⊢ (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard

Tactic:
replace h := (ncard_lt_card h).trans_le h'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
rwa : ∀ (h : 0 < (s ∩ t).ncard), (s ∩ t).Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : (s ∩ t).Nonempty), (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty

Tactic:
rwa [lt_add_iff_pos_right, ncard_pos] at h

Premises used: lt_add_iff_pos_right, Set.ncard_pos
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
contrapose! : ∀ (h : s ∪ t = univ), Nat.card α ≤ s.ncard + t.ncard
⊢ s ∪ t ≠ univ

Tactic:
contrapose! h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ∪ t = univ
rw : (s ∪ t).ncard ≤ s.ncard + t.ncard
⊢ Nat.card α ≤ s.ncard + t.ncard

Tactic:
rw [← ncard_univ, ← h]

Premises used: Set.ncard_univ
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
ncard_union_le s t

Premises used: Set.ncard_union_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
exact ncard_union_le s t

Premises used: Set.ncard_union_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
rw : s ∪ t ≠ univ
⊢ (sᶜ ∩ tᶜ).Nonempty

Tactic:
rw [← compl_union, nonempty_compl]

Premises used: Set.compl_union, Set.nonempty_compl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ

Tactic:
union_ne_univ_of_ncard_add_ncard_lt h

Premises used: Set.union_ne_univ_of_ncard_add_ncard_lt
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ

Tactic:
exact union_ne_univ_of_ncard_add_ncard_lt h

Premises used: Set.union_ne_univ_of_ncard_add_ncard_lt
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
inl : ∀ (ht : t.Infinite), ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
inr : ∀ (ht : t.Finite), ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
obtain ht | ht := t.infinite_or_finite

Premises used: Set.infinite_or_finite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
⊢ n = t.ncard

Tactic:
rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt

Premises used: Set.Infinite.ncard, Nat.le_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
hnt₁ : n = t.ncard
⊢ t.Infinite

Tactic:
rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt

Premises used: Set.Infinite.ncard, Nat.le_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n = t.ncard
ht : t.Infinite
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
⟨t, hst, Subset.rfl, hnt.symm⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n = t.ncard
ht : t.Infinite
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
exact ⟨t, hst, Subset.rfl, hnt.symm⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ s.Finite

Tactic:
ht.subset hst

Premises used: Set.Finite.subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
inr :
  ∀ (s : Finset α) (hst : (↑s : Set α) ⊆ t) (hsn : (↑s : Set α).ncard ≤ n),
    ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ t ∧ u.ncard = n
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
lift s to Finset α using ht.subset hst

Premises used: Finset, Set.Finite.subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : (↑s : Set α) ⊆ t
hsn : (↑s : Set α).ncard ≤ n
⊢ t.Finite

Tactic:
ht
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : (↑s : Set α) ⊆ t
hsn : (↑s : Set α).ncard ≤ n
inr :
  ∀ (t : Finset α) (hnt : n ≤ (↑t : Set α).ncard) (hst : (↑s : Set α) ⊆ (↑t : Set α)),
    ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n
⊢ ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
lift t to Finset α using ht

Premises used: Finset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s : Set α).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t : Set α).ncard
hst : (↑s : Set α) ⊆ (↑t : Set α)
⊢ s.card ≤ n

Tactic:
simpa using hsn
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s : Set α).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t : Set α).ncard
hst : (↑s : Set α) ⊆ (↑t : Set α)
inr :
  ∀ (u : Finset α) (hsu : s ⊆ u) (hut : u ⊆ t) (hu : u.card = n),
    ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n
⊢ ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n

Tactic:
obtain ⟨u, hsu, hut, hu⟩ := Finset.exists_subsuperset_card_eq (mod_cast hst) (by simpa using hsn)
    (mod_cast hnt)

Premises used: Finset.exists_subsuperset_card_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s : Set α).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t : Set α).ncard
hst : (↑s : Set α) ⊆ (↑t : Set α)
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : u.card = n
⊢ ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n

Tactic:
⟨u, mod_cast hsu, mod_cast hut, mod_cast hu⟩

Premises used: SetLike.coe_subset_coe._simp_1, congrArg, cast, SetLike.coe, And.intro, Exists.intro, congrFun', Eq.symm, Eq, Set.ncard_coe_finset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s : Set α).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t : Set α).ncard
hst : (↑s : Set α) ⊆ (↑t : Set α)
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : u.card = n
⊢ ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n

Tactic:
exact ⟨u, mod_cast hsu, mod_cast hut, mod_cast hu⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ncard.{u_1} (α := α) ∅ ≤ n

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∃ t ⊆ s, t.ncard = n

Tactic:
simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

Premises used: Set.exists_subsuperset_card_eq, Set.empty_subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
⊢ Infinite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
this : Infinite.{u_1 + 1} (↑s : Type u_1)
obtain : ∀ (t' : Finset (↑s : Type u_1)), ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k

Premises used: Set.Infinite.exists_subset_card_eq, Set.infinite_univ, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t' : Set (↑s : Type u_1)) ⊆ s

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
⊢ (↑t' : Set (↑s : Type u_1)).Finite

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
refine : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t' : Set (↑s : Type u_1))).ncard = t'.card
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card

Tactic:
refine ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
rw : (↑t' : Set (↑s : Type u_1)).ncard = t'.card
⊢ (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t' : Set (↑s : Type u_1))).ncard = t'.card

Tactic:
rw [ncard_image_of_injective _ Subtype.coe_injective]

Premises used: Subtype.coe_injective, Set.ncard_image_of_injective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
⊢ (↑t' : Set (↑s : Type u_1)).ncard = t'.card

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
obtain :
  ∀ (s₁ : Set α) (hs₁ : s₁ ⊆ t \ s) (hs₁fin : s₁.Finite) (hs₁card : s₁.ncard = k - s.ncard),
    ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)

Premises used: HSub.hSub, Set.Infinite.exists_subset_ncard_eq, Set.ncard, Set.Infinite.diff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans diff_subset), ?_⟩

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.union_subset, Set.subset_union_left, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
refine : (s ∪ s₁).ncard = k
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
refine ⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans diff_subset), ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
rwa : s.ncard + s₁.ncard = k
rwa₁ : s.ncard + (k - s.ncard) = k
rwa₂ : k = k
rwa₃ : s.ncard ≤ k
rwa₄ : k = k
rwa₅ rwa₆ rwa₇ : s.ncard ≤ k
⊢ (s ∪ s₁).ncard = k

Tactic:
rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
    add_tsub_cancel_of_le]

Premises used: Set.ncard_union_eq, Set.disjoint_sdiff_right, Set.disjoint_of_subset_right, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ (s ∪ t).Finite

Tactic:
have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
hu : (s ∪ t).Finite
⊢ 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card

Tactic:
rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst

Premises used: Set.subset_union_right, Set.Finite.subset, Set.subset_union_left, Set.ncard_eq_toFinset_card, Set.Finite.toFinset_union
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card
obtain :
  ∀ (r' : Finset α) (hnr' : n < r'.card) (hr' : r' ⊆ ⋯.toFinset (s := s) ∨ r' ⊆ ⋯.toFinset (s := t)),
    ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst

Premises used: Finset.exists_subset_or_subset_of_two_mul_lt_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset (s := s) ∨ r' ⊆ ⋯.toFinset (s := t)
⊢ n < (↑r' : Set α).ncard

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset (s := s) ∨ r' ⊆ ⋯.toFinset (s := t)
⊢ (↑r' : Set α) ⊆ s ∨ (↑r' : Set α) ⊆ t

Tactic:
simpa using hr'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset (s := s) ∨ r' ⊆ ⋯.toFinset (s := t)
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
exact ⟨r', by simpa, by simpa using hr'⟩