internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inr
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
by_cases l.2
Proof state after:
case pos
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

case neg
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case pos
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

case neg
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
. next l_eq_true =>
  rw [l_eq_true]
  simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
    Bool.not_eq_true] at hl
  split at hl <;> simp_all (config := { decide := true })
Proof state after:
case neg
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case neg
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
. next l_eq_false =>
  simp only [Bool.not_eq_true] at l_eq_false
  rw [l_eq_false]
  simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
    Bool.not_eq_true] at hl
  split at hl <;> simp_all (config := { decide := true })
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case pos
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
next l_eq_true =>
rw [l_eq_true]
simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
  Bool.not_eq_true] at hl
split at hl <;> simp_all (config := { decide := true })
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
rw [l_eq_true]
Proof state after:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
⊢ addAssignment true assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
⊢ addAssignment true assignments[l.fst.val] = both
Tactic:
simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
  Bool.not_eq_true] at hl
Proof state after:
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment true assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment true assignments[l.fst.val] = both
Tactic:
split at hl <;> simp_all (config := { decide := true })
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case neg
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
next l_eq_false =>
simp only [Bool.not_eq_true] at l_eq_false
rw [l_eq_false]
simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
  Bool.not_eq_true] at hl
split at hl <;> simp_all (config := { decide := true })
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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.get ⟨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
Proof state after:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment l.snd assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
rw [l_eq_false]
Proof state after:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment false assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
⊢ addAssignment false assignments[l.fst.val] = both
Tactic:
simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
  Bool.not_eq_true] at hl
Proof state after:
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment false assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_false : l.snd = false
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment false assignments[l.fst.val] = both
Tactic:
split at hl <;> simp_all (config := { decide := true })
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < insertUnit_fold_res.snd.fst.size
Tactic:
rw [insertUnit_fold_preserves_size, assignments_size]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n
Tactic:
exact j.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  (foundContradiction = true → ∃ i, assignments[i.val] = both) →
    insertUnit_fold_res.snd.snd = true → ∃ j, insertUnit_fold_res.snd.fst[j.val] = both
Tactic:
intro insertUnit_fold_res h0 insertUnit_fold_success
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both
Tactic:
let acc0 := (units, assignments, foundContradiction)
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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)
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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)
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both
Tactic:
have hb : ∃ _hsize : acc0.2.1.size = n, acc0.2.2 → ∃ j : PosFin n, acc0.2.1[j.1]'(by rw [assignments_size]; exact j.2.2) = both := by
  apply Exists.intro assignments_size
  intro foundContradiction_eq_true
  exact h0 foundContradiction_eq_true
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (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
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both