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

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then f.performRatCheck p ratHints[idx] else (f, false))

Tactic:
split

Result:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ motive (↑idx + 1) (f.performRatCheck p ratHints[idx])

case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)

Proof state:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ motive (↑idx + 1) (f.performRatCheck p ratHints[idx])

Tactic:
exact formula_performRatCheck f hf p ratHints[idx]

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints;
  performRatCheck_fold_res.fst = f

Tactic:
let motive (_idx : Nat) (acc : DefaultFormula n × Bool) := acc.1 = f

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints;
  performRatCheck_fold_res.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)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
h_inductive :
  ∀ (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool),
    motive (↑idx) acc →
      motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints;
  performRatCheck_fold_res.fst = f

Tactic:
exact Array.foldl_induction motive h_base h_inductive

Result:
no goals

Proof state:
case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)

Tactic:
rfl

Result:
no goals

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

Tactic:
intro ih

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints;
  performRatCheck_fold_res.fst = f

Tactic:
have h_base : motive 0 (f, true) := rfl

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints;
  performRatCheck_fold_res.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)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))

Tactic:
rw [ih]

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then f.performRatCheck p ratHints[idx] else (f, false))