-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
    ∃ l', Perm l (getEntry a l h :: l')

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = true
⊢ (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: t)

Tactic:
rw [getEntry_cons_of_beq hk]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
h : containsKey a [] = true
⊢ ∃ l', [].Perm (getEntry a [] h :: l')

Tactic:
simp at h

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = true
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Tactic:
exact ⟨t, by rw [getEntry_cons_of_beq hk]⟩

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ ∃ l', l.Perm (getEntry a l h :: l')

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
h : containsKey a [] = true
⊢ ∃ l', [].Perm (getEntry a [] h :: l')

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : ∀ (h : containsKey a tail✝ = true), ∃ l', tail✝.Perm (getEntry a tail✝ h :: l')
h : containsKey a (⟨k✝, v✝⟩ :: tail✝) = true
⊢ ∃ l', (⟨k✝, v✝⟩ :: tail✝).Perm (getEntry a (⟨k✝, v✝⟩ :: tail✝) h :: l')

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = false
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Tactic:
obtain ⟨l', hl'⟩ := ih (h.resolve_left (Bool.not_eq_true _ ▸ hk))

Result:
case false.intro
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = false
l' : List ((a : α) × β a)
hl' : t.Perm (getEntry a t ⋯ :: l')
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Tactic:
cases hk : k' == a

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = false
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

case true
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = true
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Proof state:
case false.intro
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = false
l' : List ((a : α) × β a)
hl' : t.Perm (getEntry a t ⋯ :: l')
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a t ⋯ :: l')

Tactic:
exact ⟨⟨k', v'⟩ :: l', (hl'.cons _).trans (Perm.swap' _ _ (Perm.refl _))⟩

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h : containsKey a (⟨k', v'⟩ :: t) = true
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h :: l')

Tactic:
simp only [containsKey_cons, Bool.or_eq_true] at h

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Proof state:
case false.intro
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = false
l' : List ((a : α) × β a)
hl' : t.Perm (getEntry a t ⋯ :: l')
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a (⟨k', v'⟩ :: t) h✝ :: l')

Tactic:
rw [getEntry_cons_of_false hk]

Result:
case false.intro
α : Type u
β : α → Type v
inst✝ : BEq α
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : ∀ (h : containsKey a t = true), ∃ l', t.Perm (getEntry a t h :: l')
h✝ : containsKey a (⟨k', v'⟩ :: t) = true
h : (k' == a) = true ∨ containsKey a t = true
hk : (k' == a) = false
l' : List ((a : α) × β a)
hl' : t.Perm (getEntry a t ⋯ :: l')
⊢ ∃ l', (⟨k', v'⟩ :: t).Perm (getEntry a t ⋯ :: l')