Theorem: LRAT.DefaultFormula.clearUnit_foldl_preserves_size (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
⊢ (List.foldl f assignments l).size = assignments.size
Tactic:
have hb : assignments.size = assignments.size := rfl
State after:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size

State before:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size
Tactic:
have hl (assignments' : Array Assignment) (hsize : assignments'.size = assignments.size) (a : α) (_ : a ∈ l) :
  (f assignments' a).size = assignments.size := by rw [f_preserves_size assignments' a, hsize]
State after:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
hl :
  ∀ (assignments' : Array Assignment),
    assignments'.size = assignments.size → ∀ (a : α), a ∈ l → (f assignments' a).size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size

State before:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
hl :
  ∀ (assignments' : Array Assignment),
    assignments'.size = assignments.size → ∀ (a : α), a ∈ l → (f assignments' a).size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size
Tactic:
exact List.foldlRecOn l f assignments hb hl
State after:
no goals

State before:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
assignments' : Array Assignment
hsize : assignments'.size = assignments.size
a : α
x✝ : a ∈ l
⊢ (f assignments' a).size = assignments.size
Tactic:
rw [f_preserves_size assignments' a, hsize]
State after:
no goals