no goals
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hf : ↑f x = x
hg : ↑f (↑g x) = ↑g x
⊢ ↑(f * g) x = ↑(g * f) x
simp [mul_apply, hf, hg]
no goals
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hf : ↑f x = x
hg : ↑g (↑g x) = ↑g x
⊢ ↑(f * g) x = ↑(g * f) x
simp [mul_apply, hf, g.injective hg]
no goals
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hg : ↑g x = x
hf : ↑f (↑f x) = ↑f x
⊢ ↑(f * g) x = ↑(g * f) x
simp [mul_apply, f.injective hf, hg]
no goals
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hg : ↑g x = x
hf : ↑g (↑f x) = ↑f x
⊢ ↑(f * g) x = ↑(g * f) x
simp [mul_apply, hf, hg]