-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem toList_alter [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
    {l : AssocList α β} :
    Perm (l.alter a f).toList (alterKey a f l.toList)

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
⊢ (match f none with
        | none => nil
        | some b => cons a b nil).toList.Perm
    (match f none with
    | none => []
    | some b => [⟨a, b⟩])

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
⊢ (alter a f nil).toList.Perm (alterKey a f nil.toList)

Tactic:
simp only [alter, toList_nil, alterKey_nil]

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
⊢ (match f none with
        | none => nil
        | some b => cons a b nil).toList.Perm
    (match f none with
    | none => []
    | some b => [⟨a, b⟩])

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (alter a f (cons key✝ value✝ tail✝)).toList.Perm (alterKey a f (⟨key✝, value✝⟩ :: tail✝.toList))

Tactic:
refine Perm.trans ?_ alterKey_cons_perm.symm

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (alter a f (cons key✝ value✝ tail✝)).toList.Perm
    (if hk : (key✝ == a) = true then
      match f (some (cast ⋯ value✝)) with
      | none => tail✝.toList
      | some v => ⟨a, v⟩ :: tail✝.toList
    else ⟨key✝, value✝⟩ :: alterKey a f tail✝.toList)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (alter a f (cons key✝ value✝ tail✝)).toList.Perm (alterKey a f (cons key✝ value✝ tail✝).toList)

Tactic:
rw [toList]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (alter a f (cons key✝ value✝ tail✝)).toList.Perm (alterKey a f (⟨key✝, value✝⟩ :: tail✝.toList))

Proof state:
case cons.isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
⊢ (let_fun h' := ⋯;
        match f (some (cast ⋯ value✝)) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    (match f (some (cast ⋯ value✝)) with
    | none => tail✝.toList
    | some v => ⟨a, v⟩ :: tail✝.toList)

Tactic:
try split

Result:
case cons.isTrue.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
x✝ : Option (β a)
heq✝ : f (some (cast ⋯ value✝)) = none
⊢ (let_fun h' := ⋯;
        match f (some (cast ⋯ value✝)) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    tail✝.toList

case cons.isTrue.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
x✝ : Option (β a)
v✝ : β a
heq✝ : f (some (cast ⋯ value✝)) = some v✝
⊢ (let_fun h' := ⋯;
        match f (some (cast ⋯ value✝)) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    (⟨a, v✝⟩ :: tail✝.toList)

Proof state:
case cons.isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
⊢ (let_fun h' := ⋯;
        match f (some (cast ⋯ value✝)) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    (match f (some (cast ⋯ value✝)) with
    | none => tail✝.toList
    | some v => ⟨a, v⟩ :: tail✝.toList)

Tactic:
split

Result:
case cons.isTrue.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
x✝ : Option (β a)
heq✝ : f (some (cast ⋯ value✝)) = none
⊢ (let_fun h' := ⋯;
        match f (some (cast ⋯ value✝)) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    tail✝.toList

case cons.isTrue.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
x✝ : Option (β a)
v✝ : β a
heq✝ : f (some (cast ⋯ value✝)) = some v✝
⊢ (let_fun h' := ⋯;
        match f (some (cast ⋯ value✝)) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    (⟨a, v✝⟩ :: tail✝.toList)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (alter a f (cons key✝ value✝ tail✝)).toList.Perm
    (if hk : (key✝ == a) = true then
      match f (some (cast ⋯ value✝)) with
      | none => tail✝.toList
      | some v => ⟨a, v⟩ :: tail✝.toList
    else ⟨key✝, value✝⟩ :: alterKey a f tail✝.toList)

Tactic:
rw [alter]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (if h : (key✝ == a) = true then
          let_fun h' := ⋯;
          match f (some (cast ⋯ value✝)) with
          | none => tail✝
          | some b => cons a b tail✝
        else
          let tail := alter a f tail✝;
          cons key✝ value✝ tail).toList.Perm
    (if hk : (key✝ == a) = true then
      match f (some (cast ⋯ value✝)) with
      | none => tail✝.toList
      | some v => ⟨a, v⟩ :: tail✝.toList
    else ⟨key✝, value✝⟩ :: alterKey a f tail✝.toList)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : AssocList α β
⊢ (alter a f l).toList.Perm (alterKey a f l.toList)

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
⊢ (alter a f nil).toList.Perm (alterKey a f nil.toList)

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (alter a f (cons key✝ value✝ tail✝)).toList.Perm (alterKey a f (cons key✝ value✝ tail✝).toList)