case mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ 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) = none
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
⊢ ∀ (a_1 : Sigma β), a_1 ∈ l → (if a = a_1.fst then some { fst := a, snd := b } else none) = none
rintro ⟨a', b'⟩ h
case mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ 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) = none
case mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ 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) = none
dsimp
case mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
a' : α
b' : β a'
h : { fst := a', snd := b' } ∈ l
h✝ : a = a'
⊢ False

case mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
a' : α
b' : β a'
h : { fst := a', snd := b' } ∈ l
h✝ : ¬a = a'
⊢ none = none
case mk
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ 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) = none
split_ifs
no goals
case mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
a' : α
b' : β a'
h : { fst := a', snd := b' } ∈ l
h✝ : ¬a = a'
⊢ none = none
. rfl
case mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
b' : β a
h : { fst := a, snd := b' } ∈ l
⊢ False
case mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
a' : α
b' : β a'
h : { fst := a', snd := b' } ∈ l
h✝ : a = a'
⊢ False
subst a'
no goals
case mk.inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
b' : β a
h : { fst := a, snd := b' } ∈ l
⊢ False
exact H _ h
no goals
case mk.inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l
a' : α
b' : β a'
h : { fst := a', snd := b' } ∈ l
h✝ : ¬a = a'
⊢ none = none
rfl