-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assignment)
    (assignments0_size : assignments0.size = n) (rupUnits : Array (Literal (PosFin n)))
    (assignments : Array Assignment) (assignments_size : assignments.size = n) (b : Bool)
    (units : CNF.Clause (PosFin n)) :
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) units
    have update_res_size : update_res.snd.fst.size = n

Proof state:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ update_res.snd.fst.size = n

Tactic:
rw [size_insertUnit]

Result:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ assignments.size = n

Proof state:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (hd :: tl);
    let_fun update_res_size := ⋯;
    InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

Tactic:
simp only [List.foldl]

Result:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
    InsertUnitInvariant assignments0 assignments0_size
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

Proof state:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
⊢ InsertUnitInvariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

Tactic:
have h := insertUnitInvariant_insertUnit assignments0 assignments0_size rupUnits assignments assignments_size b hd h0

Result:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
h :
  let update_res := insertUnit (rupUnits, assignments, b) hd;
  let_fun update_res_size := ⋯;
  InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
⊢ InsertUnitInvariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯