-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
    (foundContradiction : Bool) (l : Literal (PosFin n)) :
    let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
    ∀ l' : Literal (PosFin n), l' ∈ insertUnit_res.1.toList → l' = l ∨ l' ∈ units.toList

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ (insertUnit (units, assignments, foundContradiction) l).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Tactic:
simp only [insertUnit] at l'_in_insertUnit_res

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res :
  l' ∈
    (if hasAssignment l.snd assignments[l.fst.val]! = 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)).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Proof state:
case isTrue
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ (units, assignments, foundContradiction).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Tactic:
exact Or.inr l'_in_insertUnit_res

Result:
no goals

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ insertUnit_res.fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Tactic:
simp only [insertUnit_res] at *

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ (insertUnit (units, assignments, foundContradiction) l).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
⊢ let insertUnit_res := insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_res.fst.toList → l' = l ∨ l' ∈ units.toList

Tactic:
intro insertUnit_res l' l'_in_insertUnit_res

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ insertUnit_res.fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Proof state:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ units.toList ∨ l' = (l.fst, l.snd)
⊢ l' = l ∨ l' ∈ units.toList

Tactic:
exact Or.symm l'_in_insertUnit_res

Result:
no goals

Proof state:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Tactic:
simp only [Array.push_toList, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res

Result:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ units.toList ∨ l' = (l.fst, l.snd)
⊢ l' = l ∨ l' ∈ units.toList

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res :
  l' ∈
    (if hasAssignment l.snd assignments[l.fst.val]! = 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)).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

Tactic:
split at l'_in_insertUnit_res

Result:
case isTrue
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ (units, assignments, foundContradiction).fst.toList
⊢ l' = l ∨ l' ∈ units.toList

case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.toList
⊢ l' = l ∨ l' ∈ units.toList