-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n)
    (p : PosFin n → Bool) (pf : p ⊨ f) :
    (insertRupUnits f (negate c)).2 = true → p ⊨ c

Proof state:
case intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : InsertUnitInvariant f.assignments ⋯ f.rupUnits f.assignments ⋯
⊢ p ⊨ c

Tactic:
have insertUnit_fold_satisfies_invariant := insertUnitInvariant_insertUnit_fold f.assignments f_readyForRupAdd.2.1 f.rupUnits
  f.assignments f_readyForRupAdd.2.1 false (negate c) h0

Result:
case intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : InsertUnitInvariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  InsertUnitInvariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
⊢ p ⊨ c

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : InsertUnitInvariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  InsertUnitInvariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.toList
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ decide (p i = false) = true

Tactic:
exfalso

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : InsertUnitInvariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  InsertUnitInvariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.toList
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
⊢ p ⊨ c

Tactic:
have false_imp : false → ∃ i : PosFin n, f.assignments[i.1]'(by rw [f_readyForRupAdd.2.1]; exact i.2.2) = both := by
  intro h
  simp at h

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
⊢ p ⊨ c

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i✝ : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i✝.val] = both
i_in_bounds : i✝.val < f.assignments.size
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i

Tactic:
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i✝ : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i✝.val] = both
i_in_bounds : i✝.val < f.assignments.size
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 h,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i