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

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

Tactic:
split <;> (try split) <;> simp_all

Result:
no goals

Proof state:
case cons.isTrue
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : Option β → Option β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : (alter a f tail✝).toList.Perm (Const.alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
⊢ (match f (some value✝) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    (match f (some 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✝ : EquivBEq α
a : α
f : Option β → Option β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : (alter a f tail✝).toList.Perm (Const.alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
x✝ : Option β
heq✝ : f (some value✝) = none
⊢ tail✝.toList.Perm
    (match f (some value✝) with
    | none => tail✝.toList
    | some v => ⟨a, v⟩ :: tail✝.toList)

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

Proof state:
case cons.isTrue
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : Option β → Option β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : (alter a f tail✝).toList.Perm (Const.alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
⊢ (match f (some value✝) with
        | none => tail✝
        | some b => cons a b tail✝).toList.Perm
    (match f (some 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✝ : EquivBEq α
a : α
f : Option β → Option β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : (alter a f tail✝).toList.Perm (Const.alterKey a f tail✝.toList)
h✝ : (key✝ == a) = true
x✝ : Option β
heq✝ : f (some value✝) = none
⊢ tail✝.toList.Perm
    (match f (some value✝) with
    | none => tail✝.toList
    | some v => ⟨a, v⟩ :: tail✝.toList)

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

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

Tactic:
refine Perm.trans ?_ Const.alterKey_cons_perm.symm

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

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : AssocList α fun x => β
⊢ (alter a f l).toList.Perm (Const.alterKey a f l.toList)

Tactic:
induction l

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

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

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

Tactic:
simp only [alter, toList_nil, alterKey_nil]

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

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

Tactic:
split <;> simp_all

Result:
no goals

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

Tactic:
rw [toList]

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

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

Tactic:
rw [alter]

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