-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertList_le [BEq α]
    {l toInsert : List ((a : α) × β a)} :
    (insertList l toInsert).length ≤ l.length + toInsert.length

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertList (insertEntry hd.fst hd.snd l) tl).length ≤ l.length + (tl.length + 1)

Tactic:
apply Nat.le_trans ih

Result:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertEntry hd.fst hd.snd l).length + tl.length ≤ l.length + (tl.length + 1)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertEntry hd.fst hd.snd l).length + tl.length ≤ l.length + 1 + tl.length

Tactic:
apply Nat.add_le_add length_insertEntry_le (Nat.le_refl _)

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
⊢ (insertList l []).length ≤ l.length + [].length

Tactic:
simp only [insertList, List.length_nil, Nat.add_zero, Nat.le_refl]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l toInsert : List ((a : α) × β a)
⊢ (insertList l toInsert).length ≤ l.length + toInsert.length

Tactic:
induction toInsert generalizing l with
| nil => simp only [insertList, List.length_nil, Nat.add_zero, Nat.le_refl]
| cons hd tl ih =>
  simp only [insertList, List.length_cons]
  apply Nat.le_trans ih
  rw [Nat.add_comm tl.length 1, ← Nat.add_assoc]
  apply Nat.add_le_add length_insertEntry_le (Nat.le_refl _)

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertList l (hd :: tl)).length ≤ l.length + (hd :: tl).length

Tactic:
simp only [insertList, List.length_cons]

Result:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertList (insertEntry hd.fst hd.snd l) tl).length ≤ l.length + (tl.length + 1)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertEntry hd.fst hd.snd l).length + tl.length ≤ l.length + (tl.length + 1)

Tactic:
rw [Nat.add_comm tl.length 1, ← Nat.add_assoc]

Result:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).length ≤ l.length + tl.length
l : List ((a : α) × β a)
⊢ (insertEntry hd.fst hd.snd l).length + tl.length ≤ l.length + 1 + tl.length