internlm/Lean-Github huggingface dataset:
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
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
have l_in_bounds : l.1.1 < assignments.size := by rw [assignments_size]; exact l.1.2.2
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
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
l_in_bounds : l.fst.val < assignments.size
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.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
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
l_in_bounds : l.fst.val < assignments.size
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
split at insertUnit_success
Proof state after:
case isTrue
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
h✝ : 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

case isFalse
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
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case isTrue
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
h✝ : 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

case isFalse
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
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. next hl =>
  simp only [insertUnit, hl, Prod.mk.eta, ite_true]
  exact h insertUnit_success
Proof state after:
case isFalse
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
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case isFalse
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
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. next hl =>
  simp only [Bool.or_eq_true] at insertUnit_success
  rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
  . simp only [insertUnit, hl, Prod.mk.eta, ite_false]
    rcases h foundContradiction_eq_true with ⟨i, h⟩
    have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
    apply Exists.intro i
    by_cases l.1.1 = i.1
    . next l_eq_i =>
      simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
      exact add_of_both_eq_both l.2
    . next l_ne_i =>
      rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
      exact h
  . apply Exists.intro l.1
    simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
    simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
    by_cases l.2
    . 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 })
    . 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
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ l.fst.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 : 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 :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ l.fst.val < n
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
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ l.fst.val < n
Tactic:
exact l.1.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case isTrue
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
h✝ : 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:
next hl =>
simp only [insertUnit, hl, Prod.mk.eta, ite_true]
exact h insertUnit_success
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
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [insertUnit, hl, Prod.mk.eta, ite_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
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, assignments[j.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
insertUnit_success : (units, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, assignments[j.val] = both
Tactic:
exact h insertUnit_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case isFalse
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
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
next hl =>
simp only [Bool.or_eq_true] at insertUnit_success
rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
. simp only [insertUnit, hl, Prod.mk.eta, ite_false]
  rcases h foundContradiction_eq_true with ⟨i, h⟩
  have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
  apply Exists.intro i
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
    exact add_of_both_eq_both l.2
  . next l_ne_i =>
    rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
    exact h
. apply Exists.intro l.1
  simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
  simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
  by_cases l.2
  . 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 })
  . 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
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [Bool.or_eq_true] at insertUnit_success
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
insertUnit_success : foundContradiction = true ∨ (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.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
insertUnit_success : foundContradiction = true ∨ (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
Proof state after:
case inl
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
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

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[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inl
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
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

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[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. simp only [insertUnit, hl, Prod.mk.eta, ite_false]
  rcases h foundContradiction_eq_true with ⟨i, h⟩
  have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
  apply Exists.intro i
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
    exact add_of_both_eq_both l.2
  . next l_ne_i =>
    rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
    exact h
Proof state after:
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[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
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[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
. apply Exists.intro l.1
  simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
  simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
  by_cases l.2
  . 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 })
  . 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