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

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

Tactic:
rw [getEntry?_cons_of_true h'', getEntry?_cons_of_true h'']

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k a : α
hka : (k == a) = false
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a (eraseKey k t) = getEntry? a t
⊢ getEntry? a (eraseKey k (⟨k', v'⟩ :: t)) = getEntry? a (⟨k', v'⟩ :: t)

Tactic:
cases h' : k' == k

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

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

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

Tactic:
rw [eraseKey_cons_of_false h']

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

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k a : α
hka : (k == a) = false
⊢ getEntry? a (eraseKey k []) = getEntry? a []

Tactic:
simp

Result:
no goals

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

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

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hka : (k == a) = false
⊢ getEntry? a (eraseKey k l) = getEntry? a l

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k a : α
hka : (k == a) = false
⊢ getEntry? a (eraseKey k []) = getEntry? a []

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

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

Tactic:
rw [getEntry?_cons_of_false hx]

Result:
no goals

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

Tactic:
have hx : (k' == a) = false := BEq.neq_of_beq_of_neq h' hka

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

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

Tactic:
rw [eraseKey_cons_of_beq h']

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

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

Tactic:
cases h'' : k' == a

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

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