case intro.intro
α : Type u_1
β : Type ?u.474373
γ : Type ?u.474376
δ : Type ?u.474379
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x
α : Type u_1
β : Type ?u.474373
γ : Type ?u.474376
δ : Type ?u.474379
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
⊢ r a x
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
no goals
case intro.intro
α : Type u_1
β : Type ?u.474373
γ : Type ?u.474376
δ : Type ?u.474379
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x
rwa [eq_of_mem_replicate hb1] at hb2