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

State before:
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (lit : Nat), mem lit c → lit ≤ maxLit
Tactic:
intro lit hlit
State after:
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : mem lit c
⊢ lit ≤ maxLit

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

State before:
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
⊢ lit ≤ maxLit
Tactic:
rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
State after:
case intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ lit ≤ maxLit

State before:
case intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ lit ≤ maxLit
Tactic:
rcases Clause.maxLiteral_eq_some_of_mem clause hclause2 with ⟨localMax, hlocal⟩
State after:
case intro.intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
⊢ lit ≤ maxLit

State before:
case intro.intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
⊢ lit ≤ maxLit
Tactic:
have h1 := of_maxLiteral_eq_some' c h clause hclause1 hlocal
State after:
case intro.intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
⊢ lit ≤ maxLit

State before:
case intro.intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
⊢ lit ≤ maxLit
Tactic:
have h2 := Clause.of_maxLiteral_eq_some clause hlocal lit hclause2
State after:
case intro.intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
h2 : lit ≤ localMax
⊢ lit ≤ maxLit

State before:
case intro.intro.intro
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
h2 : lit ≤ localMax
⊢ lit ≤ maxLit
Tactic:
omega
State after:
no goals