-- 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
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete p).negate).snd =
      true
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
⊢ fc.assignments.size = n

Tactic:
rw [size_assignments_insertRatUnits, hf.2]

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
⊢ (f.performRatCheck p ratHint).fst = f

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

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
⊢ (match f.clauses[ratHint.fst]! with
      | 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)
      | none =>
        ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments },
          false)).fst =
    f