-- 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 nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys []
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst []).contains a = false
⊢ (insertList l []).Perm (l ++ [])

Tactic:
simp only [insertList, List.append_nil, Perm.refl]

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
⊢ containsKey hd.fst l = false ∧ containsKey hd.fst tl = false

Tactic:
refine ⟨Bool.not_eq_true _ ▸ fun h => ?_, distinct_toInsert.containsKey_eq_false⟩

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
h : containsKey hd.fst l = true
⊢ 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
⊢ containsKey hd.fst (insertList l tl) = false

Tactic:
simp only [containsKey_insertList, Bool.or_eq_false_iff, ← containsKey_eq_contains_map_fst]

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
⊢ containsKey hd.fst l = false ∧ containsKey hd.fst tl = 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 → (List.map Sigma.fst (hd :: tl)).contains a = false
⊢ (insertList l (hd :: tl)).Perm (l ++ hd :: tl)

Tactic:
simp only [List.map_cons, List.contains_cons, Bool.or_eq_false_iff] at distinct_both

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
⊢ (insertList l (hd :: tl)).Perm (l ++ hd :: tl)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false
⊢ (insertList l toInsert).Perm (l ++ toInsert)

Tactic:
rw [← DistinctKeys.def] at distinct_toInsert

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false
⊢ (insertList l toInsert).Perm (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
⊢ (insertEntry hd.fst hd.snd (insertList l tl)).Perm (l ++ hd :: tl)

Tactic:
rw [insertEntry_of_containsKey_eq_false]

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
⊢ (⟨hd.fst, hd.snd⟩ :: insertList l tl).Perm (l ++ hd :: tl)

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
⊢ containsKey hd.fst (insertList l tl) = false