case mk.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ ({ fst := a₂, snd := b₂ } ∈ if a = { fst := a₁, snd := b₂✝ }.fst then some { fst := a, snd := b } else none) →
    { fst := a₁, snd := b₂✝ }.fst = { fst := a₂, snd := b₂ }.fst
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
⊢ ∀ (a_1 b_1 : Sigma β), (b_1 ∈ if a = a_1.fst then some { fst := a, snd := b } else none) → a_1.fst = b_1.fst
rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩
case mk.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ ({ fst := a₂, snd := b₂ } ∈ if a = a₁ then some { fst := a, snd := b } else none) → a₁ = a₂
case mk.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ ({ fst := a₂, snd := b₂ } ∈ if a = { fst := a₁, snd := b₂✝ }.fst then some { fst := a, snd := b } else none) →
    { fst := a₁, snd := b₂✝ }.fst = { fst := a₂, snd := b₂ }.fst
dsimp
no goals
case mk.mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ ({ fst := a₂, snd := b₂ } ∈ if a = a₁ then some { fst := a, snd := b } else none) → a₁ = a₂
split_ifs with h <;> simp (config := { contextual := true }) [h]