internlm/Lean-Github huggingface dataset:
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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]
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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'⟩
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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'⟩
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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 _)
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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⟩
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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))
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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 _)
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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, ⋯⟩
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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⟩
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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'⟩
Proof state after:
no goals
Theorem: Array.isEmpty_iff
Proof state before:
α : Type u_1
a : Array α
⊢ a.isEmpty = true ↔ a = #[]
Tactic:
simp [Array.isEmpty]
Proof state after:
α : Type u_1
a : Array α
⊢ a.data = [] ↔ a = #[]
Theorem: Array.isEmpty_iff
Proof state before:
α : Type u_1
a : Array α
⊢ a.data = [] ↔ a = #[]
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
a : Array α
⊢ a.data = [] → a = #[]

case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Theorem: Array.isEmpty_iff
Proof state before:
case mp
α : Type u_1
a : Array α
⊢ a.data = [] → a = #[]

case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Tactic:
. exact ext'
Proof state after:
case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Theorem: Array.isEmpty_iff
Proof state before:
case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Tactic:
. intro h
  simp [h]
Proof state after:
no goals
Theorem: Array.isEmpty_iff
Proof state before:
case mp
α : Type u_1
a : Array α
⊢ a.data = [] → a = #[]
Tactic:
exact ext'
Proof state after:
no goals
Theorem: Array.isEmpty_iff
Proof state before:
case mpr
α : Type u_1
a : Array α
⊢ a = #[] → a.data = []
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
a : Array α
h : a = #[]
⊢ a.data = []
Theorem: Array.isEmpty_iff
Proof state before:
case mpr
α : Type u_1
a : Array α
h : a = #[]
⊢ a.data = []
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Array.mem_back'
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.back' hemp ∈ a
Tactic:
simp [back', Array.mem_def, Array.getElem_eq_data_get]
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.data.get ⟨a.size - 1, ⋯⟩ ∈ a.data
Theorem: Array.mem_back'
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.data.get ⟨a.size - 1, ⋯⟩ ∈ a.data
Tactic:
apply List.get_mem
Proof state after:
no goals
Theorem: Array.mem_push
Proof state before:
α : Type u_1
a : Array α
x y : α
⊢ y ∈ a.push x ↔ y ∈ a ∨ y = x
Tactic:
unfold Array.push
Proof state after:
α : Type u_1
a : Array α
x y : α
⊢ y ∈ { data := a.data.concat x } ↔ y ∈ a ∨ y = x
Theorem: Array.mem_push
Proof state before:
α : Type u_1
a : Array α
x y : α
⊢ y ∈ { data := a.data.concat x } ↔ y ∈ a ∨ y = x
Tactic:
simp [Array.mem_def]
Proof state after:
no goals
Theorem: Array.mem_of_push
Proof state before:
α : Type u_1
a : Array α
x : α
⊢ x ∈ a.push x
Tactic:
simp [Array.mem_def]
Proof state after:
no goals
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.pop.push (a.back' hemp) = a
Tactic:
have : 0 < a.size := zero_lt_size_of_not_empty hemp
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.push (a.back' hemp) = a
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.push (a.back' hemp) = a
Tactic:
apply Array.ext
Proof state after:
case h₁
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ (a.pop.push (a.back' hemp)).size = a.size

case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Theorem: Array.push_pop_eq
Proof state before:
case h₁
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ (a.pop.push (a.back' hemp)).size = a.size

case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
. simp [Nat.sub_add_cancel this]
Proof state after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Theorem: Array.push_pop_eq
Proof state before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
. simp [Nat.sub_add_cancel this]
  intro i h _
  rw [Array.get_push]
  split
  case inl h' => rw [Array.getElem_pop]
  case inr h' =>
    simp at h'
    have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
    simp at this
    have : i = a.size - 1 := Nat.le_antisymm this h'
    simp [back', this]
Proof state after:
no goals
Theorem: Array.push_pop_eq
Proof state before:
case h₁
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ (a.pop.push (a.back' hemp)).size = a.size
Tactic:
simp [Nat.sub_add_cancel this]
Proof state after:
no goals
Theorem: Array.push_pop_eq
Proof state before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
simp [Nat.sub_add_cancel this]
Proof state after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Theorem: Array.push_pop_eq
Proof state before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
intro i h _
Proof state after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (a.pop.push (a.back' hemp))[i] = a[i]
Theorem: Array.push_pop_eq
Proof state before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (a.pop.push (a.back' hemp))[i] = a[i]
Tactic:
rw [Array.get_push]
Proof state after:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (if h : i < a.pop.size then a.pop[i] else a.back' hemp) = a[i]
Theorem: Array.push_pop_eq
Proof state before:
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
⊢ (if h : i < a.pop.size then a.pop[i] else a.back' hemp) = a[i]
Tactic:
split
Proof state after:
case h₂.inl
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h✝ : i < a.pop.size
⊢ a.pop[i] = a[i]

case h₂.inr
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h✝ : ¬i < a.pop.size
⊢ a.back' hemp = a[i]
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : i < a.pop.size
⊢ a.pop[i] = a[i]
Tactic:
case inl h' => rw [Array.getElem_pop]
Proof state after:
no goals
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : ¬i < a.pop.size
⊢ a.back' hemp = a[i]
Tactic:
case inr h' =>
  simp at h'
  have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
  simp at this
  have : i = a.size - 1 := Nat.le_antisymm this h'
  simp [back', this]
Proof state after:
no goals
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : i < a.pop.size
⊢ a.pop[i] = a[i]
Tactic:
rw [Array.getElem_pop]
Proof state after:
no goals
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : ¬i < a.pop.size
⊢ a.back' hemp = a[i]
Tactic:
simp at h'
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
⊢ a.back' hemp = a[i]
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
⊢ a.back' hemp = a[i]
Tactic:
have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i + 1 - 1 ≤ a.size - 1
⊢ a.back' hemp = a[i]
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i + 1 - 1 ≤ a.size - 1
⊢ a.back' hemp = a[i]
Tactic:
simp at this
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i ≤ a.size - 1
⊢ a.back' hemp = a[i]