if isLt : y.val < n then
  let ⟨x, eq⟩ := surj ⟨y.val, isLt⟩
  simp [f'] at eq
  split at eq
  case inl =>
    simp at eq
    exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, Fin.eq_of_val_eq eq⟩
  case inr =>
    simp at eq
    exact ⟨n', Fin.eq_of_val_eq eq⟩
else
  have := Fin.eq_of_not_lt isLt
  simp [this]
  if isLt' : f n' < n then
    let ⟨x, eq⟩ := surj ⟨(f n').val, isLt'⟩
    simp [f'] at eq
    split at eq
    case inl =>
      simp at eq
      have := Fin.val_eq_of_eq (h _ _ (Fin.eq_of_val_eq eq))
      simp at this
      exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
    case inr nlt =>
      have := Fin.eq_of_not_lt nlt
      exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, this⟩
  else
    exact ⟨n', Fin.eq_of_not_lt isLt'⟩
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → Regex.Data.SparseSet.Bijection.surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
f' : Fin n → Fin n :=
  fun x =>
    let x' := ⟨↑x, ⋯⟩;
    let y := f x';
    if isLt : ↑y < n then ⟨↑y, isLt⟩
    else
      let_fun eqx := ⋯;
      let_fun isLt := ⋯;
      ⟨↑(f ⟨n, ⋯⟩), isLt⟩
this✝ : inj f'
surj : Regex.Data.SparseSet.Bijection.surj f'
y : Fin (n + 1)
this : ↑y ≤ n
⊢ ∃ x, f x = y
no goals