no goals
ι : Type ?u.2795604
α : Type ?u.2795607
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
⊢ closure {σ | IsCycle σ} = ⊤
classical
  cases nonempty_fintype β
  exact
    top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))
case intro
ι : Type ?u.2795604
α : Type ?u.2795607
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
val✝ : Fintype β
⊢ closure {σ | IsCycle σ} = ⊤
ι : Type ?u.2795604
α : Type ?u.2795607
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
⊢ closure {σ | IsCycle σ} = ⊤
cases nonempty_fintype β
no goals
case intro
ι : Type ?u.2795604
α : Type ?u.2795607
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite β
val✝ : Fintype β
⊢ closure {σ | IsCycle σ} = ⊤
exact
  top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))