-- 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_mem : x ∈ tl
⊢ (a == x) = false

Tactic:
rcases distinct_toInsert with ⟨left,_⟩

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

Proof state:
case cons.true
α : 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 = true
⊢ (if true = true then l.length else l.length + 1) + tl.length = l.length + (tl.length + 1)

Tactic:
simp [eq] at distinct_both

Result:
no goals

Proof state:
case cons.distinct_l
α : 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
⊢ DistinctKeys (insertEntryIfNew hd () l)

Tactic:
apply DistinctKeys.insertEntryIfNew distinct_l

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:
intro a

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

Tactic:
rw [ih]

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

case cons.distinct_l
α : 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
⊢ DistinctKeys (insertEntryIfNew hd () l)

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

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