-- 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_both.inl
α : 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
distinct_toInsert : (∀ (a' : α), a' ∈ tl → (hd == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) tl
⊢ ∀ (x : α), x ∈ tl → (a == x) = false

Tactic:
intro x x_mem

Result:
case cons.distinct_both.inl
α : 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
distinct_toInsert : (∀ (a' : α), a' ∈ tl → (hd == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) tl
x : α
x_mem : x ∈ tl
⊢ (a == x) = false

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 : ∀ (a : α), containsKey a l = true → (hd :: tl).contains a = false
⊢ (if containsKey hd l = true then l.length else l.length + 1) + tl.length = l.length + (tl.length + 1)

Tactic:
specialize distinct_both hd

Result:
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 → (hd :: tl).contains hd = false
⊢ (if containsKey hd l = true then l.length else l.length + 1) + tl.length = l.length + (tl.length + 1)

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 → (hd :: tl).contains hd = false
⊢ (if containsKey hd l = true then l.length else l.length + 1) + tl.length = l.length + (tl.length + 1)

Tactic:
simp only [List.contains_cons, BEq.refl, Bool.true_or, and_true,
  Bool.not_eq_true] at distinct_both

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

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 : α
h : containsKey a l = true
distinct_both : (a == hd) = false ∧ tl.contains a = false
⊢ tl.contains a = false

Tactic:
apply And.right distinct_both

Result:
no goals

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

Tactic:
simp [insertListIfNewUnit]

Result:
no goals

Proof state:
case cons.distinct_both.inl
α : 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
distinct_toInsert : (∀ (a' : α), a' ∈ tl → (hd == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) tl
⊢ (tl.any fun x => a == x) = false

Tactic:
simp only [List.any_eq_false, Bool.not_eq_true]

Result:
case cons.distinct_both.inl
α : 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
distinct_toInsert : (∀ (a' : α), a' ∈ tl → (hd == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) tl
⊢ ∀ (x : α), x ∈ tl → (a == x) = false