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

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
l' : Literal (PosFin n)
⊢ l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList

Tactic:
intro h

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
l' : Literal (PosFin n)
h : l' ∈ (units, assignments, foundContradiction).fst.toList
⊢ l' ∈ l ∨ l' ∈ units.toList

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList) →
      ∀ (l'' : Literal (PosFin n)),
        l'' ∈ l → ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.toList → l' ∈ l ∨ l' ∈ units.toList
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.toList → l' ∈ l ∨ l' ∈ units.toList

Tactic:
exact List.foldlRecOn l insertUnit (units, assignments, foundContradiction) hb hl

Result:
no goals

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
⊢ l' ∈ l ∨ l' ∈ units.toList

Tactic:
rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc

Result:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.toList

case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
l'_in_acc : l' ∈ acc.fst.toList
⊢ l' ∈ l ∨ l' ∈ units.toList

Proof state:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
l'_in_acc : l' ∈ acc.fst.toList
⊢ l' ∈ l ∨ l' ∈ units.toList

Tactic:
exact h l' l'_in_acc

Result:
no goals

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
⊢ ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.toList → l' ∈ l ∨ l' ∈ units.toList

Tactic:
intro l' l'_in_res

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
⊢ l' ∈ l ∨ l' ∈ units.toList

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

Tactic:
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.toList → l' ∈ l ∨ l' ∈ units.toList := by
  intro h
  exact Or.inr h

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.toList → l' ∈ l ∨ l' ∈ units.toList

Proof state:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.toList

Tactic:
exact Or.inl l''_in_l

Result:
no goals