-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertListIfNewUnit_le [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}:
    (insertListIfNewUnit l toInsert).length ≤ l.length + toInsert.length

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertEntryIfNew hd () l).length + tl.length ≤ l.length + 1 + tl.length

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

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertEntryIfNew hd () l).length ≤ l.length + 1

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertListIfNewUnit l (hd :: tl)).length ≤ l.length + (hd :: tl).length

Tactic:
simp only [insertListIfNewUnit, List.length_cons]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertListIfNewUnit (insertEntryIfNew hd () l) tl).length ≤ l.length + (tl.length + 1)

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertEntryIfNew hd () l).length ≤ l.length + 1

Tactic:
apply length_insertEntryIfNew_le

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
⊢ (insertListIfNewUnit l toInsert).length ≤ l.length + toInsert.length

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

Result:
no goals

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
⊢ (insertListIfNewUnit l []).length ≤ l.length + [].length

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

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertListIfNewUnit (insertEntryIfNew hd () l) tl).length ≤ l.length + (tl.length + 1)

Tactic:
apply Nat.le_trans ih

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertEntryIfNew hd () l).length + tl.length ≤ l.length + (tl.length + 1)

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertEntryIfNew hd () 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
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).length ≤ l.length + tl.length
l : List ((_ : α) × Unit)
⊢ (insertEntryIfNew hd () l).length + tl.length ≤ l.length + 1 + tl.length