-- 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:
case right.isFalse
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)
h✝ : ¬acc.snd = true
h : (acc.fst, false).snd = true
⊢ (f.performRatCheck p ratHints[i]!).snd = true

Tactic:
simp at h

Result:
no goals

Proof state:
case inr
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_eq_idx : ↑i = ↑idx
⊢ (f.performRatCheck p ratHints[↑idx]).snd = true

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

Result:
case inr
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
i_eq_idx : ↑i = ↑idx
h : (f.performRatCheck p ratHints[↑idx]).snd = true
⊢ (f.performRatCheck p ratHints[↑idx]).snd = true

Proof state:
case inr
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_eq_idx : ↑i = ↑idx
⊢ (f.performRatCheck p ratHints[i]!).snd = true

Tactic:
simp only [getElem!, i_eq_idx, idx.2, Fin.getElem_fin, dite_true, decidableGetElem?]

Result:
case inr
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_eq_idx : ↑i = ↑idx
⊢ (f.performRatCheck p ratHints[↑idx]).snd = true

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)
⊢ (f, true).fst = f

Tactic:
rfl

Result:
no goals