-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
    (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat)
    (f'_assignments_size : (performRupCheck f rupHints).1.assignments.size = n)
    (derivedLits : CNF.Clause (PosFin n))
    (derivedLits_satisfies_invariant:
      DerivedLitsInvariant f f_assignments_size (performRupCheck f rupHints).fst.assignments f'_assignments_size derivedLits)
    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits })
    (i j : Fin (Array.size derivedLits_arr)) (i_ne_j : i ≠ j) :
    derivedLits_arr[i] ≠ derivedLits_arr[j]

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < List.length derivedLits
j_in_bounds : ↑j < List.length derivedLits
k1 k2 : Fin (List.length derivedLits)
left✝³ : (List.get derivedLits k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (List.get derivedLits k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (List.get derivedLits k1).snd = true
k2_eq_false : (List.get derivedLits k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin (List.length derivedLits)), k ≠ k1 → k ≠ k2 → (List.get derivedLits k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
i_eq_k1 : ⟨↑i, i_in_bounds⟩ = k1
⊢ False

Tactic:
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
  intro j_eq_k1
  rw [← j_eq_k1] at i_eq_k1
  simp only [Fin.mk.injEq] at i_eq_k1
  exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < List.length derivedLits
j_in_bounds : ↑j < List.length derivedLits
k1 k2 : Fin (List.length derivedLits)
left✝³ : (List.get derivedLits k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (List.get derivedLits k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (List.get derivedLits k1).snd = true
k2_eq_false : (List.get derivedLits k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin (List.length derivedLits)), k ≠ k1 → k ≠ k2 → (List.get derivedLits k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
i_eq_k1 : ⟨↑i, i_in_bounds⟩ = k1
j_ne_k1 : ⟨↑j, j_in_bounds⟩ ≠ k1
⊢ False

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < List.length derivedLits
j_in_bounds : ↑j < List.length derivedLits
k1 k2 : Fin (List.length derivedLits)
left✝³ : (List.get derivedLits k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (List.get derivedLits k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (List.get derivedLits k1).snd = true
k2_eq_false : (List.get derivedLits k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin (List.length derivedLits)), k ≠ k1 → k ≠ k2 → (List.get derivedLits k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
⊢ False

Tactic:
have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
  intro j_eq_k2
  rw [← j_eq_k2] at k2_eq_false
  simp only [List.get_eq_getElem] at k2_eq_false
  simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
  simp [derivedLits_arr_def, k2_eq_false, li_eq_lj, li] at li_eq_true

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < List.length derivedLits
j_in_bounds : ↑j < List.length derivedLits
k1 k2 : Fin (List.length derivedLits)
left✝³ : (List.get derivedLits k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (List.get derivedLits k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (List.get derivedLits k1).snd = true
k2_eq_false : (List.get derivedLits k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin (List.length derivedLits)), k ≠ k1 → k ≠ k2 → (List.get derivedLits k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
⊢ False

Proof state:
case inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < List.length derivedLits
j_in_bounds : ↑j < List.length derivedLits
left✝ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = f.assignments[↑⟨li.fst.val, ⋯⟩]
h2 : ∀ (l : Literal (PosFin n)), l ∈ derivedLits → l.fst.val ≠ ↑⟨li.fst.val, ⋯⟩
⊢ False

Tactic:
exact h2 li li_in_derivedLits rfl

Result:
no goals