internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Tactic:
specialize ih2 idx (Nat.le_refl idx.val)
Proof state after:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Tactic:
have idx_unit_in_bounds : units[idx].1.1 < assignments.size := by
  rw [hsize]; exact units[idx].1.2.2
Proof state after:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Tactic:
have i_in_bounds : i.1 < assignments.size := by
  rw [hsize]
  exact i.2
Proof state after:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Tactic:
have h := Array.get_modify_unchanged idx_unit_in_bounds i_in_bounds (removeAssignment units[idx.val].2) ih2
Proof state after:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
h : (assignments.modify units[idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = assignments[↑i]
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
h : (assignments.modify units[idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = assignments[↑i]
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Tactic:
simp only [Fin.getElem_fin] at h
Proof state after:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
h : (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = assignments[↑i]
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
h : (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = assignments[↑i]
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = f.assignments[↑i]
Tactic:
rw [h]
Proof state after:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
h : (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = assignments[↑i]
⊢ assignments[↑i] = f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
h : (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = assignments[↑i]
⊢ assignments[↑i] = f.assignments[↑i]
Tactic:
exact ih1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ units[idx].fst.val < assignments.size
Tactic:
rw [hsize]
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ units[idx].fst.val < n
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
⊢ units[idx].fst.val < n
Tactic:
exact units[idx].1.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
⊢ ↑i < assignments.size
Tactic:
rw [hsize]
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
⊢ ↑i < n
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[idx].fst.val < assignments.size
⊢ ↑i < n
Tactic:
exact i.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
⊢ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i
Tactic:
intro j j_ge_idx_add_one
Proof state after:
case intro.inl.intro.h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
j : Fin units.size
j_ge_idx_add_one : ↑j ≥ ↑idx + 1
⊢ units[j].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case intro.inl.intro.h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
j : Fin units.size
j_ge_idx_add_one : ↑j ≥ ↑idx + 1
⊢ units[j].fst.val ≠ ↑i
Tactic:
exact ih2 j (Nat.le_of_succ_le j_ge_idx_add_one)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
h✝ : ¬idx = j
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (clearUnit assignments units[idx])[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        ↑j ≥ ↑idx + 1 ∧
          units[j] = (⟨↑i, ⋯⟩, b) ∧
            assignments_i = addAssignment b fassignments_i ∧
              ¬hasAssignment b fassignments_i = true ∧
                ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        ↑j1 ≥ ↑idx + 1 ∧
          ↑j2 ≥ ↑idx + 1 ∧
            units[j1] = (⟨↑i, ⋯⟩, true) ∧
              units[j2] = (⟨↑i, ⋯⟩, false) ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → k ≠ j2 → units[k].fst.val ≠ ↑i
Tactic:
. next idx_ne_j =>
  refine Or.inr <| Or.inl <| ⟨j,b,i_gt_zero,?_⟩
  constructor
  . rw [← Nat.succ_eq_add_one]
    apply Nat.succ_le_of_lt ∘ Nat.lt_of_le_of_ne j_ge_idx
    intro idx_eq_j
    exact idx_ne_j (Fin.eq_of_val_eq idx_eq_j)
  . constructor
    . exact ih1
    . constructor
      . simp only [clearUnit, Array.get_eq_getElem]
        specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
        have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
          rw [hsize]
          exact units[idx.1].1.2.2
        have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
        rw [Array.get_modify_unchanged idx_unit_in_bounds i_in_bounds _ ih4]
        exact ih2
      . constructor
        . exact ih3
        . intro k k_ge_idx_add_one k_ne_j
          exact ih4 k (Nat.le_of_succ_le k_ge_idx_add_one) k_ne_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
h✝ : idx = j
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (clearUnit assignments units[idx])[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        ↑j ≥ ↑idx + 1 ∧
          units[j] = (⟨↑i, ⋯⟩, b) ∧
            assignments_i = addAssignment b fassignments_i ∧
              ¬hasAssignment b fassignments_i = true ∧
                ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        ↑j1 ≥ ↑idx + 1 ∧
          ↑j2 ≥ ↑idx + 1 ∧
            units[j1] = (⟨↑i, ⋯⟩, true) ∧
              units[j2] = (⟨↑i, ⋯⟩, false) ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → k ≠ j2 → units[k].fst.val ≠ ↑i
Tactic:
next idx_eq_j =>
apply Or.inl
constructor
. simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1]
  have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
  rw [Array.get_modify_at_idx i_in_bounds, ih2, remove_add_cancel]
  exact ih3
. intro k k_ge_idx_add_one
  have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one
  have k_ne_j : k ≠ j := by
    intro k_eq_j
    rw [k_eq_j, idx_eq_j] at k_ge_idx_add_one
    exact Nat.not_succ_le_self j.val k_ge_idx_add_one
  exact ih4 k k_ge_idx k_ne_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_eq_j : idx = j
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (clearUnit assignments units[idx])[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        ↑j ≥ ↑idx + 1 ∧
          units[j] = (⟨↑i, ⋯⟩, b) ∧
            assignments_i = addAssignment b fassignments_i ∧
              ¬hasAssignment b fassignments_i = true ∧
                ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        ↑j1 ≥ ↑idx + 1 ∧
          ↑j2 ≥ ↑idx + 1 ∧
            units[j1] = (⟨↑i, ⋯⟩, true) ∧
              units[j2] = (⟨↑i, ⋯⟩, false) ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → k ≠ j2 → units[k].fst.val ≠ ↑i
Tactic:
apply Or.inl
Proof state after:
case h
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_eq_j : idx = j
⊢ (clearUnit assignments units[idx])[↑i] = f.assignments[↑i] ∧
    ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case h
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_eq_j : idx = j
⊢ (clearUnit assignments units[idx])[↑i] = f.assignments[↑i] ∧
    ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_eq_j : idx = j
⊢ (clearUnit assignments units[idx])[↑i] = f.assignments[↑i]

case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_eq_j : idx = j
⊢ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i