case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
⊢ Subgroup.closure {σ | IsSwap σ} = ⊤
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
⊢ Subgroup.closure {σ | IsSwap σ} = ⊤
cases nonempty_fintype α
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
⊢ x ∈ Subgroup.closure {σ | IsSwap σ}
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
⊢ Subgroup.closure {σ | IsSwap σ} = ⊤
refine' eq_top_iff.mpr fun x _ => _
case intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : List.prod ↑(Trunc.out (truncSwapFactors x)) = x
h2 : ∀ (g : Perm α), g ∈ ↑(Trunc.out (truncSwapFactors x)) → IsSwap g
⊢ x ∈ Subgroup.closure {σ | IsSwap σ}
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
⊢ x ∈ Subgroup.closure {σ | IsSwap σ}
obtain ⟨h1, h2⟩ := Subtype.mem (truncSwapFactors x).out
case intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : List.prod ↑(Trunc.out (truncSwapFactors x)) = x
h2 : ∀ (g : Perm α), g ∈ ↑(Trunc.out (truncSwapFactors x)) → IsSwap g
⊢ List.prod ↑(Trunc.out (truncSwapFactors x)) ∈ Subgroup.closure {σ | IsSwap σ}
case intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : List.prod ↑(Trunc.out (truncSwapFactors x)) = x
h2 : ∀ (g : Perm α), g ∈ ↑(Trunc.out (truncSwapFactors x)) → IsSwap g
⊢ x ∈ Subgroup.closure {σ | IsSwap σ}
rw [← h1]
no goals
case intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : List.prod ↑(Trunc.out (truncSwapFactors x)) = x
h2 : ∀ (g : Perm α), g ∈ ↑(Trunc.out (truncSwapFactors x)) → IsSwap g
⊢ List.prod ↑(Trunc.out (truncSwapFactors x)) ∈ Subgroup.closure {σ | IsSwap σ}
exact Subgroup.list_prod_mem _ fun y hy => Subgroup.subset_closure (h2 y hy)