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'⟩
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
isLt : ¬↑y < n
this : y = ⟨n, ⋯⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
no goals