-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (units : CNF.Clause (PosFin n)) :
      ∀ i : Fin (f.insertRupUnits units).1.rupUnits.size, ∀ j : Fin (f.insertRupUnits units).1.rupUnits.size,
      i ≠ j → (f.insertRupUnits units).1.rupUnits[i] ≠ (f.insertRupUnits units).1.rupUnits[j]

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
⊢ False

Tactic:
by_cases j = k2

Result:
case pos
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ k1

Tactic:
rw [← i_eq_k1]

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ i

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_ne_k2 : ¬i = k2
h5 : ¬(f.insertRupUnits units).fst.rupUnits[i].fst.val = li.val
⊢ False

Tactic:
rw [hi] at h5

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_ne_k2 : ¬i = k2
h5 : ¬(li, bi).fst.val = li.val
⊢ False

Proof state:
case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (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
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : ¬i = k2
⊢ False

Tactic:
next i_ne_k2 =>
specialize h5 i i_ne_k1 i_ne_k2
rw [hi] at h5
simp only [not_true] at h5

Result:
no goals