[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (ofNat α n) = n
[PROOFSTEP]
obtain ⟨a, h, e⟩ := decode_inv (α := α) n
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n
[PROOFSTEP]
rwa [ofNat_of_decode h]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type ?u.1578
β : Type ?u.1585
inst✝ : Denumerable α
e : β ≃ α
src✝ : Encodable β := Encodable.ofEquiv α e
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simp_rw [Option.mem_def, decode_ofEquiv e, encode_ofEquiv e, decode_eq_ofNat, Option.map_some', Option.some_inj,
  exists_eq_left', Equiv.apply_symm_apply, Denumerable.encode_ofNat]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = ↑e.symm (ofNat α n)
[PROOFSTEP]
letI := ofEquiv _ e
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = ↑e.symm (ofNat α n)
[PROOFSTEP]
refine ofNat_of_decode ?_
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (↑e.symm (ofNat α n))
[PROOFSTEP]
rw [decode_ofEquiv e]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (↑e.symm) (decode n) = some (↑e.symm (ofNat α n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decode zero ∧ encode a = zero
case succ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n✝ : ℕ
⊢ ∃ a, a ∈ decode (succ n✝) ∧ encode a = succ n✝
[PROOFSTEP]
case zero =>
  refine' ⟨none, _, encode_none⟩
  rw [decode_option_zero, Option.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decode zero ∧ encode a = zero
[PROOFSTEP]
case zero =>
  refine' ⟨none, _, encode_none⟩
  rw [decode_option_zero, Option.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decode zero ∧ encode a = zero
[PROOFSTEP]
refine' ⟨none, _, encode_none⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ none ∈ decode zero
[PROOFSTEP]
rw [decode_option_zero, Option.mem_def]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n✝ : ℕ
⊢ ∃ a, a ∈ decode (succ n✝) ∧ encode a = succ n✝
[PROOFSTEP]
case succ n =>
  refine' ⟨some (ofNat α n), _, _⟩
  · rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
  rw [encode_some, encode_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode (succ n) ∧ encode a = succ n
[PROOFSTEP]
case succ n =>
  refine' ⟨some (ofNat α n), _, _⟩
  · rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
  rw [encode_some, encode_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode (succ n) ∧ encode a = succ n
[PROOFSTEP]
refine' ⟨some (ofNat α n), _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (ofNat α n) ∈ decode (succ n)
[PROOFSTEP]
rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (some (ofNat α n)) = succ n
[PROOFSTEP]
rw [encode_some, encode_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
this : ∃ a, a ∈ decodeSum n ∧ encodeSum a = bit (bodd n) (div2 n)
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simpa [bit_decomp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decodeSum n ∧ encodeSum a = bit (bodd n) (div2 n)
[PROOFSTEP]
simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some', Option.mem_def, Sum.exists]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (match (bodd n, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inl a) ∧
        encodeSum (Sum.inl a) = bit (bodd n) (div2 n)) ∨
    ∃ b,
      (match (bodd n, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inr b) ∧
        encodeSum (Sum.inr b) = bit (bodd n) (div2 n)
[PROOFSTEP]
cases bodd n
[GOAL]
case false
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (match (false, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inl a) ∧
        encodeSum (Sum.inl a) = bit false (div2 n)) ∨
    ∃ b,
      (match (false, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inr b) ∧
        encodeSum (Sum.inr b) = bit false (div2 n)
[PROOFSTEP]
simp [decodeSum, bit, encodeSum, bit0_eq_two_mul, bit1]
[GOAL]
case true
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (match (true, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inl a) ∧
        encodeSum (Sum.inl a) = bit true (div2 n)) ∨
    ∃ b,
      (match (true, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inr b) ∧
        encodeSum (Sum.inr b) = bit true (div2 n)
[PROOFSTEP]
simp [decodeSum, bit, encodeSum, bit0_eq_two_mul, bit1]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simp [decodeSigma]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
[PROOFSTEP]
rw [← decode_eq_ofNat, decode_sigma_val]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ofNat (α × β) n = (ofNat α (unpair n).fst, ofNat β (unpair n).snd)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ofNat (ℕ × ℕ) = unpair
[PROOFSTEP]
funext
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : a ≥ succ ↑x
⊢ ↑x + (a - (↑x + 1)) + 1 ∈ s
[PROOFSTEP]
rwa [add_right_comm, add_tsub_cancel_of_le hax]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ (a : ℕ), a ∈ s → a < succ ↑x
⊢ ∀ (a : ℕ), a ∈ Multiset.filter (fun x => x ∈ s) (Multiset.range (succ ↑x)) → a ∈ s
[PROOFSTEP]
simp [-Multiset.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ (a : ℕ), a ∈ s → a < succ ↑x
⊢ ∀ (x_1 : { y // y ∈ s }),
    x_1 ∈
      Multiset.toFinset
        (Multiset.pmap (fun y hy => { val := y, property := hy })
          (Multiset.filter (fun x => x ∈ s) (Multiset.range (succ ↑x)))
          (_ : ∀ (a : ℕ), a ∈ Multiset.filter (fun x => x ∈ s) (Multiset.range (succ ↑x)) → a ∈ s))
[PROOFSTEP]
simpa [Subtype.ext_iff_val, Multiset.mem_filter, -Multiset.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x y : ↑s
h : y < x
hx : ∃ m, ↑y + m + 1 ∈ s
k : ℕ
hk : ↑x = ↑y + k + 1
this : Nat.find hx ≤ k
⊢ ↑y + Nat.find hx + 1 ≤ ↑x
[PROOFSTEP]
rw [hk]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x y : ↑s
h : y < x
hx : ∃ m, ↑y + m + 1 ∈ s
k : ℕ
hk : ↑x = ↑y + k + 1
this : Nat.find hx ≤ k
⊢ ↑y + Nat.find hx + 1 ≤ ↑y + k + 1
[PROOFSTEP]
exact add_le_add_right (add_le_add_left this _) _
[GOAL]
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
⊢ ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s
[PROOFSTEP]
intros a ha
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
a : ℕ
ha : a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x)
⊢ a ∈ s
[PROOFSTEP]
simpa using (List.mem_filter.mp ha).2
[GOAL]
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by simp [List.mem_filter, Subtype.ext_iff_val, ht]
[GOAL]
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
simp [List.mem_filter, Subtype.ext_iff_val, ht]
[GOAL]
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
have wf : ∀ m : s, List.maximum t = m → ↑m < x := fun m hmax => by simpa using hmt.mp (List.maximum_mem hmax)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simpa using hmt.mp (List.maximum_mem hmax)
[GOAL]
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
cases' hmax : List.maximum t with m
[GOAL]
case none
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (⊥ : s) ?_)⟩
[GOAL]
case none
α : Type u_1
β : Type u_2
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
⊢ ⊥ ∈ []
[PROOFSTEP]
rwa [← List.maximum_eq_none.1 hmax, hmt]
[GOAL]
case some
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
cases' ofNat_surjective_aux m.2 with a ha
[GOAL]
case some.intro
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
refine ⟨a + 1, le_antisymm ?_ ?_⟩
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
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 + 1) ≤ { val := x✝, property := hx }
[PROOFSTEP]
rw [ofNat]
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
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 } ≤ ofNat s (a + 1)
[PROOFSTEP]
rw [ofNat]
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
refine succ_le_of_lt ?_
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
rw [ha]
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
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 }
[PROOFSTEP]
exact wf _ hmax
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
refine le_succ_of_forall_lt_le fun z hz => ?_
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [ha]
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
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) }
[PROOFSTEP]
cases m
[GOAL]
case some.intro.refine_2.mk
α : Type u_1
β : Type u_2
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) }
[PROOFSTEP]
exact List.le_maximum_of_mem (hmt.2 hz) hmax
[GOAL]
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
t✝ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
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✝
[PROOFSTEP]
tauto
[GOAL]
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
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
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
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
h✝ :
  (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) }) =
    (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) })
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
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
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
h✝ :
  (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) }) =
    (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) })
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
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✝
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s
[PROOFSTEP]
rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ Nat.Subtype.toFunAux x = Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
[PROOFSTEP]
rw [toFunAux, List.countp_eq_length_filter]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ List.length (List.filter (fun x => decide (x ∈ s)) (List.range ↑x)) =
    Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Nat.Subtype.toFunAux (ofNat s 0) = 0
[PROOFSTEP]
rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : ℕ), ¬x ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
[PROOFSTEP]
rintro n hn
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
⊢ False
[PROOFSTEP]
rw [mem_filter, ofNat, mem_range] at hn 
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False
[PROOFSTEP]
exact bot_le.not_lt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
have h₁ : (ofNat s n : ℕ) ∉ (range (ofNat s n)).filter (· ∈ s) := by simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
⊢ ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
have h₂ : (range (succ (ofNat s n))).filter (· ∈ s) = insert ↑(ofNat s n) ((range (ofNat s n)).filter (· ∈ s)) :=
  by
  simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
  exact fun m =>
    ⟨fun h => by
      simp only [h.2, and_true_iff]
      exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)), fun h =>
      h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h => ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
⊢ filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
[PROOFSTEP]
simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
⊢ ∀ (a : ℕ), a < ↑(succ (ofNat s n)) ∧ a ∈ s ↔ a = ↑(ofNat s n) ∨ a < ↑(ofNat s n) ∧ a ∈ s
[PROOFSTEP]
exact fun m =>
  ⟨fun h => by
    simp only [h.2, and_true_iff]
    exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)), fun h =>
    h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h => ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n) ∧ m ∈ s
[PROOFSTEP]
simp only [h.2, and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n)
[PROOFSTEP]
exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
simp only [toFunAux_eq, ofNat, range_succ] at ih ⊢
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
⊢ card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
conv =>
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
rhs
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| n + 1
[PROOFSTEP]
rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
⊢ Denumerable α
[PROOFSTEP]
letI := @decidableRangeEncode α _
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this : DecidablePred fun x => x ∈ Set.range encode := decidableRangeEncode α
⊢ Denumerable α
[PROOFSTEP]
letI : Infinite (Set.range (@encode α _)) := Infinite.of_injective _ (Equiv.ofInjective _ encode_injective).injective
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝ : DecidablePred fun x => x ∈ Set.range encode := decidableRangeEncode α
this : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (↑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
⊢ Denumerable α
[PROOFSTEP]
letI := Nat.Subtype.denumerable (Set.range (@encode α _))
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝¹ : DecidablePred fun x => x ∈ Set.range encode := decidableRangeEncode α
this✝ : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (↑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
this : Denumerable ↑(Set.range encode) := Subtype.denumerable (Set.range encode)
⊢ Denumerable α
[PROOFSTEP]
exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
⊢ Nonempty (α ≃ β)
[PROOFSTEP]
cases nonempty_denumerable α
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝ : Denumerable α
⊢ Nonempty (α ≃ β)
[PROOFSTEP]
cases nonempty_denumerable β
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝¹ : Denumerable α
val✝ : Denumerable β
⊢ Nonempty (α ≃ β)
[PROOFSTEP]
exact ⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩
