Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
id : Nat
⊢ f.strong_assignments_invariant → (f.deleteOne id).strong_assignments_invariant
Tactic:
intro hf
State after:
n : Nat
f : DefaultFormula n
id : Nat
hf : f.strong_assignments_invariant
⊢ (f.deleteOne id).strong_assignments_invariant

State before:
n : Nat
f : DefaultFormula n
id : Nat
hf : f.strong_assignments_invariant
⊢ (f.deleteOne id).strong_assignments_invariant
Tactic:
rcases hf with ⟨hsize, hf⟩
State after:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ (f.deleteOne id).strong_assignments_invariant

State before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ (f.deleteOne id).strong_assignments_invariant
Tactic:
have hsize' : (deleteOne f id).assignments.size = n := by
  simp only [← hsize]
  exact deleteOne_preserves_assignments_size f id
State after:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
⊢ (f.deleteOne id).strong_assignments_invariant

State before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
⊢ (f.deleteOne id).strong_assignments_invariant
Tactic:
apply Exists.intro hsize'
State after:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (f.deleteOne id).assignments[i.val] = true → unit (i, b) ∈ (f.deleteOne id).toList

State before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (f.deleteOne id).assignments[i.val] = true → unit (i, b) ∈ (f.deleteOne id).toList
Tactic:
intro i b hb
State after:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
⊢ unit (i, b) ∈ (f.deleteOne id).toList

State before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
⊢ unit (i, b) ∈ (f.deleteOne id).toList
Tactic:
have i_in_bounds : i.1 < f.assignments.size := by rw [hsize]; exact i.2.2
State after:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
⊢ unit (i, b) ∈ (f.deleteOne id).toList

State before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
⊢ unit (i, b) ∈ (f.deleteOne id).toList
Tactic:
simp only [deleteOne]
State after:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
⊢ unit (i, b) ∈
    (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

State before:
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
⊢ unit (i, b) ∈
    (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
match heq : f.clauses[id]! with
| none =>
  simp only
  simp only [deleteOne, heq] at hb
  exact hf i b hb
| some c =>
  by_cases hl : ∃ l : Literal (PosFin n), c = unit l
  . rcases hl with ⟨l, hl⟩
    simp only [unit] at hl
    simp only [hl]
    simp only [deleteOne, heq, hl] at hb
    by_cases l.1.1 = i.1
    . next l_eq_i =>
      simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
      have l_ne_b : l.2 ≠ b := by
        intro l_eq_b
        rw [← l_eq_b] at hb
        have hb' := not_has_of_remove f.assignments[i.1] l.2
        simp [hb] at hb'
      rw [← Bool.eq_not_iff] at l_ne_b
      rw [l_ne_b] at hb
      have hb := has_of_remove_irrelevant f.assignments[i.1] b hb
      specialize hf i b hb
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
      rcases hf with hf | hf
      . apply Or.inl
        simp only [Array.set!, Array.setD]
        split
        . rcases List.get_of_mem hf with ⟨idx, hidx⟩
          simp only [← hidx, Array.data_set]
          rw [List.mem_iff_get]
          have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
            simp only [List.length_set]
            exact idx.2
          apply Exists.intro ⟨idx.1, idx_in_bounds⟩
          by_cases id = idx
          . next id_eq_idx =>
            exfalso
            have idx_in_bounds2 : idx.1 < f.clauses.size := by
              have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
              conv => rhs; rw [f_clauses_rw, Array.size_mk]
              exact idx.2
            simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
              Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
            rw [hidx, hl] at heq
            simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
            simp only [← heq, not] at l_ne_b
            split at l_ne_b
            . simp only at l_ne_b
            . simp only at l_ne_b
          . next id_ne_idx =>
            simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
        . exact hf
      . exact Or.inr hf
    . next l_ne_i =>
      have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
      simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
      specialize hf i b hb
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
      rcases hf with hf | hf
      . apply Or.inl
        simp only [Array.set!, Array.setD]
        split
        . rcases List.get_of_mem hf with ⟨idx, hidx⟩
          simp only [← hidx, Array.data_set]
          rw [List.mem_iff_get]
          have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
            simp only [List.length_set]
            exact idx.2
          apply Exists.intro ⟨idx.1, idx_in_bounds⟩
          by_cases id = idx
          . next id_eq_idx =>
            exfalso
            have idx_in_bounds2 : idx.1 < f.clauses.size := by
              have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
              conv => rhs; rw [f_clauses_rw, Array.size_mk]
              exact idx.2
            simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
              Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
            rw [hidx, hl] at heq
            simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
            have i_eq_l : i = l.1 := by rw [← heq]
            simp only [i_eq_l, not_true] at l_ne_i
          . next id_ne_idx =>
            simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
        . exact hf
      . exact Or.inr hf
  . simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
    split
    . next some_eq_none =>
      simp only at some_eq_none
    . next l _ _ heq =>
      simp only [Option.some.injEq] at heq
      rw [heq] at hl
      specialize hl l.1
      simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
      by_cases hl2 : l.2
      . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
      . simp only [Bool.not_eq_true] at hl2
        simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
    . have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
        simp only [deleteOne]
        split
        . next heq2 =>
          simp only [heq] at heq2
        . next l _ _ heq2 =>
          simp only [heq, Option.some.injEq] at heq2
          rw [heq2] at hl
          specialize hl l.1
          simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
          by_cases hl2 : l.2
          . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
          . simp only [Bool.not_eq_true] at hl2
            simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
        . rfl
      simp only [deleteOne_f_rw] at hb
      specialize hf i b hb
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
        exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
      rcases hf with hf | hf
      . apply Or.inl
        simp only [Array.set!, Array.setD]
        split
        . rcases List.get_of_mem hf with ⟨idx, hidx⟩
          simp only [← hidx, Array.data_set]
          rw [List.mem_iff_get]
          have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
            simp only [List.length_set]
            exact idx.2
          apply Exists.intro ⟨idx.1, idx_in_bounds⟩
          by_cases id = idx
          . next id_eq_idx =>
            exfalso
            have idx_in_bounds2 : idx.1 < f.clauses.size := by
              have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
              conv => rhs; rw [f_clauses_rw, Array.size_mk]
              exact idx.2
            simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
              Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
            rw [hidx] at heq
            simp only [Option.some.injEq] at heq
            rw [← heq] at hl
            specialize hl i
            simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
              Bool.not_eq_false, Bool.not_eq_true] at hl
            by_cases b_val : b
            . simp only [b_val, and_false] at hl
            . simp only [b_val, false_and] at hl
          . next id_ne_idx =>
            simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
        . exact hf
      . exact Or.inr hf
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ (f.deleteOne id).assignments.size = n
Tactic:
simp only [← hsize]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ (f.deleteOne id).assignments.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ (f.deleteOne id).assignments.size = f.assignments.size
Tactic:
exact deleteOne_preserves_assignments_size f id
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
⊢ i.val < f.assignments.size
Tactic:
rw [hsize]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
⊢ i.val < n

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
⊢ i.val < n
Tactic:
exact i.2.2
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
heq : f.clauses[id]! = none
⊢ unit (i, b) ∈
    (match none with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
simp only
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
heq : f.clauses[id]! = none
⊢ unit (i, b) ∈
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
heq : f.clauses[id]! = none
⊢ unit (i, b) ∈
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList
Tactic:
simp only [deleteOne, heq] at hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
heq : f.clauses[id]! = none
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
heq : f.clauses[id]! = none
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList
Tactic:
exact hf i b hb
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
by_cases hl : ∃ l : Literal (PosFin n), c = unit l
State after:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
. rcases hl with ⟨l, hl⟩
  simp only [unit] at hl
  simp only [hl]
  simp only [deleteOne, heq, hl] at hb
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
    have l_ne_b : l.2 ≠ b := by
      intro l_eq_b
      rw [← l_eq_b] at hb
      have hb' := not_has_of_remove f.assignments[i.1] l.2
      simp [hb] at hb'
    rw [← Bool.eq_not_iff] at l_ne_b
    rw [l_ne_b] at hb
    have hb := has_of_remove_irrelevant f.assignments[i.1] b hb
    specialize hf i b hb
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
    rcases hf with hf | hf
    . apply Or.inl
      simp only [Array.set!, Array.setD]
      split
      . rcases List.get_of_mem hf with ⟨idx, hidx⟩
        simp only [← hidx, Array.data_set]
        rw [List.mem_iff_get]
        have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
          simp only [List.length_set]
          exact idx.2
        apply Exists.intro ⟨idx.1, idx_in_bounds⟩
        by_cases id = idx
        . next id_eq_idx =>
          exfalso
          have idx_in_bounds2 : idx.1 < f.clauses.size := by
            have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
            conv => rhs; rw [f_clauses_rw, Array.size_mk]
            exact idx.2
          simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
            Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
          rw [hidx, hl] at heq
          simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
          simp only [← heq, not] at l_ne_b
          split at l_ne_b
          . simp only at l_ne_b
          . simp only at l_ne_b
        . next id_ne_idx =>
          simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
      . exact hf
    . exact Or.inr hf
  . next l_ne_i =>
    have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
    specialize hf i b hb
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
    rcases hf with hf | hf
    . apply Or.inl
      simp only [Array.set!, Array.setD]
      split
      . rcases List.get_of_mem hf with ⟨idx, hidx⟩
        simp only [← hidx, Array.data_set]
        rw [List.mem_iff_get]
        have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
          simp only [List.length_set]
          exact idx.2
        apply Exists.intro ⟨idx.1, idx_in_bounds⟩
        by_cases id = idx
        . next id_eq_idx =>
          exfalso
          have idx_in_bounds2 : idx.1 < f.clauses.size := by
            have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
            conv => rhs; rw [f_clauses_rw, Array.size_mk]
            exact idx.2
          simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
            Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
          rw [hidx, hl] at heq
          simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
          have i_eq_l : i = l.1 := by rw [← heq]
          simp only [i_eq_l, not_true] at l_ne_i
        . next id_ne_idx =>
          simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
      . exact hf
    . exact Or.inr hf
State after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
. simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
  split
  . next some_eq_none =>
    simp only at some_eq_none
  . next l _ _ heq =>
    simp only [Option.some.injEq] at heq
    rw [heq] at hl
    specialize hl l.1
    simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
    by_cases hl2 : l.2
    . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
    . simp only [Bool.not_eq_true] at hl2
      simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
  . have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
      simp only [deleteOne]
      split
      . next heq2 =>
        simp only [heq] at heq2
      . next l _ _ heq2 =>
        simp only [heq, Option.some.injEq] at heq2
        rw [heq2] at hl
        specialize hl l.1
        simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
        by_cases hl2 : l.2
        . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
        . simp only [Bool.not_eq_true] at hl2
          simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
      . rfl
    simp only [deleteOne_f_rw] at hb
    specialize hf i b hb
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
    rcases hf with hf | hf
    . apply Or.inl
      simp only [Array.set!, Array.setD]
      split
      . rcases List.get_of_mem hf with ⟨idx, hidx⟩
        simp only [← hidx, Array.data_set]
        rw [List.mem_iff_get]
        have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
          simp only [List.length_set]
          exact idx.2
        apply Exists.intro ⟨idx.1, idx_in_bounds⟩
        by_cases id = idx
        . next id_eq_idx =>
          exfalso
          have idx_in_bounds2 : idx.1 < f.clauses.size := by
            have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
            conv => rhs; rw [f_clauses_rw, Array.size_mk]
            exact idx.2
          simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
            Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
          rw [hidx] at heq
          simp only [Option.some.injEq] at heq
          rw [← heq] at hl
          specialize hl i
          simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
            Bool.not_eq_false, Bool.not_eq_true] at hl
          by_cases b_val : b
          . simp only [b_val, and_false] at hl
          . simp only [b_val, false_and] at hl
        . next id_ne_idx =>
          simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
      . exact hf
    . exact Or.inr hf
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
rcases hl with ⟨l, hl⟩
State after:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

State before:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
simp only [unit] at hl
State after:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

State before:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
simp only [hl]
State after:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [deleteOne, heq, hl] at hb
State after:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
case pos.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
by_cases l.1.1 = i.1
State after:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : ¬l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : ¬l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
. next l_eq_i =>
  simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
  have l_ne_b : l.2 ≠ b := by
    intro l_eq_b
    rw [← l_eq_b] at hb
    have hb' := not_has_of_remove f.assignments[i.1] l.2
    simp [hb] at hb'
  rw [← Bool.eq_not_iff] at l_ne_b
  rw [l_ne_b] at hb
  have hb := has_of_remove_irrelevant f.assignments[i.1] b hb
  specialize hf i b hb
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
  rcases hf with hf | hf
  . apply Or.inl
    simp only [Array.set!, Array.setD]
    split
    . rcases List.get_of_mem hf with ⟨idx, hidx⟩
      simp only [← hidx, Array.data_set]
      rw [List.mem_iff_get]
      have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
        simp only [List.length_set]
        exact idx.2
      apply Exists.intro ⟨idx.1, idx_in_bounds⟩
      by_cases id = idx
      . next id_eq_idx =>
        exfalso
        have idx_in_bounds2 : idx.1 < f.clauses.size := by
          have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
          conv => rhs; rw [f_clauses_rw, Array.size_mk]
          exact idx.2
        simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
          Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
        rw [hidx, hl] at heq
        simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
        simp only [← heq, not] at l_ne_b
        split at l_ne_b
        . simp only at l_ne_b
        . simp only at l_ne_b
      . next id_ne_idx =>
        simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
    . exact hf
  . exact Or.inr hf
State after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : ¬l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : ¬l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
. next l_ne_i =>
  have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
  simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
  specialize hf i b hb
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
  rcases hf with hf | hf
  . apply Or.inl
    simp only [Array.set!, Array.setD]
    split
    . rcases List.get_of_mem hf with ⟨idx, hidx⟩
      simp only [← hidx, Array.data_set]
      rw [List.mem_iff_get]
      have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
        simp only [List.length_set]
        exact idx.2
      apply Exists.intro ⟨idx.1, idx_in_bounds⟩
      by_cases id = idx
      . next id_eq_idx =>
        exfalso
        have idx_in_bounds2 : idx.1 < f.clauses.size := by
          have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
          conv => rhs; rw [f_clauses_rw, Array.size_mk]
          exact idx.2
        simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
          Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
        rw [hidx, hl] at heq
        simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
        have i_eq_l : i = l.1 := by rw [← heq]
        simp only [i_eq_l, not_true] at l_ne_i
      . next id_ne_idx =>
        simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
    . exact hf
  . exact Or.inr hf
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
next l_eq_i =>
simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
have l_ne_b : l.2 ≠ b := by
  intro l_eq_b
  rw [← l_eq_b] at hb
  have hb' := not_has_of_remove f.assignments[i.1] l.2
  simp [hb] at hb'
rw [← Bool.eq_not_iff] at l_ne_b
rw [l_ne_b] at hb
have hb := has_of_remove_irrelevant f.assignments[i.1] b hb
specialize hf i b hb
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
. apply Or.inl
  simp only [Array.set!, Array.setD]
  split
  . rcases List.get_of_mem hf with ⟨idx, hidx⟩
    simp only [← hidx, Array.data_set]
    rw [List.mem_iff_get]
    have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
      simp only [List.length_set]
      exact idx.2
    apply Exists.intro ⟨idx.1, idx_in_bounds⟩
    by_cases id = idx
    . next id_eq_idx =>
      exfalso
      have idx_in_bounds2 : idx.1 < f.clauses.size := by
        have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
        conv => rhs; rw [f_clauses_rw, Array.size_mk]
        exact idx.2
      simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
        Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
      rw [hidx, hl] at heq
      simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
      simp only [← heq, not] at l_ne_b
      split at l_ne_b
      . simp only at l_ne_b
      . simp only at l_ne_b
    . next id_ne_idx =>
      simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
  . exact hf
. exact Or.inr hf
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_eq_i : l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds] at hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
have l_ne_b : l.2 ≠ b := by
  intro l_eq_b
  rw [← l_eq_b] at hb
  have hb' := not_has_of_remove f.assignments[i.1] l.2
  simp [hb] at hb'
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
l_ne_b : l.snd ≠ b
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
l_ne_b : l.snd ≠ b
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
rw [← Bool.eq_not_iff] at l_ne_b
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
l_ne_b : l.snd = !b
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
l_ne_b : l.snd = !b
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
rw [l_ne_b] at hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
have hb := has_of_remove_irrelevant f.assignments[i.1] b hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
specialize hf i b hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
rcases hf with hf | hf
State after:
case inl
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

State before:
case inl
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
. apply Or.inl
  simp only [Array.set!, Array.setD]
  split
  . rcases List.get_of_mem hf with ⟨idx, hidx⟩
    simp only [← hidx, Array.data_set]
    rw [List.mem_iff_get]
    have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
      simp only [List.length_set]
      exact idx.2
    apply Exists.intro ⟨idx.1, idx_in_bounds⟩
    by_cases id = idx
    . next id_eq_idx =>
      exfalso
      have idx_in_bounds2 : idx.1 < f.clauses.size := by
        have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
        conv => rhs; rw [f_clauses_rw, Array.size_mk]
        exact idx.2
      simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
        Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
      rw [hidx, hl] at heq
      simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
      simp only [← heq, not] at l_ne_b
      split at l_ne_b
      . simp only at l_ne_b
      . simp only at l_ne_b
    . next id_ne_idx =>
      simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
  . exact hf
State after:
case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

State before:
case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
. exact Or.inr hf
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
⊢ l.snd ≠ b
Tactic:
intro l_eq_b
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
l_eq_b : l.snd = b
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment b (removeAssignment l.snd f.assignments[i.val]) = true
l_eq_b : l.snd = b
⊢ False
Tactic:
rw [← l_eq_b] at hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment l.snd (removeAssignment l.snd f.assignments[i.val]) = true
l_eq_b : l.snd = b
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment l.snd (removeAssignment l.snd f.assignments[i.val]) = true
l_eq_b : l.snd = b
⊢ False
Tactic:
have hb' := not_has_of_remove f.assignments[i.1] l.2
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment l.snd (removeAssignment l.snd f.assignments[i.val]) = true
l_eq_b : l.snd = b
hb' : ¬hasAssignment l.snd (removeAssignment l.snd f.assignments[i.val]) = true
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb : hasAssignment l.snd (removeAssignment l.snd f.assignments[i.val]) = true
l_eq_b : l.snd = b
hb' : ¬hasAssignment l.snd (removeAssignment l.snd f.assignments[i.val]) = true
⊢ False
Tactic:
simp [hb] at hb'
State after:
no goals

State before:
case inl
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
apply Or.inl
State after:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data

State before:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data
Tactic:
simp only [Array.set!, Array.setD]
State after:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (if h : id < f.clauses.size then f.clauses.set ⟨id, h⟩ none else f.clauses).data

State before:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (if h : id < f.clauses.size then f.clauses.set ⟨id, h⟩ none else f.clauses).data
Tactic:
split
State after:
case inl.h.isTrue
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data

State before:
case inl.h.isTrue
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
Tactic:
. rcases List.get_of_mem hf with ⟨idx, hidx⟩
  simp only [← hidx, Array.data_set]
  rw [List.mem_iff_get]
  have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
    simp only [List.length_set]
    exact idx.2
  apply Exists.intro ⟨idx.1, idx_in_bounds⟩
  by_cases id = idx
  . next id_eq_idx =>
    exfalso
    have idx_in_bounds2 : idx.1 < f.clauses.size := by
      have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
      conv => rhs; rw [f_clauses_rw, Array.size_mk]
      exact idx.2
    simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
      Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
    rw [hidx, hl] at heq
    simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
    simp only [← heq, not] at l_ne_b
    split at l_ne_b
    . simp only at l_ne_b
    . simp only at l_ne_b
  . next id_ne_idx =>
    simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data

State before:
case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
Tactic:
. exact hf
State after:
no goals

State before:
case inl.h.isTrue
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data
Tactic:
rcases List.get_of_mem hf with ⟨idx, hidx⟩
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data
Tactic:
simp only [← hidx, Array.data_set]
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none
Tactic:
rw [List.mem_iff_get]
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Tactic:
have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
  simp only [List.length_set]
  exact idx.2
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Tactic:
apply Exists.intro ⟨idx.1, idx_in_bounds⟩
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
by_cases id = idx
State after:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
. next id_eq_idx =>
  exfalso
  have idx_in_bounds2 : idx.1 < f.clauses.size := by
    have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
    conv => rhs; rw [f_clauses_rw, Array.size_mk]
    exact idx.2
  simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
    Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
  rw [hidx, hl] at heq
  simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
  simp only [← heq, not] at l_ne_b
  split at l_ne_b
  . simp only at l_ne_b
  . simp only at l_ne_b
State after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
. next id_ne_idx =>
  simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < (f.clauses.data.set id none).length
Tactic:
simp only [List.length_set]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < f.clauses.data.length

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < f.clauses.data.length
Tactic:
exact idx.2
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
simp only [← heq, not] at l_ne_b
split at l_ne_b
. simp only at l_ne_b
. simp only at l_ne_b
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
exfalso
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ False
Tactic:
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
⊢ False
Tactic:
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : f.clauses.data.get idx = some c
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : f.clauses.data.get idx = some c
⊢ False
Tactic:
rw [hidx, hl] at heq
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : some (unit (i, b)) = some { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : some (unit (i, b)) = some { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ False
Tactic:
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
⊢ False
Tactic:
simp only [← heq, not] at l_ne_b
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
l_ne_b :
  b =
    match b with
    | true => false
    | false => true
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
l_ne_b :
  b =
    match b with
    | true => false
    | false => true
⊢ False
Tactic:
split at l_ne_b
State after:
case h_1
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment true (removeAssignment (!true) f.assignments[i.val]) = true
hb : hasAssignment true f.assignments[i.val] = true
hf : some (unit (i, true)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, true))
heq : (i, true) = l
l_ne_b : true = false
⊢ False

case h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment false (removeAssignment (!false) f.assignments[i.val]) = true
hb : hasAssignment false f.assignments[i.val] = true
hf : some (unit (i, false)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, false))
heq : (i, false) = l
l_ne_b : false = true
⊢ False

State before:
case h_1
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment true (removeAssignment (!true) f.assignments[i.val]) = true
hb : hasAssignment true f.assignments[i.val] = true
hf : some (unit (i, true)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, true))
heq : (i, true) = l
l_ne_b : true = false
⊢ False

case h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment false (removeAssignment (!false) f.assignments[i.val]) = true
hb : hasAssignment false f.assignments[i.val] = true
hf : some (unit (i, false)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, false))
heq : (i, false) = l
l_ne_b : false = true
⊢ False
Tactic:
. simp only at l_ne_b
State after:
case h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment false (removeAssignment (!false) f.assignments[i.val]) = true
hb : hasAssignment false f.assignments[i.val] = true
hf : some (unit (i, false)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, false))
heq : (i, false) = l
l_ne_b : false = true
⊢ False

State before:
case h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment false (removeAssignment (!false) f.assignments[i.val]) = true
hb : hasAssignment false f.assignments[i.val] = true
hf : some (unit (i, false)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, false))
heq : (i, false) = l
l_ne_b : false = true
⊢ False
Tactic:
. simp only at l_ne_b
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ ↑idx < f.clauses.size
Tactic:
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.size

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.size
Tactic:
conv => rhs; rw [f_clauses_rw, Array.size_mk]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.data.length

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.data.length
Tactic:
exact idx.2
State after:
no goals

State before:
case h_1
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment true (removeAssignment (!true) f.assignments[i.val]) = true
hb : hasAssignment true f.assignments[i.val] = true
hf : some (unit (i, true)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, true))
heq : (i, true) = l
l_ne_b : true = false
⊢ False
Tactic:
simp only at l_ne_b
State after:
no goals

State before:
case h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
c✝ : Bool
hb✝ : hasAssignment false (removeAssignment (!false) f.assignments[i.val]) = true
hb : hasAssignment false f.assignments[i.val] = true
hf : some (unit (i, false)) ∈ f.clauses.data
hidx : f.clauses.data.get idx = some (unit (i, false))
heq : (i, false) = l
l_ne_b : false = true
⊢ False
Tactic:
simp only at l_ne_b
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
next id_ne_idx =>
simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_ne_idx : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
no goals

State before:
case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
Tactic:
exact hf
State after:
no goals

State before:
case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
exact Or.inr hf
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
h✝ : ¬l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
next l_ne_i =>
have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
specialize hf i b hb
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
. apply Or.inl
  simp only [Array.set!, Array.setD]
  split
  . rcases List.get_of_mem hf with ⟨idx, hidx⟩
    simp only [← hidx, Array.data_set]
    rw [List.mem_iff_get]
    have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
      simp only [List.length_set]
      exact idx.2
    apply Exists.intro ⟨idx.1, idx_in_bounds⟩
    by_cases id = idx
    . next id_eq_idx =>
      exfalso
      have idx_in_bounds2 : idx.1 < f.clauses.size := by
        have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
        conv => rhs; rw [f_clauses_rw, Array.size_mk]
        exact idx.2
      simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
        Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
      rw [hidx, hl] at heq
      simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
      have i_eq_l : i = l.1 := by rw [← heq]
      simp only [i_eq_l, not_true] at l_ne_i
    . next id_ne_idx =>
      simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
  . exact hf
. exact Or.inr hf
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_ne_i : ¬l.fst.val = i.val
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
have l_in_bounds : l.1.1 < f.assignments.size := by rw [hsize]; exact l.1.2.2
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
specialize hf i b hb
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
rcases hf with hf | hf
State after:
case inl
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

State before:
case inl
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
. apply Or.inl
  simp only [Array.set!, Array.setD]
  split
  . rcases List.get_of_mem hf with ⟨idx, hidx⟩
    simp only [← hidx, Array.data_set]
    rw [List.mem_iff_get]
    have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
      simp only [List.length_set]
      exact idx.2
    apply Exists.intro ⟨idx.1, idx_in_bounds⟩
    by_cases id = idx
    . next id_eq_idx =>
      exfalso
      have idx_in_bounds2 : idx.1 < f.clauses.size := by
        have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
        conv => rhs; rw [f_clauses_rw, Array.size_mk]
        exact idx.2
      simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
        Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
      rw [hidx, hl] at heq
      simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
      have i_eq_l : i = l.1 := by rw [← heq]
      simp only [i_eq_l, not_true] at l_ne_i
    . next id_ne_idx =>
      simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
  . exact hf
State after:
case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)

State before:
case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
. exact Or.inr hf
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_ne_i : ¬l.fst.val = i.val
⊢ l.fst.val < f.assignments.size
Tactic:
rw [hsize]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_ne_i : ¬l.fst.val = i.val
⊢ l.fst.val < n

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
hb : hasAssignment b (f.assignments.modify l.fst.val (removeAssignment l.snd))[i.val] = true
l_ne_i : ¬l.fst.val = i.val
⊢ l.fst.val < n
Tactic:
exact l.1.2.2
State after:
no goals

State before:
case inl
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
apply Or.inl
State after:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data

State before:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data
Tactic:
simp only [Array.set!, Array.setD]
State after:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (if h : id < f.clauses.size then f.clauses.set ⟨id, h⟩ none else f.clauses).data

State before:
case inl.h
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
⊢ some (unit (i, b)) ∈ (if h : id < f.clauses.size then f.clauses.set ⟨id, h⟩ none else f.clauses).data
Tactic:
split
State after:
case inl.h.isTrue
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data

State before:
case inl.h.isTrue
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
Tactic:
. rcases List.get_of_mem hf with ⟨idx, hidx⟩
  simp only [← hidx, Array.data_set]
  rw [List.mem_iff_get]
  have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
    simp only [List.length_set]
    exact idx.2
  apply Exists.intro ⟨idx.1, idx_in_bounds⟩
  by_cases id = idx
  . next id_eq_idx =>
    exfalso
    have idx_in_bounds2 : idx.1 < f.clauses.size := by
      have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
      conv => rhs; rw [f_clauses_rw, Array.size_mk]
      exact idx.2
    simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
      Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
    rw [hidx, hl] at heq
    simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
    have i_eq_l : i = l.1 := by rw [← heq]
    simp only [i_eq_l, not_true] at l_ne_i
  . next id_ne_idx =>
    simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data

State before:
case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
Tactic:
. exact hf
State after:
no goals

State before:
case inl.h.isTrue
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data
Tactic:
rcases List.get_of_mem hf with ⟨idx, hidx⟩
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data
Tactic:
simp only [← hidx, Array.data_set]
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none
Tactic:
rw [List.mem_iff_get]
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Tactic:
have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
  simp only [List.length_set]
  exact idx.2
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Tactic:
apply Exists.intro ⟨idx.1, idx_in_bounds⟩
State after:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

State before:
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
by_cases id = idx
State after:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
. next id_eq_idx =>
  exfalso
  have idx_in_bounds2 : idx.1 < f.clauses.size := by
    have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
    conv => rhs; rw [f_clauses_rw, Array.size_mk]
    exact idx.2
  simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
    Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
  rw [hidx, hl] at heq
  simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
  have i_eq_l : i = l.1 := by rw [← heq]
  simp only [i_eq_l, not_true] at l_ne_i
State after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
. next id_ne_idx =>
  simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < (f.clauses.data.set id none).length
Tactic:
simp only [List.length_set]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < f.clauses.data.length

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < f.clauses.data.length
Tactic:
exact idx.2
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
have i_eq_l : i = l.1 := by rw [← heq]
simp only [i_eq_l, not_true] at l_ne_i
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
exfalso
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ False
Tactic:
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
⊢ False
Tactic:
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : f.clauses.data.get idx = some c
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : f.clauses.data.get idx = some c
⊢ False
Tactic:
rw [hidx, hl] at heq
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : some (unit (i, b)) = some { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : some (unit (i, b)) = some { clause := [l], nodupkey := ⋯, nodup := ⋯ }
⊢ False
Tactic:
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
⊢ False
Tactic:
have i_eq_l : i = l.1 := by rw [← heq]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
i_eq_l : i = l.fst
⊢ False

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
i_eq_l : i = l.fst
⊢ False
Tactic:
simp only [i_eq_l, not_true] at l_ne_i
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ ↑idx < f.clauses.size
Tactic:
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.size

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.size
Tactic:
conv => rhs; rw [f_clauses_rw, Array.size_mk]
State after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.data.length

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
f_clauses_rw : f.clauses = { data := f.clauses.data }
⊢ ↑idx < f.clauses.data.length
Tactic:
exact idx.2
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : (i, b) = l
⊢ i = l.fst
Tactic:
rw [← heq]
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
next id_ne_idx =>
simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_ne_idx : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
State after:
no goals

State before:
case inl.h.isFalse
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
Tactic:
exact hf
State after:
no goals

State before:
case inr
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ some (unit (i, b)) ∈ (f.clauses.set! id none).data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
exact Or.inr hf
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
State after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

State before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
Tactic:
split
State after:
case neg.h_1
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝ : Option (DefaultClause n)
heq✝ : some c = none
⊢ unit (i, b) ∈
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList

case neg.h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝ : Option (DefaultClause n)
l✝ : Literal (PosFin n)
nodupkey✝ : ∀ (l : PosFin n), ¬(l, true) ∈ [l✝] ∨ ¬(l, false) ∈ [l✝]
nodup✝ : [l✝].Nodup
heq✝ : some c = some { clause := [l✝], nodupkey := nodupkey✝, nodup := nodup✝ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l✝.fst.val (removeAssignment l✝.snd) }.toList

case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList