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

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ (insertList l (List.map Prod.toSigma toInsert)).length = l.length + toInsert.length

Tactic:
rw [length_insertList distinct_l]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ l.length + (List.map Prod.toSigma toInsert).length = l.length + toInsert.length

case distinct_toInsert
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ List.Pairwise (fun a b => (a.fst == b.fst) = false) (List.map Prod.toSigma toInsert)

case distinct_both
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ ∀ (a : α), containsKey a l = true → (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains a = false

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ l.length + (List.map Prod.toSigma toInsert).length = l.length + toInsert.length

Tactic:
simp

Result:
no goals

Proof state:
case distinct_both
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ ∀ (a : α), containsKey a l = true → (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains a = false

Tactic:
simpa using distinct_both

Result:
no goals

Proof state:
case distinct_toInsert
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ List.Pairwise (fun a b => (a.fst == b.fst) = false) (List.map Prod.toSigma toInsert)

Tactic:
simpa [List.pairwise_map]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ (insertListConst l toInsert).length = l.length + toInsert.length

Tactic:
unfold insertListConst

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false
⊢ (insertList l (List.map Prod.toSigma toInsert)).length = l.length + toInsert.length