-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertList_cons_perm [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
    {p : (a : α) × β a} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys (p :: l₂)) :
    (insertList l₁ (p :: l₂)).Perm (insertEntry p.1 p.2 (insertList l₁ l₂))

Proof state:
case isTrue.isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : List.Pairwise (fun a b => (a.fst == b.fst) = false) (p :: h :: t)
k : α
hp : (h.fst == k) = true
hh : (p.fst == k) = true
⊢ some ⟨h.fst, h.snd⟩ = some ⟨p.fst, p.snd⟩

Tactic:
have := List.rel_of_pairwise_cons hl₂ (List.mem_cons_self _ _)

Result:
case isTrue.isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : List.Pairwise (fun a b => (a.fst == b.fst) = false) (p :: h :: t)
k : α
hp : (h.fst == k) = true
hh : (p.fst == k) = true
this : (p.fst == h.fst) = false
⊢ some ⟨h.fst, h.snd⟩ = some ⟨p.fst, p.snd⟩

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys [p]
⊢ (insertList l₁ [p]).Perm (insertEntry p.fst p.snd (insertList l₁ []))

Tactic:
simp [insertList]

Result:
no goals

Proof state:
case isTrue.isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : List.Pairwise (fun a b => (a.fst == b.fst) = false) (p :: h :: t)
k : α
hp : (h.fst == k) = true
hh : (p.fst == k) = true
this : (p.fst == h.fst) = false
⊢ some ⟨h.fst, h.snd⟩ = some ⟨p.fst, p.snd⟩

Tactic:
simp [BEq.trans hh (BEq.symm hp)] at this

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: h :: t)
k : α
⊢ getEntry? k (insertEntry h.fst h.snd (insertEntry p.fst p.snd (insertList l₁ t))) =
    getEntry? k (insertEntry p.fst p.snd (insertEntry h.fst h.snd (insertList l₁ t)))

Tactic:
simp only [getEntry?_insertEntry]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: h :: t)
k : α
⊢ (if (h.fst == k) = true then some ⟨h.fst, h.snd⟩
    else if (p.fst == k) = true then some ⟨p.fst, p.snd⟩ else getEntry? k (insertList l₁ t)) =
    if (p.fst == k) = true then some ⟨p.fst, p.snd⟩
    else if (h.fst == k) = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l₁ t)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l₁ l₂ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: l₂)
⊢ (insertList l₁ (p :: l₂)).Perm (insertEntry p.fst p.snd (insertList l₁ l₂))

Tactic:
induction l₂ generalizing p l₁

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys [p]
⊢ (insertList l₁ [p]).Perm (insertEntry p.fst p.snd (insertList l₁ []))

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ →
      DistinctKeys (p :: tail✝) → (insertList l₁ (p :: tail✝)).Perm (insertEntry p.fst p.snd (insertList l₁ tail✝))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: head✝ :: tail✝)
⊢ (insertList l₁ (p :: head✝ :: tail✝)).Perm (insertEntry p.fst p.snd (insertList l₁ (head✝ :: tail✝)))

Proof state:
case isFalse.isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: h :: t)
k : α
hp : ¬(h.fst == k) = true
hh : ¬(p.fst == k) = true
⊢ getEntry? k (insertList l₁ t) = getEntry? k (insertList l₁ t)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: h :: t)
⊢ (insertEntry h.fst h.snd (insertEntry p.fst p.snd (insertList l₁ t))).Perm
    (insertEntry p.fst p.snd (insertEntry h.fst h.snd (insertList l₁ t)))

Tactic:
apply getEntry?_ext hl₁.insertList.insertEntry.insertEntry
  hl₁.insertList.insertEntry.insertEntry (fun k => ?_)

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l₁ : List ((a : α) × β a)} {p : (a : α) × β a},
    DistinctKeys l₁ → DistinctKeys (p :: t) → (insertList l₁ (p :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ t))
l₁ : List ((a : α) × β a)
p : (a : α) × β a
hl₁ : DistinctKeys l₁
hl₂ : DistinctKeys (p :: h :: t)
k : α
⊢ getEntry? k (insertEntry h.fst h.snd (insertEntry p.fst p.snd (insertList l₁ t))) =
    getEntry? k (insertEntry p.fst p.snd (insertEntry h.fst h.snd (insertList l₁ t)))