-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem distinctKeys_cons_iff [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} : DistinctKeys (⟨k, v⟩ :: l) ↔ DistinctKeys l ∧ (containsKey k l) = false

Proof state:
case refine_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys (⟨k, v⟩ :: l)
h : List.Pairwise (fun a b => (a == b) = false) (keys (⟨k, v⟩ :: l))
⊢ DistinctKeys l ∧ containsKey k l = false

Tactic:
rw [keys_cons, pairwise_cons] at h

Result:
case refine_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys (⟨k, v⟩ :: l)
h : (∀ (a' : α), a' ∈ keys l → (k == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) (keys l)
⊢ DistinctKeys l ∧ containsKey k l = false

Proof state:
case refine_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys (⟨k, v⟩ :: l)
h : (∀ (a' : α), a' ∈ keys l → (k == a') = false) ∧ List.Pairwise (fun a b => (a == b) = false) (keys l)
⊢ DistinctKeys l ∧ containsKey k l = false

Tactic:
exact ⟨⟨h.2⟩, containsKey_eq_false_iff_forall_mem_keys.2 h.1⟩

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ DistinctKeys (⟨k, v⟩ :: l) ↔ DistinctKeys l ∧ containsKey k l = false

Tactic:
refine ⟨fun ⟨h⟩ => ?_, fun ⟨⟨h₁⟩, h₂⟩ => ⟨?_⟩⟩

Result:
case refine_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys (⟨k, v⟩ :: l)
h : List.Pairwise (fun a b => (a == b) = false) (keys (⟨k, v⟩ :: l))
⊢ DistinctKeys l ∧ containsKey k l = false

case refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys l ∧ containsKey k l = false
h₁ : List.Pairwise (fun a b => (a == b) = false) (keys l)
h₂ : containsKey k l = false
⊢ List.Pairwise (fun a b => (a == b) = false) (keys (⟨k, v⟩ :: l))

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys l ∧ containsKey k l = false
h₁ : List.Pairwise (fun a b => (a == b) = false) (keys l)
h₂ : containsKey k l = false
⊢ List.Pairwise (fun a b => (a == b) = false) (keys (⟨k, v⟩ :: l))

Tactic:
rw [keys_cons, pairwise_cons, ← containsKey_eq_false_iff_forall_mem_keys]

Result:
case refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys l ∧ containsKey k l = false
h₁ : List.Pairwise (fun a b => (a == b) = false) (keys l)
h₂ : containsKey k l = false
⊢ containsKey k l = false ∧ List.Pairwise (fun a b => (a == b) = false) (keys l)

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
x✝ : DistinctKeys l ∧ containsKey k l = false
h₁ : List.Pairwise (fun a b => (a == b) = false) (keys l)
h₂ : containsKey k l = false
⊢ containsKey k l = false ∧ List.Pairwise (fun a b => (a == b) = false) (keys l)

Tactic:
exact ⟨h₂, h₁⟩

Result:
no goals