-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (units : CNF.Clause (PosFin n)) :
    AssignmentsInvariant (insertRupUnits f units).1

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j1 j2 : Fin (f.insertRupUnits units).fst.rupUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRupUnits units).fst.rupUnits[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (f.insertRupUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    k ≠ j1 → k ≠ j2 → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
j1_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j1]
j1_unit_def : j1_unit = unit (f.insertRupUnits units).fst.rupUnits[j1]
⊢ (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, true) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)

Tactic:
constructor

Result:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j1 j2 : Fin (f.insertRupUnits units).fst.rupUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRupUnits units).fst.rupUnits[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (f.insertRupUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    k ≠ j1 → k ≠ j2 → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
j1_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j1]
j1_unit_def : j1_unit = unit (f.insertRupUnits units).fst.rupUnits[j1]
⊢ (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList

case right
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j1 j2 : Fin (f.insertRupUnits units).fst.rupUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRupUnits units).fst.rupUnits[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (f.insertRupUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    k ≠ j1 → k ≠ j2 → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
j1_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j1]
j1_unit_def : j1_unit = unit (f.insertRupUnits units).fst.rupUnits[j1]
⊢ unit (i, true) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)

Proof state:
case intro.inl.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRupUnits units).fst.rupUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRupUnits units).fst.rupUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRupUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    k ≠ j → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j]
j_unit_def : j_unit = unit (f.insertRupUnits units).fst.rupUnits[j]
j_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ false = b'
hp2 : decide (p ⟨i.val, ⋯⟩ = false) = true
⊢ p i = false

Tactic:
exact of_decide_eq_true hp2

Result:
no goals