Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case pos
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 : ∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

case neg
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 : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
. rcases hl with ⟨l, hl⟩
  simp only [unit] at hl
  simp only [hl]
  simp only [deleteOne, heq, hl] at hb
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
    have l_ne_b : l.2 ≠ b := by
      intro l_eq_b
      rw [← l_eq_b] at hb
      have hb' := not_has_of_remove f.assignments[i.1] l.2
      simp [hb] at hb'
    rw [← Bool.eq_not_iff] at l_ne_b
    rw [l_ne_b] at hb
    have hb := has_of_remove_irrelevant f.assignments[i.1] b 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, hl] at heq
          simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
          simp only [← heq, not] at l_ne_b
          split at l_ne_b
          . simp only at l_ne_b
          . simp only at l_ne_b
        . 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
  . next l_ne_i =>
    have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] 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, hl] at heq
          simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
          have i_eq_l : i = l.1 := by rw [← heq]
          simp only [i_eq_l, not_true] at l_ne_i
        . 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:
case neg
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 : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList