internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
⊢ (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
Tactic:
apply rest.cast' (nfa''.val.start.isLt) (Nat.le_of_lt nfa'''.property)
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
⊢ ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa'').nodes.size), (↑nfa'')[i] = (↑nfa''')[i]
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
⊢ ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa'').nodes.size), (↑nfa'')[i] = (↑nfa''')[i]
Tactic:
intro i _ h₂
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i✝ r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i✝) ↑(↑nfa'').start
h₁✝¹ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa'').nodes.size
⊢ (↑nfa'')[i] = (↑nfa''')[i]
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i✝ r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i✝) ↑(↑nfa'').start
h₁✝¹ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa'').nodes.size
⊢ (↑nfa'')[i] = (↑nfa''')[i]
Tactic:
rw [eq₃, pushNode_get_lt _ h₂]
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step.εStep.base
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
cs₂✝ cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs✝ : cs = [] ++ cs₂ ++ cs₂✝
cs₃ : List Char
path' : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₃
h✝ : nfa.nodes.size ≤ ↑(↑nfa').start
step : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa').start) (↑next) cs₂✝
heq : ↑(↑nfa').start = nfa.nodes.size ∧ cs₂✝ = []
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) (↑(↑nfa').start) cs₂
this : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) (↑(↑nfa').start) cs₂
eqs : cs₂ = cs₃
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₂
Tactic:
exact eqs ▸ path'
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step.εStep.step
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝¹ : List Char
step✝ : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝¹
heq : i' = nfa.nodes.size ∧ cs₂✝¹ = []
cs₂ : List Char
eqStart✝ : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs✝ : cs = [] ++ cs₂ ++ cs₂✝¹
rest✝ : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
this✝¹ : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
cs₃ : List Char
path' : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₃
cs₁✝ cs₂✝ : List Char
eqs : cs₂ = cs₃ ++ (cs₁✝ ++ cs₂✝)
this✝ : ↑(↑nfa').start < (↑nfa'').nodes.size
eqStart : (↑nfa'')[↑(↑nfa').start] = Node.save (2 * i + 1) ↑next
step : (↑nfa'').stepIn nfa.nodes.size (↑(↑nfa').start) (↑next) cs₁✝
rest : (↑nfa'').pathIn nfa.nodes.size (↑next) i' cs₂✝
this : nfa.nodes.size ≤ ↑next
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₂
Tactic:
exact (Nat.lt_irrefl _ (Nat.lt_of_le_of_lt this next.isLt)).elim
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝¹ : List Char
step✝ : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝¹
heq : i' = nfa.nodes.size ∧ cs₂✝¹ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs✝ : cs = [] ++ cs₂ ++ cs₂✝¹
rest✝ : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
this✝ : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
cs₃ : List Char
path' : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₃
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : (↑nfa'').stepIn nfa.nodes.size (↑(↑nfa').start) j✝ cs₁✝
rest : (↑nfa'').pathIn nfa.nodes.size j✝ i' cs₂✝
eqs : cs₂ = cs₃ ++ (cs₁✝ ++ cs₂✝)
this : ↑(↑nfa').start < (↑nfa'').nodes.size
⊢ (↑(nfa.pushNode (Node.save (2 * i + 1) ↑next)
          inBounds'✝))[↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start] =
    Node.save (2 * i + 1) ↑next
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
apply pushRegex.alternate eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
⊢ ∀ (nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa').nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → Expr.matches cs (r₁.alternate r₂)
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
⊢ ∀ (nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa').nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → Expr.matches cs (r₁.alternate r₂)
Tactic:
intro nfa₁ start₁ nfa₂ start₂ inBounds final property eq₁ eq₂ eq₃ eq₄ eq₅ eq'
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
⊢ Expr.matches cs (r₁.alternate r₂)
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
rw [eq'] at path
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
path : (↑⟨↑final, property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑final, property⟩).start) cs
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
⊢ Expr.matches cs (r₁.alternate r₂)