Theorem: LRAT.DefaultFormula.insertUnit_preserves_size (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (insertUnit (units, assignments, b) l).snd.fst.size = assignments.size
Tactic:
simp only [insertUnit]
State after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size

State before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size
Tactic:
split <;> simp
State after:
no goals