-- 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:
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

Tactic:
rw [clear_insertRup f f_readyForRupAdd (negate c)] at 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.insert c = f'
⊢ f' = f.insert c

Proof state:
case isFalse.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
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

Tactic:
simp at rupAddSuccess

Result:
no goals

Proof state:
case 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
rupAddSuccess : f.insert c = f'
⊢ f' = f.insert c

Tactic:
exact rupAddSuccess.symm

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
rupAddSuccess :
  (match f.insertRupUnits c.negate with
    | (f, foundContradiction) =>
      if foundContradiction = true then
        let f := f.clearRupUnits;
        (f.insert c, true)
      else
        match f.performRupCheck rupHints with
        | (f, derivedLits, derivedEmpty, encounteredError) =>
          if encounteredError = true then (f, false)
          else
            if (!derivedEmpty) = true then (f, false)
            else
              match f with
              | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                let assignments := restoreAssignments assignments derivedLits;
                let f :=
                  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                      assignments := assignments }.clearRupUnits;
                (f.insert c, true)) =
    (f', true)
⊢ f' = f.insert c

Tactic:
simp only [Bool.not_eq_true'] at rupAddSuccess

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
rupAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true)
    else
      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

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
rupAddSuccess :
  ({ 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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ (f.insertRupUnits c.negate).fst.assignments.size = n

Tactic:
rw [size_assignments_insertRupUnits f (negate c)]

Result:
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
rupAddSuccess :
  ({ 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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f.assignments.size = n