-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat) (f' : DefaultFormula n)
    (f_readyForRupAdd : ReadyForRupAdd f) (rupAddSuccess : performRupAdd f c rupHints = (f', true)) :
    f' = insert f c

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits,
            assignments := (f.insertRupUnits c.negate).fst.assignments }.clearRupUnits.insert
      c =
    f'
⊢ (f.insertRupUnits c.negate).fst.clearRupUnits.insert c = f'

Tactic:
rw [rupAddSuccess]

Result:
no goals

Proof state:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝ : ¬(f.insertRupUnits c.negate).snd = true
rupAddSuccess :
  (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 = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
                  rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
                  ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
                  assignments :=
                    restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c

Tactic:
split at rupAddSuccess

Result:
case isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

case isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
                rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
                ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
                assignments :=
                  restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ f' = f.insert c

Proof state:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits,
            assignments := (f.insertRupUnits c.negate).fst.assignments }.clearRupUnits.insert
      c =
    f'
⊢ f' = f.insert c

Tactic:
have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
  rw [rupAddSuccess]

Result:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess✝ :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits,
            assignments := (f.insertRupUnits c.negate).fst.assignments }.clearRupUnits.insert
      c =
    f'
rupAddSuccess : (f.insertRupUnits c.negate).fst.clearRupUnits.insert c = f'
⊢ f' = f.insert c