simp only [toList, Array.toList_eq, f_readyForRatAdd.2.1, Array.data_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
  List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
c'_in_f : some c' ∈ f.clauses.data
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'