-- 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.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

Tactic:
apply BEq.neq_of_beq_of_neq

Result:
case cons.distinct_both.inl.intro.a
α : 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 == ?cons.distinct_both.inl.intro.b) = true

case cons.distinct_both.inl.intro.a
α : 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
⊢ (?cons.distinct_both.inl.intro.b == x) = false

case cons.distinct_both.inl.intro.b
α : 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
⊢ α

Proof state:
case cons.distinct_both
α : 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
⊢ (hd == a || containsKey a l) = true → tl.contains a = false

Tactic:
simp only [Bool.or_eq_true]

Result:
case cons.distinct_both
α : 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
⊢ (hd == a) = true ∨ containsKey a l = true → tl.contains a = false

Proof state:
case cons.false
α : 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
eq : containsKey hd l = false
⊢ l.length + 1 + tl.length = l.length + (tl.length + 1)

Tactic:
rw [Nat.add_assoc, Nat.add_comm 1 _]

Result:
no goals

Proof state:
case cons.distinct_both
α : 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
a : α
⊢ containsKey a (insertEntryIfNew hd () l) = true → tl.contains a = false

Tactic:
simp only [List.contains_cons, Bool.or_eq_true, not_and, not_or,
  Bool.not_eq_true] at distinct_both

Result:
case cons.distinct_both
α : 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
⊢ containsKey a (insertEntryIfNew hd () l) = true → tl.contains a = false

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
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 : (hd == a) = true
⊢ tl.contains a = false

Tactic:
simp only [pairwise_cons] at distinct_toInsert

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
⊢ tl.contains a = false