-- 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:
α : 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)
⊢ (h :: t).Sublist (p :: h :: t)

Tactic:
simp

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)
⊢ (p :: t).Sublist (p :: h :: t)

Tactic:
simp

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₂ : DistinctKeys (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:
rw [DistinctKeys.def] at hl₂

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
⊢ some ⟨h.fst, h.snd⟩ = some ⟨p.fst, p.snd⟩

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)
⊢ (insertList l₁ (p :: h :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ (h :: t)))

Tactic:
rw [insertList]

Result:
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)
⊢ (insertList (insertEntry p.fst p.snd l₁) (h :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ (h :: t)))

Proof state:
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✝)))

Tactic:
rename_i h t ih

Result:
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)
⊢ (insertList l₁ (p :: h :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ (h :: t)))

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)
⊢ (insertList (insertEntry p.fst p.snd l₁) (h :: t)).Perm (insertEntry p.fst p.snd (insertList l₁ (h :: t)))

Tactic:
refine (ih hl₁.insertEntry hl₂.tail).trans
  ((insertEntry_of_perm hl₁.insertList
    (ih hl₁ (distinctKeys_of_sublist (by simp) hl₂))).trans
  (List.Perm.trans ?_ (insertEntry_of_perm hl₁.insertList.insertEntry
    (ih hl₁ (distinctKeys_of_sublist (by simp) hl₂)).symm)))

Result:
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)))

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 : α
⊢ (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)

Tactic:
split <;> rename_i hp <;> split <;> rename_i hh <;> try rfl

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₂ : DistinctKeys (p :: h :: t)
k : α
hp : (h.fst == k) = true
hh : (p.fst == k) = true
⊢ some ⟨h.fst, h.snd⟩ = some ⟨p.fst, p.snd⟩