-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α}
    (h : a == b) : getEntry? a l = getEntry? b l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

Tactic:
cases h' : k == a

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
h' : (k == a) = false
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
h' : (k == a) = true
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a b : α
h : (a == b) = true
⊢ getEntry? a l = getEntry? b l

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
⊢ getEntry? a [] = getEntry? b []

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : getEntry? a tail✝ = getEntry? b tail✝
⊢ getEntry? a (⟨k✝, v✝⟩ :: tail✝) = getEntry? b (⟨k✝, v✝⟩ :: tail✝)

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
⊢ getEntry? a [] = getEntry? b []

Tactic:
simp

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
h' : (k == a) = false
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

Tactic:
have h₂ : (k == b) = false := BEq.neq_of_neq_of_beq h' h

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
h' : (k == a) = false
h₂ : (k == b) = false
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
h' : (k == a) = false
h₂ : (k == b) = false
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

Tactic:
rw [getEntry?_cons_of_false h', getEntry?_cons_of_false h₂, ih]

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a b : α
h : (a == b) = true
k : α
v : β k
l : List ((a : α) × β a)
ih : getEntry? a l = getEntry? b l
h' : (k == a) = true
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? b (⟨k, v⟩ :: l)

Tactic:
rw [getEntry?_cons_of_true h', getEntry?_cons_of_true (BEq.trans h' h)]

Result:
no goals