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

Tactic:
apply BEq.symm h

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

Tactic:
cases h with
| inl h =>
  simp only [pairwise_cons] at distinct_toInsert
  rw [List.contains_eq_any_beq]
  simp only [List.any_eq_false, Bool.not_eq_true]
  intro x x_mem
  rcases distinct_toInsert with ⟨left,_⟩
  specialize left x x_mem
  apply BEq.neq_of_beq_of_neq
  apply BEq.symm h
  exact left
| inr h =>
  specialize distinct_both a h
  rw [Bool.or_eq_false_iff] at distinct_both
  apply And.right distinct_both

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

Tactic:
rw [containsKey_insertEntryIfNew]

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 || containsKey a l) = true → tl.contains a = 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) = true ∨ containsKey a l = true → tl.contains a = false

Tactic:
intro h

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