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

Tactic:
exact i.2.2

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
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)

Tactic:
have plb := limplies_of_reducedToUnit c acc.1 ⟨l, b⟩ heq p pacc pc

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)
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)

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

Tactic:
have i_in_bounds : i.1 < acc.1.size := by rw [hsize]; exact i.2.2

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

Proof state:
case pos
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
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : (if decide (true = false) = true then hasPosAssignment else hasNegAssignment) acc.fst[i.val] = false
hb : b = true
⊢ (if decide (true = false) = true then hasPosAssignment else hasNegAssignment)
      ((if True then addPosAssignment else addNegAssignment) acc.fst[i.val]) =
    false

Tactic:
simp [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_addPos]

Result:
case pos
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
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : (if decide (true = false) = true then hasPosAssignment else hasNegAssignment) acc.fst[i.val] = false
hb : b = true
⊢ acc.fst[i.val].hasNegAssignment = false

Proof state:
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))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

Tactic:
apply And.intro hsize ∘ And.intro h1

Result:
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))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → Incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f