ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ (∀ (f_1 : Perm α), f_1 ∈ cycleFactorsFinset f ∪ cycleFactorsFinset g → IsCycle f_1) ∧
    ∃ h,
      noncommProd (cycleFactorsFinset f ∪ cycleFactorsFinset g) id
          (_ : Set.Pairwise ↑(cycleFactorsFinset f ∪ cycleFactorsFinset g) fun a b => _root_.Commute (id a) (id b)) =
        f * g
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ cycleFactorsFinset (f * g) = cycleFactorsFinset f ∪ cycleFactorsFinset g
rw [cycleFactorsFinset_eq_finset]
case refine'_1
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ ∀ (f_1 : Perm α), f_1 ∈ cycleFactorsFinset f ∪ cycleFactorsFinset g → IsCycle f_1

case refine'_2
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ Set.Pairwise (↑(cycleFactorsFinset f ∪ cycleFactorsFinset g)) Disjoint

case refine'_3
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ noncommProd (cycleFactorsFinset f ∪ cycleFactorsFinset g) id
      (_ : Set.Pairwise ↑(cycleFactorsFinset f ∪ cycleFactorsFinset g) fun a b => _root_.Commute (id a) (id b)) =
    f * g
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ (∀ (f_1 : Perm α), f_1 ∈ cycleFactorsFinset f ∪ cycleFactorsFinset g → IsCycle f_1) ∧
    ∃ h,
      noncommProd (cycleFactorsFinset f ∪ cycleFactorsFinset g) id
          (_ : Set.Pairwise ↑(cycleFactorsFinset f ∪ cycleFactorsFinset g) fun a b => _root_.Commute (id a) (id b)) =
        f * g
refine' ⟨_, _, _⟩
no goals
case refine'_1
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ ∀ (f_1 : Perm α), f_1 ∈ cycleFactorsFinset f ∪ cycleFactorsFinset g → IsCycle f_1
simp [or_imp, mem_cycleFactorsFinset_iff, forall_swap]
case refine'_2
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ Set.Pairwise (↑(cycleFactorsFinset f)) Disjoint ∧
    Set.Pairwise (↑(cycleFactorsFinset g)) Disjoint ∧
      ∀ (a : Perm α), a ∈ ↑(cycleFactorsFinset f) → ∀ (b : Perm α), b ∈ ↑(cycleFactorsFinset g) → a ≠ b → Disjoint a b
case refine'_2
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ Set.Pairwise (↑(cycleFactorsFinset f ∪ cycleFactorsFinset g)) Disjoint
rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]
no goals
case refine'_2
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ Set.Pairwise (↑(cycleFactorsFinset f)) Disjoint ∧
    Set.Pairwise (↑(cycleFactorsFinset g)) Disjoint ∧
      ∀ (a : Perm α), a ∈ ↑(cycleFactorsFinset f) → ∀ (b : Perm α), b ∈ ↑(cycleFactorsFinset g) → a ≠ b → Disjoint a b
exact
  ⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
    fun x hx y hy _ =>
    h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩
case refine'_3
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ noncommProd (cycleFactorsFinset f) id
        (_ : Set.Pairwise ↑(cycleFactorsFinset f) fun a b => _root_.Commute (id a) (id b)) *
      noncommProd (cycleFactorsFinset g) id
        (_ : Set.Pairwise ↑(cycleFactorsFinset g) fun a b => _root_.Commute (id a) (id b)) =
    f * g
case refine'_3
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ noncommProd (cycleFactorsFinset f ∪ cycleFactorsFinset g) id
      (_ : Set.Pairwise ↑(cycleFactorsFinset f ∪ cycleFactorsFinset g) fun a b => _root_.Commute (id a) (id b)) =
    f * g
rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]
no goals
case refine'_3
ι : Type ?u.2759828
α : Type u_1
β : Type ?u.2759834
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ noncommProd (cycleFactorsFinset f) id
        (_ : Set.Pairwise ↑(cycleFactorsFinset f) fun a b => _root_.Commute (id a) (id b)) *
      noncommProd (cycleFactorsFinset g) id
        (_ : Set.Pairwise ↑(cycleFactorsFinset g) fun a b => _root_.Commute (id a) (id b)) =
    f * g
rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]