α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
⊢ ∀ {a_1 b_1 : Sigma β},
    a_1.fst ≠ b_1.fst →
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some { fst := a, snd := b } else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some { fst := a, snd := b } else none) → a_1 = b_1 ∧ c = d
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
⊢ Pairwise
    (fun a_1 b_1 =>
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some { fst := a, snd := b } else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some { fst := a, snd := b } else none) → a_1 = b_1 ∧ c = d)
    l₁
refine' nd.pairwise_ne.imp _
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some { fst := a, snd := b } else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some { fst := a, snd := b } else none
⊢ x = y ∧ z = w
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
⊢ ∀ {a_1 b_1 : Sigma β},
    a_1.fst ≠ b_1.fst →
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some { fst := a, snd := b } else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some { fst := a, snd := b } else none) → a_1 = b_1 ∧ c = d
intro x y h z h₁ w h₂
case inl.inl.refl.refl
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ { fst := a, snd := b } = { fst := a, snd := b }
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some { fst := a, snd := b } else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some { fst := a, snd := b } else none
⊢ x = y ∧ z = w
split_ifs  at h₁ h₂ with h_2 h_1 <;> cases h₁ <;> cases h₂
no goals
case inl.inl.refl.refl
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : NodupKeys l₁
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ { fst := a, snd := b } = { fst := a, snd := b }
exact (h (h_2.symm.trans h_1)).elim