-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem nodup_insertRatUnits {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) :
    ∀ i : Fin (f.insertRatUnits units).1.ratUnits.size, ∀ j : Fin (f.insertRatUnits units).1.ratUnits.size,
      i ≠ j → (f.insertRatUnits units).1.ratUnits[i] ≠ (f.insertRatUnits units).1.ratUnits[j]

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
⊢ (f.insertRatUnits units).fst.ratUnits[i] ≠ (f.insertRatUnits units).fst.ratUnits[j]

Tactic:
rcases hi : (insertRatUnits f units).fst.ratUnits[i] with ⟨li, bi⟩

Result:
case mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
⊢ (li, bi) ≠ (f.insertRatUnits units).fst.ratUnits[j]

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
i_eq_k : i = k
j_ne_k : j ≠ k
h4 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

Tactic:
simp +decide only [hj] at h4

Result:
no goals

Proof state:
case mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
⊢ (li, bi) ≠ (f.insertRatUnits units).fst.ratUnits[j]

Tactic:
rcases hj : (insertRatUnits f units).fst.ratUnits[j] with ⟨lj, bj⟩

Result:
case mk.mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRatUnits units).fst.ratUnits[j] = (lj, bj)
⊢ (li, bi) ≠ (lj, bj)

Proof state:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
h :
  ((f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val] ∧
      ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size),
        ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val) ∨
    (∃ j b,
        (∃ x, (f.insertRatUnits units).fst.ratUnits[j] = (⟨li.val, ⋯⟩, b)) ∧
          (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val] ∧
            hasAssignment b f.assignments[li.val] = false ∧
              ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                ¬k = j → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val) ∨
      ∃ j1 j2 h,
        (f.insertRatUnits units).fst.ratUnits[j1] = (⟨li.val, ⋯⟩, true) ∧
          (f.insertRatUnits units).fst.ratUnits[j2] = (⟨li.val, ⋯⟩, false) ∧
            (f.insertRatUnits units).fst.assignments[li.val] = both ∧
              f.assignments[li.val] = unassigned ∧
                ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                  ¬k = j1 → ¬k = j2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False

Tactic:
rcases h with ⟨_, h2⟩ | ⟨k, b, _, _, _, h4⟩ | ⟨k1, k2, li_gt_zero, h1, h2, h3, h4, h5⟩

Result:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (li, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_eq_k1 : i = k1
⊢ False

Tactic:
simp at h1

Result:
no goals