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

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ (m : Raw₀ α β)
    (t :
      { m' //
        ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ tl
m : Raw₀ α β
t : { m' // ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ (hd :: tl)

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

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ (m : Raw₀ α β)
    (t :
      { m' //
        ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ tl
m : Raw₀ α β
t : { m' // ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 =
    (t.val.insert hd.fst hd.snd).insertListₘ tl

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ (m : Raw₀ α β)
    (t :
      { m' //
        ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ tl
m : Raw₀ α β
t : { m' // ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 =
    (t.val.insert hd.fst hd.snd).insertListₘ tl

Tactic:
apply ih

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
l : List ((a : α) × β a)
⊢ (m.insertMany l).val = m.insertListₘ 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₀ α β
l : List ((a : α) × β a)
⊢ (List.foldl (fun b a => ⟨b.val.insert a.fst a.snd, ⋯⟩) ⟨m, ⋯⟩ l).val = m.insertListₘ l

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

Tactic:
suffices ∀ (t : { m' // ∀ (P : Raw₀ α β → Prop),
  (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 =
  t.val.insertListₘ l from this _

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
l : List ((a : α) × β a)
⊢ ∀
    (t :
      { m' //
        ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
l : List ((a : α) × β a)
⊢ ∀
    (t :
      { m' //
        ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ l

Tactic:
intro t

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
l : List ((a : α) × β a)
t : { m' // ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ l

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
t : { m' // ∀ (P : Raw₀ α β → Prop), (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, 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 = t.val.insertListₘ []

Tactic:
simp [insertListₘ]

Result:
no goals