α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
hf : support x ≤ support f
hg : support y ≤ support g
⊢ _root_.Disjoint (support x) (support y)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : Disjoint f g
hf : support x ≤ support f
hg : support y ≤ support g
⊢ Disjoint x y
rw [disjoint_iff_disjoint_support] at h⊢
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
hf : support x ≤ support f
hg : support y ≤ support g
⊢ _root_.Disjoint (support x) (support y)
exact h.mono hf hg