have h : i.1 ∈ (ratHints.map (fun x => x.1)).data := by
  rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
  have i_eq_range_i : i.1 = (Array.range f.clauses.size)[i.1]'i_in_bounds := by
    have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
    rw [Array.range_idx]
    conv => rhs; rw [f_clauses_rw, Array.size]
    exact i.2
  rw [i_eq_range_i]
  apply Misc.Array.mem_filter i.1 i_in_bounds
  simp only [getElem!, Array.range_idx i_lt_f_clauses_size, i_lt_f_clauses_size, dite_true,
    c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem]
  simp only [Clause.toList] at negPivot_in_c'
  exact negPivot_in_c'
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'