have := Fin.val_eq_of_eq (h _ _ (Fin.eq_of_val_eq eq))
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, ⋯⟩
isLt' : ↑(f n') < n
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f n')
⊢ ∃ x, f x = ⟨n, ⋯⟩
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, ⋯⟩
isLt' : ↑(f n') < n
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f n')
this : ↑⟨↑x, ⋯⟩ = ↑n'
⊢ ∃ x, f x = ⟨n, ⋯⟩