-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
    (f_readyForRatAdd : ReadyForRatAdd f) (c : DefaultClause n) (pivot : Literal (PosFin n))
    (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (pivot_in_c : pivot ∈ Clause.toList c)
    (ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true)
    (performRatCheck_fold_success :
      (Array.foldl
        (fun x ratHint => if x.2 = true then performRatCheck x.1 (Literal.negate pivot) ratHint else (x.1, false))
        ((performRupCheck (insertRupUnits f (negate c)).1 rupHints).1, true) ratHints 0 (Array.size ratHints)).2 = true) :
    Equisat (PosFin n) f (insert f c)

Proof state:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : Limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (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 =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negate ratHints[i]).snd = true
performRupCheck_res_satisfies_AssignmentsInvariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.AssignmentsInvariant
⊢ p ⊨ c'.delete pivot.negate

Tactic:
have h :=
  c_without_negPivot_of_performRatCheck_success (performRupCheck (insertRupUnits f (negate c)).fst rupHints).1
    ⟨h_performRupCheck_res.1, performRupCheck_res_satisfies_AssignmentsInvariant⟩ (Literal.negate pivot) ratHints[i]
    performRatCheck_success

Result:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : Limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (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 =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negate ratHints[i]).snd = true
performRupCheck_res_satisfies_AssignmentsInvariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.AssignmentsInvariant
h :
  ∀ (c_1 : DefaultClause n),
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.clauses[ratHints[i].fst]! = some c_1 →
      Limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst (c_1.delete pivot.negate)
⊢ p ⊨ c'.delete pivot.negate

Proof state:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : Limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (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 =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negate ratHints[i]).snd = true
performRupCheck_res_satisfies_AssignmentsInvariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.AssignmentsInvariant
h :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      Limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst (c_1.delete pivot.negate)
⊢ (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.toList.all fun s =>
      decide ((List.any (Clause.toList s) fun l => decide (p l.fst = l.snd)) = true)) =
    true

Tactic:
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool,
  Bool.decide_coe, List.all_eq_true, decide_eq_true_eq]

Result:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : Limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (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 =
    true
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negate ratHints[i]).snd = true
performRupCheck_res_satisfies_AssignmentsInvariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.AssignmentsInvariant
h :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      Limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst (c_1.delete pivot.negate)
⊢ ∀ (x : DefaultClause n),
    x ∈ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.toList →
      ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true