Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ 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.insertRatUnits units).fst.ratUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j1] = (⟨i.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[↑j2] = (⟨i.val, ⋯⟩, false)
left✝¹ : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j1 → k ≠ j2 → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
j1_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j1]
j1_unit_def : j1_unit = unit (f.insertRatUnits units).fst.ratUnits[j1]
j1_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRatUnits units).fst.ratUnits[j2]
j2_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j2_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j2_unit
i1 i2 : PosFin n
hp1 :
  (i1, false) = (f.insertRatUnits units).fst.ratUnits[j1] ∧ decide (p i1 = false) = true ∨
    (i1, true) = (f.insertRatUnits units).fst.ratUnits[j1] ∧ p i1 = true
hp2 :
  (i2, false) = (f.insertRatUnits units).fst.ratUnits[j2] ∧ decide (p i2 = false) = true ∨
    (i2, true) = (f.insertRatUnits units).fst.ratUnits[j2] ∧ p i2 = true
⊢ p ⊨ (i, b)
Tactic:
simp_all only [Bool.decide_eq_false, Bool.not_eq_true', ne_eq, Fin.getElem_fin, Prod.mk.injEq,
  and_false, false_and, and_true, false_or, or_false]
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
j1 j2 : Fin (f.insertRatUnits units).fst.ratUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
j1_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j1]
j2_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j2]
i1 i2 : PosFin n
h :
  insertUnit_invariant f.assignments ⋯ (f.insertRatUnits units).fst.ratUnits (f.insertRatUnits units).fst.assignments ⋯
hb : hasAssignment b both = true
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
h1 : (f.insertRatUnits units).fst.ratUnits[↑j1] = (⟨i.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[↑j2] = (⟨i.val, ⋯⟩, false)
left✝¹ : (f.insertRatUnits units).fst.assignments[i.val] = both
left✝ : f.assignments[i.val] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = j1 → ¬k = j2 → ¬(f.insertRatUnits units).fst.ratUnits[↑k].fst.val = i.val
j1_unit_def : j1_unit = unit (⟨i.val, ⋯⟩, true)
j1_unit_in_insertRatUnits_res :
  ∃ i_1,
    (i_1, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i_1, false) = unit (⟨i.val, ⋯⟩, true) ∨
      (i_1, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i_1, true) = unit (⟨i.val, ⋯⟩, true)
j2_unit_def : j2_unit = unit (⟨i.val, ⋯⟩, false)
j2_unit_in_insertRatUnits_res :
  ∃ i_1,
    (i_1, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i_1, false) = unit (⟨i.val, ⋯⟩, false) ∨
      (i_1, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i_1, true) = unit (⟨i.val, ⋯⟩, false)
hp1 : i1 = ⟨i.val, ⋯⟩ ∧ p i1 = true
hp2 : i2 = ⟨i.val, ⋯⟩ ∧ p i2 = false
⊢ p ⊨ (i, b)