split at h1 <;> first
| exact h1
| rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
  rw [toList, List.mem_append, List.mem_append, or_assoc]
  rcases h1 with h1 | h1 | h1
  . apply Or.inl
    simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
    simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
    rw [Array.set!, Array.setD] at h1
    split at h1
    . simp only [Array.data_set] at h1
      rcases List.get_of_mem h1 with ⟨i, h4⟩
      rw [List.get_set] at h4
      split at h4
      . exact False.elim h4
      . rw [← h4]
        apply List.get_mem
    . exact h1
  . exact (Or.inr ∘ Or.inl) h1
  . exact (Or.inr ∘ Or.inr) h1
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
h1 :
  c ∈
    (match f.clauses[id]! 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
⊢ c ∈ f.toList
no goals