-- 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:
case intro.intro
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
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
    (if acc.2.2.snd = true ∨ acc.2.2.fst = true then (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd)
    else
      match f.clauses[rupHints[↑idx]]? with
      | some (some c) =>
        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)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true))

Tactic:
split

Result:
case intro.intro.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
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd)

case intro.intro.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
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      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)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))

Proof state:
case inl.h
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
p : PosFin n → Bool
pc : ¬Clause.eval p c = true
pf : decide (Clause.eval p c = true) = true
⊢ False

Tactic:
exact pc <| of_decide_eq_true pf

Result:
no goals

Proof state:
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
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
⊢ ∀ (i : PosFin n), hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

Tactic:
intro i

Result:
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
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

Proof state:
case h.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
h✝ : rupHints[↑idx] < f.clauses.size
hc : some f.clauses[rupHints[↑idx]] = some (some c)
⊢ some c ∈ f.clauses.toList

Tactic:
simp only [Option.some.injEq] at hc

Result:
case h.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
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses[rupHints[↑idx]] = some c
⊢ some c ∈ f.clauses.toList