awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
x : α
hx : x ∈ s
h₁ : ∃ (x_1 : α) (y : α) (z : α), x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
⊢ x ∈ s

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (4 : ℕ∞) = 3 + 1),
      WithTop.add_right_inj WithTop.one_ne_top, encard_eq_three] at h

Premises used: WithTop.one_ne_top, Set.encard_eq_three, Set.insert_eq_of_mem, WithTop.add_right_inj, Set.insert_diff_singleton, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : ∃ (x_1 : α) (y : α) (z : α), x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
hx : x ∈ s
refine_1 :
  ∀ (y z w : α) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) (hs : s \ {x} = {y, z, w}),
    ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
obtain ⟨y, z, w, hyz, hyw, hzw, hs⟩ := h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : x ≠ y
refine_1₁ : x ≠ z
refine_1₂ : x ≠ w
refine_1₃ : s = {x, y, z, w}
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z w : α
hzw : z ≠ w
hyz : x ≠ z
hyw : x ≠ w
hs : s \ {x} = {x, z, w}
⊢ False

Tactic:
(hs.symm.subset (Or.inl rfl)).2 rfl

Premises used: Eq.subset, And.right, Or.inl, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z w : α
hzw : z ≠ w
hyz : x ≠ z
hyw : x ≠ w
hs : s \ {x} = {x, z, w}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inl rfl)).2 rfl

Premises used: Eq.subset, And.right, Or.inl, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y w : α
hyw : y ≠ w
hyz : y ≠ x
hzw : x ≠ w
hs : s \ {x} = {y, x, w}
⊢ False

Tactic:
(hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl

Premises used: Eq.subset, And.right, Or.inl, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y w : α
hyw : y ≠ w
hyz : y ≠ x
hzw : x ≠ w
hs : s \ {x} = {y, x, w}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl

Premises used: Eq.subset, And.right, Or.inl, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hyz : y ≠ z
hyw : y ≠ x
hzw : z ≠ x
hs : s \ {x} = {y, z, x}
⊢ False

Tactic:
(hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl

Premises used: Eq.subset, And.right, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hyz : y ≠ z
hyw : y ≠ x
hzw : z ≠ x
hs : s \ {x} = {y, z, x}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl

Premises used: Eq.subset, And.right, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : s = insert x (s \ {x})
refine_1₁ : s = insert x s
refine_1₂ refine_1₃ : s = s
⊢ s = {x, y, z, w}

Tactic:
rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 + 1 = 4
refine_2₁ : z ∉ {w}
refine_2₂ : y ∉ {z, w}
refine_2₃ : x ∉ {y, z, w}
⊢ s.encard = 4

Tactic:
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton]

Premises used: Set.encard_insert_of_notMem, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ HAdd.hAdd (α := ℕ∞) 1 1 + 1 + 1 = 4

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ z ∉ {w}

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ y ∉ {z, w}

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ x ∉ {y, z, w}

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
k : ℕ
⊢ (↑(Finset.range k) : Set ℕ).encard = (↑(Finset.range k).card : ℕ∞)

Tactic:
encard_coe_eq_coe_finsetCard (Finset.range k)

Premises used: Finset.range, Set.encard_coe_eq_coe_finsetCard
-- Module: Mathlib.Data.Set.Card
Goal:
k : ℕ
h : encard (α := ℕ) {i : ℕ | i < k} = (↑(Finset.range k) : Set ℕ).encard
h₁ : Eq (α := ℕ∞) (↑k : ℕ∞) (↑(Finset.range k).card : ℕ∞)
⊢ encard (α := ℕ) {i : ℕ | i < k} = (↑k : ℕ∞)

Tactic:
convert! encard_coe_eq_coe_finsetCard (Finset.range k) using 1

Premises used: Finset.range, Set.encard_coe_eq_coe_finsetCard
-- Module: Mathlib.Data.Set.Card
Goal:
k : ℕ
h : encard (α := ℕ) {i : ℕ | i < k} = (Iio k).encard
h₁ h₂ : (Iio k).encard = (Iio k).encard
⊢ encard (α := ℕ) {i : ℕ | i < k} = (↑(Finset.range k) : Set ℕ).encard

Tactic:
rw [Finset.coe_range, Iio_def]

Premises used: Set.Iio_def, Finset.coe_range
-- Module: Mathlib.Data.Set.Card
Goal:
k : ℕ
h h₁ : Eq (α := ℕ∞) (↑k : ℕ∞) (↑k : ℕ∞)
⊢ Eq (α := ℕ∞) (↑k : ℕ∞) (↑(Finset.range k).card : ℕ∞)

Tactic:
rw [Finset.card_range]

Premises used: Finset.card_range
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : t.encard = s.encard + 1
⊢ ∃ (x : α), t \ s = {x}

Tactic:
rw [← encard_diff_add_encard_of_subset h, add_comm, WithTop.add_left_inj hs.encard_lt_top.ne,
    encard_eq_one] at hst

Premises used: Set.Finite.encard_lt_top, Set.encard_diff_add_encard_of_subset, add_comm, Set.encard_eq_one, LT.lt.ne, WithTop.add_left_inj
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : ∃ (x : α), t \ s = {x}
obtain : ∀ (x : α) (hx : t \ s = {x}), ∃ (a : α), t = insert a s
⊢ ∃ (a : α), t = insert a s

Tactic:
obtain ⟨x, hx⟩ := hst
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
h₁ : t = insert x s
⊢ ∃ (a : α), t = insert a s

Tactic:
use x
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
h₁ : t \ s ∪ s = insert x s
h₂ : {x} ∪ s = insert x s
h₃ h₄ : insert x s = insert x s
⊢ t = insert x s

Tactic:
rw [← diff_union_of_subset h, hx, singleton_union]

Premises used: Set.singleton_union, Set.diff_union_of_subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hk : 0 ≤ s.encard
⊢ encard.{u_1} (α := α) ∅ = 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hk : 0 ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = 0

Tactic:
exact ⟨∅, empty_subset _, by simp⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : (↑n.succ : ℕ∞) ≤ s.encard
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑n.succ : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : (↑n.succ : ℕ∞) ≤ s.encard
succ : ∀ (t₀ : Set α) (ht₀s : t₀ ⊆ s) (ht₀ : t₀.encard = (↑n : ℕ∞)), ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
⊢ ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)

Tactic:
obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)

Premises used: le_trans
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : (↑n.succ : ℕ∞) ≤ s.encard
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard

Tactic:
simp only [Nat.cast_succ] at *

Premises used: Nat.cast_succ
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = (↑n : ℕ∞)
IH : ∀ (hk : (↑n : ℕ∞) ≤ t₀.encard), ∃ t ⊆ t₀, t.encard = (↑n : ℕ∞)
ht₀s : t₀ ⊆ t₀
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ t₀.encard
⊢ n + 1 ≤ n

Tactic:
rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk

Premises used: Nat.cast_add, Nat.cast_le, Nat.cast_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = (↑n : ℕ∞)
IH : ∀ (hk : (↑n : ℕ∞) ≤ t₀.encard), ∃ t ⊆ t₀, t.encard = (↑n : ℕ∞)
ht₀s : t₀ ⊆ t₀
hk : n + 1 ≤ n
⊢ False

Tactic:
simp at hk
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
⊢ t₀ ≠ s

Tactic:
have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
hne : t₀ ≠ s
succ : ∀ (x : α) (hx : x ∈ s ∧ x ∉ t₀), ∃ t ⊆ s, t.encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ ∃ t ⊆ s, t.encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)

Premises used: Set.exists_of_ssubset, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
rw : t₀.encard + 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
rw₁ rw₂ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ (insert x t₀).encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
rw [encard_insert_of_notMem hx.2, ht₀]

Premises used: And.right, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ ∃ t ⊆ s, t.encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∀ (n : ℕ) (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : ⊤ ≤ s.encard
⊢ s.encard = ⊤

Tactic:
rw [top_le_iff] at hk

Premises used: top_le_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∀ (n : ℕ) (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : s.encard = ⊤
⊢ ∃ t ⊆ s, t.encard = ⊤

Tactic:
⟨s, Subset.rfl, hk⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∀ (n : ℕ) (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : s.encard = ⊤
⊢ ∃ t ⊆ s, t.encard = ⊤

Tactic:
exact ⟨s, Subset.rfl, hk⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
zero : ∀ (hk : 0 ≤ s.encard), ∃ t ⊆ s, t.encard = 0
succ :
  ∀ (n : ℕ) (IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)) (hk : (↑n.succ : ℕ∞) ≤ s.encard),
    ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
top :
  (∀ (n : ℕ) (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)) → ∀ (hk : ⊤ ≤ s.encard), ∃ t ⊆ s, t.encard = ⊤
⊢ ∃ t ⊆ s, t.encard = k

Tactic:
induction k using ENat.nat_induction with
  | zero => exact ⟨∅, empty_subset _, by simp⟩
  | succ n IH =>
    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
    simp only [Nat.cast_succ] at *
    have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
    obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
    exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩

Premises used: Nat.cast_succ, top_le_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
inl : ∀ (hs : s.encard = ⊤), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
inr : ∀ (hs : s.encard ≠ ⊤), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
obtain (hs | hs) := eq_or_ne s.encard ⊤

Premises used: Set.encard, eq_or_ne, Top.top
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ k = ⊤

Tactic:
rw [hs, top_le_iff] at hsk

Premises used: top_le_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
hsk₁ : k = ⊤
⊢ k ≤ t.encard

Tactic:
rw [hs, top_le_iff] at hsk

Premises used: top_le_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
hsk₁ : k = ⊤
hkt₁ : k ≤ t.encard
⊢ s.encard = ⊤

Tactic:
rw [hs, top_le_iff] at hsk

Premises used: top_le_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
inl : ∀ (hkt : ⊤ ≤ t.encard), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
subst hsk
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤

Tactic:
⟨s, Subset.rfl, hst, hs⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤

Tactic:
exact ⟨s, Subset.rfl, hst, hs⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard ≠ ⊤
inr :
  ∀ (k : ℕ∞) (hsk : s.encard ≤ s.encard + k) (hkt : s.encard + k ≤ t.encard),
    ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
obtain ⟨k, rfl⟩ := exists_add_of_le hsk

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
inr : ∀ (k' : ℕ∞) (hk' : t.encard = s.encard + k + k'), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Tactic:
obtain ⟨k', hk'⟩ := exists_add_of_le hkt

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
rw :
  ∀ (hkt : k + s.encard ≤ (t \ s).encard + s.encard) (k' : ℕ∞) (hk' : t.encard = s.encard + k + k'), k ≤ (t \ s).encard
⊢ k ≤ (t \ s).encard

Tactic:
rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt

Premises used: Set.encard_diff_add_encard_of_subset, add_comm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
WithTop.le_of_add_le_add_right hs hkt

Premises used: WithTop.le_of_add_le_add_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
exact WithTop.le_of_add_le_add_right hs hkt

Premises used: WithTop.le_of_add_le_add_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
have hk : k ≤ encard (t \ s) := by
    rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt
    exact WithTop.le_of_add_le_add_right hs hkt
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
hk : k ≤ (t \ s).encard
inr :
  ∀ (r' : Set α) (hr' : r' ⊆ t \ s) (hsk : s.encard ≤ s.encard + r'.encard) (hkt : s.encard + r'.encard ≤ t.encard)
    (hk' : t.encard = s.encard + r'.encard + k') (hk : r'.encard ≤ (t \ s).encard),
    ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Tactic:
obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk

Premises used: Set.exists_subset_encard_eq, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard

Tactic:
⟨s ∪ r', subset_union_left, union_subset hst (hr'.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 α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
inr : (s ∪ r').encard = s.encard + r'.encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard

Tactic:
refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans diff_subset), ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
inr inr₁ : s.encard + r'.encard = s.encard + r'.encard
⊢ (s ∪ r').encard = s.encard + r'.encard

Tactic:
rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]

Premises used: Set.encard_union_eq, Set.disjoint_sdiff_right, Set.disjoint_of_subset_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
rw : ENat.card.{u_2} (↑(f '' s) : Type u_2) = s.encard
rw₁ : ENat.card.{u_1} (↑s : Type u_1) = s.encard
rw₂ rw₃ : ENat.card.{u_1} (↑s : Type u_1) = ENat.card.{u_1} (↑s : Type u_1)
⊢ (f '' s).encard = s.encard

Tactic:
rw [encard, ENat.card_image_of_injOn h, encard]

Premises used: Set.encard, ENat.card_image_of_injOn
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : Equiv.{u_1 + 1, u_2 + 1} (↑s : Type u_1) (↑t : Type u_2)
⊢ s.encard = t.encard

Tactic:
ENat.card_congr e

Premises used: ENat.card_congr, Set.encard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
s : Set α
⊢ (f '' s).encard = s.encard

Tactic:
hf.injOn.encard_image

Premises used: Function.Injective.injOn, Set.InjOn.encard_image
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
rw : ENat.card α ≤ (f '' univ).encard
rw₁ : ENat.card α ≤ encard.{u_1} (α := α) univ
rw₂ rw₃ : ENat.card α ≤ ENat.card α
⊢ ENat.card α ≤ (range f).encard

Tactic:
rw [← image_univ, hf.encard_image, encard_univ]

Premises used: Set.image_univ, Set.encard_univ, Function.Injective.encard_image
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : Function.Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) (↑t : Type u_2)
⊢ s.encard ≤ t.encard

Tactic:
ENat.card_le_card_of_injective e.injective

Premises used: ENat.card_le_card_of_injective, Set.encard, Function.Embedding.injective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
inl : ∀ (h : IsEmpty α), (f '' s).encard ≤ s.encard
inr : ∀ (h : Nonempty α), (f '' s).encard ≤ s.encard
⊢ (f '' s).encard ≤ s.encard

Tactic:
obtain (h | h) := isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
inl : (f '' ∅).encard ≤ encard.{u_1} (α := α) ∅
⊢ (f '' s).encard ≤ s.encard

Tactic:
rw [s.eq_empty_of_isEmpty]

Premises used: Set.eq_empty_of_isEmpty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' ∅).encard ≤ encard.{u_1} (α := α) ∅

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
inr : (Function.invFunOn f s '' f '' s).encard ≤ s.encard
inr₁ inr₂ : s.encard ≤ s.encard
⊢ (f '' s).encard ≤ s.encard

Tactic:
grw [← (f.invFunOn_injOn_image s).encard_image, f.invFunOn_image_image_subset s]

Premises used: Function.invFunOn_injOn_image, Set.InjOn.encard_image, Function.invFunOn_image_image_subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
inl : ∀ (h' : IsEmpty α), InjOn f s
inr : ∀ (hne : Nonempty α), InjOn f s
⊢ InjOn f s

Tactic:
obtain (h' | hne) := isEmpty_or_nonempty α

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

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ (Function.invFunOn f s '' f '' s).encard = s.encard

Tactic:
rw [← (f.invFunOn_injOn_image s).encard_image] at h

Premises used: Function.invFunOn_injOn_image, Set.InjOn.encard_image
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
inr : Function.invFunOn f s '' f '' s = s
⊢ InjOn f s

Tactic:
rw [injOn_iff_invFunOn_image_image_eq_self]

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

Tactic:
hs.eq_of_subset_of_encard_le' (f.invFunOn_image_image_subset s) h.symm.le

Premises used: Eq.le, Set.Finite.eq_of_subset_of_encard_le', Function.invFunOn_image_image_subset, Eq.symm