-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (units : CNF.Clause (PosFin n)) :
    let assignments := (insertRupUnits f units).fst.assignments
    have hsize : assignments.size = n

Proof state:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
j✝ : Fin f.rupUnits.size
j : Fin 0
⊢ ¬f.rupUnits[↑j✝].fst.val = ↑i

Tactic:
exact Fin.elim0 j

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = n

Tactic:
rw [← f_readyForRupAdd.2.1]

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = f.assignments.size

Proof state:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
j : Fin f.rupUnits.size
⊢ ¬f.rupUnits[↑j].fst.val = ↑i

Tactic:
simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j

Result:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
j✝ : Fin f.rupUnits.size
j : Fin 0
⊢ ¬f.rupUnits[↑j✝].fst.val = ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
⊢ InsertUnitInvariant f.assignments hsize f.rupUnits f.assignments hsize

Tactic:
intro i

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
⊢ let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize

Tactic:
simp only [insertRupUnits]

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

Tactic:
have hsize : f.assignments.size = n := by rw [f_readyForRupAdd.2.1]

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = f.assignments.size

Tactic:
exact size_assignments_insertRupUnits f units

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
h0 : InsertUnitInvariant f.assignments hsize f.rupUnits f.assignments hsize
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

Tactic:
exact insertUnitInvariant_insertUnit_fold f.assignments hsize f.rupUnits f.assignments hsize false units h0

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i

Tactic:
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 h,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯

Tactic:
have h0 : InsertUnitInvariant f.assignments hsize f.rupUnits f.assignments hsize := by
  intro i
  simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
  apply Or.inl
  intro j
  simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
  exact Fin.elim0 j

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
h0 : InsertUnitInvariant f.assignments hsize f.rupUnits f.assignments hsize
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯