case refine'_1
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
⊢ ∀ (a_1 : Sigma β),
    a_1 ∈ l → (if a = a_1.fst then some { fst := a, snd := b } else none) = Option.guard (fun s => a = s.fst) a_1

case refine'_2
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s => a = s.fst) a_1 → a_1 = b
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
⊢ kreplace a b l = l
refine' (lookmap_congr _).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) _ _)
case refine'_1.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
⊢ (if a = { fst := a', snd := b' }.fst then some { fst := a, snd := b } else none) =
    Option.guard (fun s => a = s.fst) { fst := a', snd := b' }
case refine'_1
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
⊢ ∀ (a_1 : Sigma β),
    a_1 ∈ l → (if a = a_1.fst then some { fst := a, snd := b } else none) = Option.guard (fun s => a = s.fst) a_1
rintro ⟨a', b'⟩ h'
case refine'_1.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
⊢ (if a = a' then some { fst := a, snd := b } else none) = if a = a' then some { fst := a', snd := b' } else none
case refine'_1.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
⊢ (if a = { fst := a', snd := b' }.fst then some { fst := a, snd := b } else none) =
    Option.guard (fun s => a = s.fst) { fst := a', snd := b' }
dsimp [Option.guard]
case refine'_1.mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
h✝ : a = a'
⊢ some { fst := a, snd := b } = some { fst := a', snd := b' }

case refine'_1.mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
h✝ : ¬a = a'
⊢ none = none
case refine'_1.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
⊢ (if a = a' then some { fst := a, snd := b } else none) = if a = a' then some { fst := a', snd := b' } else none
split_ifs
case refine'_1.mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
b' : β a
h' : { fst := a, snd := b' } ∈ l
⊢ some { fst := a, snd := b } = some { fst := a, snd := b' }
case refine'_1.mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
h✝ : a = a'
⊢ some { fst := a, snd := b } = some { fst := a', snd := b' }
subst a'
no goals
case refine'_1.mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
b' : β a
h' : { fst := a, snd := b' } ∈ l
⊢ some { fst := a, snd := b } = some { fst := a, snd := b' }
simp [nd.eq_of_mk_mem h h']
no goals
case refine'_1.mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a' : α
b' : β a'
h' : { fst := a', snd := b' } ∈ l
h✝ : ¬a = a'
⊢ none = none
rfl
case refine'_2.mk.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ { fst := a₂, snd := b₂ } ∈ Option.guard (fun s => a = s.fst) { fst := a₁, snd := b₁ } →
    { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
case refine'_2
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s => a = s.fst) a_1 → a_1 = b
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
case refine'_2.mk.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ ({ fst := a₂, snd := b₂ } ∈ if a = a₁ then some { fst := a₁, snd := b₁ } else none) →
    { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
case refine'_2.mk.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ { fst := a₂, snd := b₂ } ∈ Option.guard (fun s => a = s.fst) { fst := a₁, snd := b₁ } →
    { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
dsimp [Option.guard]
case refine'_2.mk.mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : a = a₁
⊢ { fst := a₂, snd := b₂ } ∈ some { fst := a₁, snd := b₁ } → { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }

case refine'_2.mk.mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : ¬a = a₁
⊢ { fst := a₂, snd := b₂ } ∈ none → { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
case refine'_2.mk.mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
⊢ ({ fst := a₂, snd := b₂ } ∈ if a = a₁ then some { fst := a₁, snd := b₁ } else none) →
    { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
split_ifs
no goals
case refine'_2.mk.mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : a = a₁
⊢ { fst := a₂, snd := b₂ } ∈ some { fst := a₁, snd := b₁ } → { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
simp
no goals
case refine'_2.mk.mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
a₁ : α
b₁ : β a₁
a₂ : α
b₂ : β a₂
h✝ : ¬a = a₁
⊢ { fst := a₂, snd := b₂ } ∈ none → { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
rintro ⟨⟩