-- Mathlib/Data/Set/Card.lean
theorem exists_subset_encard_eq {k : ℕ∞} (hk : k ≤ s.encard) : ∃ t, t ⊆ s ∧ t.encard = k

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hle : ↑n.succ ≤ s.encard
⊢ ↑n ≤ ↑n.succ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
⊢ t₀ ≠ s

Tactic:
rintro rfl

Result:
α : Type u_1
k : ℕ∞
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hle : ↑n + 1 ≤ t₀.encard
⊢ False

Proof state:
case refine_1.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n + 1

Tactic:
have hne : t₀ ≠ s := by
  rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hle; simp at hle

Result:
case refine_1.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
⊢ ∃ t ⊆ s, t.encard = ↑n + 1

Proof state:
case refine_1.intro.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ ∃ t ⊆ s, t.encard = ↑n + 1

Tactic:
exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_not_mem hx.2, ht₀]⟩

Result:
no goals

Proof state:
α : Type u_1
k : ℕ∞
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hle : n + 1 ≤ n
⊢ False

Tactic:
simp at hle

Result:
no goals

Proof state:
case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n) → s.Infinite → ∃ t ⊆ s, t.Infinite

Tactic:
exact fun _ hi ↦ ⟨s, Subset.rfl, hi⟩

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = k

Tactic:
revert hk

Result:
α : Type u_1
s : Set α
k : ℕ∞
⊢ k ≤ s.encard → ∃ t ⊆ s, t.encard = k

Proof state:
α : Type u_1
k : ℕ∞
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hle : ↑n + 1 ≤ t₀.encard
⊢ False

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

Result:
α : Type u_1
k : ℕ∞
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hle : n + 1 ≤ n
⊢ False

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ (insert x t₀).encard = ↑n + 1

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

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
⊢ k ≤ s.encard → ∃ t ⊆ s, t.encard = k

Tactic:
refine ENat.nat_induction k (fun _ ↦ ⟨∅, empty_subset _, by simp⟩) (fun n IH hle ↦ ?_) ?_

Result:
case refine_1
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hle : ↑n.succ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n) → ⊤ ≤ s.encard → ∃ t ⊆ s, t.encard = ⊤

Proof state:
case refine_1
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hle : ↑n.succ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

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

Result:
case refine_1.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hle : ↑n.succ ≤ s.encard
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

Proof state:
case refine_1.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hle : ↑n.succ ≤ s.encard
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

Tactic:
simp only [Nat.cast_succ] at *

Result:
case refine_1.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n + 1

Proof state:
case refine_1.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
⊢ ∃ t ⊆ s, t.encard = ↑n + 1

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

Result:
case refine_1.intro.intro.intro
α : Type u_1
s : Set α
k : ℕ∞
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hle : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ ∃ t ⊆ s, t.encard = ↑n + 1

Proof state:
case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n) → ⊤ ≤ s.encard → ∃ t ⊆ s, t.encard = ⊤

Tactic:
simp only [top_le_iff, encard_eq_top_iff]

Result:
case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n) → s.Infinite → ∃ t ⊆ s, t.Infinite

Proof state:
α : Type u_1
s : Set α
k : ℕ∞
x✝ : 0 ≤ s.encard
⊢ ∅.encard = 0

Tactic:
simp

Result:
no goals