α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
⊢ f = 1
α : Type u_1
f g h : Perm α
⊢ Disjoint f f ↔ f = 1
refine' ⟨fun h => _, fun h => h.symm ▸ disjoint_one_left 1⟩
case H
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
⊢ ↑f x = ↑1 x
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
⊢ f = 1
ext x
no goals
case H
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
⊢ ↑f x = ↑1 x
cases' h x with hx hx <;> simp [hx]