Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case mk.mk.intro.inl.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
left✝ : (f.insertRupUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ∀ (j : Fin (f.insertRupUnits units).fst.rupUnits.size), ¬(f.insertRupUnits units).fst.rupUnits[j].fst.val = li.val
⊢ False

case mk.mk.intro.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k : Fin (f.insertRupUnits units).fst.rupUnits.size
b : Bool
left✝² : ∃ x, (f.insertRupUnits units).fst.rupUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRupUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k_1 = k → ¬(f.insertRupUnits units).fst.rupUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
⊢ False
Tactic:
. specialize h2 j
  rw [hj, li_eq_lj] at h2
  simp only [not_true] at h2
Proof state after:
case mk.mk.intro.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k : Fin (f.insertRupUnits units).fst.rupUnits.size
b : Bool
left✝² : ∃ x, (f.insertRupUnits units).fst.rupUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRupUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k_1 = k → ¬(f.insertRupUnits units).fst.rupUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
⊢ False