case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.517618
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a | a ∈ m} fun a₁ a₂ => r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : f a₁ ∈ {b | b ∈ map f m}
a₂ : α
H₂ : a₂ ∈ m
h₂ : f a₂ ∈ {b | b ∈ map f m}
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)
α : Type u_1
β : Type u_2
γ : Type ?u.517618
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a | a ∈ m} fun a₁ a₂ => r (f a₁) (f a₂)
b₁ : β
h₁ : b₁ ∈ {b | b ∈ map f m}
b₂ : β
h₂ : b₂ ∈ {b | b ∈ map f m}
hn : b₁ ≠ b₂
⊢ r b₁ b₂
obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.517618
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a | a ∈ m} fun a₁ a₂ => r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : f a₁ ∈ {b | b ∈ map f m}
a₂ : α
H₂ : a₂ ∈ m
h₂ : f a₂ ∈ {b | b ∈ map f m}
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)
exact h H₁ H₂ (mt (congr_arg f) hn)