-- 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:
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
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck p.negate ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c

Tactic:
simp only [Bool.not_eq_true'] at ratAddSuccess

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 : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
      else
        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)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c

Proof state:
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
ratAddSuccess : f.performRatAdd c p rupHints ratHints = (f', true)
⊢ f' = f.insert c

Tactic:
rw [performRatAdd] at ratAddSuccess

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 : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck p.negate ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c