-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n)
    (f_AssignmentsInvariant : AssignmentsInvariant f) (rupHints : Array Nat) :
    AssignmentsInvariant (performRupCheck f rupHints).1

Proof state:
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
rupHints : Array Nat
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := f.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑idx) acc → f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = n
right✝ :
  (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).snd.snd.fst = true →
    Incompatible (PosFin n) (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst f
i : PosFin n
b : Bool
h✝ :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val] = true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst }
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val]! =
    false
in_bounds_motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun _idx acc => acc.fst.size = n
in_bounds_base : in_bounds_motive 0 (f.assignments, [], false, false)
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
ih : in_bounds_motive (↑idx) acc
h :
  (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) rupHints[idx]).fst.size =
    acc.fst.size
this : (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) = acc
⊢ in_bounds_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])

Tactic:
simp [this] at *

Result:
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
rupHints : Array Nat
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := f.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (f.assignments, [], false, false)
hsize : (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = n
right✝ :
  (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).snd.snd.fst = true →
    Incompatible (PosFin n) (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst f
i : PosFin n
b : Bool
h✝ :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val] = true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst }
in_bounds_motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun _idx acc => acc.fst.size = n
in_bounds_base : in_bounds_motive 0 (f.assignments, [], false, false)
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
ih : in_bounds_motive (↑idx) acc
h_inductive :
  ∀ (idx : Fin rupHints.size) (a : Array Assignment) (a_1 : CNF.Clause (PosFin n)),
    ((motive ↑idx (a, a_1, false, false) →
          f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
            (confirmRupHint f.clauses (a, a_1, false, false) rupHints[↑idx])) ∧
        (motive ↑idx (a, a_1, false, true) →
          f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
            (confirmRupHint f.clauses (a, a_1, false, true) rupHints[↑idx]))) ∧
      (motive ↑idx (a, a_1, true, false) →
          f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
            (confirmRupHint f.clauses (a, a_1, true, false) rupHints[↑idx])) ∧
        (motive ↑idx (a, a_1, true, true) →
          f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint f.clauses (a, a_1, true, true) rupHints[↑idx]))
h1 :
  hasAssignment (!p i) (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val]! =
    false
h : (confirmRupHint f.clauses acc rupHints[↑idx]).fst.size = acc.fst.size
this : True
⊢ in_bounds_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[↑idx])

Proof state:
case pos
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
rupHints : Array Nat
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := f.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑idx) acc → f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = n
right✝ :
  (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).snd.snd.fst = true →
    Incompatible (PosFin n) (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val] = true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val] =
    false
hb : b = true
⊢ p i = b

Tactic:
rw [hb]

Result:
case pos
n : Nat
f : DefaultFormula n
f_AssignmentsInvariant : f.AssignmentsInvariant
rupHints : Array Nat
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := f.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑idx) acc → f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = n
right✝ :
  (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).snd.snd.fst = true →
    Incompatible (PosFin n) (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val] = true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst[i.val] =
    false
hb : b = true
⊢ p i = true