Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case right.isTrue
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 0).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.performRatCheck p ratHints[idx]).snd = true
⊢ (f.performRatCheck p ratHints[i]!).snd = true

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 0).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 : False
⊢ (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
. next acc_eq_true =>
  have i_lt_or_eq_idx : i.1 < idx.1 ∨ i.1 = idx.1 := by
    omega
  rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx
  . exact ih.2 acc_eq_true ⟨i.1, i_lt_idx⟩
  . simp only [getElem!, i_eq_idx, idx.2, Fin.getElem_fin, dite_true]
    simp only [Fin.getElem_fin, ih.1] at h
    exact h
Proof state after:
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 0).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 : False
⊢ (f.performRatCheck p ratHints[i]!).snd = true