-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_insertList_of_mem [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k') {v : β k}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert) :
    getValueCast? k' (insertList l toInsert) =
    some (cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v)

Proof state:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ k = k'

Tactic:
exact LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ getEntry? k' (insertList l toInsert) = getEntry? k' toInsert

Tactic:
apply getEntry?_insertList_of_contains_eq_true distinct_l distinct_toInsert

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ containsKey k' toInsert = true

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ containsKey k toInsert = true

Tactic:
exact containsKey_of_mem mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ containsKey k' toInsert = true

Tactic:
apply containsKey_of_beq _ k_beq

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ containsKey k toInsert = true

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ k = k'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ getValueCast? k' (insertList l toInsert) = some (cast ⋯ v)

Tactic:
rw [getValueCast?_eq_getEntry?]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = some ⟨k, v⟩
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)

Tactic:
rw [Option.dmap_congr this]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = some ⟨k, v⟩
⊢ (Std.DHashMap.Internal.List.Option.dmap (some ⟨k, v⟩) fun a h' => cast ⋯ a.snd) = some (cast ⋯ v)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = some ⟨k, v⟩
⊢ (Std.DHashMap.Internal.List.Option.dmap (some ⟨k, v⟩) fun a h' => cast ⋯ a.snd) = some (cast ⋯ v)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)

Tactic:
have : getEntry? k' (insertList l toInsert) = getEntry? k' toInsert := by
  apply getEntry?_insertList_of_contains_eq_true distinct_l distinct_toInsert
  apply containsKey_of_beq _ k_beq
  exact containsKey_of_mem mem

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = getEntry? k' toInsert
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = getEntry? k' toInsert
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)

Tactic:
rw [← DistinctKeys.def] at distinct_toInsert

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = getEntry? k' toInsert
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)