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

Proof state:
case inr.inl.intro.inl.intro
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units →
          ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.toList ∨
      (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c

Tactic:
rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold

Result:
case inr.inl.intro.inl.intro.inl
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units →
          ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ f.rupUnits.toList
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.toList ∨
      (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c

case inr.inl.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units →
          ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.toList ∨
      (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c

Proof state:
case inr.inl.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units →
          ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.rupUnits.toList
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.toList ∨
      (∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c

Tactic:
apply Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro i ∘ Or.inr

Result:
case inr.inl.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units →
          ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.rupUnits.toList
⊢ (i, true) ∈ f.rupUnits.toList ∧ unit (i, true) = c

Proof state:
case inr.inl.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units →
          ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.rupUnits.toList
⊢ (i, true) ∈ f.rupUnits.toList ∧ unit (i, true) = c

Tactic:
exact ⟨h_insertUnit_fold, h2⟩

Result:
no goals