-- 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 neg.inr
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
k :
  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
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ¬↑k < units.size
k_property : ↑k < units.size + 1
k_eq_units_size : ↑k = units.size
k_ne_l : ¬k = ⟨↑k, ⋯⟩
⊢ False

Tactic:
exact k_ne_l rfl

Result:
no goals

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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
j1_lt_updatedUnits_size : ↑j1 < (insertUnit (units, assignments, foundContradiction) l).fst.size
j2_lt_updatedUnits_size : ↑j2 < (insertUnit (units, assignments, foundContradiction) l).fst.size
k :
  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
k_ne_j1 : ¬k = ⟨↑j1, j1_lt_updatedUnits_size⟩
k_ne_j2 : ¬k = ⟨↑j2, j2_lt_updatedUnits_size⟩
k_not_lt_units_size : ¬↑k < units.size
⊢ ¬(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[↑k].fst.val =
      ↑i

Tactic:
split

Result:
case isTrue
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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
j1_lt_updatedUnits_size : ↑j1 < (insertUnit (units, assignments, foundContradiction) l).fst.size
j2_lt_updatedUnits_size : ↑j2 < (insertUnit (units, assignments, foundContradiction) l).fst.size
k :
  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
k_ne_j1 : ¬k = ⟨↑j1, j1_lt_updatedUnits_size⟩
k_ne_j2 : ¬k = ⟨↑j2, j2_lt_updatedUnits_size⟩
k_not_lt_units_size : ¬↑k < units.size
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ¬(units, assignments, foundContradiction).fst[↑k].fst.val = ↑i

case isFalse
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
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
j1_lt_updatedUnits_size : ↑j1 < (insertUnit (units, assignments, foundContradiction) l).fst.size
j2_lt_updatedUnits_size : ↑j2 < (insertUnit (units, assignments, foundContradiction) l).fst.size
k :
  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
k_ne_j1 : ¬k = ⟨↑j1, j1_lt_updatedUnits_size⟩
k_ne_j2 : ¬k = ⟨↑j2, j2_lt_updatedUnits_size⟩
k_not_lt_units_size : ¬↑k < units.size
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ¬(units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned).fst[↑k].fst.val =
      ↑i

Proof state:
case left
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
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
i_gt_zero : ↑i > 0
⊢ (l.fst, l.snd) = (⟨l.fst.val, ⋯⟩, l.snd)

Tactic:
rfl

Result:
no goals