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

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (f.delete arr).toList → c ∈ f.toList
Tactic:
simp only [delete, Array.foldl_eq_foldl_data]
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Tactic:
have hb : c ∈ toList f → c ∈ toList f := id
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Tactic:
have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.data) :
  c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih $ deleteOne_subset f' id c h
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.data → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.data → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
⊢ c ∈ (f'.deleteOne id).toList → c ∈ f.toList
Tactic:
intro h
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList
Tactic:
exact ih $ deleteOne_subset f' id c h
State after:
no goals