-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
    (performRupCheck f rupHints).1.assignments.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.toList
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size

Tactic:
have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id

Result:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.toList
h : (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.toList
h : (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size

Tactic:
rw [h, hsize]

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = f.assignments.size

Tactic:
rw [← Array.foldl_toList]

Result:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.toList).fst.size =
    f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.toList).fst.size =
    f.assignments.size

Tactic:
have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl

Result:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.toList).fst.size =
    f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.toList).fst.size =
    f.assignments.size

Tactic:
have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
  (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
  have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
  rw [h, hsize]

Result:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.toList → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.toList).fst.size =
    f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.assignments.size = f.assignments.size

Tactic:
simp only [performRupCheck]

Result:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints).fst.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.toList → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.toList).fst.size =
    f.assignments.size

Tactic:
exact List.foldlRecOn rupHints.toList (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl

Result:
no goals