Theorem: CNF.Clause.of_maxLiteral_eq_none (LeanSAT/Reflect/CNF/Decidable.lean)

State before:
c : Clause Nat
h : c.maxLiteral = none
⊢ ∀ (lit : Nat), ¬mem lit c
Tactic:
intro lit hlit
State after:
c : Clause Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False

State before:
c : Clause Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False
Tactic:
simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil] at h
State after:
c : Clause Nat
lit : Nat
hlit : mem lit c
h : c = []
⊢ False

State before:
c : Clause Nat
lit : Nat
hlit : mem lit c
h : c = []
⊢ False
Tactic:
simp only [h, not_mem_nil] at hlit
State after:
no goals