-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (negPivot : Literal (PosFin n))
    (ratHint : Nat × Array Nat) (performRatCheck_success : (performRatCheck f negPivot ratHint).2)
    (c : DefaultClause n) :
    f.clauses[ratHint.1]! = some c → Limplies (PosFin n) f (c.delete negPivot)

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ c.delete negPivot

Tactic:
simp only [performRatCheck, hc, Bool.or_eq_true, Bool.not_eq_true'] at performRatCheck_success

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
performRatCheck_success :
  (if
          ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments := f.assignments }.insertRatUnits
                (c.delete negPivot).negate).snd =
            true then
        (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments := f.assignments }.insertRatUnits
                (c.delete negPivot).negate).fst.clearRatUnits,
          true)
      else
        if
            (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).2.2.snd =
                true ∨
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).2.2.fst =
                false then
          ({
                clauses :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).1.clauses,
                rupUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).1.rupUnits,
                ratUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete negPivot).negate).fst.performRupCheck
                          ratHint.snd).1.assignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete negPivot).negate).fst.performRupCheck
                          ratHint.snd).2.fst }.clearRatUnits,
            false)
        else
          ({
                clauses :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).1.clauses,
                rupUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).1.rupUnits,
                ratUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete negPivot).negate).fst.performRupCheck
                        ratHint.snd).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete negPivot).negate).fst.performRupCheck
                          ratHint.snd).1.assignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete negPivot).negate).fst.performRupCheck
                          ratHint.snd).2.fst }.clearRatUnits,
            true)).snd =
    true
⊢ p ⊨ c.delete negPivot