-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem insertRatUnits_postcondition {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n)
    (units : CNF.Clause (PosFin n)) :
    let assignments := (insertRatUnits f units).fst.assignments
    have hsize : assignments.size = n

Proof state:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ f.assignments[↑i] = f.assignments[↑i] ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i

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

Result:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.ratUnits.size), ¬f.ratUnits[↑j].fst.val = ↑i

Proof state:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.ratUnits.size), ¬f.ratUnits[↑j].fst.val = ↑i

Tactic:
intro j

Result:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
j : Fin f.ratUnits.size
⊢ ¬f.ratUnits[↑j].fst.val = ↑i

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

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

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

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
⊢ InsertUnitInvariant f.assignments ⋯ f.ratUnits f.assignments hsize

Tactic:
intro i

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
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.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.ratUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.ratUnits.size), k ≠ j → f.ratUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.ratUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.ratUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.ratUnits.size), k ≠ j1 → k ≠ j2 → f.ratUnits[k].fst.val ≠ ↑i

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = f.assignments.size

Tactic:
exact size_assignments_insertRatUnits f units

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯

Tactic:
have hsize : f.assignments.size = n := by rw [hf.2]

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = n

Tactic:
rw [← hf.2]

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
⊢ let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize

Tactic:
simp only [insertRatUnits]

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
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.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.ratUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.ratUnits.size), k ≠ j → f.ratUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.ratUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.ratUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.ratUnits.size), k ≠ j1 → k ≠ j2 → f.ratUnits[k].fst.val ≠ ↑i

Tactic:
apply Or.inl

Result:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ f.assignments[↑i] = f.assignments[↑i] ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i

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

Tactic:
exact Fin.elim0 j

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯

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

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
h0 : InsertUnitInvariant f.assignments ⋯ f.ratUnits f.assignments hsize
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯