-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ [BEq α] [Hashable α]
    (m : Raw₀ α (fun _ => Unit)) (l: List α):
    (Const.insertManyIfNewUnit m l).1 = Const.insertListIfNewUnitₘ m l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
⊢ (insertManyIfNewUnit m l).val = insertListIfNewUnitₘ m l

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

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
⊢ (List.foldl (fun b a => ⟨b.val.insertIfNew a (), ⋯⟩) ⟨m, ⋯⟩ l).val = insertListIfNewUnitₘ m l

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

Tactic:
intro t

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

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

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

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

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

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

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
⊢ (List.foldl (fun b a => ⟨b.val.insertIfNew a (), ⋯⟩) ⟨m, ⋯⟩ l).val = insertListIfNewUnitₘ m l

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

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

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

Tactic:
simp [insertListIfNewUnitₘ]

Result:
no goals

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

Tactic:
apply ih

Result:
no goals