-- Mathlib/GroupTheory/Perm/Support.lean
theorem mem_support_of_mem_noncommProd_support {α β : Type*} [DecidableEq β] [Fintype β]
    {s : Finset α} {f : α → Perm β}
    {comm : (s : Set α).Pairwise (Commute on f)} {x : β} (hx : x ∈ (s.noncommProd f comm).support) :
    ∃ a ∈ s, x ∈ (f a).support

Proof state:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ ((insert a s).noncommProd f comm).support

Tactic:
rw [Finset.noncommProd_insert_of_not_mem s a f comm ha]

Result:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a * s.noncommProd f ⋯).support

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {s : Finset α} {comm : (↑s).Pairwise (Commute on f)},
    (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support

Tactic:
apply Finset.induction

Result:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅).Pairwise (Commute on f)}, (∀ a ∈ ∅, x ∉ (f a).support) → x ∉ (∅.noncommProd f comm).support

case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support

Proof state:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support

Tactic:
intro a s ha ih comm hs

Result:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ ((insert a s).noncommProd f comm).support

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s).Pairwise (Commute on f)
x : β
hx : x ∈ (s.noncommProd f comm).support
⊢ ∃ a ∈ s, x ∈ (f a).support

Tactic:
contrapose! hx

Result:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s).Pairwise (Commute on f)
x : β
hx : ∀ a ∈ s, x ∉ (f a).support
⊢ x ∉ (s.noncommProd f comm).support

Proof state:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support

Tactic:
rw [Finset.sup_eq_union, Finset.not_mem_union]

Result:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ∧ x ∉ (s.noncommProd f ⋯).support

Proof state:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅).Pairwise (Commute on f)}, (∀ a ∈ ∅, x ∉ (f a).support) → x ∉ (∅.noncommProd f comm).support

Tactic:
simp

Result:
no goals

Proof state:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ∧ x ∉ (s.noncommProd f ⋯).support

Tactic:
exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩

Result:
no goals

Proof state:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a * s.noncommProd f ⋯).support

Tactic:
apply mt (Finset.mem_of_subset (support_mul_le _ _))

Result:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s).Pairwise (Commute on f)
x : β
hx : ∀ a ∈ s, x ∉ (f a).support
⊢ x ∉ (s.noncommProd f comm).support

Tactic:
revert hx comm s

Result:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {s : Finset α} {comm : (↑s).Pairwise (Commute on f)},
    (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support