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

State before:
maxLit localMax : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (clause : Clause Nat), clause ∈ c → clause.maxLiteral = some localMax → localMax ≤ maxLit
Tactic:
intro clause hclause1 hclause2
State after:
maxLit localMax : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
⊢ localMax ≤ maxLit

State before:
maxLit localMax : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
⊢ localMax ≤ maxLit
Tactic:
simp[maxLiteral, List.maximum?_eq_some_iff'] at h
State after:
maxLit localMax : Nat
c : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
h : (∃ a, a ∈ c ∧ a.maxLiteral = some maxLit) ∧ ∀ (b : Nat) (x : Clause Nat), x ∈ c → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit

State before:
maxLit localMax : Nat
c : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
h : (∃ a, a ∈ c ∧ a.maxLiteral = some maxLit) ∧ ∀ (b : Nat) (x : Clause Nat), x ∈ c → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit
Tactic:
rcases h with ⟨_, hclause3⟩
State after:
case intro
maxLit localMax : Nat
c : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
left✝ : ∃ a, a ∈ c ∧ a.maxLiteral = some maxLit
hclause3 : ∀ (b : Nat) (x : Clause Nat), x ∈ c → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit

State before:
case intro
maxLit localMax : Nat
c : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
left✝ : ∃ a, a ∈ c ∧ a.maxLiteral = some maxLit
hclause3 : ∀ (b : Nat) (x : Clause Nat), x ∈ c → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit
Tactic:
apply hclause3 localMax clause hclause1 hclause2
State after:
no goals