Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le (Regex/NFA/Basic.lean)

State before:
size size' : Nat
n : Node
h : n.inBounds size
le : size ≤ size'
⊢ n.inBounds size'
Tactic:
simp [inBounds] at *
State after:
size size' : Nat
n : Node
h :
  match n with
  | done => True
  | fail => True
  | epsilon next => next < size
  | char c next => next < size
  | split next₁ next₂ => next₁ < size ∧ next₂ < size
  | save offset next => next < size
  | sparse cs next => next < size
le : size ≤ size'
⊢ match n with
  | done => True
  | fail => True
  | epsilon next => next < size'
  | char c next => next < size'
  | split next₁ next₂ => next₁ < size' ∧ next₂ < size'
  | save offset next => next < size'
  | sparse cs next => next < size'

State before:
size size' : Nat
n : Node
h :
  match n with
  | done => True
  | fail => True
  | epsilon next => next < size
  | char c next => next < size
  | split next₁ next₂ => next₁ < size ∧ next₂ < size
  | save offset next => next < size
  | sparse cs next => next < size
le : size ≤ size'
⊢ match n with
  | done => True
  | fail => True
  | epsilon next => next < size'
  | char c next => next < size'
  | split next₁ next₂ => next₁ < size' ∧ next₂ < size'
  | save offset next => next < size'
  | sparse cs next => next < size'
Tactic:
split <;> simp at h <;> try simp
State after:
case h_3
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

State before:
case h_3
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
State after:
case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

State before:
case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
State after:
case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

State before:
case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact ⟨Nat.lt_of_lt_of_le h.left le, Nat.lt_of_lt_of_le h.right le⟩
State after:
case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

State before:
case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
State after:
case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

State before:
case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
State after:
no goals

State before:
case h_2
size size' : Nat
le : size ≤ size'
x✝ : Node
h : True
⊢ True
Tactic:
simp
State after:
no goals

State before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
State after:
no goals

State before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
State after:
no goals

State before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'
Tactic:
exact ⟨Nat.lt_of_lt_of_le h.left le, Nat.lt_of_lt_of_le h.right le⟩
State after:
no goals

State before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
State after:
no goals

State before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
State after:
no goals