-- Mathlib/Logic/Denumerable.lean
theorem ofNat_surjective : Surjective (ofNat s)
  | ⟨x, hx⟩ => by
    set t : List s :=
      ((List.range x).filter fun y => y ∈ s).pmap
        (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
        (by intros a ha; simpa using (List.mem_filter.mp ha).2) with ht
    have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
ha : a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x)
⊢ a ∈ s

Tactic:
simpa using (List.mem_filter.mp ha).2

Result:
no goals

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
cases hmax : List.maximum t with
| bot =>
  refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (⊥ : s) ?_)⟩
  rwa [← List.maximum_eq_bot.1 hmax, hmt]
| coe m =>
  have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
  rcases ofNat_surjective m with ⟨a, rfl⟩
  refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
  exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

Result:
no goals

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
⊢ ↑m < x

Tactic:
simpa using hmt.mp (List.maximum_mem hmax)

Result:
no goals

Proof state:
case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
wf : ↑m < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
rcases ofNat_surjective m with ⟨a, rfl⟩

Result:
case coe.intro
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by
  simp [List.mem_filter, Subtype.ext_iff_val, ht]

Result:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∀ a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x), a ∈ s

Tactic:
intros a ha

Result:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
ha : a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x)
⊢ a ∈ s

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
set t : List s :=
  ((List.range x).filter fun y => y ∈ s).pmap
    (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
    (by intros a ha; simpa using (List.mem_filter.mp ha).2) with ht

Result:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
⊢ ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩

Tactic:
simp [List.mem_filter, Subtype.ext_iff_val, ht]

Result:
no goals

Proof state:
case coe.intro
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ⟨x, hx⟩ ≤ ofNat s (a + 1)

Tactic:
exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

Result:
no goals

Proof state:
case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)

Result:
case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
wf : ↑m < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Proof state:
case coe.intro
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩

Result:
case coe.intro
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ⟨x, hx⟩ ≤ ofNat s (a + 1)