-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
    (c : DefaultClause n) :
    c ∈ toList (insertRatUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
h :
  some c ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl :
  l ∈
    (if hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true then (acc.fst, acc.2.fst, acc.2.snd)
        else
          (acc.fst.push (unit.fst, unit.snd), acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
            acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned)).fst.toList
⊢ l ∈ f.ratUnits.toList ∨ l ∈ units

Tactic:
split at hl

Result:
case isTrue
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
h :
  some c ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ (acc.fst, acc.2.fst, acc.2.snd).fst.toList
⊢ l ∈ f.ratUnits.toList ∨ l ∈ units

case isFalse
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
h :
  some c ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.ratUnits.toList ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl :
  l ∈
    (acc.fst.push (unit.fst, unit.snd), acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
          acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned).fst.toList
⊢ l ∈ f.ratUnits.toList ∨ l ∈ units