-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat) (i : Fin rupHints.size)
    (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
    (ih : ∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1) :
    let rupHint_res := (confirmRupHint f.clauses) acc rupHints[i]
    ∃ hsize : rupHint_res.1.size = n, DerivedLitsInvariant f f_assignments_size rupHint_res.1 hsize rupHint_res.2.1

Proof state:
case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_options :
  f.clauses[rupHints[↑i]]? = none ∨ f.clauses[rupHints[↑i]]? = some none ∨ ∃ c, f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.DerivedLitsInvariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

Tactic:
rcases rupHint_clause_options with rupHint_clause_eq_none | rupHint_clause_eq_some_none | ⟨c, rupHint_clause_eq_c⟩

Result:
case intro.isFalse.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_none : f.clauses[rupHints[↑i]]? = none
⊢ f.DerivedLitsInvariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.DerivedLitsInvariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.DerivedLitsInvariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst