case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (bind s f) (bind t g)
apply rel_join
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b => Rel p (f a) (g b)) s t
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
rw [rel_map]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b => Rel p (f a) (g b)) s t
exact hst.mono fun a _ b _ hr => h hr