-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat)
    (f'_assignments_size : (performRupCheck f rupHints).1.assignments.size = n) :
    let rupCheckRes := performRupCheck f rupHints
    DerivedLitsInvariant f f_assignments_size rupCheckRes.1.assignments f'_assignments_size rupCheckRes.2.1

Proof state:
case h
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i] ∧
    ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

Tactic:
constructor

Result:
case h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]

case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

Proof state:
case h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Tactic:
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h⟩

Result:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = n
h :
  f.DerivedLitsInvariant f_assignments_size
    (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst w✝
    (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Tactic:
have h_inductive (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
  (ih : motive i.1 acc) := derivedLitsInvariant_confirmRupHint f f_assignments_size rupHints i acc ih

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Proof state:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = n
h :
  f.DerivedLitsInvariant f_assignments_size
    (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst w✝
    (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Tactic:
exact h

Result:
no goals