-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat)
    (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
    (ih : ConfirmRupHintFoldEntailsMotive f idx.1 acc) :
    ConfirmRupHintFoldEntailsMotive f (idx.1 + 1) ((confirmRupHint f.clauses) acc rupHints[idx])

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
    (match c.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | 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)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))

Tactic:
split

Result:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = encounteredBoth
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToEmpty
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c.reduce acc.fst = reducedToUnit (l✝, b✝)
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
    (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))

case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = 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)).fst.size =
      n ∧
    Limplies (PosFin n) f
        (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)).fst ∧
      ((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)).snd.snd.fst =
          true →
        Incompatible (PosFin n)
          (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)).fst
          f)

Tactic:
split

Result:
case isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst, acc.2.fst, false, false).fst.size = n ∧
    Limplies (PosFin n) f (acc.fst, acc.2.fst, false, false).fst ∧
      ((acc.fst, acc.2.fst, false, false).snd.snd.fst = true →
        Incompatible (PosFin n) (acc.fst, acc.2.fst, false, false).fst f)

case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
h1 : Limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → Incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    Limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      ((acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).snd.snd.fst = true →
        Incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)