internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
i : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → ∀ (h : i < nfa.nodes.size), (↑result)[i] = nfa[i]
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h : i < nfa.nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
ih : (↑compiled)[i] = (↑placeholder)[i]
this : i < (↑compiled).nodes.size
⊢ ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i] = nfa[i]
Tactic:
rw [Array.get_set (hj := this)]
Proof state after:
i : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → ∀ (h : i < nfa.nodes.size), (↑result)[i] = nfa[i]
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h : i < nfa.nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
ih : (↑compiled)[i] = (↑placeholder)[i]
this : i < (↑compiled).nodes.size
⊢ (if ↑⟨nfa.nodes.size, ⋯⟩ = i then Node.split ↑(↑compiled).start ↑next else (↑compiled).nodes[i]) = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
i : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → ∀ (h : i < nfa.nodes.size), (↑result)[i] = nfa[i]
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h : i < nfa.nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
ih : (↑compiled)[i] = (↑placeholder)[i]
this : i < (↑compiled).nodes.size
⊢ (if ↑⟨nfa.nodes.size, ⋯⟩ = i then Node.split ↑(↑compiled).start ↑next else (↑compiled).nodes[i]) = nfa[i]
Tactic:
have : nfa.nodes.size ≠ i := Nat.ne_of_gt h
Proof state after:
i : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → ∀ (h : i < nfa.nodes.size), (↑result)[i] = nfa[i]
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h : i < nfa.nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
ih : (↑compiled)[i] = (↑placeholder)[i]
this✝ : i < (↑compiled).nodes.size
this : nfa.nodes.size ≠ i
⊢ (if ↑⟨nfa.nodes.size, ⋯⟩ = i then Node.split ↑(↑compiled).start ↑next else (↑compiled).nodes[i]) = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
i : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → ∀ (h : i < nfa.nodes.size), (↑result)[i] = nfa[i]
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h : i < nfa.nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
ih : (↑compiled)[i] = (↑placeholder)[i]
this✝ : i < (↑compiled).nodes.size
this : nfa.nodes.size ≠ i
⊢ (if ↑⟨nfa.nodes.size, ⋯⟩ = i then Node.split ↑(↑compiled).start ↑next else (↑compiled).nodes[i]) = nfa[i]
Tactic:
simp [this, ←get_eq_nodes_get, ih, eq₁, pushNode_get_lt _ h]
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
induction r generalizing nfa next with
| empty =>
  apply pushRegex.empty eq
  intro eq
  subst eq
  simp
| epsilon =>
  apply pushRegex.epsilon eq
  intro eq
  subst eq
  simp
| char c =>
  apply pushRegex.char eq
  intro eq
  subst eq
  simp
| classes c =>
  apply pushRegex.sparse eq
  intro eq
  subst eq
  simp
| group =>
  apply pushRegex.group eq
  intro nfa' nfa'' nfa''' property _ _ _ _ eq₃ eq
  rw [eq]
  simp
  rw [eq₃]
  simp
  apply Nat.le_of_lt (Nat.lt_trans nfa'.property nfa''.property)
| alternate r₁ r₂ =>
  apply pushRegex.alternate eq
  intro nfa₁ _ nfa₂ _ _ _ _ _ _ _ _ eq₅ eq
  rw [eq]
  simp
  rw [eq₅]
  simp [pushNode]
  exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
| concat r₁ r₂ ih₁ =>
  apply pushRegex.concat eq
  intro nfa₂ nfa₁ _ _ eq₁ eq
  rw [eq]
  simp
  exact Nat.le_trans (Nat.le_of_lt nfa₂.property) (ih₁ eq₁.symm)
| star r =>
  apply pushRegex.star eq
  intro _ _ _ nfa' _ _ _ _ _ _ eq₄ eq
  rw [eq]
  simp
  rw [eq₄]
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case empty
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.empty eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
⊢ result = nfa.pushNode Node.fail ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
⊢ result = nfa.pushNode Node.fail ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode Node.fail ⋯)).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode Node.fail ⋯)).start
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case epsilon
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.epsilon eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.epsilon = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.epsilon = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.char eq
Proof state after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = result
⊢ result = nfa.pushNode (Node.char c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = result
⊢ result = nfa.pushNode (Node.char c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
Proof state after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
Proof state after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case classes
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes c) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.sparse eq
Proof state after:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes c) = result
⊢ result = nfa.pushNode (Node.sparse c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes c) = result
⊢ result = nfa.pushNode (Node.sparse c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
Proof state after:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes c) = result
eq : result = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes c) = result
eq : result = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
Proof state after:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes c) = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.sparse c ↑next) ⋯)).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes c) = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.sparse c ↑next) ⋯)).start
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case group
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.group eq
Proof state after:
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ ∀ (nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size })
    (nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * a✝¹ + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * a✝¹) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa' = nfa.pushNode (Node.save (2 * a✝¹ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start a✝ →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝¹) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ ∀ (nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size })
    (nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * a✝¹ + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * a✝¹) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa' = nfa.pushNode (Node.save (2 * a✝¹ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start a✝ →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝¹) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro nfa' nfa'' nfa''' property _ _ _ _ eq₃ eq
Proof state after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
Proof state after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa''', property⟩).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa''', property⟩).start
Tactic:
simp
Proof state after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa''').start