Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_assignments_invariant (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j2_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j2_unit
Tactic:
apply Exists.intro i ∘ Or.inl
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j2_unit

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j2_unit
Tactic:
rw [j2_unit_def, h2]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
Tactic:
constructor
State after:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data

case right
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)

State before:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data

case right
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
Tactic:
. have h2 : (insertRupUnits f units).fst.rupUnits[j2] = (i, false) := by
    rw [h2]
    simp only [Prod.mk.injEq, and_true]
    apply Subtype.ext
    rfl
  rw [← h2]
  apply Array.getElem_mem_data
State after:
case right
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)

State before:
case right
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
Tactic:
. rfl
State after:
no goals

State before:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data
Tactic:
have h2 : (insertRupUnits f units).fst.rupUnits[j2] = (i, false) := by
  rw [h2]
  simp only [Prod.mk.injEq, and_true]
  apply Subtype.ext
  rfl
State after:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (i, false)
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data

State before:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (i, false)
⊢ (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data
Tactic:
rw [← h2]
State after:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (i, false)
⊢ (f.insertRupUnits units).fst.rupUnits[j2] ∈ (f.insertRupUnits units).fst.rupUnits.data

State before:
case left
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
h2 : (f.insertRupUnits units).fst.rupUnits[j2] = (i, false)
⊢ (f.insertRupUnits units).fst.rupUnits[j2] ∈ (f.insertRupUnits units).fst.rupUnits.data
Tactic:
apply Array.getElem_mem_data
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (f.insertRupUnits units).fst.rupUnits[j2] = (i, false)
Tactic:
rw [h2]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false) = (i, false)

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false) = (i, false)
Tactic:
simp only [Prod.mk.injEq, and_true]
State after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ ⟨i.val, ⋯⟩ = i

State before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ ⟨i.val, ⋯⟩ = i
Tactic:
apply Subtype.ext
State after:
case a
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ ⟨i.val, ⋯⟩.val = i.val

State before:
case a
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ ⟨i.val, ⋯⟩.val = i.val
Tactic:
rfl
State after:
no goals

State before:
case right
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant 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.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits 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.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]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.data ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
Tactic:
rfl
State after:
no goals