-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β))
    (l: List (α × β)):
    (Const.insertMany m l).1 = Const.insertListₘ m l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
⊢ (List.foldl (fun b a => ⟨b.val.insert a.fst a.snd, ⋯⟩) ⟨m, ⋯⟩ l).val = insertListₘ m l

Tactic:
suffices ∀ (t : { m' // ∀ (P : Raw₀ α (fun _ => β) → Prop),
  (∀ {m'' : Raw₀ α (fun _ => β)} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
    (List.foldl (fun m' p => ⟨m'.val.insert p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val =
  Const.insertListₘ t.val l from this _

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
⊢ ∀
    (t :
      { m' //
        ∀ (P : (Raw₀ α fun x => β) → Prop),
          (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
    (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t l).val = insertListₘ t.val l

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α × β
tl : List (α × β)
ih :
  ∀ (m : Raw₀ α fun x => β)
    (t :
      { m' //
        ∀ (P : (Raw₀ α fun x => β) → Prop),
          (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
    (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t tl).val = insertListₘ t.val tl
m : Raw₀ α fun x => β
t :
  { m' //
    ∀ (P : (Raw₀ α fun x => β) → Prop),
      (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }
⊢ (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t (hd :: tl)).val = insertListₘ t.val (hd :: tl)

Tactic:
simp only [List.foldl_cons, insertListₘ]

Result:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α × β
tl : List (α × β)
ih :
  ∀ (m : Raw₀ α fun x => β)
    (t :
      { m' //
        ∀ (P : (Raw₀ α fun x => β) → Prop),
          (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
    (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t tl).val = insertListₘ t.val tl
m : Raw₀ α fun x => β
t :
  { m' //
    ∀ (P : (Raw₀ α fun x => β) → Prop),
      (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }
⊢ (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) ⟨t.val.insert hd.fst hd.snd, ⋯⟩ tl).val =
    insertListₘ (t.val.insert hd.fst hd.snd) tl

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
⊢ (insertMany m l).val = insertListₘ m l

Tactic:
simp only [insertMany, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
⊢ (List.foldl (fun b a => ⟨b.val.insert a.fst a.snd, ⋯⟩) ⟨m, ⋯⟩ l).val = insertListₘ m l

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α × β
tl : List (α × β)
ih :
  ∀ (m : Raw₀ α fun x => β)
    (t :
      { m' //
        ∀ (P : (Raw₀ α fun x => β) → Prop),
          (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
    (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t tl).val = insertListₘ t.val tl
m : Raw₀ α fun x => β
t :
  { m' //
    ∀ (P : (Raw₀ α fun x => β) → Prop),
      (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }
⊢ (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) ⟨t.val.insert hd.fst hd.snd, ⋯⟩ tl).val =
    insertListₘ (t.val.insert hd.fst hd.snd) tl

Tactic:
apply ih

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
t :
  { m' //
    ∀ (P : (Raw₀ α fun x => β) → Prop),
      (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }
⊢ (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t l).val = insertListₘ t.val l

Tactic:
induction l generalizing m with
| nil => simp [insertListₘ]
| cons hd tl ih =>
  simp only [List.foldl_cons, insertListₘ]
  apply ih

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
t :
  { m' //
    ∀ (P : (Raw₀ α fun x => β) → Prop),
      (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }
⊢ (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t []).val = insertListₘ t.val []

Tactic:
simp [insertListₘ]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
⊢ ∀
    (t :
      { m' //
        ∀ (P : (Raw₀ α fun x => β) → Prop),
          (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
    (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t l).val = insertListₘ t.val l

Tactic:
intro t

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
l : List (α × β)
t :
  { m' //
    ∀ (P : (Raw₀ α fun x => β) → Prop),
      (∀ {m'' : Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }
⊢ (List.foldl (fun m' p => ⟨m'.val.insert p.fst p.snd, ⋯⟩) t l).val = insertListₘ t.val l