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

State before:
l : Nat
c : Clause Nat
h : mem l c
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Tactic:
dsimp[mem] at h
State after:
l : Nat
c : Clause Nat
h : (l, false) ∈ c ∨ (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

State before:
l : Nat
c : Clause Nat
h : (l, false) ∈ c ∨ (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Tactic:
cases h <;> rename_i h
State after:
case inl
l : Nat
c : Clause Nat
h : (l, false) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

State before:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Tactic:
have h1 := List.ne_nil_of_mem h
State after:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
⊢ ∃ maxLit, c.maxLiteral = some maxLit

State before:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
h2 : ¬(List.map (fun x => x.fst) c).maximum? = none ↔ ¬List.map (fun x => x.fst) c = []
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Tactic:
simp[← Option.ne_none_iff_exists', h1, h2, maxLiteral]
State after:
no goals