-- 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:
case isFalse
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
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
performRatCheck_success :
  (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

Tactic:
split at performRatCheck_success

Result:
case isFalse.isTrue
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
h✝¹ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
h✝ :
  (({ 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
performRatCheck_success :
  ({
            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).snd =
    true
⊢ p ⊨ c.delete negPivot

case isFalse.isFalse
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
h✝¹ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
h✝ :
  ¬((({ 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)
performRatCheck_success :
  ({
            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