α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
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
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by
  simp [List.mem_filter, Subtype.ext_iff_val, ht]
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
have wf : ∀ m : s, List.maximum t = m → ↑m < x := fun m hmax => by
  simpa using hmt.mp (List.maximum_mem hmax)
case none
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
hmax : List.maximum t = none
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }

case some
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
cases' hmax : List.maximum t with m
case some.intro
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
case some
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
cases' ofNat_surjective_aux m.2 with a ha
case some.intro.refine_1
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ succ (ofNat s a) ≤ { val := x✝, property := hx }

case some.intro.refine_2
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := x✝, property := hx } ≤ succ (ofNat s a)
case some.intro
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
refine ⟨a + 1, le_antisymm ?_ ?_⟩ <;> rw [ofNat]
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
a : ℕ
ha : a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x)
⊢ a ∈ s
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
⊢ ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s
intros a ha
no goals
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
a : ℕ
ha : a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x)
⊢ a ∈ s
simpa using (List.mem_filter.mp ha).2
no goals
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
⊢ ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
simp [List.mem_filter, Subtype.ext_iff_val, ht]
no goals
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
m : ↑s
hmax : List.maximum t = ↑m
⊢ ↑m < x
simpa using hmt.mp (List.maximum_mem hmax)
case none
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
hmax : List.maximum t = none
h : { val := x✝, property := hx } > ofNat s 0
⊢ ⊥ ∈ []
case none
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
hmax : List.maximum t = none
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (⊥ : s) ?_)⟩
no goals
case none
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
hmax : List.maximum t = none
h : { val := x✝, property := hx } > ofNat s 0
⊢ ⊥ ∈ []
rwa [← List.maximum_eq_none.1 hmax, hmt]
case some.intro.refine_1
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ofNat s a < { val := x✝, property := hx }
case some.intro.refine_1
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ succ (ofNat s a) ≤ { val := x✝, property := hx }
refine succ_le_of_lt ?_
case some.intro.refine_1
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := ↑m, property := (_ : ↑m ∈ s) } < { val := x✝, property := hx }
case some.intro.refine_1
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ofNat s a < { val := x✝, property := hx }
rw [ha]
no goals
case some.intro.refine_1
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := ↑m, property := (_ : ↑m ∈ s) } < { val := x✝, property := hx }
exact wf _ hmax
case some.intro.refine_2
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
z : ↑s
hz : z < { val := x✝, property := hx }
⊢ z ≤ ofNat s a
case some.intro.refine_2
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := x✝, property := hx } ≤ succ (ofNat s a)
refine le_succ_of_forall_lt_le fun z hz => ?_
case some.intro.refine_2
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
z : ↑s
hz : z < { val := x✝, property := hx }
⊢ z ≤ { val := ↑m, property := (_ : ↑m ∈ s) }
case some.intro.refine_2
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
z : ↑s
hz : z < { val := x✝, property := hx }
⊢ z ≤ ofNat s a
rw [ha]
case some.intro.refine_2.mk
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
a : ℕ
z : ↑s
hz : z < { val := x✝, property := hx }
val✝ : ℕ
property✝ : val✝ ∈ s
hmax : List.maximum t = some { val := val✝, property := property✝ }
ha :
  ofNat s a =
    { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ s) }
⊢ z ≤ { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ s) }
case some.intro.refine_2
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
z : ↑s
hz : z < { val := x✝, property := hx }
⊢ z ≤ { val := ↑m, property := (_ : ↑m ∈ s) }
cases m
no goals
case some.intro.refine_2.mk
α : Type ?u.49351
β : Type ?u.49354
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
a : ℕ
z : ↑s
hz : z < { val := x✝, property := hx }
val✝ : ℕ
property✝ : val✝ ∈ s
hmax : List.maximum t = some { val := val✝, property := property✝ }
ha :
  ofNat s a =
    { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ s) }
⊢ z ≤ { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ s) }
exact List.le_maximum_of_mem (hmt.2 hz) hmax
no goals
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝ hmax : List.maximum t = some m
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
tauto