awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
this : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
x : { l : List (Perm β) // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l } := σ.truncCycleFactors.out
⊢ P σ

Tactic:
exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)

Premises used: Eq.mp, congr_arg, And.right, And.left, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
this : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
let let₁ let₂ : P σ
⊢ P σ

Tactic:
classical
      let x := σ.truncCycleFactors.out
      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
intro : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ P σ

Tactic:
suffices ∀ l : List (Perm β),
      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
    classical
      let x := σ.truncCycleFactors.out
      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
⊢ (∀ (τ : Perm β), Membership.mem (γ := List (Perm β)) [] τ → τ.IsCycle) →
    List.Pairwise.{u_3} (α := Perm β) Disjoint [] → P (List.prod [])

Tactic:
fun _ _ => base_one

Premises used: List.foldr, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
⊢ (∀ (τ : Perm β), Membership.mem (γ := List (Perm β)) [] τ → τ.IsCycle) →
    List.Pairwise.{u_3} (α := Perm β) Disjoint [] → P (List.prod [])

Tactic:
exact fun _ _ => base_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ_1 : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
intro : P (σ * l.prod)
⊢ P (σ :: l).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ_1 : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ * l.prod)

Tactic:
induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)

Premises used: List.mem_cons_of_mem, Equiv.Perm.disjoint_prod_right, List.pairwise_cons, And.left, Iff.mp, List.mem_cons_self, List.Pairwise.of_cons, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ_1 : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ * l.prod)

Tactic:
exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)

Premises used: List.mem_cons_of_mem, Equiv.Perm.disjoint_prod_right, List.pairwise_cons, And.left, Iff.mp, List.mem_cons_self, List.Pairwise.of_cons, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
l : List (Perm β)
intro :
  (∀ (τ : Perm β), Membership.mem (γ := List (Perm β)) [] τ → τ.IsCycle) →
    List.Pairwise.{u_3} (α := Perm β) Disjoint [] → P (List.prod [])
intro₁ :
  ∀ (σ : Perm β) (l : List (Perm β)) (ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod),
    (∀ τ ∈ σ :: l, τ.IsCycle) → List.Pairwise Disjoint (σ :: l) → P (σ :: l).prod
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Tactic:
induction l with
  | nil => exact fun _ _ => base_one
  | cons σ l ih =>
    intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)

Premises used: Finset.cons, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f ∈ g.cycleFactorsFinset
revert : ∀ {f : Perm α} (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
⊢ (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}

Tactic:
revert f
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f : Perm α
⊢ ∀ (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}

Tactic:
cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ ?_ ?_ ?_

Premises used: Equiv.Perm.cycle_induction_on
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_1 :
  ∀ {f : Perm α},
    (fun {g : Perm α} ↦
        ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
      (g := 1)
refine_2 :
  ∀ {f : Perm α} (σ : Perm α),
    σ.IsCycle →
      (fun {g : Perm α} ↦
          ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
        (g := σ)
refine_3 :
  ∀ {f : Perm α} (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (fun {g : Perm α} ↦
              ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
            (g := σ) →
          (fun {g : Perm α} ↦
                ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
              (g := τ) →
            (fun {g : Perm α} ↦
                ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
              (g := σ * τ)
⊢ ∀ {f : Perm α} (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}

Tactic:
refine
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ ?_ ?_ ?_

Premises used: Equiv.Perm.cycle_induction_on
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f : Perm α
⊢ (fun {g : Perm α} ↦
      ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
    (g := 1)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ : Perm α
hσ : σ.IsCycle
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
refine_2 : ∀ (hf : f = σ), (σ * f⁻¹).cycleFactorsFinset = {σ} \ {f}
⊢ (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}

Tactic:
simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢

Premises used: Iff.mpr, Finset.mem_singleton, Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ : Perm α
hσ : σ.IsCycle
f : Perm α
hf : f = σ
⊢ (σ * f⁻¹).cycleFactorsFinset = {σ} \ {f}

Tactic:
simp [hf]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f σ τ : Perm α
hd : σ.Disjoint τ
refine_3 :
  σ.IsCycle →
    (fun {g : Perm α} ↦
          ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
        (g := σ) →
      (fun {g : Perm α} ↦
            ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
          (g := τ) →
        (fun {g : Perm α} ↦
            ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
          (g := σ * τ)
⊢ σ.IsCycle →
    (fun {g : Perm α} ↦
          ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
        (g := σ) →
      (fun {g : Perm α} ↦
            ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
          (g := τ) →
        (fun {g : Perm α} ↦
            ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
          (g := σ * τ)

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
refine_3 :
  f ∈ σ.cycleFactorsFinset ∨ f ∈ τ.cycleFactorsFinset →
    (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
⊢ f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}

Tactic:
simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]

Premises used: Finset.mem_union, Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
refine_3 : τ.Disjoint (σ * f⁻¹)
refine_3₁ : f ∉ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}

Tactic:
rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_notMem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]

Premises used: Finset.sdiff_singleton_eq_erase, Equiv.Perm.Disjoint.commute, Finset.union_comm, mul_assoc, Finset.union_sdiff_distrib, Finset.erase_eq_of_notMem, Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)

Tactic:
rw [mem_cycleFactorsFinset_iff] at hf

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
refine_3 : ∀ (hx : (τ : (a : α) → α) x = x), (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
refine_3₁ : ∀ (hx : (σ : (a : α) → α) x = x), (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
rcases hd.symm x with hx | hx

Premises used: Equiv.Perm.Disjoint.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
exact Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
refine_3 : (σ * f⁻¹ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
pos : ∀ (hfx : (f : (a : α) → α) x = x), (σ * f⁻¹ : (a : α) → α) x = x
neg : ∀ (hfx : ¬(f : (a : α) → α) x = x), (σ * f⁻¹ : (a : α) → α) x = x
⊢ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
by_cases hfx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : (f : (a : α) → α) x = x
pos : Eq (α := α) ((σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
rw [← hfx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : (f : (a : α) → α) x = x
⊢ Eq (α := α) ((σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)

Tactic:
simpa [hx] using hfx.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
neg : (σ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
⊢ (σ * f⁻¹ : (a : α) → α) x = x

Tactic:
rw [mul_apply]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (f : (a : α) → α) x = x

Tactic:
rw [← hf.right _ (mem_support.mpr hfx)] at hx

Premises used: Iff.mpr, Equiv.Perm.mem_support, And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
hx₁ : (f : (a : α) → α) x = x
⊢ ¬(f : (a : α) → α) x = x

Tactic:
rw [← hf.right _ (mem_support.mpr hfx)] at hx

Premises used: Iff.mpr, Equiv.Perm.mem_support, And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (f : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (σ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset

Tactic:
fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))

Premises used: Disjoint.le_bot, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, Finset.notMem_empty, Finset.mem_inter_of_mem, Not
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset

Tactic:
exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))

Premises used: Disjoint.le_bot, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, Finset.notMem_empty, Finset.mem_inter_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
refine_3 : σ.Disjoint (τ * f⁻¹)
refine_3₁ : f ∉ σ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}

Tactic:
rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_notMem, mul_assoc,
        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]

Premises used: Finset.sdiff_singleton_eq_erase, mul_assoc, Finset.union_sdiff_distrib, Finset.erase_eq_of_notMem, Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)

Tactic:
rw [mem_cycleFactorsFinset_iff] at hf

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff