-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
    (pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (f' : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (pivot_in_c : pivot ∈ Clause.toList c)
    (ratAddSuccess : performRatAdd f c pivot rupHints ratHints = (f', true)) :
    Equisat (PosFin n) f f'

Proof state:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot 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 pivot.negate ratHint else (x.fst, false))
              (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
          false then
      ((Array.foldl
            (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).fst,
        false)
    else
      ({
                clauses :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.clauses,
                rupUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.rupUnits,
                ratUnits :=
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (Array.foldl
                          (fun x ratHint =>
                            if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ Equisat (PosFin n) f f'

Tactic:
split at ratAddSuccess

Result:
case isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot 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 pivot.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    false
ratAddSuccess :
  ((Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).fst,
      false) =
    (f', true)
⊢ Equisat (PosFin n) f f'

case isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot 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 pivot.negate ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ Equisat (PosFin n) f f'

Proof state:
case isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot 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)
⊢ Equisat (PosFin n) f f'

Tactic:
simp at ratAddSuccess

Result:
no goals

Proof state:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝ : (f.insertRupUnits c.negate).snd = true
ratAddSuccess : ((f.insertRupUnits c.negate).fst, false) = (f', true)
⊢ Equisat (PosFin n) f f'

Tactic:
simp at ratAddSuccess

Result:
no goals