-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignment)
    (assignments0_size : assignments0.size = n) (units : Array (Literal (PosFin n)))
    (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (foundContradiction : Bool) (l : Literal (PosFin n)) :
    InsertUnitInvariant assignments0 assignments0_size units assignments assignments_size →
    let update_res := insertUnit (units, assignments, foundContradiction) l
    have update_res_size : update_res.snd.fst.size = n

Proof state:
case inl.intro
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
⊢ ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
      ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
        ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
    (∃ j b h,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
          (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧
              ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 h,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
              assignments0[↑i] = unassigned ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i

Tactic:
by_cases hasAssignment l.2 assignments[l.1.1]!

Result:
case pos
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
      ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
        ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
    (∃ j b h,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
          (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧
              ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 h,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
              assignments0[↑i] = unassigned ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i

case neg
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
      ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
        ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
    (∃ j b h,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
          (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧
              ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 h,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
              assignments0[↑i] = unassigned ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i

Proof state:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
j :
  Fin
    (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size
hsize : (insertUnit (units, assignments, foundContradiction) l).fst.size = units.size
⊢ ↑j < units.size

Tactic:
rw [← hsize]

Result:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
j :
  Fin
    (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size
hsize : (insertUnit (units, assignments, foundContradiction) l).fst.size = units.size
⊢ ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size