internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
⊢ ∀ (i : ℕ) (isLt : i < (↑⟨↑nfa', property⟩).nodes.size), (↑⟨↑nfa', property⟩)[i] = Node.done ↔ i = 0
Tactic:
simp
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
⊢ ∀ (i : ℕ) (isLt : i < (↑nfa').nodes.size), (↑nfa')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
⊢ ∀ (i : ℕ) (isLt : i < (↑nfa').nodes.size), (↑nfa')[i] = Node.done ↔ i = 0
Tactic:
intro i isLt
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
i : ℕ
isLt : i < (↑nfa').nodes.size
⊢ (↑nfa')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
i : ℕ
isLt : i < (↑nfa').nodes.size
⊢ (↑nfa')[i] = Node.done ↔ i = 0
Tactic:
simp [eq₅] at isLt
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
i : ℕ
isLt✝ : i < (↑nfa').nodes.size
isLt : i < (↑nfa₂).nodes.size + 1
⊢ (↑nfa')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
i : ℕ
isLt✝ : i < (↑nfa').nodes.size
isLt : i < (↑nfa₂).nodes.size + 1
⊢ (↑nfa')[i] = Node.done ↔ i = 0
Tactic:
cases Nat.eq_or_lt_of_le isLt with
| inl eq =>
  simp at eq
  simp [eq₅, eq, -List.length_eq_zero]
  exact Nat.ne_of_gt (Nat.zero_lt_of_lt nfa₂.property)
| inr lt =>
  have lt := Nat.lt_of_succ_lt_succ lt
  simp [eq₅, pushNode_get_lt _ lt]
  apply ih₂ eq₃.symm (Nat.zero_lt_of_lt nfa₁.property) ?_ i lt
  intro i isLt
  apply ih₁ eq₁.symm (Nat.zero_lt_of_lt h₁) h₂ i isLt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inl
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
i : ℕ
isLt✝ : i < (↑nfa').nodes.size
isLt : i < (↑nfa₂).nodes.size + 1
eq : i = (↑nfa₂).nodes.size
⊢ ¬(↑nfa₂).nodes.size = 0
Tactic:
exact Nat.ne_of_gt (Nat.zero_lt_of_lt nfa₂.property)
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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
eq₁ : nfa₁ = nfa.pushRegex next r₁
a✝¹ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa.pushRegex next (r₁.alternate r₂) = ⟨↑nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < (↑nfa').nodes.size
isLt✝ : i✝ < (↑nfa₂).nodes.size + 1
lt✝ : i✝.succ < (↑nfa₂).nodes.size + 1
lt : i✝ < (↑nfa₂).nodes.size
i : ℕ
isLt : i < (↑nfa₁).nodes.size
⊢ (↑nfa₁)[i] = Node.done ↔ i = 0
Tactic:
apply ih₁ eq₁.symm (Nat.zero_lt_of_lt h₁) h₂ i isLt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case concat
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
⊢ ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
Tactic:
apply pushRegex.concat eq
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
⊢ ∀ (nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size })
    (property : nfa.nodes.size < (↑nfa₁).nodes.size),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ →
        result = ⟨↑nfa₁, property⟩ → ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
⊢ ∀ (nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size })
    (property : nfa.nodes.size < (↑nfa₁).nodes.size),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ →
        result = ⟨↑nfa₁, property⟩ → ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
Tactic:
intro nfa₂ nfa₁ property eq₂ eq₁ eq
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property⟩
⊢ ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property⟩
⊢ ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
Tactic:
subst eq
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa.pushRegex next (r₁.concat r₂) = ⟨↑nfa₁, property⟩
⊢ ∀ (i : ℕ) (isLt : i < (↑⟨↑nfa₁, property⟩).nodes.size), (↑⟨↑nfa₁, property⟩)[i] = Node.done ↔ i = 0