-- Mathlib/Logic/Denumerable.lean
theorem right_inverse_aux : ∀ n, toFunAux (ofNat s n) = n
  | 0 => by
    rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_not_mem]
    rintro n hn
    rw [mem_filter, ofNat, mem_range] at hn
    exact bot_le.not_lt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)
  | n + 1 => by
    have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
    have h₁ : (ofNat s n : ℕ) ∉ {x ∈ range (ofNat s n) | x ∈ s}

Proof state:
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

Tactic:
have h₂ : {x ∈ range (succ (ofNat s n)) | x ∈ s} =
    insert ↑(ofNat s n) {x ∈ range (ofNat s n) | x ∈ 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]
      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⟩⟩

Result:
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

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n ∈ filter (fun y => y ∈ s) (range ↑(ofNat s 0))
⊢ False

Tactic:
rw [mem_filter, ofNat, mem_range] at hn

Result:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False

Proof state:
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

Tactic:
have h₁ : (ofNat s n : ℕ) ∉ {x ∈ range (ofNat s n) | x ∈ s} := by simp

Result:
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

Proof state:
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))

Tactic:
simp

Result:
no goals

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : ℕ), x ∉ filter (fun y => y ∈ s) (range ↑(ofNat s 0))

Tactic:
rintro n hn

Result:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n ∈ filter (fun y => y ∈ s) (range ↑(ofNat s 0))
⊢ False

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Nat.Subtype.toFunAux (ofNat s 0) = 0

Tactic:
rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_not_mem]

Result:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : ℕ), x ∉ filter (fun y => y ∈ s) (range ↑(ofNat s 0))

Proof state:
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

Tactic:
exact fun m =>
  ⟨fun h => by
    simp only [h.2, and_true]
    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⟩⟩

Result:
no goals

Proof state:
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

Tactic:
simp only [h.2, and_true]

Result:
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)

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False

Tactic:
exact bot_le.not_lt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)

Result:
no goals

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1

Tactic:
have ih : toFunAux (ofNat s n) = n := right_inverse_aux n

Result:
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

Proof state:
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

Tactic:
simp only [toFunAux_eq, ofNat, range_succ] at ih ⊢

Result:
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 : #(filter (fun y => y ∈ s) (range ↑(ofNat s n))) = n
⊢ #(filter (fun y => y ∈ s) (range ↑(succ (ofNat s n)))) = n + 1

Proof state:
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)

Tactic:
exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))

Result:
no goals

Proof state:
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)))

Tactic:
simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]

Result:
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

Proof state:
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 : #(filter (fun y => y ∈ s) (range ↑(ofNat s n))) = n
⊢ #(filter (fun y => y ∈ s) (range ↑(succ (ofNat s n)))) = n + 1

Tactic:
conv =>
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]

Result:
no goals