-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assignment)
    (assignments_size : assignments.size = n)
    (units : Array (Literal (PosFin n))) (foundContradiction : Bool) (l : Literal (PosFin n)) :
    let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
    (foundContradiction → ∃ i : PosFin n, assignments[i.1]'(by rw [assignments_size]; exact i.2.2) = both) → insertUnit_res.2.2 →
    ∃ j : PosFin n, insertUnit_res.2.1[j.1]'(by rw [size_insertUnit, assignments_size]; exact j.2.2) = both

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val] != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment false assignments[l.fst.val] = both

Tactic:
simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val] != unassigned) = true
l_eq_false : l.snd = false
hl :
  (match assignments[l.fst.val] with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment false assignments[l.fst.val] = both

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val] != unassigned) = true
l_eq_false : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

Tactic:
simp only [Bool.not_eq_true] at l_eq_false

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val] != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment l.snd assignments[l.fst.val] = both

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

Tactic:
simp only [insertUnit, hl, ite_true]

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, assignments[j.val] = both

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
⊢ let insertUnit_res := insertUnit (units, assignments, foundContradiction) l;
  (foundContradiction = true → ∃ i, assignments[i.val] = both) →
    insertUnit_res.snd.snd = true → ∃ j, insertUnit_res.snd.fst[j.val] = both

Tactic:
intro insertUnit_res h insertUnit_success

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
l_ne_i : ¬l.fst.val = i.val
⊢ (if false = 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)).snd.fst[i.val] =
    both

Tactic:
simp [Array.getElem_modify_of_ne l_ne_i]

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
l_ne_i : ¬l.fst.val = i.val
⊢ assignments[i.val] = both

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n

Tactic:
exact j.2.2

Result:
no goals