-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β)
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue? k' (alterKey k f l) =
      if k == k' then
        f (getValue? k l)
      else
        getValue? k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
x✝ : Option β
hnone : f (getValue? k l) = none
⊢ getValue? k' (eraseKey k l) = getValue? k' l

Tactic:
simp only [heq, hnone, hl, beq_iff_eq, getValue?_eraseKey, ite_false, Bool.false_eq_true,
  reduceIte]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
⊢ getValue? k' (alterKey k f l) = getValue? k' l

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
⊢ getValue? k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    getValue? k' l

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ getValue? k' (eraseKey k l) = getValue? k' l

Tactic:
next hnone =>
simp only [heq, hnone, hl, beq_iff_eq, getValue?_eraseKey, ite_false, Bool.false_eq_true,
  reduceIte]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
⊢ getValue? k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    f (getValue? k l)

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ getValue? k' (eraseKey k l) = f (getValue? k l)

case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ getValue? k' (insertEntry k v✝ l) = f (getValue? k l)

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValue? k' (alterKey k f l) = if (k == k') = true then f (getValue? k l) else getValue? k' l

Tactic:
split

Result:
case isTrue
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : (k == k') = true
⊢ getValue? k' (alterKey k f l) = f (getValue? k l)

case isFalse
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : ¬(k == k') = true
⊢ getValue? k' (alterKey k f l) = getValue? k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
x✝ : Option β
v✝ : β
hsome : f (getValue? k l) = some v✝
⊢ getValue? k' (insertEntry k v✝ l) = getValue? k' l

Tactic:
simp only [getValue?_insertEntry, heq, Bool.false_eq_true, reduceIte]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
⊢ getValue? k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    getValue? k' l

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ getValue? k' (eraseKey k l) = getValue? k' l

case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ getValue? k' (insertEntry k v✝ l) = getValue? k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
⊢ getValue? k' (alterKey k f l) = f (getValue? k l)

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
⊢ getValue? k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    f (getValue? k l)

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
x✝ : Option β
hnone : f (getValue? k l) = none
⊢ getValue? k' (eraseKey k l) = f (getValue? k l)

Tactic:
simp only [getValue?_eraseKey_of_beq hl heq, hnone]

Result:
no goals

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : ¬(k == k') = true
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ getValue? k' (insertEntry k v✝ l) = getValue? k' l

Tactic:
next hsome =>
simp only [getValue?_insertEntry, heq, Bool.false_eq_true, reduceIte]

Result:
no goals

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ getValue? k' (eraseKey k l) = f (getValue? k l)

Tactic:
next hnone =>
simp only [getValue?_eraseKey_of_beq hl heq, hnone]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
x✝ : Option β
v✝ : β
hsome : f (getValue? k l) = some v✝
⊢ getValue? k' (insertEntry k v✝ l) = f (getValue? k l)

Tactic:
rw [hsome, getValue?_insertEntry_of_beq heq]

Result:
no goals

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
heq : (k == k') = true
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ getValue? k' (insertEntry k v✝ l) = f (getValue? k l)

Tactic:
next hsome =>
rw [hsome, getValue?_insertEntry_of_beq heq]

Result:
no goals