-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
    (ratHints : Array (Nat × Array Nat)) (i : Fin ratHints.size)
    (performRatCheck_fold_success :
    (ratHints.foldl
      (fun acc ratHint => if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false))
      (f, true) 0 ratHints.size).2 = true) : (performRatCheck f p ratHints[i]).2 = true

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i✝ : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
i : Fin (↑idx + 1)
acc_eq_true : acc.snd = true
h : (acc.fst.performRatCheck p ratHints[idx]).snd = true
⊢ ↑i < ↑idx ∨ ↑i = ↑idx

Tactic:
omega

Result:
no goals

Proof state:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ (fold_fn acc ratHints[idx]).fst = f

Tactic:
simp only [Fin.getElem_fin, fold_fn_def, ih.1]

Result:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ (if acc.snd = true then f.performRatCheck p ratHints[↑idx] else (f, false)).fst = f

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
⊢ (f.performRatCheck p ratHints[i]).snd = true

Tactic:
have fold_fn_def (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) :
  fold_fn acc ratHint = if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false) := rfl

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
⊢ (f.performRatCheck p ratHints[i]).snd = true