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

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
⊢ f.readyForRatAdd → (f.delete arr).readyForRatAdd
Tactic:
intro h
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRatAdd

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRatAdd
Tactic:
constructor
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

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
State after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd

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
State after:
no goals

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]
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 = #[]

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
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 = #[]

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]
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 = #[]

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals