rw [hf.2] at insertRatUnits_assignments_size
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
insertRatUnits_assignments_size : (f.insertRatUnits units).fst.assignments.size = f.assignments.size
⊢ let insertRat_res := f.insertRatUnits units;
  f.clear_insert_induction_motive ⋯ insertRat_res.fst.ratUnits 0 insertRat_res.fst.assignments
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
insertRatUnits_assignments_size : (f.insertRatUnits units).fst.assignments.size = n
⊢ let insertRat_res := f.insertRatUnits units;
  f.clear_insert_induction_motive ⋯ insertRat_res.fst.ratUnits 0 insertRat_res.fst.assignments