Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
Proof state after:
case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)