Theorem: Regex.NFA.Node.lt_of_inBounds.split (Regex/NFA/Basic.lean)

State before:
size next₁ next₂ : Nat
h : (Node.split next₁ next₂).inBounds size
⊢ next₁ < size ∧ next₂ < size
Tactic:
simp [inBounds] at h
State after:
size next₁ next₂ : Nat
h : next₁ < size ∧ next₂ < size
⊢ next₁ < size ∧ next₂ < size

State before:
size next₁ next₂ : Nat
h : next₁ < size ∧ next₂ < size
⊢ next₁ < size ∧ next₂ < size
Tactic:
exact h
State after:
no goals