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

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if hk : (k' == k) = true then
      match f (some (cast ⋯ 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
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = true
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if hk : (k' == k) = true then
      match f (some (cast ⋯ v')) with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

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

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = true
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if hk : (k' == k) = true then
      match f (some (cast ⋯ 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
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = true
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (match f (some (cast ⋯ v')) with
    | none => l
    | some v => ⟨k, v⟩ :: l)

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

Tactic:
rw [alterKey]

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

Proof state:
case neg.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = false
x✝ : Option (β k)
v✝ : β k
heq✝ : f (getValueCast? k l) = some v✝
⊢ (insertEntry k v✝ (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: insertEntry k v✝ l)

Tactic:
exact insertEntry_cons_of_false hk'

Result:
no goals

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

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

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

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

Tactic:
rw [Bool.not_eq_true] at hk'

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

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = true
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (match f (some (cast ⋯ v')) with
    | none => l
    | some v => ⟨k, v⟩ :: l)

Tactic:
rw [getValueCast?_cons_of_true hk', eraseKey_cons_of_beq hk']

Result:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = true
⊢ (match f (some (cast ⋯ v')) with
      | none => l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (match f (some (cast ⋯ v')) with
    | none => l
    | some v => ⟨k, v⟩ :: l)

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = true
⊢ (match f (some (cast ⋯ v')) with
      | none => l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (match f (some (cast ⋯ v')) with
    | none => l
    | some v => ⟨k, v⟩ :: l)

Tactic:
simp [insertEntry_cons_of_beq hk']

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : ¬(k' == k) = true
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if hk : (k' == k) = true then
      match f (some (cast ⋯ 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
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : ¬(k' == k) = true
⊢ (match f (getValueCast? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (⟨k', v'⟩ :: alterKey k f l)