-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_cons_perm {k : α} {f : Option β → Option β} {k' : α} {v' : β}
    {l : List ((_ : α) × β)} :
    Perm (alterKey k f (⟨k', v'⟩ :: l))
      (if k' == k then
        match f (some v') with
          | none => l
          | some v => ⟨k, v⟩ :: l
        else
          ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : ¬(k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
rw [Bool.not_eq_true] at hk'

Result:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : ¬(k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
simp only [hk', Bool.false_eq_true, ↓reduceDIte]

Result:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : ¬(k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
⊢ (alterKey k f (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg.h_1
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ (⟨k', v'⟩ :: eraseKey k l).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: eraseKey k l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
by_cases hk' : k' == k

Result:
case pos
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : ¬(k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg.h_2
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ (insertEntry k v✝ (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: insertEntry k v✝ l)

Tactic:
simp [insertEntry_cons_of_false hk']

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
simp only [hk', ↓reduceDIte]

Result:
case pos
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if True then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
rw [getValue?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey]

Result:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
⊢ (match f (getValue? k l) with
      | none => ⟨k', v'⟩ :: eraseKey k l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else
      ⟨k', v'⟩ ::
        match f (getValue? k l) with
        | none => eraseKey k l
        | some v => insertEntry k v l)