internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ ∃ j b i_gt_zero,
    (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
Tactic:
refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
Proof state after:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (insertUnit (units, assignments, foundContradiction) l).fst[↑⟨↑j, j_lt_updatedUnits_size⟩] = (⟨↑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, j_lt_updatedUnits_size⟩ →
            ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (insertUnit (units, assignments, foundContradiction) l).fst[↑⟨↑j, j_lt_updatedUnits_size⟩] = (⟨↑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, j_lt_updatedUnits_size⟩ →
            ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Tactic:
simp only [insertUnit, h5, Prod.mk.eta, ite_false]
Proof state after:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (units.push l)[↑j] = (⟨↑i, ⋯⟩, b) ∧
    (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment b assignments0[↑i] ∧
      hasAssignment b assignments0[↑i] = false ∧
        ∀
          (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 = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment b assignments0[↑i] ∧
    hasAssignment b assignments0[↑i] = false ∧
      ∀
        (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 = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
. constructor
  . rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l), h2]
  . constructor
    . exact h3
    . intro k k_ne_j
      rw [Array.get_push]
      by_cases h : k.val < units.size
      . simp only [h, dite_true]
        have k_ne_j : ⟨k.1, h⟩ ≠ j := by
          intro k_eq_j
          simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j
        exact h4 ⟨k.1, h⟩ k_ne_j
      . simp only [h, dite_false]
        exact Ne.symm i_ne_l
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
⊢ ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
Tactic:
simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push]
Proof state after:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
⊢ ↑j < units.size + 1
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
⊢ ↑j < units.size + 1
Tactic:
exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (units.push l)[↑j] = (⟨↑i, ⋯⟩, b)
Tactic:
rw [Array.get_push_lt units l j.1 j.2, h1]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ hasAssignment b assignments0[↑i] = false ∧
    ∀
      (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 = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
. constructor
  . exact h3
  . intro k k_ne_j
    rw [Array.get_push]
    by_cases h : k.val < units.size
    . simp only [h, dite_true]
      have k_ne_j : ⟨k.1, h⟩ ≠ j := by
        intro k_eq_j
        simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j
      exact h4 ⟨k.1, h⟩ k_ne_j
    . simp only [h, dite_false]
      exact Ne.symm i_ne_l
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment b assignments0[↑i]
Tactic:
rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l), h2]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (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 = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
. intro k k_ne_j
  rw [Array.get_push]
  by_cases h : k.val < units.size
  . simp only [h, dite_true]
    have k_ne_j : ⟨k.1, h⟩ ≠ j := by
      intro k_eq_j
      simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j
    exact h4 ⟨k.1, h⟩ k_ne_j
  . simp only [h, dite_false]
    exact Ne.symm i_ne_l
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ hasAssignment b assignments0[↑i] = false
Tactic:
exact h3
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (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 = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
intro k k_ne_j
Proof state after:
case right.right.right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬(units.push l)[↑k].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
rw [Array.get_push]
Proof state after:
case right.right.right
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
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬(if h : ↑k < units.size then units[↑k] else l).fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_ne_l : ¬↑i = l.fst.val
j_lt_updatedUnits_size : ↑j < (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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ¬↑k < units.size
⊢ ¬(if h : ↑k < units.size then units[↑k] else l).fst.val = ↑i
Tactic:
. simp only [h, dite_false]
  exact Ne.symm i_ne_l
Proof state after:
no goals