-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (rupHints : Array Nat)
    (p : PosFin n → Bool) (pf : p ⊨ f) :
    let fc := insertRatUnits f (negate c)
    let confirmRupHint_fold_res := rupHints.foldl (confirmRupHint fc.1.clauses) (fc.1.assignments, [], false, false) 0 rupHints.size
    confirmRupHint_fold_res.2.2.1 = true → p ⊨ c

Proof state:
case neg.intro.intro.inl.intro.inl.intro.intro.inr.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := fc.fst.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝ : (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst.size = n
h1 :
  Limplies (PosFin n) fc.fst
    (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst
h2 :
  (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).snd.snd.fst = true →
    Incompatible (PosFin n)
      (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst fc.fst
fc_incompatible_confirmRupHint_fold_res :
  Incompatible (PosFin n) fc.fst
    (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, false) = unsat_c
v' : PosFin n
v'_in_c : (v', true) ∈ c.toList
v'_eq_v : Literal.negate (v', true) = (v, false)
⊢ False

Tactic:
simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_true] at v'_eq_v

Result:
case neg.intro.intro.inl.intro.inl.intro.intro.inr.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := fc.fst.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝ : (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst.size = n
h1 :
  Limplies (PosFin n) fc.fst
    (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst
h2 :
  (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).snd.snd.fst = true →
    Incompatible (PosFin n)
      (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst fc.fst
fc_incompatible_confirmRupHint_fold_res :
  Incompatible (PosFin n) fc.fst
    (Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, false) = unsat_c
v' : PosFin n
v'_in_c : (v', true) ∈ c.toList
v'_eq_v : v' = v
⊢ False

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := fc.fst.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (fc.fst.assignments, [], false, false)
⊢ p ⊨ c

Tactic:
have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : motive idx.1 acc) :=
  confirmRupHint_preserves_motive fc.1 rupHints idx acc ih

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := fc.fst.ConfirmRupHintFoldEntailsMotive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
⊢ p ⊨ c

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := fc.fst.ConfirmRupHintFoldEntailsMotive
⊢ Limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments

Tactic:
have fc_satisfies_AssignmentsInvariant : AssignmentsInvariant fc.1 :=
  assignmentsInvariant_insertRatUnits f hf (negate c)

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop := fc.fst.ConfirmRupHintFoldEntailsMotive
fc_satisfies_AssignmentsInvariant : fc.fst.AssignmentsInvariant
⊢ Limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments