Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj (Regex/Data/SparseSet/Bijection.lean)

State before:
n : Nat
f : Fin n → Fin n
h : inj f
⊢ surj f
Tactic:
induction n with
| zero =>
  intro y
  have : y.val < 0 := y.isLt
  contradiction
| succ n ih =>
  let n' : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  let f' (x : Fin n) : Fin n :=
    let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
    let y := f x'
    if isLt : y.val < n then
      ⟨y.val, isLt⟩
    else
      have eqx : f x' = n' := Fin.eq_of_not_lt isLt
      have isLt : f n' < n' := by
        by_contra nlt
        have eqn : f n' = n' := Fin.eq_of_not_lt nlt
        have : f x' = f n' := by rw [eqx, eqn]
        have : x' = n' := h _ _ this
        have : x.val = n := by
          have : x'.val = n'.val := by rw [this]
          exact this
        exact Nat.lt_irrefl _ (this ▸ x.isLt)
      ⟨f ⟨n, Nat.lt_succ_self n⟩, isLt⟩
  have : inj f' := by
    intro x y eq
    let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
    let y' : Fin (n + 1) := ⟨y.val, Nat.lt_trans y.isLt (Nat.lt_succ_self n)⟩
    if hx : f x' < n then
      if hy : f y' < n then
        simp [f', hx, hy] at eq
        have := h _ _ (Fin.eq_of_val_eq eq)
        simp at this
        exact Fin.eq_of_val_eq this
      else
        simp [f', hx, hy] at eq
        have := h _ _ (Fin.eq_of_val_eq eq)
        simp at this
        exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
    else
      if hy : f y' < n then
        simp [f', hx, hy] at eq
        have := h _ _ (Fin.eq_of_val_eq eq)
        simp at this
        exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
      else
        have eqx := Fin.eq_of_not_lt hx
        have eqy := Fin.eq_of_not_lt hy
        have : f x' = f y' := by rw [eqx, eqy]
        have : x' = y' := h _ _ this
        have : x.val = y.val := by
          have : x'.val = y'.val := by rw [this]
          exact this
        exact Fin.eq_of_val_eq this
  have surj : surj f' := ih _ this
  intro y
  have : y.val ≤ n := Nat.le_of_succ_le_succ y.isLt
  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'⟩
State after:
no goals

State before:
case zero
f : Fin 0 → Fin 0
h : inj f
⊢ surj f
Tactic:
intro y
State after:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
⊢ ∃ x, f x = y

State before:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
⊢ ∃ x, f x = y
Tactic:
have : y.val < 0 := y.isLt
State after:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
this : ↑y < 0
⊢ ∃ x, f x = y

State before:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
this : ↑y < 0
⊢ ∃ x, f x = y
Tactic:
contradiction
State after:
no goals

State before:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
⊢ surj f
Tactic:
let n' : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
State after:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
⊢ surj f

State before:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
⊢ surj f
Tactic:
let f' (x : Fin n) : Fin n :=
  let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
  let y := f x'
  if isLt : y.val < n then
    ⟨y.val, isLt⟩
  else
    have eqx : f x' = n' := Fin.eq_of_not_lt isLt
    have isLt : f n' < n' := by
      by_contra nlt
      have eqn : f n' = n' := Fin.eq_of_not_lt nlt
      have : f x' = f n' := by rw [eqx, eqn]
      have : x' = n' := h _ _ this
      have : x.val = n := by
        have : x'.val = n'.val := by rw [this]
        exact this
      exact Nat.lt_irrefl _ (this ▸ x.isLt)
    ⟨f ⟨n, Nat.lt_succ_self n⟩, isLt⟩
State after:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
⊢ surj f

State before:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
⊢ surj f
Tactic:
have : inj f' := by
  intro x y eq
  let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
  let y' : Fin (n + 1) := ⟨y.val, Nat.lt_trans y.isLt (Nat.lt_succ_self n)⟩
  if hx : f x' < n then
    if hy : f y' < n then
      simp [f', hx, hy] at eq
      have := h _ _ (Fin.eq_of_val_eq eq)
      simp at this
      exact Fin.eq_of_val_eq this
    else
      simp [f', hx, hy] at eq
      have := h _ _ (Fin.eq_of_val_eq eq)
      simp at this
      exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
  else
    if hy : f y' < n then
      simp [f', hx, hy] at eq
      have := h _ _ (Fin.eq_of_val_eq eq)
      simp at this
      exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
    else
      have eqx := Fin.eq_of_not_lt hx
      have eqy := Fin.eq_of_not_lt hy
      have : f x' = f y' := by rw [eqx, eqy]
      have : x' = y' := h _ _ this
      have : x.val = y.val := by
        have : x'.val = y'.val := by rw [this]
        exact this
      exact Fin.eq_of_val_eq this
State after:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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 f

State before:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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 f
Tactic:
have surj : surj f' := ih _ this
State after:
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'
⊢ Regex.Data.SparseSet.Bijection.surj f

State before:
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'
⊢ Regex.Data.SparseSet.Bijection.surj f
Tactic:
intro y
State after:
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)
⊢ ∃ x, f x = y

State before:
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)
⊢ ∃ x, f x = y
Tactic:
have : y.val ≤ n := Nat.le_of_succ_le_succ y.isLt
State after:
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

State before:
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
Tactic:
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'⟩
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
⊢ f n' < n'
Tactic:
by_contra nlt
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
⊢ False

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
⊢ False
Tactic:
have eqn : f n' = n' := Fin.eq_of_not_lt nlt
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
⊢ False

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
⊢ False
Tactic:
have : f x' = f n' := by rw [eqx, eqn]
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this : f x' = f n'
⊢ False

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this : f x' = f n'
⊢ False
Tactic:
have : x' = n' := h _ _ this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝ : f x' = f n'
this : x' = n'
⊢ False

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝ : f x' = f n'
this : x' = n'
⊢ False
Tactic:
have : x.val = n := by
  have : x'.val = n'.val := by rw [this]
  exact this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝¹ : f x' = f n'
this✝ : x' = n'
this : ↑x = n
⊢ False

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝¹ : f x' = f n'
this✝ : x' = n'
this : ↑x = n
⊢ False
Tactic:
exact Nat.lt_irrefl _ (this ▸ x.isLt)
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
⊢ f x' = f n'
Tactic:
rw [eqx, eqn]
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝ : f x' = f n'
this : x' = n'
⊢ ↑x = n
Tactic:
have : x'.val = n'.val := by rw [this]
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝¹ : f x' = f n'
this✝ : x' = n'
this : ↑x' = ↑n'
⊢ ↑x = n

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝¹ : f x' = f n'
this✝ : x' = n'
this : ↑x' = ↑n'
⊢ ↑x = n
Tactic:
exact this
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
eqn : f n' = n'
this✝ : f x' = f n'
this : x' = n'
⊢ ↑x' = ↑n'
Tactic:
rw [this]
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
⊢ inj f'
Tactic:
intro x y eq
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
⊢ x = y
Tactic:
let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
⊢ x = y
Tactic:
let y' : Fin (n + 1) := ⟨y.val, Nat.lt_trans y.isLt (Nat.lt_succ_self n)⟩
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
⊢ x = y
Tactic:
if hx : f x' < n then
  if hy : f y' < n then
    simp [f', hx, hy] at eq
    have := h _ _ (Fin.eq_of_val_eq eq)
    simp at this
    exact Fin.eq_of_val_eq this
  else
    simp [f', hx, hy] at eq
    have := h _ _ (Fin.eq_of_val_eq eq)
    simp at this
    exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
else
  if hy : f y' < n then
    simp [f', hx, hy] at eq
    have := h _ _ (Fin.eq_of_val_eq eq)
    simp at this
    exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
  else
    have eqx := Fin.eq_of_not_lt hx
    have eqy := Fin.eq_of_not_lt hy
    have : f x' = f y' := by rw [eqx, eqy]
    have : x' = y' := h _ _ this
    have : x.val = y.val := by
      have : x'.val = y'.val := by rw [this]
      exact this
    exact Fin.eq_of_val_eq this
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
⊢ x = y
Tactic:
if hy : f y' < n then
  simp [f', hx, hy] at eq
  have := h _ _ (Fin.eq_of_val_eq eq)
  simp at this
  exact Fin.eq_of_val_eq this
else
  simp [f', hx, hy] at eq
  have := h _ _ (Fin.eq_of_val_eq eq)
  simp at this
  exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
⊢ x = y
Tactic:
simp [f', hx, hy] at eq
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
⊢ x = y
Tactic:
have := h _ _ (Fin.eq_of_val_eq eq)
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : ⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : ⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩
⊢ x = y
Tactic:
simp at this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : ↑x = ↑y
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : ↑x = ↑y
⊢ x = y
Tactic:
exact Fin.eq_of_val_eq this
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
⊢ x = y
Tactic:
simp [f', hx, hy] at eq
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨n, ⋯⟩)
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨n, ⋯⟩)
⊢ x = y
Tactic:
have := h _ _ (Fin.eq_of_val_eq eq)
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨n, ⋯⟩)
this : ⟨↑x, ⋯⟩ = ⟨n, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨n, ⋯⟩)
this : ⟨↑x, ⋯⟩ = ⟨n, ⋯⟩
⊢ x = y
Tactic:
simp at this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨n, ⋯⟩)
this : ↑x = n
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ↑(f x') < n
hy : ¬↑(f y') < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑(f ⟨n, ⋯⟩)
this : ↑x = n
⊢ x = y
Tactic:
exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
⊢ x = y
Tactic:
if hy : f y' < n then
  simp [f', hx, hy] at eq
  have := h _ _ (Fin.eq_of_val_eq eq)
  simp at this
  exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
else
  have eqx := Fin.eq_of_not_lt hx
  have eqy := Fin.eq_of_not_lt hy
  have : f x' = f y' := by rw [eqx, eqy]
  have : x' = y' := h _ _ this
  have : x.val = y.val := by
    have : x'.val = y'.val := by rw [this]
    exact this
  exact Fin.eq_of_val_eq this
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
⊢ x = y
Tactic:
simp [f', hx, hy] at eq
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨n, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨n, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
⊢ x = y
Tactic:
have := h _ _ (Fin.eq_of_val_eq eq)
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨n, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : ⟨n, ⋯⟩ = ⟨↑y, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨n, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : ⟨n, ⋯⟩ = ⟨↑y, ⋯⟩
⊢ x = y
Tactic:
simp at this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨n, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : n = ↑y
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ↑(f y') < n
eq : ↑(f ⟨n, ⋯⟩) = ↑(f ⟨↑y, ⋯⟩)
this : n = ↑y
⊢ x = y
Tactic:
exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
⊢ x = y
Tactic:
have eqx := Fin.eq_of_not_lt hx
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
⊢ x = y
Tactic:
have eqy := Fin.eq_of_not_lt hy
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
⊢ x = y
Tactic:
have : f x' = f y' := by rw [eqx, eqy]
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this : f x' = f y'
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this : f x' = f y'
⊢ x = y
Tactic:
have : x' = y' := h _ _ this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝ : f x' = f y'
this : x' = y'
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝ : f x' = f y'
this : x' = y'
⊢ x = y
Tactic:
have : x.val = y.val := by
  have : x'.val = y'.val := by rw [this]
  exact this
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝¹ : f x' = f y'
this✝ : x' = y'
this : ↑x = ↑y
⊢ x = y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝¹ : f x' = f y'
this✝ : x' = y'
this : ↑x = ↑y
⊢ x = y
Tactic:
exact Fin.eq_of_val_eq this
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
⊢ f x' = f y'
Tactic:
rw [eqx, eqy]
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝ : f x' = f y'
this : x' = y'
⊢ ↑x = ↑y
Tactic:
have : x'.val = y'.val := by rw [this]
State after:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝¹ : f x' = f y'
this✝ : x' = y'
this : ↑x' = ↑y'
⊢ ↑x = ↑y

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝¹ : f x' = f y'
this✝ : x' = y'
this : ↑x' = ↑y'
⊢ ↑x = ↑y
Tactic:
exact this
State after:
no goals

State before:
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → 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⟩
x y : Fin n
eq : f' x = f' y
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y' : Fin (n + 1) := ⟨↑y, ⋯⟩
hx : ¬↑(f x') < n
hy : ¬↑(f y') < n
eqx : f x' = ⟨n, ⋯⟩
eqy : f y' = ⟨n, ⋯⟩
this✝ : f x' = f y'
this : x' = y'
⊢ ↑x' = ↑y'
Tactic:
rw [this]
State after:
no goals

State before:
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
⊢ ∃ x, f x = y
Tactic:
let ⟨x, eq⟩ := surj ⟨y.val, isLt⟩
State after:
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
x : Fin n
eq : f' x = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y

State before:
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
x : Fin n
eq : f' x = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
Tactic:
simp [f'] at eq
State after:
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
x : Fin n
eq : (if h : ↑(f ⟨↑x, ⋯⟩) < n then ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ else ⟨↑(f ⟨n, ⋯⟩), ⋯⟩) = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y

State before:
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
x : Fin n
eq : (if h : ↑(f ⟨↑x, ⋯⟩) < n then ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ else ⟨↑(f ⟨n, ⋯⟩), ⋯⟩) = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
Tactic:
split at eq
State after:
case inl
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y

case inr
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y

State before:
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
Tactic:
case inl =>
  simp at eq
  exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, Fin.eq_of_val_eq eq⟩
State after:
no goals

State before:
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
Tactic:
case inr =>
  simp at eq
  exact ⟨n', Fin.eq_of_val_eq eq⟩
State after:
no goals

State before:
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
Tactic:
simp at eq
State after:
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑y
⊢ ∃ x, f x = y

State before:
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑y
⊢ ∃ x, f x = y
Tactic:
exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, Fin.eq_of_val_eq eq⟩
State after:
no goals

State before:
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
Tactic:
simp at eq
State after:
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨n, ⋯⟩) = ↑y
⊢ ∃ x, f x = y

State before:
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨n, ⋯⟩) = ↑y
⊢ ∃ x, f x = y
Tactic:
exact ⟨n', Fin.eq_of_val_eq eq⟩
State after:
no goals

State before:
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
⊢ ∃ x, f x = y
Tactic:
have := Fin.eq_of_not_lt isLt
State after:
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 = y

State before:
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 = y
Tactic:
simp [this]
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
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'⟩
State after:
no goals

State before:
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, f x = ⟨n, ⋯⟩
Tactic:
let ⟨x, eq⟩ := surj ⟨(f n').val, isLt'⟩
State after:
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
eq : f' x = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩

State before:
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
eq : f' x = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
simp [f'] at eq
State after:
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
eq : (if h : ↑(f ⟨↑x, ⋯⟩) < n then ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ else ⟨↑(f ⟨n, ⋯⟩), ⋯⟩) = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩

State before:
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
eq : (if h : ↑(f ⟨↑x, ⋯⟩) < n then ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ else ⟨↑(f ⟨n, ⋯⟩), ⋯⟩) = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
split at eq
State after:
case inl
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'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩

case inr
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 ⟨n, ⋯⟩), ⋯⟩ = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩

State before:
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'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
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 _)
State after:
no goals

State before:
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
nlt : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
case inr nlt =>
  have := Fin.eq_of_not_lt nlt
  exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, this⟩
State after:
no goals

State before:
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'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
simp at eq
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
have := Fin.val_eq_of_eq (h _ _ (Fin.eq_of_val_eq eq))
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
simp at this
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
State after:
no goals

State before:
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
nlt : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑(f n'), isLt'⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
have := Fin.eq_of_not_lt nlt
State after:
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
nlt : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑(f n'), isLt'⟩
this : f ⟨↑x, ⋯⟩ = ⟨n, ⋯⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩

State before:
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
nlt : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑(f n'), isLt'⟩
this : f ⟨↑x, ⋯⟩ = ⟨n, ⋯⟩
⊢ ∃ x, f x = ⟨n, ⋯⟩
Tactic:
exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, this⟩
State after:
no goals

State before:
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, f x = ⟨n, ⋯⟩
Tactic:
exact ⟨n', Fin.eq_of_not_lt isLt'⟩
State after:
no goals