awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
a : ↥f.cycleFactorsFinset
h_1 : a ∈ (↑univ : Set ↥f.cycleFactorsFinset)
b : ↥f.cycleFactorsFinset
h_2 : b ∈ (↑univ : Set ↥f.cycleFactorsFinset)
h : a ≠ b
⊢ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑b : Perm α))
    ((fun (i : ↥f.cycleFactorsFinset) ↦
        (((fun (i : ↥f.cycleFactorsFinset) ↦
                  (Subgroup.subtype
                      ((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) :
                    ↥((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) →*
                      Perm α))
                i :
              (a :
                  (fun (i : ↥f.cycleFactorsFinset) ↦
                      ↥((fun (i : ↥f.cycleFactorsFinset) ↦ Subgroup.zpowers (↑i : Perm α)) i))
                    i) →
                Perm α)
            (v i) :
          Perm α))
      b)

Tactic:
simp only [Subgroup.coe_subtype, SetLike.coe_mem]

Premises used: SetLike.coe_mem, Subgroup.coe_subtype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
x y : Perm α
⊢ Disjoint
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
        u)
      x →
    Disjoint
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
          u)
        y →
      Disjoint
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
          u)
        (x * y)

Tactic:
Disjoint.mul_right

Premises used: Equiv.Perm.Disjoint.mul_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
x y : Perm α
⊢ Disjoint
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
        u)
      x →
    Disjoint
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
          u)
        y →
      Disjoint
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
          u)
        (x * y)

Tactic:
exact Disjoint.mul_right

Premises used: Equiv.Perm.Disjoint.mul_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
⊢ Disjoint.{u_2} (α := α)
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    1

Tactic:
disjoint_one_right _

Premises used: Equiv.Perm.disjoint_one_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
⊢ Disjoint.{u_2} (α := α)
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    1

Tactic:
exact disjoint_one_right _

Premises used: Equiv.Perm.disjoint_one_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
c : ↥f.cycleFactorsFinset
base :
  Membership.mem (γ := Finset ↥f.cycleFactorsFinset) univ c →
    Disjoint.{u_2} (α := α)
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
        u)
      (((fun (i : ↥f.cycleFactorsFinset) ↦
              (Subgroup.subtype
                  ((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) :
                ↥((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) →*
                  Perm α))
            c :
          (a :
              (fun (i : ↥f.cycleFactorsFinset) ↦
                  ↥((fun (i : ↥f.cycleFactorsFinset) ↦ Subgroup.zpowers (↑i : Perm α)) i))
                c) →
            Perm α)
        (v c))
⊢ Membership.mem (γ := Finset ↥f.cycleFactorsFinset) univ c →
    Disjoint.{u_2} (α := α)
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
        u)
      (((fun (i : ↥f.cycleFactorsFinset) ↦
              (Subgroup.subtype
                  ((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) :
                ↥((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) →*
                  Perm α))
            c :
          (a :
              (fun (i : ↥f.cycleFactorsFinset) ↦
                  ↥((fun (i : ↥f.cycleFactorsFinset) ↦ Subgroup.zpowers (↑i : Perm α)) i))
                c) →
            Perm α)
        (v c))

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
c : ↥f.cycleFactorsFinset
h : Membership.mem (γ := Finset ↥f.cycleFactorsFinset) univ c
base :
  Disjoint
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    (↑(v c) : Perm α)
⊢ Disjoint.{u_2} (α := α)
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    (((fun (i : ↥f.cycleFactorsFinset) ↦
            (Subgroup.subtype
                ((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) :
              ↥((fun (i : ↥f.cycleFactorsFinset) ↦ (Subgroup.zpowers (↑i : Perm α) : Subgroup (Perm α))) i) →* Perm α))
          c :
        (a :
            (fun (i : ↥f.cycleFactorsFinset) ↦ ↥((fun (i : ↥f.cycleFactorsFinset) ↦ Subgroup.zpowers (↑i : Perm α)) i))
              c) →
          Perm α)
      (v c))

Tactic:
simp only [Subgroup.coe_subtype]

Premises used: Subgroup.coe_subtype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
c : ↥f.cycleFactorsFinset
h : Membership.mem (γ := Finset ↥f.cycleFactorsFinset) univ c
⊢ Disjoint
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    (↑(v c) : Perm α)

Tactic:
Disjoint.mono (disjoint_ofSubtype_of_memFixedPoints_self u)
      le_rfl (support_zpowers_of_mem_cycleFactorsFinset_le (v c))

Premises used: le_rfl, Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, Equiv.Perm.Disjoint.mono
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
c : ↥f.cycleFactorsFinset
h : Membership.mem (γ := Finset ↥f.cycleFactorsFinset) univ c
⊢ Disjoint
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
        (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
      u)
    (↑(v c) : Perm α)

Tactic:
exact Disjoint.mono (disjoint_ofSubtype_of_memFixedPoints_self u)
      le_rfl (support_zpowers_of_mem_cycleFactorsFinset_le (v c))

Premises used: le_rfl, Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, Equiv.Perm.Disjoint.mono
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
u : Perm (↑(fixedPoints (⇑f : (a : α) → α)) : Type u_2)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
⊢ Commute (S := Perm α)
    ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑f : (a : α) → α) }) → Perm α)
        u :
      Perm α)
    ((Subgroup.noncommPiCoprod ⋯ : (a : (i : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑i : Perm α))) → Perm α) v :
      Perm α)

Tactic:
Disjoint.commute (f.disjoint_ofSubtype_noncommPiCoprod u v)

Premises used: Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, Equiv.Perm.Disjoint.commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
mp : x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
mpr : (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support
⊢ x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
h : x ∈ g.support
right : x ∈ (g.cycleOf x).support
⊢ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h

Premises used: Iff.mpr, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
h : x ∈ g.support
right : g.SameCycle x x ∧ x ∈ g.support
⊢ x ∈ (g.cycleOf x).support

Tactic:
rw [mem_support_cycleOf_iff]

Premises used: Equiv.Perm.mem_support_cycleOf_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ g.SameCycle x x ∧ x ∈ g.support

Tactic:
⟨SameCycle.refl g x, h⟩

Premises used: Equiv.Perm.SameCycle.refl, And.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ g.SameCycle x x ∧ x ∈ g.support

Tactic:
exact ⟨SameCycle.refl g x, h⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
hx : x ∈ c.support
⊢ x ∈ g.support

Tactic:
mem_cycleFactorsFinset_support_le hc hx

Premises used: Equiv.Perm.mem_cycleFactorsFinset_support_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
hx : x ∈ c.support
⊢ x ∈ g.support

Tactic:
exact mem_cycleFactorsFinset_support_le hc hx

Premises used: Equiv.Perm.mem_cycleFactorsFinset_support_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ f.cycleFactorsFinset = ∅ ↔ f = 1

Tactic:
simpa [cycleFactorsFinset_eq_finset] using eq_comm

Premises used: Equiv.Perm.cycleFactorsFinset_eq_finset, eq_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset (Perm α)) (cycleFactorsFinset 1) ∅

Tactic:
simp [cycleFactorsFinset_eq_empty_iff]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_empty_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ f.cycleFactorsFinset = {f} ↔ f.IsCycle

Tactic:
simp [cycleFactorsFinset_eq_finset]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_finset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
⊢ f.cycleFactorsFinset = {f}

Tactic:
cycleFactorsFinset_eq_singleton_self_iff.mpr hf

Premises used: Iff.mpr, Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
rw :
  ((∀ (f : Perm α), Membership.mem (γ := Finset (Perm α)) {g} f → f.IsCycle) ∧
      ∃ (h : (↑{g} : Set (Perm α)).Pairwise Disjoint), noncommProd {g} id ⋯ = f) ↔
    f.IsCycle ∧ f = g
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
rw [cycleFactorsFinset_eq_finset]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_finset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ ((∀ (f : Perm α), Membership.mem (γ := Finset (Perm α)) {g} f → f.IsCycle) ∧
      ∃ (h : (↑{g} : Set (Perm α)).Pairwise Disjoint), noncommProd {g} id ⋯ = f) ↔
    f.IsCycle ∧ f = g

Tactic:
simpa [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
suffices : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
suffices f = g → (g.IsCycle ↔ f.IsCycle) by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ f.IsCycle ↔ f.IsCycle

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ f.IsCycle ↔ f.IsCycle

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
rw : f.cycleFactorsFinset.noncommProd id ⋯ = g
⊢ f = g

Tactic:
rw [← cycleFactorsFinset_noncommProd f]

Premises used: Equiv.Perm.cycleFactorsFinset_noncommProd, Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f.cycleFactorsFinset.noncommProd id ⋯ = g

Tactic:
simpa [h] using cycleFactorsFinset_noncommProd g

Premises used: Equiv.Perm.cycleFactorsFinset_noncommProd, Equiv.Perm.cycleFactorsFinset_mem_commute
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
rw [disjoint_iff_disjoint_support] at h

Premises used: Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
rw : ∀ ⦃a : Perm α⦄, a ∈ f.cycleFactorsFinset → a ∉ g.cycleFactorsFinset
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
rw [Finset.disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x ∈ f.cycleFactorsFinset
hy : x ∈ g.cycleFactorsFinset
⊢ x.IsCycle ∧ ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)

Tactic:
simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy

Premises used: Equiv.Perm.mem_support, Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x ∈ f.cycleFactorsFinset
hy : x ∈ g.cycleFactorsFinset
hx₁ : x.IsCycle ∧ ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
⊢ x.IsCycle ∧ ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy

Premises used: Equiv.Perm.mem_support, Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x.IsCycle ∧ ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
hy : x.IsCycle ∧ ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
obtain :
  ∀ (hf : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)) (a : α)
    (ha : (x : (a : α) → α) a ≠ a)
    (hg : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((g : (a : α) → α) a : α)), False
⊢ False

Tactic:
obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
a : α
ha : (x : (a : α) → α) a ≠ a
hg : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ a ∈ f.support ∩ g.support

Tactic:
simp [ha, ← hf a ha, ← hg a ha]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
a : α
ha : (x : (a : α) → α) a ≠ a
hg : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ Membership.mem (γ := Finset α) ⊥ a

Tactic:
have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((f : (a : α) → α) a : α)
a : α
ha : (x : (a : α) → α) a ≠ a
hg : ∀ (a : α), (x : (a : α) → α) a ≠ a → Eq (α := α) ((x : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
this : Membership.mem (γ := Finset α) ⊥ a
⊢ False

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
rw :
  (∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle) ∧
    ∃ (h : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint),
      (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g
⊢ (f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset

Tactic:
rw [cycleFactorsFinset_eq_finset]

Premises used: Equiv.Perm.cycleFactorsFinset_eq_finset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle) ∧
    ∃ (h : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint),
      (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
refine_1 : ∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle
refine_2 : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint
refine_3 : (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g
⊢ (∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle) ∧
    ∃ (h : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint),
      (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ ∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle

Tactic:
simp [or_imp, mem_cycleFactorsFinset_iff, forall_comm]

Premises used: forall_comm, or_imp, Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
refine_2 :
  (↑f.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint ∧
    (↑g.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint ∧
      ∀ a ∈ (↑f.cycleFactorsFinset : Set (Perm α)), ∀ b ∈ (↑g.cycleFactorsFinset : Set (Perm α)), a ≠ b → a.Disjoint b
⊢ (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint

Tactic:
rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]

Premises used: Equiv.Perm.Disjoint.symmetric, Set.pairwise_union_of_symmetric, Finset.coe_union
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑f.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint ∧
    (↑g.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint ∧
      ∀ a ∈ (↑f.cycleFactorsFinset : Set (Perm α)), ∀ b ∈ (↑g.cycleFactorsFinset : Set (Perm α)), a ≠ b → a.Disjoint b

Tactic:
⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
        fun x hx y hy _ =>
        h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩

Premises used: Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, And.intro, Equiv.Perm.Disjoint.mono, Equiv.Perm.mem_cycleFactorsFinset_support_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑f.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint ∧
    (↑g.cycleFactorsFinset : Set (Perm α)).Pairwise Disjoint ∧
      ∀ a ∈ (↑f.cycleFactorsFinset : Set (Perm α)), ∀ b ∈ (↑g.cycleFactorsFinset : Set (Perm α)), a ≠ b → a.Disjoint b

Tactic:
exact
      ⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
        fun x hx y hy _ =>
        h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
refine_3 : f.cycleFactorsFinset.noncommProd id ⋯ * g.cycleFactorsFinset.noncommProd id ⋯ = f * g
⊢ (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g

Tactic:
rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]

Premises used: Finset.noncommProd_union_of_disjoint, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset