Theorem: LRAT.DefaultFormula.performRatCheck_preserves_formula (LeanSAT/LRAT/Formula/RatAddResult.lean)

State before:
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']
State after:
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

State before:
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
Tactic:
split
State after:
case h_1
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

case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f

State before:
case h_1
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

case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f
Tactic:
. next c _ =>
  split
  . rw [clear_insertRat f hf]
  . let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1
    have fc_assignments_size : fc.assignments.size = n := by rw [insertRatUnits_preserves_assignments_size, hf.2]
    have insertRatUnits_rw : (insertRatUnits f (negate (DefaultClause.delete c p))).1 =
      ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
       (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
       (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
       (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
    simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits]
    rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
      clear_insertRat f hf (negate (DefaultClause.delete c p))]
    split <;> rfl
State after:
case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f

State before:
case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f
Tactic:
. rfl
State after:
no goals

State before:
case h_1
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:
next c _ =>
split
. rw [clear_insertRat f hf]
. let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1
  have fc_assignments_size : fc.assignments.size = n := by rw [insertRatUnits_preserves_assignments_size, hf.2]
  have insertRatUnits_rw : (insertRatUnits f (negate (DefaultClause.delete c p))).1 =
    ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
  simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits]
  rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
    clear_insertRat f hf (negate (DefaultClause.delete c p))]
  split <;> rfl
State after:
no goals

State before:
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
State after:
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

State before:
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
Tactic:
. rw [clear_insertRat f hf]
State after:
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

State before:
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
Tactic:
. let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1
  have fc_assignments_size : fc.assignments.size = n := by rw [insertRatUnits_preserves_assignments_size, hf.2]
  have insertRatUnits_rw : (insertRatUnits f (negate (DefaultClause.delete c p))).1 =
    ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
  simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits]
  rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
    clear_insertRat f hf (negate (DefaultClause.delete c p))]
  split <;> rfl
State after:
no goals

State before:
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
Tactic:
rw [clear_insertRat f hf]
State after:
no goals

State before:
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
Tactic:
let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1
State after:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
⊢ (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

State before:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
⊢ (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:
have fc_assignments_size : fc.assignments.size = n := by rw [insertRatUnits_preserves_assignments_size, hf.2]
State after:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
⊢ (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

State before:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
⊢ (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:
have insertRatUnits_rw : (insertRatUnits f (negate (DefaultClause.delete c p))).1 =
  ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
   (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
   (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
   (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
State after:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (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

State before:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (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:
simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits]
State after:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (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.clauses,
              rupUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.rupUnits,
              ratUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.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.clauses,
              rupUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.rupUnits,
              ratUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.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

State before:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (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.clauses,
              rupUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.rupUnits,
              ratUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.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.clauses,
              rupUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.rupUnits,
              ratUnits :=
                ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                          assignments := f.assignments }.insertRatUnits
                      (c.delete p).negate).fst.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:
rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
  clear_insertRat f hf (negate (DefaultClause.delete c p))]
State after:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (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
        (f, false)
      else (f, true)).fst =
    f

State before:
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
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (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
        (f, false)
      else (f, true)).fst =
    f
Tactic:
split <;> rfl
State after:
no goals

State before:
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 [insertRatUnits_preserves_assignments_size, hf.2]
State after:
no goals

State before:
case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f
Tactic:
rfl
State after:
no goals