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

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

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ replaceEntry a b tail✝ ↔ p ∈ tail✝
h✝ : (head✝.fst == a) = true
⊢ p ∈ ⟨a, b⟩ :: tail✝ ↔ p ∈ head✝ :: tail✝

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

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

Tactic:
simp only [List.mem_cons, Sigma.ext_iff]

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

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

Tactic:
simp_all only [BEq.refl, Bool.true_eq_false]

Result:
no goals

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

Tactic:
simp only [List.mem_cons, ih]

Result:
no goals

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
p : (a : α) × β a
hne : (p.fst == a) = false
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : p ∈ replaceEntry a b tail✝ ↔ p ∈ tail✝
h✝ : (head✝.fst == a) = true
⊢ p ∈ ⟨a, b⟩ :: tail✝ ↔ p ∈ head✝ :: tail✝

Tactic:
next h =>
simp only [List.mem_cons, Sigma.ext_iff]
apply Iff.intro <;> exact fun
| Or.inr y => Or.inr y
| Or.inl y => by simp_all only [BEq.refl, Bool.true_eq_false]

Result:
no goals

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

Tactic:
simp only [replaceEntry_nil]

Result:
no goals

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

Tactic:
simp only [replaceEntry, cond_eq_if]

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

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

Tactic:
apply Iff.intro <;> exact fun
| Or.inr y => Or.inr y
| Or.inl y => by simp_all only [BEq.refl, Bool.true_eq_false]

Result:
no goals

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

Tactic:
induction l

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

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