Theorem: CNF.lt_numLiterals (LeanSAT/Reflect/CNF/Decidable.lean)

State before:
a : Nat
g : CNF Nat
h : mem a g
⊢ a < g.numLiterals
Tactic:
dsimp[numLiterals]
State after:
a : Nat
g : CNF Nat
h : mem a g
⊢ a <
    match g.maxLiteral with
    | none => 0
    | some n => n + 1

State before:
a : Nat
g : CNF Nat
h : mem a g
⊢ a <
    match g.maxLiteral with
    | none => 0
    | some n => n + 1
Tactic:
split <;> rename_i h2
State after:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ a < 0

case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1

State before:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ a < 0

case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Tactic:
. exfalso
  apply of_maxLiteral_eq_none g h2 a h
State after:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1

State before:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Tactic:
. have := of_maxLiteral_eq_some g h2 a h
  omega
State after:
no goals

State before:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ a < 0
Tactic:
exfalso
State after:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ False

State before:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ False
Tactic:
apply of_maxLiteral_eq_none g h2 a h
State after:
no goals

State before:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Tactic:
have := of_maxLiteral_eq_some g h2 a h
State after:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
this : a ≤ n✝
⊢ a < n✝ + 1

State before:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
this : a ≤ n✝
⊢ a < n✝ + 1
Tactic:
omega
State after:
no goals