-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem Disjoint.cycleType_noncommProd {ι : Type*} {k : ι → Perm α} {s : Finset ι}
    (hs : Set.Pairwise s fun i j ↦ Disjoint (k i) (k j))
    (hs' : Set.Pairwise s fun i j ↦ Commute (k i) (k j) :=
      hs.imp (fun _ _ ↦ Perm.Disjoint.commute)) :
    (s.noncommProd k hs').cycleType = s.sum fun i ↦ (k i).cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
classical
induction s using Finset.induction_on with
| empty => simp
| @insert i s hi hrec =>
  have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
    hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
  rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, Finset.sum_insert hi]
  rw [Equiv.Perm.Disjoint.cycleType_mul, hrec hs']
  apply disjoint_noncommProd_right
  intro j hj
  apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
    simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Result:
no goals

Proof state:
case insert.hg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ (k i).Disjoint (k j)

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
  simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs' : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
⊢ ((insert i s).noncommProd k hs').cycleType = ∑ i ∈ insert i s, (k i).cycleType

Tactic:
have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
  hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])

Result:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k hs'✝).cycleType = ∑ i ∈ insert i s, (k i).cycleType

Proof state:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k hs'✝).cycleType = ∑ i ∈ insert i s, (k i).cycleType

Tactic:
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, Finset.sum_insert hi]

Result:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
induction s using Finset.induction_on with
| empty => simp
| @insert i s hi hrec =>
  have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
    hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
  rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, Finset.sum_insert hi]
  rw [Equiv.Perm.Disjoint.cycleType_mul, hrec hs']
  apply disjoint_noncommProd_right
  intro j hj
  apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
    simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Result:
no goals

Proof state:
case insert.hg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ∀ i_1 ∈ s, (k i).Disjoint (k i_1)

Tactic:
intro j hj

Result:
case insert.hg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ (k i).Disjoint (k j)

Proof state:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (k i).Disjoint (s.noncommProd k ⋯)

Tactic:
apply disjoint_noncommProd_right

Result:
case insert.hg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ∀ i_1 ∈ s, (k i).Disjoint (k i_1)