-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
    ReadyForRupAdd f → ReadyForRupAdd (delete f arr)

Proof state:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
hb : f.StrongAssignmentsInvariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.StrongAssignmentsInvariant → ∀ (id : Nat), id ∈ arr.toList → (acc.deleteOne id).StrongAssignmentsInvariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).StrongAssignmentsInvariant

Tactic:
exact List.foldlRecOn arr.toList deleteOne f hb hl

Result:
no goals

Proof state:
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.toList).rupUnits = #[]

Tactic:
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
  (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]

Result:
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.toList → (acc.deleteOne id).rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).rupUnits = #[]

Proof state:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).StrongAssignmentsInvariant

Tactic:
have hb : StrongAssignmentsInvariant f := h.2

Result:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
hb : f.StrongAssignmentsInvariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).StrongAssignmentsInvariant

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
⊢ f.ReadyForRupAdd → (f.delete arr).ReadyForRupAdd

Tactic:
intro h

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (f.delete arr).ReadyForRupAdd

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ReadyForRupAdd

Tactic:
constructor

Result:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).rupUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).StrongAssignmentsInvariant

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (f.delete arr).ReadyForRupAdd

Tactic:
rw [delete, ← Array.foldl_toList]

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ReadyForRupAdd

Proof state:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).rupUnits = #[]

Tactic:
have hb : f.rupUnits = #[] := h.1

Result:
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.toList).rupUnits = #[]

Proof state:
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.toList → (acc.deleteOne id).rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).rupUnits = #[]

Tactic:
exact List.foldlRecOn arr.toList deleteOne f hb hl

Result:
no goals

Proof state:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
hb : f.StrongAssignmentsInvariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).StrongAssignmentsInvariant

Tactic:
have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
  StrongAssignmentsInvariant (deleteOne acc id) := deleteOne_preserves_strongAssignmentsInvariant acc id ih

Result:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRupAdd
hb : f.StrongAssignmentsInvariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.StrongAssignmentsInvariant → ∀ (id : Nat), id ∈ arr.toList → (acc.deleteOne id).StrongAssignmentsInvariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).StrongAssignmentsInvariant

Proof state:
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.toList
⊢ (acc.deleteOne id).rupUnits = #[]

Tactic:
rw [deleteOne_preserves_rupUnits, ih]

Result:
no goals