case intro.intro
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
h₂ : (a₁, b₁) ∈ map (Prod.mk a₂) l₂
⊢ False
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ map (Prod.mk a₁) l₂
h₂ : x ∈ map (Prod.mk a₂) l₂
⊢ 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 : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
mb₂ : b₁ ∈ l₂
⊢ False
case intro.intro
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
h₂ : (a₁, b₁) ∈ map (Prod.mk a₂) l₂
⊢ 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 : α
l₂ : List β
d₁ : Nodup l₁
d₂ : Nodup l₂
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂
mb₂ : b₁ ∈ l₂
⊢ False
exact n rfl