-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) :
    ∀ lit, Mem lit c → lit ≤ maxLit

Proof state:
case intro.inl
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Literal Nat), 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 : Literal Nat), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ lit ≤ maxLit

Tactic:
all_goals
  have := hbar (lit, _) (by assumption)
  omega

Result:
no goals

Proof state:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : Mem lit c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Literal Nat), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

Tactic:
simp only [Mem] at hlit

Result:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Literal Nat), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

Proof state:
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (lit : Nat), Mem lit c → lit ≤ maxLit

Tactic:
intro lit hlit

Result:
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : Mem lit c
⊢ lit ≤ maxLit

Proof state:
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : Mem lit c
⊢ lit ≤ maxLit

Tactic:
simp only [maxLiteral, List.max?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂] at h

Result:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : Mem lit c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Literal Nat), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

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

Tactic:
have := hbar (lit, _) (by assumption)

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

Proof state:
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Literal Nat), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

Tactic:
rcases h with ⟨_, hbar⟩

Result:
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 : Literal Nat), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

Proof state:
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Literal Nat), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ (lit, ?m.864) ∈ c

Tactic:
assumption

Result:
no goals

Proof state:
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 : Literal Nat), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit

Tactic:
cases hlit

Result:
case intro.inl
maxLit : Nat
c : Clause Nat
lit : Nat
left✝ : ∃ a, a ∈ c ∧ a.fst = maxLit
hbar : ∀ (a : Literal Nat), 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 : Literal Nat), a ∈ c → a.fst ≤ maxLit
h✝ : (lit, true) ∈ c
⊢ lit ≤ maxLit

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

Tactic:
omega

Result:
no goals