-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
    (ratHint : Nat × Array Nat) :
    (performRatCheck f p ratHint).1 = f

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
c : DefaultClause n
heq✝ : f.clauses[ratHint.fst]! = some c
⊢ (if
          ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments := f.assignments }.insertRatUnits
                (c.delete p).negate).snd =
            true then
        (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments := f.assignments }.insertRatUnits
                (c.delete p).negate).fst.clearRatUnits,
          true)
      else
        if
            (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).2.2.snd =
                true ∨
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).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 p).negate).fst.performRupCheck
                        ratHint.snd).1.clauses,
                rupUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.rupUnits,
                ratUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete p).negate).fst.performRupCheck
                          ratHint.snd).1.assignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete p).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 p).negate).fst.performRupCheck
                        ratHint.snd).1.clauses,
                rupUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.rupUnits,
                ratUnits :=
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete p).negate).fst.performRupCheck
                          ratHint.snd).1.assignments
                    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                    assignments := f.assignments }.insertRatUnits
                                (c.delete p).negate).fst.performRupCheck
                          ratHint.snd).2.fst }.clearRatUnits,
            true)).fst =
    f

Tactic:
split

Result:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
c : DefaultClause n
heq✝ : f.clauses[ratHint.fst]! = some c
h✝ :
  ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.insertRatUnits
        (c.delete p).negate).snd =
    true
⊢ (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments := f.assignments }.insertRatUnits
              (c.delete p).negate).fst.clearRatUnits,
        true).fst =
    f

case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
c : DefaultClause n
heq✝ : f.clauses[ratHint.fst]! = some c
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete p).negate).snd =
      true
⊢ (if
          (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).2.2.snd =
              true ∨
            (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).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 p).negate).fst.performRupCheck
                      ratHint.snd).1.clauses,
              rupUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.rupUnits,
              ratUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.ratUnits,
              assignments :=
                restoreAssignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.assignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).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 p).negate).fst.performRupCheck
                      ratHint.snd).1.clauses,
              rupUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.rupUnits,
              ratUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.ratUnits,
              assignments :=
                restoreAssignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.assignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).2.fst }.clearRatUnits,
          true)).fst =
    f