internlm/Lean-Github huggingface dataset:
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h✝ : ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ⋯ } }, assign⟧ = true
h : ⟦{ aig := aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ?mp } }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true

case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ⋯ } }, assign⟧ = true
⊢ (s.getRef idx hidx).gate < aig.decls.size
Tactic:
rw [← h]
Proof state after:
no goals
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ (∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true) →
    ∀ (idx : Nat) (hidx1 : idx < len),
      ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx1).gate, hgate := ⋯ } }, assign⟧ = true
Tactic:
intro h idx hidx
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
h : ∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
idx : Nat
hidx : idx < len
⊢ ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ⋯ } }, assign⟧ = true
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
h : ∀ (idx : Nat) (hidx : idx < len), ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
idx : Nat
hidx : idx < len
⊢ ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ⋯ } }, assign⟧ = true
Tactic:
specialize h idx hidx
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ⋯ } }, assign⟧ = true
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ ⟦{ aig := (aig.mkConstCached true).aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ⋯ } }, assign⟧ = true
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)]
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ?mpr } }, assign⟧ = true

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ (s.getRef idx hidx).gate < aig.decls.size
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ?mpr } }, assign⟧ = true

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ (s.getRef idx hidx).gate < aig.decls.size
Tactic:
. simp only [← h]
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ (s.getRef idx hidx).gate < aig.decls.size
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ (s.getRef idx hidx).gate < aig.decls.size
Tactic:
. apply RefStream.hrefs
  simp [FoldTarget.mkAnd, hidx]
Proof state after:
no goals
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ ⟦{ aig := aig, ref := { gate := (s.getRef idx hidx).gate, hgate := ?mpr } }, assign⟧ = true
Tactic:
simp only [← h]
Proof state after:
no goals
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ (s.getRef idx hidx).gate < aig.decls.size
Tactic:
apply RefStream.hrefs
Proof state after:
case mpr.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ idx < len
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case mpr.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
idx : Nat
hidx : idx < len
h : ⟦{ aig := aig, ref := s.getRef idx hidx }, assign⟧ = true
⊢ idx < len
Tactic:
simp [FoldTarget.mkAnd, hidx]
Proof state after:
no goals
Theorem: AIG.RefStream.denote_fold_and
Proof state before:
case hcurr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefStream len
⊢ 0 ≤ len
Tactic:
omega
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1733
Proof state before:
⊢ ∀ (A B : BitVec 64), (A != 0) = true ∨ (B != 0) = (A ||| B != 0)
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ != 0) = true ∨ (B✝ != 0) = (A✝ ||| B✝ != 0)
Theorem: bitvec_AndOrXor_1733
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ != 0) = true ∨ (B✝ != 0) = (A✝ ||| B✝ != 0)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof state before:
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (lit : Nat), mem lit c → lit ≤ maxLit
Tactic:
intro lit hlit
Proof state after:
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : mem lit c
⊢ lit ≤ maxLit
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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
Proof 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
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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
Proof 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
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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⟩
Proof 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
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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
Proof 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
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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
Proof state after:
no goals
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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)
Proof 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
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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
Proof state after:
no goals
Theorem: CNF.Clause.of_maxLiteral_eq_some
Proof 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
Proof state after:
no goals
Theorem: CNF.Clause.maxLiteral_eq_some_of_mem
Proof state before:
l : Nat
c : Clause Nat
h : mem l c
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Tactic:
dsimp[mem] at h
Proof state after:
l : Nat
c : Clause Nat
h : (l, false) ∈ c ∨ (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Theorem: CNF.Clause.maxLiteral_eq_some_of_mem
Proof 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
Proof 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
Theorem: CNF.Clause.maxLiteral_eq_some_of_mem
Proof 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
Proof state after:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
⊢ ∃ maxLit, c.maxLiteral = some maxLit
Theorem: CNF.Clause.maxLiteral_eq_some_of_mem
Proof 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]
Proof state after:
no goals
Theorem: CNF.Clause.of_maxLiteral_eq_none
Proof state before:
c : Clause Nat
h : c.maxLiteral = none
⊢ ∀ (lit : Nat), ¬mem lit c
Tactic:
intro lit hlit
Proof state after:
c : Clause Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False
Theorem: CNF.Clause.of_maxLiteral_eq_none
Proof state before:
c : Clause Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False
Tactic:
simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil] at h
Proof state after:
c : Clause Nat
lit : Nat
hlit : mem lit c
h : c = []
⊢ False
Theorem: CNF.Clause.of_maxLiteral_eq_none
Proof state before:
c : Clause Nat
lit : Nat
hlit : mem lit c
h : c = []
⊢ False
Tactic:
simp only [h, not_mem_nil] at hlit
Proof state after:
no goals
Theorem: CNF.of_maxLiteral_eq_some'
Proof 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
Proof 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
Theorem: CNF.of_maxLiteral_eq_some'
Proof 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
Proof 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
Theorem: CNF.of_maxLiteral_eq_some'
Proof 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⟩
Proof 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
Theorem: CNF.of_maxLiteral_eq_some'
Proof 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
Proof state after:
no goals
Theorem: CNF.of_maxLiteral_eq_some
Proof state before:
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (lit : Nat), mem lit c → lit ≤ maxLit
Tactic:
intro lit hlit
Proof state after:
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : mem lit c
⊢ lit ≤ maxLit
Theorem: CNF.of_maxLiteral_eq_some
Proof 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
Proof 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
Theorem: CNF.of_maxLiteral_eq_some
Proof 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⟩⟩
Proof 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
Theorem: CNF.of_maxLiteral_eq_some
Proof 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⟩
Proof 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
Theorem: CNF.of_maxLiteral_eq_some
Proof 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
Proof 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
Theorem: CNF.of_maxLiteral_eq_some
Proof 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
Proof 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
Theorem: CNF.of_maxLiteral_eq_some
Proof 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
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
⊢ ∀ (x : α✝¹), x ∈ xs → f x = none
Tactic:
intro x hx
Proof state after:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
x : α✝¹
hx : x ∈ xs
⊢ f x = none
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
x : α✝¹
hx : x ∈ xs
⊢ f x = none
Tactic:
induction xs with
| nil => contradiction
| cons y ys ih =>
  simp [List.filterMap] at h
  split at h
  . cases hx with
    | head => assumption
    | tail _ hmem => exact ih h hmem
  . contradiction
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case nil
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
h : List.filterMap f [] = []
hx : x ∈ []
⊢ f x = none
Tactic:
contradiction
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
h : List.filterMap f (y :: ys) = []
hx : x ∈ y :: ys
⊢ f x = none
Tactic:
simp [List.filterMap] at h
Proof state after:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
h :
  (match f y with
    | none => List.filterMap f ys
    | some b => b :: List.filterMap f ys) =
    []
hx : x ∈ y :: ys
⊢ f x = none
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
h :
  (match f y with
    | none => List.filterMap f ys
    | some b => b :: List.filterMap f ys) =
    []
hx : x ∈ y :: ys
⊢ f x = none
Tactic:
split at h
Proof state after:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
⊢ f x = none

case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
⊢ f x = none

case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Tactic:
. cases hx with
  | head => assumption
  | tail _ hmem => exact ih h hmem
Proof state after:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Tactic:
. contradiction
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
⊢ f x = none
Tactic:
cases hx with
| head => assumption
| tail _ hmem => exact ih h hmem
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons.h_1.head
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
h : List.filterMap f ys = []
heq✝ : f x = none
⊢ f x = none
Tactic:
assumption
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons.h_1.tail
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
heq✝ : f y = none
h : List.filterMap f ys = []
hmem : List.Mem x ys
⊢ f x = none
Tactic:
exact ih h hmem
Proof state after:
no goals
Theorem: CNF.List.all_none_of_filterMap_eq_nil
Proof state before:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: List.filterMap f ys = []
⊢ f x = none
Tactic:
contradiction
Proof state after:
no goals
Theorem: CNF.of_maxLiteral_eq_none
Proof state before:
c : CNF Nat
h : c.maxLiteral = none
⊢ ∀ (lit : Nat), ¬mem lit c
Tactic:
intro lit hlit
Proof state after:
c : CNF Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False
Theorem: CNF.of_maxLiteral_eq_none
Proof state before:
c : CNF Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False
Tactic:
simp only [maxLiteral, List.maximum?_eq_none_iff] at h
Proof state after:
c : CNF Nat
lit : Nat
hlit : mem lit c
h : List.filterMap Clause.maxLiteral c = []
⊢ False