-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem mem_eraseKey_of_key_beq_eq_false [BEq α] {a : α}
    {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.1 == a) = false) :
    p ∈ eraseKey a l ↔ p ∈ l

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h✝ : ¬(head✝.fst == a) = true
⊢ p ∈ ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝ ↔ p = head✝ ∨ p ∈ tail✝

Tactic:
next h =>
simp only [List.mem_cons, ih]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
⊢ p ∈ eraseKey a l ↔ p ∈ l

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
⊢ p ∈ eraseKey a [] ↔ p ∈ []

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
⊢ p ∈ eraseKey a (head✝ :: tail✝) ↔ p ∈ head✝ :: tail✝

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
h₁ : p.fst = head✝.fst
h₂ : HEq p.snd head✝.snd
⊢ p ∈ tail✝

Tactic:
rw [h₁, h] at hne

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p head✝ : (a : α) × β a
hne : true = false
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
h₁ : p.fst = head✝.fst
h₂ : HEq p.snd head✝.snd
⊢ p ∈ tail✝

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
⊢ p.fst = head✝.fst ∧ HEq p.snd head✝.snd → p ∈ tail✝

Tactic:
intro ⟨h₁, h₂⟩

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
h₁ : p.fst = head✝.fst
h₂ : HEq p.snd head✝.snd
⊢ p ∈ tail✝

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
⊢ (p ∈ if (head✝.fst == a) = true then tail✝ else ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝) ↔ p = head✝ ∨ p ∈ tail✝

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h✝ : (head✝.fst == a) = true
⊢ p ∈ tail✝ ↔ p = head✝ ∨ p ∈ tail✝

case isFalse
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h✝ : ¬(head✝.fst == a) = true
⊢ p ∈ ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝ ↔ p = head✝ ∨ p ∈ tail✝

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
⊢ p ∈ eraseKey a [] ↔ p ∈ []

Tactic:
simp only [eraseKey_nil]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p head✝ : (a : α) × β a
hne : true = false
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
h₁ : p.fst = head✝.fst
h₂ : HEq p.snd head✝.snd
⊢ p ∈ tail✝

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
⊢ (p ∈ bif head✝.fst == a then tail✝ else ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝) ↔ p = head✝ ∨ p ∈ tail✝

Tactic:
rw [cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
⊢ (p ∈ if (head✝.fst == a) = true then tail✝ else ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝) ↔ p = head✝ ∨ p ∈ tail✝

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
⊢ p ∈ eraseKey a (head✝ :: tail✝) ↔ p ∈ head✝ :: tail✝

Tactic:
simp only [eraseKey, List.mem_cons]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
⊢ (p ∈ bif head✝.fst == a then tail✝ else ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝) ↔ p = head✝ ∨ p ∈ tail✝

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
⊢ p ∈ tail✝ ↔ p = head✝ ∨ p ∈ tail✝

Tactic:
rw [iff_or_self, Sigma.ext_iff]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : (head✝.fst == a) = true
⊢ p.fst = head✝.fst ∧ HEq p.snd head✝.snd → p ∈ tail✝

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h✝ : (head✝.fst == a) = true
⊢ p ∈ tail✝ ↔ p = head✝ ∨ p ∈ tail✝

Tactic:
next h =>
rw [iff_or_self, Sigma.ext_iff]
intro ⟨h₁, h₂⟩
rw [h₁, h] at hne
contradiction

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ eraseKey a tail✝ ↔ p ∈ tail✝
h : ¬(head✝.fst == a) = true
⊢ p ∈ ⟨head✝.fst, head✝.snd⟩ :: eraseKey a tail✝ ↔ p = head✝ ∨ p ∈ tail✝

Tactic:
simp only [List.mem_cons, ih]

Result:
no goals