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 → 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
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 → 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
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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)
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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 _)
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 → 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
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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]
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
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 → 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]
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 → 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]
Proof 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
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof 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
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 → 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]
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
⊢ ∃ x, f x = y
Tactic:
let ⟨x, eq⟩ := surj ⟨y.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
x : Fin n
eq : f' x = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
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
x : Fin n
eq : f' x = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
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
x : Fin n
eq : (if h : ↑(f ⟨↑x, ⋯⟩) < n then ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ else ⟨↑(f ⟨n, ⋯⟩), ⋯⟩) = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
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
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
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
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
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
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⟩
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
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⟩
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
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
x : Fin n
h✝ : ↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨↑x, ⋯⟩) = ↑y
⊢ ∃ x, f x = y
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
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⟩
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ⟨↑(f ⟨n, ⋯⟩), ⋯⟩ = ⟨↑y, isLt⟩
⊢ ∃ x, f x = y
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨n, ⋯⟩) = ↑y
⊢ ∃ x, f x = y
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
x : Fin n
h✝ : ¬↑(f ⟨↑x, ⋯⟩) < n
eq : ↑(f ⟨n, ⋯⟩) = ↑y
⊢ ∃ x, f x = y
Tactic:
exact ⟨n', Fin.eq_of_val_eq eq⟩
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
⊢ ∃ x, f x = y
Tactic:
have := Fin.eq_of_not_lt 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, ⋯⟩
⊢ ∃ x, f x = y