-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p : Literal (PosFin n))
  (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : DefaultFormula n)
  (f_readyForRatAdd : ReadyForRatAdd f) (_pc : p ∈ Clause.toList c)
  (ratAddSuccess : performRatAdd f c p rupHints ratHints = (f', true)) : f' = insert f c

Proof state:
case isTrue.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : ¬(f.insertRupUnits c.negate).snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if
            (Array.foldl
                  (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
              false then
          ((Array.foldl
                (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).fst,
            false)
        else
          ({
                    clauses :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.clauses,
                    rupUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.rupUnits,
                    ratUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.ratUnits,
                    assignments :=
                      restoreAssignments
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true)
                              ratHints).1.assignments
                        ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
              c,
            true)) =
    (f', true)
⊢ f' = f.insert c

Tactic:
split at ratAddSuccess

Result:
case isTrue.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if
          (Array.foldl
                (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
            false then
        ((Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).fst,
          false)
      else
        ({
                  clauses :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.clauses,
                  rupUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.rupUnits,
                  ratUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.ratUnits,
                  assignments :=
                    restoreAssignments
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true)
                            ratHints).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c