singleton_eq_get_zero'

formal source

 260private lemma not_isSome_iff_isNone' {α : Type*} (o : Option α) : ¬o.isSome ↔ o.isNone := by
 261  cases o <;> simp
 262
 263private lemma singleton_eq_get_zero' {α : Type*} (l : List α) (h : l.length = 1) :
 264    ∃ x, l = [x] ∧ x = l.get ⟨0, by omega⟩ := by
 265  match l with
 266  | [] => simp at h
 267  | [x] => exact ⟨x, rfl, rfl⟩
 268  | _ :: _ :: _ => simp at h
 269
 270private lemma mem_zip_of_getElem' {α β : Type*} (l1 : List α) (l2 : List β) (i : Nat)
 271    (hi1 : i < l1.length) (hi2 : i < l2.length) :
 272    (l1[i], l2[i]) ∈ l1.zip l2 := by
 273  rw [List.mem_iff_getElem]
 274  have hi : i < (l1.zip l2).length := by simp; omega
 275  exact ⟨i, hi, by simp⟩
 276
 277private lemma known_lit_false'' {n} (σ : PartialAssignment n) (a : Assignment n) (l : Lit n)
 278    (hcompat : compatible σ a) (hsome : (valueOfLit σ l).isSome)
 279    (hfalse : (valueOfLit σ l).getD false = false) :
 280    evalLit a l = false := by
 281  have heq : valueOfLit σ l = some (evalLit a l) := by
 282    cases l with
 283    | pos v =>
 284      simp only [valueOfLit, evalLit] at *
 285      rcases hcompat v with h | h
 286      · exact h
 287      · simp [h] at hsome
 288    | neg v =>
 289      simp only [valueOfLit, evalLit, Option.map] at *
 290      rcases hcompat v with h | h
 291      · simp [h]
 292      · simp [h] at hsome
 293  cases hv : valueOfLit σ l with