-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem forIn_eq [Monad m] (l : AssocList α β) (init : δ)
    (f : (α × β) → δ → m (ForInStep δ)) : forIn l init f = forIn l.toList init f

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = forIn' tail✝.toList init fun a x => f a
init : δ
⊢ (do
      let __do_lift ← f (key✝, value✝) init
      match __do_lift with
        | ForInStep.done d => pure d
        | ForInStep.yield d => tail✝.forIn d f) =
    do
    let x ← f (key✝, value✝) init
    match x with
      | ForInStep.done d => pure d
      | ForInStep.yield b => forIn tail✝.toList b f

Tactic:
congr

Result:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = forIn' tail✝.toList init fun a x => f a
init : δ
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => tail✝.forIn d f) =
    fun x =>
    match x with
    | ForInStep.done d => pure d
    | ForInStep.yield b => forIn tail✝.toList b f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
l : AssocList α β
init : δ
f : α × β → δ → m (ForInStep δ)
⊢ l.forIn init f = forIn' l.toList init fun a x => f a

Tactic:
induction l generalizing init <;> simp [AssocList.forIn]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = forIn' tail✝.toList init fun a x => f a
init : δ
⊢ (do
      let __do_lift ← f (key✝, value✝) init
      match __do_lift with
        | ForInStep.done d => pure d
        | ForInStep.yield d => tail✝.forIn d f) =
    do
    let x ← f (key✝, value✝) init
    match x with
      | ForInStep.done d => pure d
      | ForInStep.yield b => forIn tail✝.toList b f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
l : AssocList α β
init : δ
f : α × β → δ → m (ForInStep δ)
⊢ forIn l init f = forIn l.toList init f

Tactic:
simp only [forIn]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
l : AssocList α β
init : δ
f : α × β → δ → m (ForInStep δ)
⊢ l.forIn init f = forIn' l.toList init fun a x => f a

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = forIn' tail✝.toList init fun a x => f a
init : δ
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => tail✝.forIn d f) =
    fun x =>
    match x with
    | ForInStep.done d => pure d
    | ForInStep.yield b => forIn tail✝.toList b f

Tactic:
funext a

Result:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = forIn' tail✝.toList init fun a x => f a
init : δ
a : ForInStep δ
⊢ (match a with
    | ForInStep.done d => pure d
    | ForInStep.yield d => tail✝.forIn d f) =
    match a with
    | ForInStep.done d => pure d
    | ForInStep.yield b => forIn tail✝.toList b f

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
δ : Type u_1
inst✝ : Monad m
f : α × β → δ → m (ForInStep δ)
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = forIn' tail✝.toList init fun a x => f a
init : δ
a : ForInStep δ
⊢ (match a with
    | ForInStep.done d => pure d
    | ForInStep.yield d => tail✝.forIn d f) =
    match a with
    | ForInStep.done d => pure d
    | ForInStep.yield b => forIn tail✝.toList b f

Tactic:
split <;> simp [*]

Result:
no goals