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

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

State before:
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : mem lit c
⊢ lit ≤ maxLit
Tactic:
simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h
State after:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : mem lit c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

State before:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : mem lit c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit
Tactic:
simp only [mem] at hlit
State after:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

State before:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit
Tactic:
rcases h with ⟨_, hbar⟩
State after:
case intro
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

State before:
case intro
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit
Tactic:
cases hlit
State after:
case intro.inl
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, false) ∈ c
⊢ lit ≤ maxLit

case intro.inr
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ lit ≤ maxLit

State before:
case intro.inl
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, false) ∈ c
⊢ lit ≤ maxLit

case intro.inr
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ lit ≤ maxLit
Tactic:
all_goals
  have := hbar (lit, _) (by assumption)
  omega
State after:
no goals

State before:
case intro.inr
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ lit ≤ maxLit
Tactic:
have := hbar (lit, _) (by assumption)
State after:
case intro.inr
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
this : (lit, true).fst ≤ maxLit
⊢ lit ≤ maxLit

State before:
case intro.inr
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
this : (lit, true).fst ≤ maxLit
⊢ lit ≤ maxLit
Tactic:
omega
State after:
no goals

State before:
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ (lit, ?m.863) ∈ c
Tactic:
assumption
State after:
no goals