-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_alterKey (k k' : α) (f : Option (β k) → Option (β k))
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast? k' (alterKey k f l) =
      if h : k == k' then
        cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (getValueCast? k l))
      else
        getValueCast? k' l

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

Tactic:
simp only [beq_iff_eq, getValueCast?_insertEntry, dite_false, heq, Bool.false_eq_true]

Result:
no goals

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

Tactic:
next hsome =>
simp only [beq_iff_eq, getValueCast?_insertEntry, dite_false, heq, Bool.false_eq_true]

Result:
no goals

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

Tactic:
split

Result:
case refl.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
x✝ : Option (β k)
heq✝ : f (getValueCast? k l) = none
⊢ getValueCast? k (eraseKey k l) = f (getValueCast? k l)

case refl.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
x✝ : Option (β k)
v✝ : β k
heq✝ : f (getValueCast? k l) = some v✝
⊢ getValueCast? k (insertEntry k v✝ l) = f (getValueCast? k l)

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

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

Result:
no goals

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

Tactic:
rw [alterKey]

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

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCast? k' (alterKey k f l) =
    if h : (k == k') = true then cast ⋯ (f (getValueCast? k l)) else getValueCast? k' l

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
h✝ : (k == k') = true
⊢ getValueCast? k' (alterKey k f l) = cast ⋯ (f (getValueCast? k l))

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

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

Tactic:
simp only [getValueCast?_eraseKey_self hl, hnone]

Result:
no goals

Proof state:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
⊢ getValueCast? k (alterKey k f l) = f (getValueCast? k l)

Tactic:
rw [alterKey]

Result:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
⊢ getValueCast? k
      (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    f (getValueCast? k l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k') = true
⊢ getValueCast? k' (alterKey k f l) = cast ⋯ (f (getValueCast? k l))

Tactic:
cases eq_of_beq heq

Result:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
⊢ getValueCast? k (alterKey k f l) = cast ⋯ (f (getValueCast? k l))

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

Tactic:
split

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

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

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

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

Result:
no goals

Proof state:
case refl.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
x✝ : Option (β k)
heq✝ : f (getValueCast? k l) = none
⊢ getValueCast? k (eraseKey k l) = f (getValueCast? k l)

Tactic:
next hnone =>
simp only [getValueCast?_eraseKey_self hl, hnone]

Result:
no goals

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

Tactic:
rw [hsome, getValueCast?_insertEntry_self]

Result:
no goals