-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (units : CNF.Clause (PosFin n)) :
    AssignmentsInvariant (insertRupUnits f units).1

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
c : DefaultClause n
cf :
  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
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true

Tactic:
rcases cf with cf | cf | cf

Result:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
c : DefaultClause n
cf : some c ∈ f.clauses.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true

case inr.inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
c : DefaultClause n
cf : ∃ a, (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = c
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true

case inr.inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
c : DefaultClause n
cf : ∃ a, (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = c
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true