Theorem: LRAT.DefaultFormula.insertRatUnits_nodup (LeanSAT/LRAT/Formula/RatAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ ∀ (i j : Fin (f.insertRatUnits units).fst.ratUnits.size),
    i ≠ j → (f.insertRatUnits units).fst.ratUnits[i] ≠ (f.insertRatUnits units).fst.ratUnits[j]
Tactic:
intro i j i_ne_j
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
⊢ (f.insertRatUnits units).fst.ratUnits[i] ≠ (f.insertRatUnits units).fst.ratUnits[j]

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
⊢ (f.insertRatUnits units).fst.ratUnits[i] ≠ (f.insertRatUnits units).fst.ratUnits[j]
Tactic:
rcases hi : (insertRatUnits f units).fst.ratUnits[i] with ⟨li, bi⟩
State after:
case mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
⊢ (li, bi) ≠ (f.insertRatUnits units).fst.ratUnits[j]

State before:
case mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
⊢ (li, bi) ≠ (f.insertRatUnits units).fst.ratUnits[j]
Tactic:
rcases hj : (insertRatUnits f units).fst.ratUnits[j] with ⟨lj, bj⟩
State after:
case mk.mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRatUnits units).fst.ratUnits[j] = (lj, bj)
⊢ (li, bi) ≠ (lj, bj)

State before:
case mk.mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRatUnits units).fst.ratUnits[j] = (lj, bj)
⊢ (li, bi) ≠ (lj, bj)
Tactic:
intro heq
State after:
case mk.mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRatUnits units).fst.ratUnits[j] = (lj, bj)
heq : (li, bi) = (lj, bj)
⊢ False

State before:
case mk.mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRatUnits units).fst.ratUnits[j] = (lj, bj)
heq : (li, bi) = (lj, bj)
⊢ False
Tactic:
cases heq
State after:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
⊢ False

State before:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
⊢ False
Tactic:
have h := insertRatUnits_postcondition f hf units ⟨li.1, li.2.2⟩
State after:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
h :
  let assignments_i := (f.insertRatUnits units).fst.assignments[↑⟨li.val, ⋯⟩];
  let original_assignments_i := f.assignments[↑⟨li.val, ⋯⟩];
  (assignments_i = original_assignments_i ∧
      ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size),
        (f.insertRatUnits units).fst.ratUnits[j].fst.val ≠ ↑⟨li.val, ⋯⟩) ∨
    (∃ j b i_gt_zero,
        (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨li.val, ⋯⟩) ∨
      ∃ j1 j2 i_gt_zero,
        (f.insertRatUnits units).fst.ratUnits[j1] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, true) ∧
          (f.insertRatUnits units).fst.ratUnits[j2] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                  k ≠ j1 → k ≠ j2 → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨li.val, ⋯⟩
⊢ False

State before:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
h :
  let assignments_i := (f.insertRatUnits units).fst.assignments[↑⟨li.val, ⋯⟩];
  let original_assignments_i := f.assignments[↑⟨li.val, ⋯⟩];
  (assignments_i = original_assignments_i ∧
      ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size),
        (f.insertRatUnits units).fst.ratUnits[j].fst.val ≠ ↑⟨li.val, ⋯⟩) ∨
    (∃ j b i_gt_zero,
        (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨li.val, ⋯⟩) ∨
      ∃ j1 j2 i_gt_zero,
        (f.insertRatUnits units).fst.ratUnits[j1] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, true) ∧
          (f.insertRatUnits units).fst.ratUnits[j2] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                  k ≠ j1 → k ≠ j2 → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨li.val, ⋯⟩
⊢ False
Tactic:
simp only [ne_eq, Bool.not_eq_true, exists_and_right] at h
State after:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
h :
  ((f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val] ∧
      ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size),
        ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val) ∨
    (∃ j b,
        (∃ x, (f.insertRatUnits units).fst.ratUnits[j] = (⟨li.val, ⋯⟩, b)) ∧
          (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val] ∧
            hasAssignment b f.assignments[li.val] = false ∧
              ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                ¬k = j → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val) ∨
      ∃ j1 j2 i_gt_zero,
        (f.insertRatUnits units).fst.ratUnits[j1] = (⟨li.val, ⋯⟩, true) ∧
          (f.insertRatUnits units).fst.ratUnits[j2] = (⟨li.val, ⋯⟩, false) ∧
            (f.insertRatUnits units).fst.assignments[li.val] = both ∧
              f.assignments[li.val] = unassigned ∧
                ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                  ¬k = j1 → ¬k = j2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False

State before:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
h :
  ((f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val] ∧
      ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size),
        ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val) ∨
    (∃ j b,
        (∃ x, (f.insertRatUnits units).fst.ratUnits[j] = (⟨li.val, ⋯⟩, b)) ∧
          (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val] ∧
            hasAssignment b f.assignments[li.val] = false ∧
              ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                ¬k = j → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val) ∨
      ∃ j1 j2 i_gt_zero,
        (f.insertRatUnits units).fst.ratUnits[j1] = (⟨li.val, ⋯⟩, true) ∧
          (f.insertRatUnits units).fst.ratUnits[j2] = (⟨li.val, ⋯⟩, false) ∧
            (f.insertRatUnits units).fst.assignments[li.val] = both ∧
              f.assignments[li.val] = unassigned ∧
                ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
                  ¬k = j1 → ¬k = j2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False
Tactic:
rcases h with ⟨_, h2⟩ | ⟨k, b, _, _, _, h4⟩ | ⟨k1, k2, li_gt_zero, h1, h2, h3, h4, h5⟩
State after:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False

State before:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False
Tactic:
. specialize h2 j
  rw [hj] at h2
  contradiction
State after:
case mk.mk.refl.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False

State before:
case mk.mk.refl.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
⊢ False

case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False
Tactic:
. by_cases i = k
  . next i_eq_k =>
    have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm
    specialize h4 j j_ne_k
    simp (config := { decide := true }) only [hj] at h4
  . next i_ne_k =>
    specialize h4 i i_ne_k
    simp (config := { decide := true }) only [hi] at h4
State after:
case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False

State before:
case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False
Tactic:
. by_cases bi
  . next bi_eq_true =>
    by_cases i = k1
    . next i_eq_k1 =>
      have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
      by_cases j = k2
      . next j_eq_k2 =>
        rw [← j_eq_k2, hj, bi_eq_true] at h2
        simp at h2
      . next j_ne_k2 =>
        specialize h5 j j_ne_k1 j_ne_k2
        simp (config := { decide := true }) only [hj] at h5
    . next i_ne_k1 =>
      by_cases i = k2
      . next i_eq_k2 =>
        rw [← i_eq_k2, hi, bi_eq_true] at h2
        simp at h2
      . next i_ne_k2 =>
        specialize h5 i i_ne_k1 i_ne_k2
        simp only [hi, not_true] at h5
  . next bi_eq_false =>
    simp only [Bool.not_eq_true] at bi_eq_false
    by_cases i = k2
    . next i_eq_k2 =>
      have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
      by_cases j = k1
      . next j_eq_k1 =>
        rw [← j_eq_k1, hj, bi_eq_false] at h1
        simp at h1
      . next j_ne_k1 =>
        specialize h5 j j_ne_k1 j_ne_k2
        simp (config := { decide := true }) only [hj] at h5
    . next i_ne_k2 =>
      by_cases i = k1
      . next i_eq_k1 =>
        rw [← i_eq_k1, hi, bi_eq_false] at h1
        simp at h1
      . next i_ne_k1 =>
        specialize h5 i i_ne_k1 i_ne_k2
        simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Tactic:
specialize h2 j
State after:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

State before:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Tactic:
rw [hj] at h2
State after:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ¬(li, bi).fst.val = li.val
⊢ False

State before:
case mk.mk.refl.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
left✝ : (f.insertRatUnits units).fst.assignments[li.val] = f.assignments[li.val]
h2 : ¬(li, bi).fst.val = li.val
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case mk.mk.refl.inr.inl.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
⊢ False
Tactic:
by_cases i = k
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : i = k
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : ¬i = k
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : i = k
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : ¬i = k
⊢ False
Tactic:
. next i_eq_k =>
  have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm
  specialize h4 j j_ne_k
  simp (config := { decide := true }) only [hj] at h4
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : ¬i = k
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : ¬i = k
⊢ False
Tactic:
. next i_ne_k =>
  specialize h4 i i_ne_k
  simp (config := { decide := true }) only [hi] at h4
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : i = k
⊢ False
Tactic:
next i_eq_k =>
have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm
specialize h4 j j_ne_k
simp (config := { decide := true }) only [hj] at h4
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_eq_k : i = k
⊢ False
Tactic:
have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_eq_k : i = k
j_ne_k : j ≠ k
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_eq_k : i = k
j_ne_k : j ≠ k
⊢ False
Tactic:
specialize h4 j j_ne_k
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
i_eq_k : i = k
j_ne_k : j ≠ k
h4 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
i_eq_k : i = k
j_ne_k : j ≠ k
h4 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Tactic:
simp (config := { decide := true }) only [hj] at h4
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_eq_k : i = k
⊢ j ≠ k
Tactic:
rw [← i_eq_k]
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_eq_k : i = k
⊢ j ≠ i

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_eq_k : i = k
⊢ j ≠ i
Tactic:
exact i_ne_j.symm
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
h✝ : ¬i = k
⊢ False
Tactic:
next i_ne_k =>
specialize h4 i i_ne_k
simp (config := { decide := true }) only [hi] at h4
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
h4 :
  ∀ (k_1 : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k_1 = k → ¬(f.insertRatUnits units).fst.ratUnits[k_1].fst.val = li.val
i_ne_k : ¬i = k
⊢ False
Tactic:
specialize h4 i i_ne_k
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
i_ne_k : ¬i = k
h4 : ¬(f.insertRatUnits units).fst.ratUnits[i].fst.val = li.val
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k : Fin (f.insertRatUnits units).fst.ratUnits.size
b : Bool
left✝² : ∃ x, (f.insertRatUnits units).fst.ratUnits[k] = (⟨li.val, ⋯⟩, b)
left✝¹ : (f.insertRatUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val]
left✝ : hasAssignment b f.assignments[li.val] = false
i_ne_k : ¬i = k
h4 : ¬(f.insertRatUnits units).fst.ratUnits[i].fst.val = li.val
⊢ False
Tactic:
simp (config := { decide := true }) only [hi] at h4
State after:
no goals

State before:
case mk.mk.refl.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
⊢ False
Tactic:
by_cases bi
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : bi = true
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : ¬bi = true
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : bi = true
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : ¬bi = true
⊢ False
Tactic:
. next bi_eq_true =>
  by_cases i = k1
  . next i_eq_k1 =>
    have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
    by_cases j = k2
    . next j_eq_k2 =>
      rw [← j_eq_k2, hj, bi_eq_true] at h2
      simp at h2
    . next j_ne_k2 =>
      specialize h5 j j_ne_k1 j_ne_k2
      simp (config := { decide := true }) only [hj] at h5
  . next i_ne_k1 =>
    by_cases i = k2
    . next i_eq_k2 =>
      rw [← i_eq_k2, hi, bi_eq_true] at h2
      simp at h2
    . next i_ne_k2 =>
      specialize h5 i i_ne_k1 i_ne_k2
      simp only [hi, not_true] at h5
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : ¬bi = true
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : ¬bi = true
⊢ False
Tactic:
. next bi_eq_false =>
  simp only [Bool.not_eq_true] at bi_eq_false
  by_cases i = k2
  . next i_eq_k2 =>
    have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
    by_cases j = k1
    . next j_eq_k1 =>
      rw [← j_eq_k1, hj, bi_eq_false] at h1
      simp at h1
    . next j_ne_k1 =>
      specialize h5 j j_ne_k1 j_ne_k2
      simp (config := { decide := true }) only [hj] at h5
  . next i_ne_k2 =>
    by_cases i = k1
    . next i_eq_k1 =>
      rw [← i_eq_k1, hi, bi_eq_false] at h1
      simp at h1
    . next i_ne_k1 =>
      specialize h5 i i_ne_k1 i_ne_k2
      simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : bi = true
⊢ False
Tactic:
next bi_eq_true =>
by_cases i = k1
. next i_eq_k1 =>
  have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
  by_cases j = k2
  . next j_eq_k2 =>
    rw [← j_eq_k2, hj, bi_eq_true] at h2
    simp at h2
  . next j_ne_k2 =>
    specialize h5 j j_ne_k1 j_ne_k2
    simp (config := { decide := true }) only [hj] at h5
. next i_ne_k1 =>
  by_cases i = k2
  . next i_eq_k2 =>
    rw [← i_eq_k2, hi, bi_eq_true] at h2
    simp at h2
  . next i_ne_k2 =>
    specialize h5 i i_ne_k1 i_ne_k2
    simp only [hi, not_true] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
⊢ False
Tactic:
by_cases i = k1
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : i = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : i = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False
Tactic:
. next i_eq_k1 =>
  have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
  by_cases j = k2
  . next j_eq_k2 =>
    rw [← j_eq_k2, hj, bi_eq_true] at h2
    simp at h2
  . next j_ne_k2 =>
    specialize h5 j j_ne_k1 j_ne_k2
    simp (config := { decide := true }) only [hj] at h5
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False
Tactic:
. next i_ne_k1 =>
  by_cases i = k2
  . next i_eq_k2 =>
    rw [← i_eq_k2, hi, bi_eq_true] at h2
    simp at h2
  . next i_ne_k2 =>
    specialize h5 i i_ne_k1 i_ne_k2
    simp only [hi, not_true] at h5
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : i = k1
⊢ False
Tactic:
next i_eq_k1 =>
have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
by_cases j = k2
. next j_eq_k2 =>
  rw [← j_eq_k2, hj, bi_eq_true] at h2
  simp at h2
. next j_ne_k2 =>
  specialize h5 j j_ne_k1 j_ne_k2
  simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ False
Tactic:
have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
⊢ False
Tactic:
by_cases j = k2
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Tactic:
. next j_eq_k2 =>
  rw [← j_eq_k2, hj, bi_eq_true] at h2
  simp at h2
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Tactic:
. next j_ne_k2 =>
  specialize h5 j j_ne_k1 j_ne_k2
  simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ k1
Tactic:
rw [← i_eq_k1]
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ i

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ i
Tactic:
exact i_ne_j.symm
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False
Tactic:
next j_eq_k2 =>
rw [← j_eq_k2, hj, bi_eq_true] at h2
simp at h2
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_eq_k2 : j = k2
⊢ False
Tactic:
rw [← j_eq_k2, hj, bi_eq_true] at h2
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_eq_k2 : j = k2
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_eq_k2 : j = k2
⊢ False
Tactic:
simp at h2
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Tactic:
next j_ne_k2 =>
specialize h5 j j_ne_k1 j_ne_k2
simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_ne_k2 : ¬j = k2
⊢ False
Tactic:
specialize h5 j j_ne_k1 j_ne_k2
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_ne_k2 : ¬j = k2
h5 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_ne_k2 : ¬j = k2
h5 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Tactic:
simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False
Tactic:
next i_ne_k1 =>
by_cases i = k2
. next i_eq_k2 =>
  rw [← i_eq_k2, hi, bi_eq_true] at h2
  simp at h2
. next i_ne_k2 =>
  specialize h5 i i_ne_k1 i_ne_k2
  simp only [hi, not_true] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
⊢ False
Tactic:
by_cases i = k2
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : i = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : ¬i = k2
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : i = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : ¬i = k2
⊢ False
Tactic:
. next i_eq_k2 =>
  rw [← i_eq_k2, hi, bi_eq_true] at h2
  simp at h2
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : ¬i = k2
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : ¬i = k2
⊢ False
Tactic:
. next i_ne_k2 =>
  specialize h5 i i_ne_k1 i_ne_k2
  simp only [hi, not_true] at h5
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : i = k2
⊢ False
Tactic:
next i_eq_k2 =>
rw [← i_eq_k2, hi, bi_eq_true] at h2
simp at h2
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_eq_k2 : i = k2
⊢ False
Tactic:
rw [← i_eq_k2, hi, bi_eq_true] at h2
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_eq_k2 : i = k2
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_eq_k2 : i = k2
⊢ False
Tactic:
simp at h2
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
h✝ : ¬i = k2
⊢ False
Tactic:
next i_ne_k2 =>
specialize h5 i i_ne_k1 i_ne_k2
simp only [hi, not_true] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_ne_k2 : ¬i = k2
⊢ False
Tactic:
specialize h5 i i_ne_k1 i_ne_k2
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_ne_k2 : ¬i = k2
h5 : ¬(f.insertRatUnits units).fst.ratUnits[i].fst.val = li.val
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_ne_k2 : ¬i = k2
h5 : ¬(f.insertRatUnits units).fst.ratUnits[i].fst.val = li.val
⊢ False
Tactic:
simp only [hi, not_true] at h5
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
h✝ : ¬bi = true
⊢ False
Tactic:
next bi_eq_false =>
simp only [Bool.not_eq_true] at bi_eq_false
by_cases i = k2
. next i_eq_k2 =>
  have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
  by_cases j = k1
  . next j_eq_k1 =>
    rw [← j_eq_k1, hj, bi_eq_false] at h1
    simp at h1
  . next j_ne_k1 =>
    specialize h5 j j_ne_k1 j_ne_k2
    simp (config := { decide := true }) only [hj] at h5
. next i_ne_k2 =>
  by_cases i = k1
  . next i_eq_k1 =>
    rw [← i_eq_k1, hi, bi_eq_false] at h1
    simp at h1
  . next i_ne_k1 =>
    specialize h5 i i_ne_k1 i_ne_k2
    simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : ¬bi = true
⊢ False
Tactic:
simp only [Bool.not_eq_true] at bi_eq_false
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
⊢ False
Tactic:
by_cases i = k2
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : i = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : ¬i = k2
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : i = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : ¬i = k2
⊢ False
Tactic:
. next i_eq_k2 =>
  have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
  by_cases j = k1
  . next j_eq_k1 =>
    rw [← j_eq_k1, hj, bi_eq_false] at h1
    simp at h1
  . next j_ne_k1 =>
    specialize h5 j j_ne_k1 j_ne_k2
    simp (config := { decide := true }) only [hj] at h5
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : ¬i = k2
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : ¬i = k2
⊢ False
Tactic:
. next i_ne_k2 =>
  by_cases i = k1
  . next i_eq_k1 =>
    rw [← i_eq_k1, hi, bi_eq_false] at h1
    simp at h1
  . next i_ne_k1 =>
    specialize h5 i i_ne_k1 i_ne_k2
    simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : i = k2
⊢ False
Tactic:
next i_eq_k2 =>
have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
by_cases j = k1
. next j_eq_k1 =>
  rw [← j_eq_k1, hj, bi_eq_false] at h1
  simp at h1
. next j_ne_k1 =>
  specialize h5 j j_ne_k1 j_ne_k2
  simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ False
Tactic:
have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
⊢ False
Tactic:
by_cases j = k1
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : j = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : j = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Tactic:
. next j_eq_k1 =>
  rw [← j_eq_k1, hj, bi_eq_false] at h1
  simp at h1
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Tactic:
. next j_ne_k1 =>
  specialize h5 j j_ne_k1 j_ne_k2
  simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ j ≠ k2
Tactic:
rw [← i_eq_k2]
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ j ≠ i

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ j ≠ i
Tactic:
exact i_ne_j.symm
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : j = k1
⊢ False
Tactic:
next j_eq_k1 =>
rw [← j_eq_k1, hj, bi_eq_false] at h1
simp at h1
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_eq_k1 : j = k1
⊢ False
Tactic:
rw [← j_eq_k1, hj, bi_eq_false] at h1
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (li, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_eq_k1 : j = k1
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (li, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_eq_k1 : j = k1
⊢ False
Tactic:
simp at h1
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Tactic:
next j_ne_k1 =>
specialize h5 j j_ne_k1 j_ne_k2
simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
⊢ False
Tactic:
specialize h5 j j_ne_k1 j_ne_k2
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
h5 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
h5 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Tactic:
simp (config := { decide := true }) only [hj] at h5
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : ¬i = k2
⊢ False
Tactic:
next i_ne_k2 =>
by_cases i = k1
. next i_eq_k1 =>
  rw [← i_eq_k1, hi, bi_eq_false] at h1
  simp at h1
. next i_ne_k1 =>
  specialize h5 i i_ne_k1 i_ne_k2
  simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
⊢ False
Tactic:
by_cases i = k1
State after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : i = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : ¬i = k1
⊢ False

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : i = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : ¬i = k1
⊢ False
Tactic:
. next i_eq_k1 =>
  rw [← i_eq_k1, hi, bi_eq_false] at h1
  simp at h1
State after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : ¬i = k1
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : ¬i = k1
⊢ False
Tactic:
. next i_ne_k1 =>
  specialize h5 i i_ne_k1 i_ne_k2
  simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : i = k1
⊢ False
Tactic:
next i_eq_k1 =>
rw [← i_eq_k1, hi, bi_eq_false] at h1
simp at h1
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_eq_k1 : i = k1
⊢ False
Tactic:
rw [← i_eq_k1, hi, bi_eq_false] at h1
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (li, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_eq_k1 : i = k1
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (li, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_eq_k1 : i = k1
⊢ False
Tactic:
simp at h1
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
h✝ : ¬i = k1
⊢ False
Tactic:
next i_ne_k1 =>
specialize h5 i i_ne_k1 i_ne_k2
simp (config := { decide := true }) only [hi] at h5
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_ne_k1 : ¬i = k1
⊢ False
Tactic:
specialize h5 i i_ne_k1 i_ne_k2
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_ne_k1 : ¬i = k1
h5 : ¬(f.insertRatUnits units).fst.ratUnits[i].fst.val = li.val
⊢ False

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_ne_k2 : ¬i = k2
i_ne_k1 : ¬i = k1
h5 : ¬(f.insertRatUnits units).fst.ratUnits[i].fst.val = li.val
⊢ False
Tactic:
simp (config := { decide := true }) only [hi] at h5
State after:
no goals