internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ (pn//pd).denominator → pn//pd ≃ 1
Tactic:
intro (_ : pn ≃ pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ pd
⊢ pn//pd ≃ 1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ pd
⊢ pn//pd ≃ 1
Tactic:
show pn//pd ≃ 1//1
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ pd
⊢ pn//pd ≃ 1//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ pd
⊢ pn//pd ≃ 1//1
Tactic:
show pn * 1 ≃ 1 * pd
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ pd
⊢ pn * 1 ≃ 1 * pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ pd
⊢ pn * 1 ≃ 1 * pd
Tactic:
calc
  pn * 1 ≃ _ := AA.substL ‹pn ≃ pd›
  pd * 1 ≃ _ := AA.comm
  1 * pd ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.subst_neqv
Proof state before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Injective f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
⊢ x₁ ≄ x₂ → f x₁ ≄ f x₂
Tactic:
intro (_ : x₁ ≃ x₂ → False) (_ : f x₁ ≃ f x₂)
Proof state after:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Injective f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : x₁ ≃ x₂ → False
x✝ : f x₁ ≃ f x₂
⊢ False
Theorem: Lean4Axiomatic.AA.subst_neqv
Proof state before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Injective f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : x₁ ≃ x₂ → False
x✝ : f x₁ ≃ f x₂
⊢ False
Tactic:
apply ‹x₁ ≃ x₂ → False›
Proof state after:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Injective f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : x₁ ≃ x₂ → False
x✝ : f x₁ ≃ f x₂
⊢ x₁ ≃ x₂
Theorem: Lean4Axiomatic.AA.subst_neqv
Proof state before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Injective f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : x₁ ≃ x₂ → False
x✝ : f x₁ ≃ f x₂
⊢ x₁ ≃ x₂
Tactic:
exact inject ‹f x₁ ≃ f x₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.inject_neqv
Proof state before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
⊢ f x₁ ≄ f x₂ → x₁ ≄ x₂
Tactic:
intro (_ : f x₁ ≃ f x₂ → False) (_ : x₁ ≃ x₂)
Proof state after:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ False
Theorem: Lean4Axiomatic.AA.inject_neqv
Proof state before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ False
Tactic:
apply ‹f x₁ ≃ f x₂ → False›
Proof state after:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ f x₁ ≃ f x₂
Theorem: Lean4Axiomatic.AA.inject_neqv
Proof state before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ f x₁ ≃ f x₂
Tactic:
exact subst₁ ‹x₁ ≃ x₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.eqv_substL
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
⊢ x₁ ≃ x₂ → x₁ ≃ y → x₂ ≃ y
Tactic:
intro (_ : x₁ ≃ x₂) (_ : x₁ ≃ y)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝¹ : x₁ ≃ x₂
x✝ : x₁ ≃ y
⊢ x₂ ≃ y
Theorem: Lean4Axiomatic.AA.eqv_substL
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝¹ : x₁ ≃ x₂
x✝ : x₁ ≃ y
⊢ x₂ ≃ y
Tactic:
exact Rel.trans (Rel.symm ‹x₁ ≃ x₂›) ‹x₁ ≃ y›
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.eqv_substL_iff
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
⊢ x₁ ≃ x₂ → (x₁ ≃ y ↔ x₂ ≃ y)
Tactic:
intro (_ : x₁ ≃ x₂)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝ : x₁ ≃ x₂
⊢ x₁ ≃ y ↔ x₂ ≃ y
Theorem: Lean4Axiomatic.AA.eqv_substL_iff
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝ : x₁ ≃ x₂
⊢ x₁ ≃ y ↔ x₂ ≃ y
Tactic:
exact Iff.intro (eqv_substL ‹x₁ ≃ x₂›) (eqv_substL (Rel.symm ‹x₁ ≃ x₂›))
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.eqv_substR
Proof state before:
α : Sort u
inst✝ : EqvOp α
x y₁ y₂ : α
⊢ y₁ ≃ y₂ → x ≃ y₁ → x ≃ y₂
Tactic:
intro (_ : y₁ ≃ y₂) (_ : x ≃ y₁)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x y₁ y₂ : α
x✝¹ : y₁ ≃ y₂
x✝ : x ≃ y₁
⊢ x ≃ y₂
Theorem: Lean4Axiomatic.AA.eqv_substR
Proof state before:
α : Sort u
inst✝ : EqvOp α
x y₁ y₂ : α
x✝¹ : y₁ ≃ y₂
x✝ : x ≃ y₁
⊢ x ≃ y₂
Tactic:
exact Rel.trans ‹x ≃ y₁› ‹y₁ ≃ y₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.eqv_substR_iff
Proof state before:
α : Sort u
inst✝ : EqvOp α
x y₁ y₂ : α
⊢ y₁ ≃ y₂ → (x ≃ y₁ ↔ x ≃ y₂)
Tactic:
intro (_ : y₁ ≃ y₂)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x y₁ y₂ : α
x✝ : y₁ ≃ y₂
⊢ x ≃ y₁ ↔ x ≃ y₂
Theorem: Lean4Axiomatic.AA.eqv_substR_iff
Proof state before:
α : Sort u
inst✝ : EqvOp α
x y₁ y₂ : α
x✝ : y₁ ≃ y₂
⊢ x ≃ y₁ ↔ x ≃ y₂
Tactic:
exact Iff.intro (eqv_substR ‹y₁ ≃ y₂›) (eqv_substR (Rel.symm ‹y₁ ≃ y₂›))
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.neqv_substL
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
⊢ x₁ ≃ x₂ → x₁ ≄ y → x₂ ≄ y
Tactic:
intro (_ : x₁ ≃ x₂) (_ : x₁ ≄ y) (_ : x₂ ≃ y)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
⊢ False
Theorem: Lean4Axiomatic.AA.neqv_substL
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
⊢ False
Tactic:
have : x₁ ≃ y := Rel.trans ‹x₁ ≃ x₂› ‹x₂ ≃ y›
Proof state after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
this : x₁ ≃ y
⊢ False
Theorem: Lean4Axiomatic.AA.neqv_substL
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
this : x₁ ≃ y
⊢ False
Tactic:
exact absurd ‹x₁ ≃ y› ‹x₁ ≄ y›
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.neqv_substR
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
⊢ x₁ ≃ x₂ → y ≄ x₁ → y ≄ x₂
Tactic:
intro (_ : x₁ ≃ x₂) (_ : y ≄ x₁) (_ : y ≃ x₂)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : y ≄ x₁
x✝ : y ≃ x₂
⊢ False
Theorem: Lean4Axiomatic.AA.neqv_substR
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : y ≄ x₁
x✝ : y ≃ x₂
⊢ False
Tactic:
have : y ≃ x₁ := Rel.trans ‹y ≃ x₂› (Rel.symm ‹x₁ ≃ x₂›)
Proof state after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : y ≄ x₁
x✝ : y ≃ x₂
this : y ≃ x₁
⊢ False
Theorem: Lean4Axiomatic.AA.neqv_substR
Proof state before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : y ≄ x₁
x✝ : y ≃ x₂
this : y ≃ x₁
⊢ False
Tactic:
exact absurd ‹y ≃ x₁› ‹y ≄ x₁›
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.Prod.substL
Proof state before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : α
y : β
⊢ x₁ ≃ x₂ → (x₁, y) ≃ (x₂, y)
Tactic:
intro (_ : x₁ ≃ x₂)
Proof state after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : α
y : β
x✝ : x₁ ≃ x₂
⊢ (x₁, y) ≃ (x₂, y)
Theorem: Lean4Axiomatic.AA.Prod.substL
Proof state before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : α
y : β
x✝ : x₁ ≃ x₂
⊢ (x₁, y) ≃ (x₂, y)
Tactic:
apply eqv_defn.mpr
Proof state after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : α
y : β
x✝ : x₁ ≃ x₂
⊢ x₁ ≃ x₂ ∧ y ≃ y
Theorem: Lean4Axiomatic.AA.Prod.substL
Proof state before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : α
y : β
x✝ : x₁ ≃ x₂
⊢ x₁ ≃ x₂ ∧ y ≃ y
Tactic:
exact And.intro ‹x₁ ≃ x₂› Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.AA.Prod.substR
Proof state before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
⊢ x₁ ≃ x₂ → (y, x₁) ≃ (y, x₂)
Tactic:
intro (_ : x₁ ≃ x₂)
Proof state after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ (y, x₁) ≃ (y, x₂)
Theorem: Lean4Axiomatic.AA.Prod.substR
Proof state before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ (y, x₁) ≃ (y, x₂)
Tactic:
apply eqv_defn.mpr
Proof state after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ y ≃ y ∧ x₁ ≃ x₂
Theorem: Lean4Axiomatic.AA.Prod.substR
Proof state before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ y ≃ y ∧ x₁ ≃ x₂
Tactic:
exact And.intro Rel.refl ‹x₁ ≃ x₂›
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
h : captureNext.go nfa saveSize it current next saveSlots lastMatch = matched
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
unfold captureNext.go at h
Proof state after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h :
  (if it.atEnd = true then lastMatch
    else
      if (current.isEmpty && lastMatch.isSome) = true then lastMatch
      else
        let currentAndSaveSlots :=
          if lastMatch.isNone = true then
            let explored :=
              exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
            explored.2
          else (current, saveSlots);
        let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
        captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
          (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h :
  (if it.atEnd = true then lastMatch
    else
      if (current.isEmpty && lastMatch.isSome) = true then lastMatch
      else
        let currentAndSaveSlots :=
          if lastMatch.isNone = true then
            let explored :=
              exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
            explored.2
          else (current, saveSlots);
        let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
        captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
          (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
split at h
Proof state after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
next =>
  subst h
  exact eqs ▸ inv.acceptOfLastMatch
Proof state after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
subst h
Proof state after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
⊢ lastMatch.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
⊢ lastMatch.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact eqs ▸ inv.acceptOfLastMatch
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
split at h
Proof state after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : (current.isEmpty && lastMatch.isSome) = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done