-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem perm_insertList [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (distinct_both : ∀ (a : α), containsKey a l → (toInsert.map Sigma.fst).contains a = false) :
    Perm (insertList l toInsert) (l ++ toInsert)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      DistinctKeys tl →
        (∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false) →
          (insertList l tl).Perm (l ++ tl)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd.fst) = false ∧ (List.map Sigma.fst tl).contains a = false
⊢ ∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false

Tactic:
exact fun a ha => (distinct_both a ha).2

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      DistinctKeys tl →
        (∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false) →
          (insertList l tl).Perm (l ++ tl)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd.fst) = false ∧ (List.map Sigma.fst tl).contains a = false
⊢ (⟨hd.fst, hd.snd⟩ :: insertList l tl).Perm (l ++ hd :: tl)

Tactic:
refine (Perm.cons _ (ih distinct_l (distinct_toInsert).tail ?_)).trans List.perm_middle.symm

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      DistinctKeys tl →
        (∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false) →
          (insertList l tl).Perm (l ++ tl)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd.fst) = false ∧ (List.map Sigma.fst tl).contains a = false
⊢ ∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      DistinctKeys tl →
        (∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false) →
          (insertList l tl).Perm (l ++ tl)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd.fst) = false ∧ (List.map Sigma.fst tl).contains a = false
h : containsKey hd.fst l = true
⊢ False

Tactic:
simpa using (distinct_both _ h).1

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      DistinctKeys tl →
        (∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false) →
          (insertList l tl).Perm (l ++ tl)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd.fst) = false ∧ (List.map Sigma.fst tl).contains a = false
⊢ (insertList l (hd :: tl)).Perm (l ++ hd :: tl)

Tactic:
refine (insertList_cons_perm distinct_l distinct_toInsert).trans ?_

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      DistinctKeys tl →
        (∀ (a : α), containsKey a l = true → (List.map Sigma.fst tl).contains a = false) →
          (insertList l tl).Perm (l ++ tl)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd.fst) = false ∧ (List.map Sigma.fst tl).contains a = false
⊢ (insertEntry hd.fst hd.snd (insertList l tl)).Perm (l ++ hd :: tl)