-- 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:
case intro.intro
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
h1 : Limplies (PosFin n) f (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst
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 }
⊢ p ⊨ (i, b)

Tactic:
specialize h1 p pf

Result:
case intro.intro
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 : p ⊨ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst
⊢ p ⊨ (i, b)

Proof state:
case intro.intro
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
h1 : Limplies (PosFin n) f (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst
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
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst }.AssignmentsInvariant

Tactic:
apply Exists.intro hsize

Result:
case intro.intro
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
h1 : Limplies (PosFin n) f (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst
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),
    hasAssignment b
          { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments :=
                  (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false)
                      rupHints).fst }.assignments[i.val] =
        true →
      Limplies (PosFin n)
        { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst }
        (i, b)