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

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

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

State before:
c : CNF Nat
lit : Nat
hlit : mem lit c
h : List.filterMap Clause.maxLiteral c = []
⊢ False
Tactic:
dsimp [mem] at hlit
State after:
c : CNF Nat
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
h : List.filterMap Clause.maxLiteral c = []
⊢ False

State before:
c : CNF Nat
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
h : List.filterMap Clause.maxLiteral c = []
⊢ False
Tactic:
rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
State after:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ False

State before:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ False
Tactic:
have := Clause.of_maxLiteral_eq_none clause (List.all_none_of_filterMap_eq_nil h clause hclause1) lit
State after:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
this : ¬Clause.mem lit clause
⊢ False

State before:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
this : ¬Clause.mem lit clause
⊢ False
Tactic:
contradiction
State after:
no goals