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

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c p rupHints ratHints = (f', true)
⊢ f' = f.insert c
Tactic:
rw [performRatAdd] at ratAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck p.negateLiteral ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints 0 with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck p.negateLiteral ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints 0 with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
          else
            if
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
                  false then
              ((Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
                false)
            else
              ({
                        clauses :=
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.clauses,
                        rupUnits :=
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.rupUnits,
                        ratUnits :=
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.ratUnits,
                        assignments :=
                          restoreAssignments
                            (Array.foldl
                                  (fun x ratHint =>
                                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                    else (x.fst, false))
                                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                  0).1.assignments
                            ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
                  c,
                true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
          else
            if
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
                  false then
              ((Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
                false)
            else
              ({
                        clauses :=
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.clauses,
                        rupUnits :=
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.rupUnits,
                        ratUnits :=
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.ratUnits,
                        assignments :=
                          restoreAssignments
                            (Array.foldl
                                  (fun x ratHint =>
                                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                    else (x.fst, false))
                                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                  0).1.assignments
                            ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
                  c,
                true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
split at ratAddSuccess
State after:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : f.ratHintsExhaustive p ratHints = true
ratAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
                false then
            ((Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
              false)
          else
            ({
                      clauses :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.clauses,
                      rupUnits :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.rupUnits,
                      ratUnits :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.ratUnits,
                      assignments :=
                        restoreAssignments
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.assignments
                          ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
                c,
              true)) =
    (f', true)
⊢ f' = f.insert c

case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c

State before:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : f.ratHintsExhaustive p ratHints = true
ratAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
                false then
            ((Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
              false)
          else
            ({
                      clauses :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.clauses,
                      rupUnits :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.rupUnits,
                      ratUnits :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.ratUnits,
                      assignments :=
                        restoreAssignments
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.assignments
                          ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
                c,
              true)) =
    (f', true)
⊢ f' = f.insert c

case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c
Tactic:
. split at ratAddSuccess
  . simp at ratAddSuccess
  . split at ratAddSuccess
    . simp at ratAddSuccess
    . split at ratAddSuccess
      . simp at ratAddSuccess
      . split at ratAddSuccess
        . simp at ratAddSuccess
        . next performRatCheck_fold_success =>
          simp only [Bool.not_eq_false] at performRatCheck_fold_success
          let fc := (insertRupUnits f (negate c)).1
          have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
            rw [insertRupUnits_preserves_assignments_size f (negate c)]
            exact f_readyForRatAdd.2.2.1
          simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
            restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
          rw [← ratAddSuccess]
          clear f' ratAddSuccess
          let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
          have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
            have hsize : performRupCheck_res.assignments.size = n := by
              rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
            exact And.intro f_readyForRatAdd.1 hsize
          have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
            ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
             (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
          simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
            performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
            restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
            clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c

State before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c
Tactic:
. simp at ratAddSuccess
State after:
no goals

State before:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : f.ratHintsExhaustive p ratHints = true
ratAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
                false then
            ((Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
              false)
          else
            ({
                      clauses :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.clauses,
                      rupUnits :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.rupUnits,
                      ratUnits :=
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.ratUnits,
                      assignments :=
                        restoreAssignments
                          (Array.foldl
                                (fun x ratHint =>
                                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint
                                  else (x.fst, false))
                                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                                0).1.assignments
                          ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
                c,
              true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
split at ratAddSuccess
State after:
case isTrue.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : (f.insertRupUnits c.negate).snd = true
ratAddSuccess : ((f.insertRupUnits c.negate).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : ¬(f.insertRupUnits c.negate).snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if
            (Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
              false then
          ((Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
            false)
        else
          ({
                    clauses :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.clauses,
                    rupUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.rupUnits,
                    ratUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.ratUnits,
                    assignments :=
                      restoreAssignments
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.assignments
                        ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
              c,
            true)) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : (f.insertRupUnits c.negate).snd = true
ratAddSuccess : ((f.insertRupUnits c.negate).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : ¬(f.insertRupUnits c.negate).snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if
            (Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
              false then
          ((Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
            false)
        else
          ({
                    clauses :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.clauses,
                    rupUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.rupUnits,
                    ratUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.ratUnits,
                    assignments :=
                      restoreAssignments
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.assignments
                        ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
              c,
            true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. simp at ratAddSuccess
State after:
case isTrue.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : ¬(f.insertRupUnits c.negate).snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if
            (Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
              false then
          ((Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
            false)
        else
          ({
                    clauses :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.clauses,
                    rupUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.rupUnits,
                    ratUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.ratUnits,
                    assignments :=
                      restoreAssignments
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.assignments
                        ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
              c,
            true)) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : ¬(f.insertRupUnits c.negate).snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if
            (Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
              false then
          ((Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
            false)
        else
          ({
                    clauses :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.clauses,
                    rupUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.rupUnits,
                    ratUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.ratUnits,
                    assignments :=
                      restoreAssignments
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.assignments
                        ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
              c,
            true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. split at ratAddSuccess
  . simp at ratAddSuccess
  . split at ratAddSuccess
    . simp at ratAddSuccess
    . split at ratAddSuccess
      . simp at ratAddSuccess
      . next performRatCheck_fold_success =>
        simp only [Bool.not_eq_false] at performRatCheck_fold_success
        let fc := (insertRupUnits f (negate c)).1
        have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
          rw [insertRupUnits_preserves_assignments_size f (negate c)]
          exact f_readyForRatAdd.2.2.1
        simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
          restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
        rw [← ratAddSuccess]
        clear f' ratAddSuccess
        let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
        have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
          have hsize : performRupCheck_res.assignments.size = n := by
            rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
          exact And.intro f_readyForRatAdd.1 hsize
        have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
          ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
           (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
        simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
          performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
          restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
          clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
no goals

State before:
case isTrue.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : (f.insertRupUnits c.negate).snd = true
ratAddSuccess : ((f.insertRupUnits c.negate).fst, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
State after:
no goals

State before:
case isTrue.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : ¬(f.insertRupUnits c.negate).snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if
            (Array.foldl
                  (fun x ratHint =>
                    if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
              false then
          ((Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
            false)
        else
          ({
                    clauses :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.clauses,
                    rupUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.rupUnits,
                    ratUnits :=
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.ratUnits,
                    assignments :=
                      restoreAssignments
                        (Array.foldl
                              (fun x ratHint =>
                                if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                              0).1.assignments
                        ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
              c,
            true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
split at ratAddSuccess
State after:
case isTrue.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if
          (Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
            false then
        ((Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
          false)
      else
        ({
                  clauses :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                  rupUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                  ratUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                  assignments :=
                    restoreAssignments
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if
          (Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
            false then
        ((Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
          false)
      else
        ({
                  clauses :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                  rupUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                  ratUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                  assignments :=
                    restoreAssignments
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. simp at ratAddSuccess
State after:
case isTrue.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if
          (Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
            false then
        ((Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
          false)
      else
        ({
                  clauses :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                  rupUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                  ratUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                  assignments :=
                    restoreAssignments
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if
          (Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
            false then
        ((Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
          false)
      else
        ({
                  clauses :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                  rupUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                  ratUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                  assignments :=
                    restoreAssignments
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. split at ratAddSuccess
  . simp at ratAddSuccess
  . split at ratAddSuccess
    . simp at ratAddSuccess
    . next performRatCheck_fold_success =>
      simp only [Bool.not_eq_false] at performRatCheck_fold_success
      let fc := (insertRupUnits f (negate c)).1
      have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
        rw [insertRupUnits_preserves_assignments_size f (negate c)]
        exact f_readyForRatAdd.2.2.1
      simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
        restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
      rw [← ratAddSuccess]
      clear f' ratAddSuccess
      let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
      have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
        have hsize : performRupCheck_res.assignments.size = n := by
          rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
        exact And.intro f_readyForRatAdd.1 hsize
      have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
        ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
         (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
      simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
        performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
        restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
        clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
no goals

State before:
case isTrue.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
State after:
no goals

State before:
case isTrue.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if
          (Array.foldl
                (fun x ratHint =>
                  if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
            false then
        ((Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
          false)
      else
        ({
                  clauses :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                  rupUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                  ratUnits :=
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                  assignments :=
                    restoreAssignments
                      (Array.foldl
                            (fun x ratHint =>
                              if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                            0).1.assignments
                      ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
            c,
          true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
split at ratAddSuccess
State after:
case isTrue.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  (if
        (Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
          false then
      ((Array.foldl
            (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
        false)
    else
      ({
                clauses :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                rupUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                ratUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                          0).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  (if
        (Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
          false then
      ((Array.foldl
            (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
        false)
    else
      ({
                clauses :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                rupUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                ratUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                          0).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. simp at ratAddSuccess
State after:
case isTrue.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  (if
        (Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
          false then
      ((Array.foldl
            (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
        false)
    else
      ({
                clauses :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                rupUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                ratUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                          0).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  (if
        (Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
          false then
      ((Array.foldl
            (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
        false)
    else
      ({
                clauses :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                rupUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                ratUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                          0).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. split at ratAddSuccess
  . simp at ratAddSuccess
  . next performRatCheck_fold_success =>
    simp only [Bool.not_eq_false] at performRatCheck_fold_success
    let fc := (insertRupUnits f (negate c)).1
    have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
      rw [insertRupUnits_preserves_assignments_size f (negate c)]
      exact f_readyForRatAdd.2.2.1
    simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
      restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
    rw [← ratAddSuccess]
    clear f' ratAddSuccess
    let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
    have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
      have hsize : performRupCheck_res.assignments.size = n := by
        rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
      exact And.intro f_readyForRatAdd.1 hsize
    have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
      ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
       (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
    simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
      performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
      restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
      clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
no goals

State before:
case isTrue.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
State after:
no goals

State before:
case isTrue.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  (if
        (Array.foldl
              (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
          false then
      ((Array.foldl
            (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
        false)
    else
      ({
                clauses :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
                rupUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
                ratUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints
                          0).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ f' = f.insert c
Tactic:
split at ratAddSuccess
State after:
case isTrue.isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    false
ratAddSuccess :
  ((Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
      false) =
    (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    false
ratAddSuccess :
  ((Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
      false) =
    (f', true)
⊢ f' = f.insert c

case isTrue.isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. simp at ratAddSuccess
State after:
case isTrue.isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c

State before:
case isTrue.isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. next performRatCheck_fold_success =>
  simp only [Bool.not_eq_false] at performRatCheck_fold_success
  let fc := (insertRupUnits f (negate c)).1
  have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
    rw [insertRupUnits_preserves_assignments_size f (negate c)]
    exact f_readyForRatAdd.2.2.1
  simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
    restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
  rw [← ratAddSuccess]
  clear f' ratAddSuccess
  let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
  have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
    have hsize : performRupCheck_res.assignments.size = n := by
      rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
    exact And.intro f_readyForRatAdd.1 hsize
  have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
    ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
     (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
  simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
    performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
    restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
    clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
no goals

State before:
case isTrue.isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    false
ratAddSuccess :
  ((Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
      false) =
    (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
State after:
no goals

State before:
case isTrue.isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c
Tactic:
next performRatCheck_fold_success =>
simp only [Bool.not_eq_false] at performRatCheck_fold_success
let fc := (insertRupUnits f (negate c)).1
have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
  rw [insertRupUnits_preserves_assignments_size f (negate c)]
  exact f_readyForRatAdd.2.2.1
simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
  restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
rw [← ratAddSuccess]
clear f' ratAddSuccess
let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
  have hsize : performRupCheck_res.assignments.size = n := by
    rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
  exact And.intro f_readyForRatAdd.1 hsize
have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
  ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
   (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
  performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
  restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
  clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c
Tactic:
simp only [Bool.not_eq_false] at performRatCheck_fold_success
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
⊢ f' = f.insert c
Tactic:
let fc := (insertRupUnits f (negate c)).1
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f' = f.insert c
Tactic:
have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
  rw [insertRupUnits_preserves_assignments_size f (negate c)]
  exact f_readyForRatAdd.2.2.1
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ f' = f.insert c
Tactic:
simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
  restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
ratAddSuccess :
  {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f'
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
ratAddSuccess :
  {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f'
⊢ f' = f.insert c
Tactic:
rw [← ratAddSuccess]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
ratAddSuccess :
  {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f'
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
ratAddSuccess :
  {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f'
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c
Tactic:
clear f' ratAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c
Tactic:
let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c
Tactic:
have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
  have hsize : performRupCheck_res.assignments.size = n := by
    rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
  exact And.intro f_readyForRatAdd.1 hsize
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c
Tactic:
have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
  ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
   (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
insertRupUnits_rw :
  (f.insertRupUnits c.negate).fst =
    { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
      ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := (f.insertRupUnits c.negate).fst.assignments }
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
insertRupUnits_rw :
  (f.insertRupUnits c.negate).fst =
    { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
      ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := (f.insertRupUnits c.negate).fst.assignments }
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
            rupUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
            ratUnits :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                    (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
            assignments :=
              restoreAssignments
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
      c =
    f.insert c
Tactic:
simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
  performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
  restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
  clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ (f.insertRupUnits c.negate).fst.assignments.size = n
Tactic:
rw [insertRupUnits_preserves_assignments_size f (negate c)]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f.assignments.size = n

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f.assignments.size = n
Tactic:
exact f_readyForRatAdd.2.2.1
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
Tactic:
have hsize : performRupCheck_res.assignments.size = n := by
  rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
hsize : performRupCheck_res.assignments.size = n
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
hsize : performRupCheck_res.assignments.size = n
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
Tactic:
exact And.intro f_readyForRatAdd.1 hsize
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ performRupCheck_res.assignments.size = n
Tactic:
rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
State after:
no goals

State before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
State after:
no goals