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
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
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✝
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
Tactic:
. have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
    simp only [deleteOne]
    split
    . next heq2 =>
      simp only [heq] at heq2
    . next l _ _ heq2 =>
      simp only [heq, Option.some.injEq] at heq2
      rw [heq2] at hl
      specialize hl l.1
      simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
      by_cases hl2 : l.2
      . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
      . simp only [Bool.not_eq_true] at hl2
        simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
    . rfl
  simp only [deleteOne_f_rw] at hb
  specialize hf i b hb
  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] at hf
  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]
  rcases hf with hf | hf
  . apply Or.inl
    simp only [Array.set!, Array.setD]
    split
    . rcases List.get_of_mem hf with ⟨idx, hidx⟩
      simp only [← hidx, Array.data_set]
      rw [List.mem_iff_get]
      have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
        simp only [List.length_set]
        exact idx.2
      apply Exists.intro ⟨idx.1, idx_in_bounds⟩
      by_cases id = idx
      . next id_eq_idx =>
        exfalso
        have idx_in_bounds2 : idx.1 < f.clauses.size := by
          have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
          conv => rhs; rw [f_clauses_rw, Array.size_mk]
          exact idx.2
        simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
          Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
        rw [hidx] at heq
        simp only [Option.some.injEq] at heq
        rw [← heq] at hl
        specialize hl i
        simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
          Bool.not_eq_false, Bool.not_eq_true] at hl
        by_cases b_val : b
        . simp only [b_val, and_false] at hl
        . simp only [b_val, false_and] at hl
      . next id_ne_idx =>
        simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
    . exact hf
  . exact Or.inr hf
Proof state after:
no goals