-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (units : Array (Literal (PosFin n))) (foundContradiction : Bool) (l : CNF.Clause (PosFin n)) :
    let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l
    (foundContradiction → ∃ i : PosFin n, assignments[i.1]'(by rw [assignments_size]; exact i.2.2) = both) → insertUnit_fold_res.2.2 →
    ∃ j : PosFin n, insertUnit_fold_res.2.1[j.1]'(by rw [size_insertUnit_fold, 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 : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
⊢ insertUnit_res.snd.fst.size = n

Tactic:
rw [size_insertUnit, h.1]

Result:
no goals

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
_hsize : acc0.snd.fst.size = n
j : PosFin n
⊢ j.val < n

Tactic:
exact j.2.2

Result:
no goals

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
⊢ acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both

Tactic:
intro foundContradiction_eq_true

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
foundContradiction_eq_true : acc0.snd.snd = true
⊢ ∃ j, acc0.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 : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
hsize : acc.snd.fst.size = n
j : PosFin n
⊢ j.val < acc.snd.fst.size

Tactic:
rw [hsize]

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
hsize : acc.snd.fst.size = n
j : PosFin n
⊢ j.val < n

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < assignments.size

Tactic:
rw [assignments_size]

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < n

Proof state:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
⊢ let insertUnit_res := insertUnit acc l';
  ∃ hsize, insertUnit_res.snd.snd = true → ∃ j, insertUnit_res.snd.fst[j.val] = both

Tactic:
intro insertUnit_res

Result:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : CNF.Clause (PosFin n)
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
⊢ ∃ hsize, insertUnit_res.snd.snd = true → ∃ j, insertUnit_res.snd.fst[j.val] = both