-- 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_lt_or_eq_idx : ↑i < ↑idx ∨ ↑i = ↑idx
⊢ (f.performRatCheck p ratHints[i]!).snd = true

Tactic:
rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx

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

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

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)
⊢ motive 0 (f, true)

Tactic:
constructor

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

case right
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).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true

Proof state:
case right
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).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true

Tactic:
intro _ i

Result:
case right
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)
a✝ : (f, true).snd = true
i : Fin 0
⊢ (f.performRatCheck p ratHints[i]!).snd = true