awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
comm : (↑(Insert.insert a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ Insert.insert a s), x ∉ (f a_1).support
insert : x ∉ (f a).support ∧ x ∉ (s.noncommProd f ⋯).support
⊢ x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support

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

Premises used: Finset.notMem_union, Finset.sup_eq_union
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ insert a s), x ∉ (f a_1).support
⊢ x ∉ (f a).support ∧ x ∉ (s.noncommProd f ⋯).support

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

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, And.intro
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : 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))⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s : Set α).Pairwise (Commute on f)
x : β
hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support
revert :
  ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
empty :
  ∀ {comm : (↑∅ : Set α).Pairwise (Commute on f)}
    (hx : ∀ (a : α) (_ : Membership.mem (γ := Finset α) ∅ a), x ∉ (f a).support), x ∉ (noncommProd ∅ f comm).support
insert insert₁ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
          x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(Insert.insert a s) : Set α).Pairwise (Commute on f)}
          (hx : ∀ (a_3 : α) (_ : a_3 ∈ Insert.insert a s), x ∉ (f a_3).support),
          x ∉ ((Insert.insert a s).noncommProd f comm).support
⊢ x ∉ (s.noncommProd f comm).support

Tactic:
classical
  revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.notMem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩

Premises used: mt, Equiv.Perm.support_mul_le, Finset.notMem_union, Finset.sup_eq_union, Finset.mem_of_subset
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
⊢ Membership.mem (α := α) f.support ((f ^ n : (a : α) → α) x : α) ↔ x ∈ f.support

Tactic:
simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]

Premises used: Equiv.Perm.mem_support, ne_eq, Equiv.Perm.apply_pow_apply_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℤ
x : α
⊢ Membership.mem (α := α) f.support ((f ^ n : (a : α) → α) x : α) ↔ x ∈ f.support

Tactic:
simp only [mem_support, ne_eq, apply_zpow_apply_eq_iff]

Premises used: Equiv.Perm.mem_support, ne_eq, Equiv.Perm.apply_zpow_apply_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ ∀ x ∈ f.support ∩ g.support,
    Eq (α := α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) g 0 : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
succ : Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (k + 1) : (a : α) → α) x : α) ((g ^ (k + 1) : (a : α) → α) x : α)

Tactic:
rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]

Premises used: pow_succ, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
succ :
  Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧
    Membership.mem (α := α) g.support ((g : (a : α) → α) x : α)
succ₁ : Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧ x ∈ g.support
succ₂ : Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ∧ x ∈ g.support
succ₃ : x ∈ f.support ∧ x ∈ g.support
succ₄ succ₅ succ₆ succ₇ : x ∈ f.support ∩ g.support
⊢ Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)

Tactic:
rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]

Premises used: Equiv.Perm.apply_mem_support, Finset.mem_inter
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
zero :
  ∀ x ∈ f.support ∩ g.support,
    Eq (α := α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) g 0 : (a : α) → α) x : α)
succ :
  ∀ (k : ℕ) (hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)),
    ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ (k + 1) : (a : α) → α) x : α) ((g ^ (k + 1) : (a : α) → α) x : α)
⊢ ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)

Tactic:
induction k with
  | zero => simp
  | succ k hk =>
    intro x hx
    rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]
    rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]

Premises used: pow_succ, Equiv.Perm.apply_mem_support, Equiv.Perm.mul_apply, Finset.mem_inter
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
⊢ f.Disjoint g ↔ _root_.Disjoint f.support g.support

Tactic:
simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff,
    imp_iff_not_or]

Premises used: disjoint_iff, Finset.ext_iff, imp_iff_not_or, Equiv.Perm.disjoint_iff_eq_or_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
disjoint_iff_disjoint_support.1 h

Premises used: Iff.mp, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support

Tactic:
le_antisymm (support_mul_le _ _) fun a => ?_

Premises used: Equiv.Perm.support_mul_le, le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
refine : ∀ a ∈ f.support ∪ g.support, a ∈ (f * g).support
⊢ (f * g).support = f.support ∪ g.support

Tactic:
refine le_antisymm (support_mul_le _ _) fun a => ?_

Premises used: Equiv.Perm.support_mul_le, le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
rw : (f : (a : α) → α) ((g : (a : α) → α) a : α) = a → (f : (a : α) → α) a = a ∧ (g : (a : α) → α) a = a
⊢ a ∈ f.support ∪ g.support → a ∈ (f * g).support

Tactic:
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]

Premises used: Equiv.Perm.mem_support, not_and_or, Finset.mem_union, Equiv.Perm.mul_apply, not_imp_not
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ (f : (a : α) → α) ((g : (a : α) → α) a : α) = a → (f : (a : α) → α) a = a ∧ (g : (a : α) → α) a = a

Tactic:
(h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
      ⟨(congr_arg f hg).symm.trans h, hg⟩

Premises used: congr_arg, And.intro, Iff.mp, Or.elim, Equiv.apply_eq_iff_eq, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ (f : (a : α) → α) ((g : (a : α) → α) a : α) = a → (f : (a : α) → α) a = a ∧ (g : (a : α) → α) a = a

Tactic:
exact
    (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
      ⟨(congr_arg f hg).symm.trans h, hg⟩

Premises used: Or.elim
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : List.Pairwise.{u_1} (α := Perm α) Disjoint []
⊢ Eq.{u_1 + 1} (α := Finset α) (support (List.prod []))
    (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl :
  ∀ (h : List.Pairwise Disjoint tl),
    tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl

Tactic:
rw [List.pairwise_cons] at h

Premises used: List.pairwise_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl :
  ∀ (h : List.Pairwise Disjoint tl),
    tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ hd.Disjoint tl.prod

Tactic:
have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl :
  ∀ (h : List.Pairwise Disjoint tl),
    tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
this : hd.Disjoint tl.prod
⊢ (hd :: tl).prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
simp [this.support_mul, hl h.right]

Premises used: Equiv.Perm.Disjoint.support_mul, And.right
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
nil :
  ∀ (h : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
    Eq.{u_1 + 1} (α := Finset α) (support (List.prod []))
      (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))
cons :
  ∀ (hd : Perm α) (tl : List (Perm α))
    (hl :
      ∀ (h : List.Pairwise Disjoint tl),
        tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl))
    (h : List.Pairwise Disjoint (hd :: tl)),
    (hd :: tl).prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
⊢ l.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support l)

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.pairwise_cons] at h
    have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
    simp [this.support_mul, hl h.right]

Premises used: Finset.cons, List.pairwise_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (noncommProd ∅ k ⋯).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (↑s : Set ι) ⊆ (↑(insert i s) : Set ι)

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

Premises used: Finset.coe_insert, Set.subset_insert
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)

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])
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
insert : (k i * s.noncommProd k ⋯).support = (k i).support ∪ s.biUnion fun (i : ι) ↦ (k i).support
⊢ ((Insert.insert i s).noncommProd k ⋯).support = (Insert.insert i s).biUnion fun (i : ι) ↦ (k i).support

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

Premises used: Finset.biUnion_insert, Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
insert : (k i).Disjoint (s.noncommProd k ⋯)
⊢ (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']

Premises used: Equiv.Perm.Disjoint.support_mul
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
insert : ∀ i_1 ∈ s, (k i).Disjoint (k i_1)
⊢ (k i).Disjoint (s.noncommProd k ⋯)

Tactic:
apply disjoint_noncommProd_right

Premises used: Equiv.Perm.disjoint_noncommProd_right
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
apply : i ∈ (↑(insert i s) : Set ι)
apply₁ : j ∈ (↑(insert i s) : Set ι)
⊢ (k i).Disjoint (k j)

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ (↑(insert i s) : Set ι)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Premises used: true_or, Set.mem_insert_iff, Finset.coe_insert, or_true, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ (↑(insert i s) : Set ι)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Premises used: true_or, Set.mem_insert_iff, Finset.coe_insert, or_true, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (noncommProd ∅ k ⋯).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (hrec :
      ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
        (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support)
    (hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    ((Insert.insert i s).noncommProd k ⋯).support = (Insert.insert i s).biUnion fun (i : ι) ↦ (k i).support
⊢ (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_notMem _ _ _ _ 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]

Premises used: true_or, Equiv.Perm.Disjoint.support_mul, Insert.insert, Finset.biUnion_insert, Set.mem_insert_iff, Finset.coe_insert, or_true, Equiv.Perm.disjoint_noncommProd_right, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (noncommProd ∅ k ⋯).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (hrec :
      ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
        (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support)
    (hs : (↑(Insert.insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    ((Insert.insert i s).noncommProd k ⋯).support = (Insert.insert i s).biUnion fun (i : ι) ↦ (k i).support
⊢ (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_notMem _ _ _ _ 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]

Premises used: true_or, Equiv.Perm.Disjoint.support_mul, Insert.insert, Finset.biUnion_insert, Set.mem_insert_iff, Finset.coe_insert, or_true, Equiv.Perm.disjoint_noncommProd_right, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ LE.le.{u_1} (α := Finset α) (support (List.prod []))
    (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)

Tactic:
(support_mul_le hd tl.prod).trans ?_

Premises used: Equiv.Perm.support_mul_le, LE.le.trans, List.prod
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
cons : hd.support ⊔ tl.prod.support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)

Tactic:
refine (support_mul_le hd tl.prod).trans ?_

Premises used: Equiv.Perm.support_mul_le, LE.le.trans, List.prod
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ hd.support ⊔ tl.prod.support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)

Tactic:
sup_le_sup le_rfl hl

Premises used: sup_le_sup, le_rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ hd.support ⊔ tl.prod.support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)

Tactic:
exact sup_le_sup le_rfl hl

Premises used: sup_le_sup, le_rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
nil :
  LE.le.{u_1} (α := Finset α) (support (List.prod []))
    (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))
cons :
  ∀ (hd : Perm α) (tl : List (Perm α))
    (hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)),
    (hd :: tl).prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
⊢ l.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support l)

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.map_cons, List.foldr_cons]
    refine (support_mul_le hd tl.prod).trans ?_
    exact sup_le_sup le_rfl hl

Premises used: List.foldr_cons, List.map_cons, Finset.cons, List.prod_cons