α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : ℕ), ¬x ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Nat.Subtype.toFunAux (ofNat s 0) = 0
rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_not_mem]
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
⊢ False
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : ℕ), ¬x ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
rintro n hn
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
⊢ False
rw [mem_filter, ofNat, mem_range] at hn
no goals
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False
exact bot_le.not_lt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)
α : Type ?u.72857
β : Type ?u.72860
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
α : Type ?u.72857
β : Type ?u.72860
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
α : Type ?u.72857
β : Type ?u.72860
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
α : Type ?u.72857
β : Type ?u.72860
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
simp only [toFunAux_eq, ofNat, range_succ] at ih⊢
no goals
α : Type ?u.72857
β : Type ?u.72860
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
conv =>
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
no goals
α : Type ?u.72857
β : Type ?u.72860
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))
simp
α : Type ?u.72857
β : Type ?u.72860
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
α : Type ?u.72857
β : Type ?u.72860
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)))
simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
no goals
α : Type ?u.72857
β : Type ?u.72860
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
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⟩⟩
α : Type ?u.72857
β : Type ?u.72860
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)
α : Type ?u.72857
β : Type ?u.72860
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
simp only [h.2, and_true_iff]
no goals
α : Type ?u.72857
β : Type ?u.72860
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)
exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))