no goals
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a✝ b✝ : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a : α
x✝ : a ∈ l₁
b b' : (fun a => σ a) a
h : { fst := a, snd := b } = { fst := a, snd := b' }
⊢ b = b'
injection h with _ h
case intro.intro
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
h₂ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₂) (l₂ a₂)
⊢ False
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ map (Sigma.mk a₁) (l₂ a₁)
h₂ : x ∈ map (Sigma.mk a₂) (l₂ a₂)
⊢ False
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
case intro.intro.intro.intro.refl
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
n : a₁ ≠ a₁
h₂ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
mb₂ : b₁ ∈ l₂ a₁
⊢ False
case intro.intro
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
h₂ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₂) (l₂ a₂)
⊢ False
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
no goals
case intro.intro.intro.intro.refl
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : Nodup l₁
d₂ : ∀ (a : α), Nodup (l₂ a)
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
n : a₁ ≠ a₁
h₂ : { fst := a₁, snd := b₁ } ∈ map (Sigma.mk a₁) (l₂ a₁)
mb₂ : b₁ ∈ l₂ a₁
⊢ False
exact n rfl