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_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' : Perm α
hg' : g' ∈ g.cycleOf x :: m
⊢ g'.IsCycle

Tactic:
((List.mem_cons).1 hg').elim (fun hg' => hg'.symm ▸ isCycle_cycleOf _ hx) (hm₂ g')

Premises used: Equiv.Perm.isCycle_cycleOf, Eq.rec, Iff.mp, List.mem_cons, Or.elim, Eq.symm
-- 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' : Perm α
hg' : g' ∈ g.cycleOf x :: m
⊢ g'.IsCycle

Tactic:
exact ((List.mem_cons).1 hg').elim (fun hg' => hg'.symm ▸ isCycle_cycleOf _ hx) (hm₂ g')

Premises used: Iff.mp, List.mem_cons, Or.elim
-- 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' : Perm α
hg' : g' ∈ m
y : α
refine_3 : ∀ (hgy : (g.cycleOf x : (a : α) → α) y ≠ y) (hg'y : (g' : (a : α) → α) y ≠ y), False
⊢ (g.cycleOf x : (a : α) → α) y = y ∨ (g' : (a : α) → α) y = y

Tactic:
by_contra! ⟨hgy, hg'y⟩
-- 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' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
⊢ g.SameCycle x y

Tactic:
have hxy : SameCycle g x y := not_imp_comm.1 cycleOf_apply_of_not_sameCycle hgy
-- 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' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
⊢ g' :: m.erase g' ~ m

Tactic:
have hg'm : g' :: m.erase g' ~ m := List.cons_perm_iff_perm_erase.2 ⟨hg', .refl _⟩
-- 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' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
⊢ ∀ h ∈ m.erase g', g'.Disjoint h

Tactic:
have : ∀ h ∈ m.erase g', Disjoint g' h :=
          (List.pairwise_cons.1 ((hg'm.pairwise_iff Disjoint.symm).2 hm₃)).1
-- 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' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ False

Tactic:
hg'y <| (disjoint_prod_right _ this y).resolve_right ?_

Premises used: Equiv.Perm.disjoint_prod_right, Or.resolve_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
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
refine_3 : ¬((m.erase g').prod : (a : α) → α) y = y
⊢ False

Tactic:
refine hg'y <| (disjoint_prod_right _ this y).resolve_right ?_

Premises used: Equiv.Perm.disjoint_prod_right, Or.resolve_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
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
rwa : g.SameCycle x ((g : (a : α) → α) y)
rwa₁ rwa₂ rwa₃ rwa₄ : g.SameCycle x y
⊢ g⁻¹.SameCycle x ((g : (a : α) → α) y)

Tactic:
rwa [sameCycle_inv, sameCycle_apply_right]

Premises used: Equiv.Perm.sameCycle_apply_right, Equiv.Perm.sameCycle_inv
-- 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' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ g⁻¹.SameCycle x ((g : (a : α) → α) y)

Tactic:
have hsc : SameCycle g⁻¹ x (g y) := by rwa [sameCycle_inv, sameCycle_apply_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
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x ((g : (a : α) → α) y)
refine_3 :
  ∀ (hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)) (hg' : g' ∈ m) (y : α)
    (hgy : (g.cycleOf x : (a : α) → α) y ≠ y) (hg'y : (g' : (a : α) → α) y ≠ y) (hxy : g.SameCycle x y)
    (hg'm : g' :: m.erase g' ~ m) (this : ∀ h ∈ m.erase g', g'.Disjoint h)
    (hsc : g⁻¹.SameCycle x ((g : (a : α) → α) y)), ¬((m.erase g').prod : (a : α) → α) y = y
⊢ ¬((m.erase g').prod : (a : α) → α) y = y

Tactic:
rw [disjoint_prod_perm hm₃ hg'm.symm, List.prod_cons, ← eq_inv_mul_iff_mul_eq] at hm₁

Premises used: eq_inv_mul_iff_mul_eq, Equiv.Perm.disjoint_prod_perm, List.Perm.symm, List.prod_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₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x ((g : (a : α) → α) y)
⊢ ¬((m.erase g').prod : (a : α) → α) y = y

Tactic:
simpa [hm₁, cycleOf_inv, hsc.cycleOf_apply, eq_symm_apply, eq_comm] using hg'y

Premises used: Equiv.Perm.cycleOf_inv, eq_comm, Equiv.Perm.SameCycle.cycleOf_apply, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
this :
  σ.IsCycle →
    (σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α))
⊢ σ ∈ l ↔
    σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
this :
  σ.IsCycle →
    (σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α))
⊢ σ ∈ l ↔
    σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
suffices :
  σ.IsCycle →
    (σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α))
⊢ σ ∈ l ↔
    σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
suffices σ.IsCycle → (σ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
intro :
  ∀ (val : Fintype α),
    σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
intro :
  σ ∈ l → ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
intro₁ :
  (∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)) → σ ∈ l
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : σ ∈ l
a : α
ha : (σ : (a : α) → α) a ≠ a
⊢ Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)

Premises used: Iff.mpr, Equiv.Perm.eq_on_support_mem_disjoint, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : σ ∈ l
a : α
ha : (σ : (a : α) → α) a ≠ a
⊢ Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)

Tactic:
exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)

Premises used: Iff.mpr, Equiv.Perm.eq_on_support_mem_disjoint, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
x : α
hx : x ∈ σ.support
⊢ (σ : (a : α) → α) x ≠ x

Tactic:
rw [mem_support] at hx

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x ≠ x
rwa : (l.prod : (a : α) → α) x ≠ x
rwa₁ rwa₂ rwa₃ rwa₄ : (σ : (a : α) → α) x ≠ x
⊢ x ∈ l.prod.support

Tactic:
rwa [mem_support, ← h _ hx]

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
⊢ σ.support ⊆ l.prod.support

Tactic:
have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
intro : ∀ (a : α) (ha : (σ : (a : α) → α) a ≠ a), σ ∈ l
⊢ σ ∈ l

Tactic:
obtain ⟨a, ha, -⟩ := id h3

Premises used: id
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : (σ : (a : α) → α) a ≠ a
⊢ a ∈ σ.support

Tactic:
rw [← mem_support] at ha

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
intro : ∀ (τ : Perm α) (hτ : τ ∈ l) (hτa : a ∈ τ.support), σ ∈ l
⊢ σ ∈ l

Tactic:
obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)

Premises used: Equiv.Perm.exists_mem_support_of_mem_support_prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
⊢ ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)

Tactic:
have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
x : α
hx : x ∈ σ.support ∩ τ.support
rw : Eq (α := α) ((l.prod : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
rw₁ rw₂ : Eq (α := α) ((l.prod : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
⊢ Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)

Tactic:
rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]

Premises used: Finset.mem_of_mem_inter_left, Equiv.Perm.mem_support, Finset.mem_of_mem_inter_right, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
⊢ ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)

Tactic:
have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ τ ∈ l

Tactic:
hτ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
h₁ : σ = τ
⊢ σ ∈ l

Tactic:
convert! hτ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ σ = τ

Tactic:
h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha

Premises used: Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
h₁ : Eq (α := α) ((σ : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
⊢ σ = τ

Tactic:
refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha

Premises used: Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ Eq (α := α) ((σ : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)

Tactic:
key a (mem_inter_of_mem ha hτa)

Premises used: Finset.mem_inter_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ Eq (α := α) ((σ : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)

Tactic:
exact key a (mem_inter_of_mem ha hτa)

Premises used: Finset.mem_inter_of_mem