-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) :
    AssignmentsInvariant (insertRatUnits f units).1

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (i, true) = j_unit
hp :
  ∃ a,
    (a, false) ∈ Clause.toList (unit (f.insertRatUnits units).fst.ratUnits[↑j]) ∧ decide (p a = false) = true ∨
      (a, true) ∈ Clause.toList (unit (f.insertRatUnits units).fst.ratUnits[↑j]) ∧ p a = true
⊢ p ⊨ (i, b)

Tactic:
rcases hp with ⟨i', hp⟩

Result:
case intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (i, true) = j_unit
i' : PosFin n
hp :
  (i', false) ∈ Clause.toList (unit (f.insertRatUnits units).fst.ratUnits[↑j]) ∧ decide (p i' = false) = true ∨
    (i', true) ∈ Clause.toList (unit (f.insertRatUnits units).fst.ratUnits[↑j]) ∧ p i' = true
⊢ p ⊨ (i, b)

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

Tactic:
rw [hp1.1] at hp2

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