-- Mathlib/Data/List/Sigma.lean
theorem kreplace_self {a : α} {b : β a} {l : List (Sigma β)} (nd : NodupKeys l)
    (h : Sigma.mk a b ∈ l) : kreplace a b l = l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β a
h' : ⟨a, b'⟩ ∈ l
⊢ some ⟨a, b⟩ = some ⟨a, b'⟩

Tactic:
simp [nd.eq_of_mk_mem h h']

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝ : a = a'
⊢ some ⟨a, b⟩ = some ⟨a', b'⟩

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β a
h' : ⟨a, b'⟩ ∈ l
⊢ some ⟨a, b⟩ = some ⟨a, b'⟩

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s => a = s.fst) a_1 → a_1 = b

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩

Result:
case refine_2.mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ ⟨a₂, b₂⟩ ∈ Option.guard (fun s => a = s.fst) ⟨a₁, b₁⟩ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Proof state:
case refine_2.mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = a₁ then some ⟨a₁, b₁⟩ else none) → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Tactic:
split_ifs

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : a = a₁
⊢ ⟨a₂, b₂⟩ ∈ some ⟨a₁, b₁⟩ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : ¬a = a₁
⊢ ⟨a₂, b₂⟩ ∈ none → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Proof state:
case refine_2.mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ ⟨a₂, b₂⟩ ∈ Option.guard (fun s => a = s.fst) ⟨a₁, b₁⟩ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Tactic:
dsimp [Option.guard]

Result:
case refine_2.mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = a₁ then some ⟨a₁, b₁⟩ else none) → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : a = a₁
⊢ ⟨a₂, b₂⟩ ∈ some ⟨a₁, b₁⟩ → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝ : ¬a = a'
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ kreplace a b l = l

Tactic:
refine (lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)

Result:
case refine_1
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ a_1 ∈ l, (if a = a_1.fst then some ⟨a, b⟩ else none) = Option.guard (fun s => a = s.fst) a_1

case refine_2
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s => a = s.fst) a_1 → a_1 = b

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : ¬a = a₁
⊢ ⟨a₂, b₂⟩ ∈ none → ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
case refine_1.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
⊢ (if a = ⟨a', b'⟩.fst then some ⟨a, b⟩ else none) = Option.guard (fun s => a = s.fst) ⟨a', b'⟩

Tactic:
dsimp [Option.guard]

Result:
case refine_1.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
⊢ (if a = a' then some ⟨a, b⟩ else none) = if a = a' then some ⟨a', b'⟩ else none

Proof state:
case refine_1.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
⊢ (if a = a' then some ⟨a, b⟩ else none) = if a = a' then some ⟨a', b'⟩ else none

Tactic:
split_ifs

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝ : a = a'
⊢ some ⟨a, b⟩ = some ⟨a', b'⟩

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝ : ¬a = a'
⊢ none = none

Proof state:
case refine_1
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ a_1 ∈ l, (if a = a_1.fst then some ⟨a, b⟩ else none) = Option.guard (fun s => a = s.fst) a_1

Tactic:
rintro ⟨a', b'⟩ h'

Result:
case refine_1.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
⊢ (if a = ⟨a', b'⟩.fst then some ⟨a, b⟩ else none) = Option.guard (fun s => a = s.fst) ⟨a', b'⟩