-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_noncommProd {ι : Type*} {k : ι → Perm α} {s : Finset ι}
    (hs : Set.Pairwise s fun i j ↦ Disjoint (k i) (k j)) :
    (s.noncommProd k (hs.imp (fun _ _ ↦ Perm.Disjoint.commute))).support =
      s.biUnion fun i ↦ (k i).support

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

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✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun i => (k i).support

Proof state:
case empty
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
hs : (↑∅).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (∅.noncommProd k ⋯).support = ∅.biUnion fun i => (k i).support

Tactic:
simp

Result:
no goals

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

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

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

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

Tactic:
rw [Equiv.Perm.Disjoint.support_mul, hrec hs']

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

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support

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.biUnion_insert]
  rw [Equiv.Perm.Disjoint.support_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:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ↑s ⊆ ↑(insert i s)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support

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.biUnion_insert]
  rw [Equiv.Perm.Disjoint.support_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
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (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✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ ∀ i_1 ∈ s, (k i).Disjoint (k i_1)

Proof state:
case insert.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (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✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (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.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (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