-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} (h : DistinctKeys l) : DistinctKeys (replaceEntry k v l)

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = true
⊢ DistinctKeys (List.replaceEntry k v (⟨k', v'⟩ :: l))

Tactic:
rw [replaceEntry_cons_of_true hk'k, distinctKeys_cons_iff]

Result:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = true
⊢ DistinctKeys l ∧ containsKey k l = false

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
h : DistinctKeys []
⊢ DistinctKeys (List.replaceEntry k v [])

Tactic:
simp

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = false
⊢ DistinctKeys (List.replaceEntry k v l) ∧ containsKey k' (List.replaceEntry k v l) = false

Tactic:
refine ⟨ih h.1, ?_⟩

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = false
⊢ containsKey k' (List.replaceEntry k v l) = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
⊢ DistinctKeys (List.replaceEntry k v l)

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
h : DistinctKeys []
⊢ DistinctKeys (List.replaceEntry k v [])

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : DistinctKeys tail✝ → DistinctKeys (List.replaceEntry k v tail✝)
h : DistinctKeys (⟨k✝, v✝⟩ :: tail✝)
⊢ DistinctKeys (List.replaceEntry k v (⟨k✝, v✝⟩ :: tail✝))

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

Tactic:
cases hk'k : k' == k

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = false
⊢ DistinctKeys (List.replaceEntry k v (⟨k', v'⟩ :: l))

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = true
⊢ DistinctKeys (List.replaceEntry k v (⟨k', v'⟩ :: l))

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = true
⊢ DistinctKeys l ∧ containsKey k l = false

Tactic:
refine ⟨h.1, ?_⟩

Result:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = true
⊢ containsKey k l = false

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = false
⊢ containsKey k' (List.replaceEntry k v l) = false

Tactic:
simpa using h.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys (⟨k', v'⟩ :: l)
⊢ DistinctKeys (List.replaceEntry k v (⟨k', v'⟩ :: l))

Tactic:
rw [distinctKeys_cons_iff] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
⊢ DistinctKeys (List.replaceEntry k v (⟨k', v'⟩ :: l))

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = true
⊢ containsKey k l = false

Tactic:
simpa [containsKey_congr (BEq.symm hk'k)] using h.2

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = false
⊢ DistinctKeys (List.replaceEntry k v (⟨k', v'⟩ :: l))

Tactic:
rw [replaceEntry_cons_of_false hk'k, distinctKeys_cons_iff]

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : DistinctKeys l → DistinctKeys (List.replaceEntry k v l)
h : DistinctKeys l ∧ containsKey k' l = false
hk'k : (k' == k) = false
⊢ DistinctKeys (List.replaceEntry k v l) ∧ containsKey k' (List.replaceEntry k v l) = false