awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x = x
H : ∀ (x : α), Eq (α := α) ((1 : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ 1 = g

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x = x
x : α
⊢ Eq (α := α) ((1 : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
simp : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x), 1 = g
H : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x) (x : α), Eq (α := α) ((1 : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ List.prod [] = g ∧
    (∀ (g' : Perm α), Membership.mem (γ := List (Perm α)) [] g' → g'.IsCycle) ∧
      List.Pairwise.{u_2} (α := Perm α) Disjoint []

Tactic:
{ simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
        ext
        simp [*]}

Premises used: and_true, Classical.not_not, imp_false, forall_prop_of_false, List.Pairwise.nil, List.prod_nil, forall_const, not_false_iff, List.not_mem_nil
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : (g : (a : α) → α) x = x
y : α
hy : (g : (a : α) → α) y ≠ y
h : y = x
rwa rwa₁ rwa₂ rwa₃ : (g : (a : α) → α) x = x
⊢ (g : (a : α) → α) y = y

Tactic:
rwa [h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : (g : (a : α) → α) x = x
y : α
hy : (g : (a : α) → α) y ≠ y
⊢ y ∈ l

Tactic:
exact List.mem_of_ne_of_mem (fun h => hy (by rwa [h])) (hg hy)

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
rw : ∀ {x_1 : α}, ((g.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ l
⊢ ∀ {x_1 : α}, ((f.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ l

Tactic:
rw [hfg hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
h : y = x
⊢ ¬Eq (α := α) ((g : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy

Premises used: Equiv.Perm.inv_eq_iff_eq, Ne, Equiv.Perm.mul_apply, Equiv.Perm.cycleOf_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
h : y = x
hy₁ : ¬Eq (α := α) ((g : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ y = x

Tactic:
rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy

Premises used: Equiv.Perm.inv_eq_iff_eq, Ne, Equiv.Perm.mul_apply, Equiv.Perm.cycleOf_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬Eq (α := α) ((g : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
h : y = x
⊢ False

Tactic:
hy rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬Eq (α := α) ((g : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
h : y = x
⊢ False

Tactic:
exact hy rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
h : (g : (a : α) → α) y = y
⊢ ¬y = if g.SameCycle x y then (g : (a : α) → α) y else y

Tactic:
rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy

Premises used: Equiv.Perm.inv_eq_iff_eq, Ne, Equiv.Perm.cycleOf_apply, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
h : (g : (a : α) → α) y = y
hy₁ : ¬y = if g.SameCycle x y then (g : (a : α) → α) y else y
⊢ (g : (a : α) → α) y = y

Tactic:
rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy

Premises used: Equiv.Perm.inv_eq_iff_eq, Ne, Equiv.Perm.cycleOf_apply, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬y = if g.SameCycle x y then (g : (a : α) → α) y else y
h : (g : (a : α) → α) y = y
pos : g.SameCycle x y → ∀ (hy : ¬y = (g : (a : α) → α) y), False
neg : ¬g.SameCycle x y → ∀ (hy : ¬y = y), False
⊢ False

Tactic:
split_ifs at hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
h : (g : (a : α) → α) y = y
h_2 : g.SameCycle x y
hy : ¬y = (g : (a : α) → α) y
⊢ False

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
h : (g : (a : α) → α) y = y
h_2 : ¬g.SameCycle x y
hy : ¬y = y
⊢ False

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
⊢ y ∈ l

Tactic:
exact List.mem_of_ne_of_mem
              (fun h : y = x => by
                rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy
                exact hy rfl)
              (hg fun h : g y = y => by
                rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy
                split_ifs at hy <;> tauto)

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
rw : ∀ {x_1 : α}, ((g.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → f.cycleOf x_1 = ((g.cycleOf x)⁻¹ * g).cycleOf x_1
⊢ ∀ {x_1 : α}, ((f.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → f.cycleOf x_1 = ((f.cycleOf x)⁻¹ * g).cycleOf x_1

Tactic:
rw [hfg hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
⊢ ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y

Tactic:
simp [symm_apply_eq, cycleOf_apply, eq_comm (a := g y)] at hy

Premises used: Equiv.symm_apply_eq, eq_comm, Equiv.Perm.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
rw : g.cycleOf y * ((g.cycleOf x)⁻¹ * g)⁻¹.cycleOf y = 1
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y

Tactic:
rw [hfg (Ne.symm hy.right), ← mul_inv_eq_one (a := g.cycleOf y), cycleOf_inv]

Premises used: Equiv.Perm.cycleOf_inv, mul_inv_eq_one, Ne.symm, And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
simp_rw : g.cycleOf y * (g⁻¹ * (g.cycleOf x)⁻¹⁻¹).cycleOf y = 1
⊢ g.cycleOf y * ((g.cycleOf x)⁻¹ * g)⁻¹.cycleOf y = 1

Tactic:
simp_rw [mul_inv_rev]

Premises used: mul_inv_rev
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
h₁ : Commute g⁻¹ (g.cycleOf x)
hx₁ : (g.cycleOf x : (a : α) → α) y = y
⊢ g.cycleOf y * (g⁻¹ * (g.cycleOf x)⁻¹⁻¹).cycleOf y = 1

Tactic:
rw [inv_inv, cycleOf_mul_of_apply_right_eq_self, ← cycleOf_inv, mul_inv_eq_one]

Premises used: Equiv.Perm.cycleOf_inv, mul_inv_eq_one, inv_inv, Equiv.Perm.cycleOf_mul_of_apply_right_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
h₁ : g * g.cycleOf x = g.cycleOf x * g
⊢ Commute g⁻¹ (g.cycleOf x)

Tactic:
rw [Commute.inv_left_iff, commute_iff_eq]

Premises used: Commute.inv_left_iff, commute_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
h₁ : ∀ (z : α), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
⊢ g * g.cycleOf x = g.cycleOf x * g

Tactic:
ext z
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
z : α
pos :
  ∀ (hz : g.SameCycle x z), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
neg :
  ∀ (hz : ¬g.SameCycle x z), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
⊢ Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)

Tactic:
by_cases hz : SameCycle g x z

Premises used: Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
z : α
hz : g.SameCycle x z
⊢ Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)

Tactic:
simp [cycleOf_apply, hz]

Premises used: Equiv.Perm.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
z : α
hz : ¬g.SameCycle x z
⊢ Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)

Tactic:
simp [cycleOf_apply_of_not_sameCycle, hz]

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ (g.cycleOf x : (a : α) → α) y = y

Tactic:
cycleOf_apply_of_not_sameCycle hy.left

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ (g.cycleOf x : (a : α) → α) y = y

Tactic:
exact cycleOf_apply_of_not_sameCycle hy.left

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm : m.prod = (f.cycleOf x)⁻¹ * g ∧ (∀ g' ∈ m, g'.IsCycle) ∧ List.Pairwise Disjoint m
⊢ m.prod = (f.cycleOf x)⁻¹ * g

Tactic:
obtain ⟨hm₁, hm₂, hm₃⟩ := hm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm : m.prod = (f.cycleOf x)⁻¹ * g ∧ (∀ g' ∈ m, g'.IsCycle) ∧ List.Pairwise Disjoint m
hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
⊢ ∀ g' ∈ m, g'.IsCycle

Tactic:
obtain ⟨hm₁, hm₂, hm₃⟩ := hm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm : m.prod = (f.cycleOf x)⁻¹ * g ∧ (∀ g' ∈ m, g'.IsCycle) ∧ List.Pairwise Disjoint m
hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
⊢ List.Pairwise Disjoint m

Tactic:
obtain ⟨hm₁, hm₂, hm₃⟩ := hm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
rw :
  ∀ (hm₁ : m.prod = (g.cycleOf x)⁻¹ * g) (hm₂ : ∀ g' ∈ m, g'.IsCycle) (hm₃ : List.Pairwise Disjoint m),
    (g.cycleOf x :: m).prod = g ∧ (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (g.cycleOf x :: m)
⊢ (f.cycleOf x :: m).prod = g ∧ (∀ g' ∈ f.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (f.cycleOf x :: m)

Tactic:
rw [hfg hx] at hm₁ ⊢
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
rw :
  (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧ (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (g.cycleOf x :: m)

Tactic:
rw [List.pairwise_cons]

Premises used: List.pairwise_cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m

Tactic:
⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
refine_1 : (g.cycleOf x :: m).prod = g
refine_2 : ∀ (g' : Perm α) (hg' : g' ∈ g.cycleOf x :: m), g'.IsCycle
refine_3 : ∀ (g' : Perm α) (hg' : g' ∈ m) (y : α), (g.cycleOf x : (a : α) → α) y = y ∨ (g' : (a : α) → α) y = y
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m

Tactic:
refine ⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g

Tactic:
simp [List.prod_cons, hm₁]

Premises used: List.prod_cons