internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof 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
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✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
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]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3.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
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✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3.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
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✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
⊢ f.readyForRupAdd → (f.delete arr).readyForRupAdd
Tactic:
intro h
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (f.delete arr).readyForRupAdd
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (f.delete arr).readyForRupAdd
Tactic:
rw [delete, Array.foldl_eq_foldl_data]
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).readyForRupAdd
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).readyForRupAdd
Tactic:
constructor
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
. have hb : f.rupUnits = #[] := h.1
  have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
  exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
. have hb : strong_assignments_invariant f := h.2
  have hl (acc : DefaultFormula n) (ih : strong_assignments_invariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    strong_assignments_invariant (deleteOne acc id) := deleteOne_preserves_strong_assignments_invariant acc id ih
  exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Tactic:
have hb : f.rupUnits = #[] := h.1
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Tactic:
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
  (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.rupUnits = #[] → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.rupUnits = #[] → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
acc : DefaultFormula n
ih : acc.rupUnits = #[]
id : Nat
_id_in_arr : id ∈ arr.data
⊢ (acc.deleteOne id).rupUnits = #[]
Tactic:
rw [deleteOne_preserves_rupUnits, ih]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
have hb : strong_assignments_invariant f := h.2
Proof state after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
have hl (acc : DefaultFormula n) (ih : strong_assignments_invariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
  strong_assignments_invariant (deleteOne acc id) := deleteOne_preserves_strong_assignments_invariant acc id ih
Proof state after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.strong_assignments_invariant → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Theorem: LRAT.DefaultFormula.delete_readyForRupAdd
Proof state before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.strong_assignments_invariant → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_ratUnits
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (f.deleteOne id).ratUnits = f.ratUnits
Tactic:
simp only [deleteOne]
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (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 }).ratUnits =
    f.ratUnits
Theorem: LRAT.DefaultFormula.deleteOne_preserves_ratUnits
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (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 }).ratUnits =
    f.ratUnits
Tactic:
split <;> simp only
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
⊢ f.readyForRatAdd → (f.delete arr).readyForRatAdd
Tactic:
intro h
Proof state after:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRatAdd
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRatAdd
Tactic:
constructor
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd
Tactic:
. rw [delete, Array.foldl_eq_foldl_data]
  have hb : f.ratUnits = #[] := h.1
  have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
  exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd
Tactic:
. exact delete_readyForRupAdd f arr h.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).ratUnits = #[]
Tactic:
rw [delete, Array.foldl_eq_foldl_data]
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).ratUnits = #[]
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).ratUnits = #[]
Tactic:
have hb : f.ratUnits = #[] := h.1
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
hb : f.ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).ratUnits = #[]
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
hb : f.ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).ratUnits = #[]
Tactic:
have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
  (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
Proof state after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
hb : f.ratUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.ratUnits = #[] → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).ratUnits = #[]
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
hb : f.ratUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.ratUnits = #[] → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).ratUnits = #[]
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
hb : f.ratUnits = #[]
acc : DefaultFormula n
ih : acc.ratUnits = #[]
id : Nat
_id_in_arr : id ∈ arr.data
⊢ (acc.deleteOne id).ratUnits = #[]
Tactic:
rw [deleteOne_preserves_ratUnits, ih]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.delete_readyForRatAdd
Proof state before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd
Tactic:
exact delete_readyForRupAdd f arr h.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈ (f.deleteOne id).toList → c ∈ f.toList
Tactic:
simp only [deleteOne]
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈
      (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 →
    c ∈ f.toList
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈
      (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 →
    c ∈ f.toList
Tactic:
intro h1
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
h1 :
  c ∈
    (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
⊢ c ∈ f.toList
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
h1 :
  c ∈
    (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
⊢ c ∈ f.toList
Tactic:
split at h1 <;> first
| exact h1
| rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
  rw [toList, List.mem_append, List.mem_append, or_assoc]
  rcases h1 with h1 | h1 | h1
  . apply Or.inl
    simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
    simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
    rw [Array.set!, Array.setD] at h1
    split at h1
    . simp only [Array.data_set] at h1
      rcases List.get_of_mem h1 with ⟨i, h4⟩
      rw [List.get_set] at h4
      split at h4
      . exact False.elim h4
      . rw [← h4]
        apply List.get_mem
    . exact h1
  . exact (Or.inr ∘ Or.inl) h1
  . exact (Or.inr ∘ Or.inr) h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
case h_1
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[id]! = none
h1 : c ∈ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList
⊢ c ∈ f.toList
Tactic:
exact h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
case h_3
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
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✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
⊢ c ∈ f.toList
Tactic:
rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
Proof state after:
case h_3
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
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✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
      List.filterMap _root_.id
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.clauses.toList ∨
    c ∈
        List.map unit
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments }.rupUnits.toList ∨
      c ∈
        List.map unit
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments }.ratUnits.toList
⊢ c ∈ f.toList