ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
⊢ f = g → (IsCycle g ↔ IsCycle f)
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
⊢ cycleFactorsFinset f = {g} ↔ IsCycle f ∧ f = g
suffices f = g → (g.IsCycle ↔ f.IsCycle) by
  rw [cycleFactorsFinset_eq_finset]
  simpa [eq_comm]
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
⊢ IsCycle f ↔ IsCycle f
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
⊢ f = g → (IsCycle g ↔ IsCycle f)
rintro rfl
no goals
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
⊢ IsCycle f ↔ IsCycle f
exact Iff.rfl
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
this : f = g → (IsCycle g ↔ IsCycle f)
⊢ ((∀ (f : Perm α), f ∈ {g} → IsCycle f) ∧
      ∃ h, noncommProd {g} id (_ : Set.Pairwise ↑{g} fun a b => _root_.Commute (id a) (id b)) = f) ↔
    IsCycle f ∧ f = g
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
this : f = g → (IsCycle g ↔ IsCycle f)
⊢ cycleFactorsFinset f = {g} ↔ IsCycle f ∧ f = g
rw [cycleFactorsFinset_eq_finset]
no goals
ι : Type ?u.2753358
α : Type u_1
β : Type ?u.2753364
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
this : f = g → (IsCycle g ↔ IsCycle f)
⊢ ((∀ (f : Perm α), f ∈ {g} → IsCycle f) ∧
      ∃ h, noncommProd {g} id (_ : Set.Pairwise ↑{g} fun a b => _root_.Commute (id a) (id b)) = f) ↔
    IsCycle f ∧ f = g
simpa [eq_comm]