-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a == b) = false))
    (distinct_both : ∀ (a : α), containsKey a l → toInsert.contains a = false) :
    (insertListIfNewUnit l toInsert).length = l.length + toInsert.length

Proof state:
case cons.distinct_toInsert
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) (hd :: tl)
distinct_both : ∀ (a : α), containsKey a l = true → (hd :: tl).contains a = false
⊢ List.Pairwise (fun a b => (a == b) = false) tl

Tactic:
simp only [pairwise_cons] at distinct_toInsert

Result:
case cons.distinct_toInsert
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
distinct_both : ∀ (a : α), containsKey a l = true → (hd :: tl).contains a = false
distinct_toInsert : (∀ (a' : α), a' ∈ tl → (hd == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) tl
⊢ List.Pairwise (fun a b => (a == b) = false) tl

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) (hd :: tl)
distinct_both : containsKey hd l = true → true = false
⊢ (if containsKey hd l = true then l.length else l.length + 1) + tl.length = l.length + (tl.length + 1)

Tactic:
cases eq : containsKey hd l with
| true => simp [eq] at distinct_both
| false =>
  simp only [Bool.false_eq_true, ↓reduceIte]
  rw [Nat.add_assoc, Nat.add_comm 1 _]

Result:
no goals

Proof state:
case cons.distinct_toInsert
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
distinct_both : ∀ (a : α), containsKey a l = true → (hd :: tl).contains a = false
distinct_toInsert : (∀ (a' : α), a' ∈ tl → (hd == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) tl
⊢ List.Pairwise (fun a b => (a == b) = false) tl

Tactic:
apply And.right distinct_toInsert

Result:
no goals

Proof state:
case cons.distinct_both.inr
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) (hd :: tl)
a : α
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd || tl.contains a) = false
h : containsKey a l = true
⊢ tl.contains a = false

Tactic:
specialize distinct_both a h

Result:
case cons.distinct_both.inr
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) (hd :: tl)
a : α
h : containsKey a l = true
distinct_both : (a == hd || tl.contains a) = false
⊢ tl.contains a = false

Proof state:
case cons.distinct_both.inl.intro
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
a : α
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd || tl.contains a) = false
h : (hd == a) = true
x : α
x_mem : x ∈ tl
left : ∀ (a' : α), a' ∈ tl → (hd == a') = false
right✝ : List.Pairwise (fun a b => (a == b) = false) tl
⊢ (a == x) = false

Tactic:
specialize left x x_mem

Result:
case cons.distinct_both.inl.intro
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a == b) = false) tl →
        (∀ (a : α), containsKey a l = true → tl.contains a = false) →
          (insertListIfNewUnit l tl).length = l.length + tl.length
l : List ((_ : α) × Unit)
distinct_l : DistinctKeys l
a : α
distinct_both : ∀ (a : α), containsKey a l = true → (a == hd || tl.contains a) = false
h : (hd == a) = true
x : α
x_mem : x ∈ tl
right✝ : List.Pairwise (fun a b => (a == b) = false) tl
left : (hd == x) = false
⊢ (a == x) = false