awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
comm :
  Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers (↑a : 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 α))
      a)
⊢ onFun (β := Perm α) Commute
    (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))
    a b
have comm₁ : 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: apply f.pairwise_commute_of_mem_zpowers h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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.{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))
have 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 α)
Tactic: simp only [Subgroup.coe_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
have mp : x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
mp : x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
⊢ x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
have mpr : (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
have right : x ∈ (g.cycleOf x).support
Tactic: use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ x ∈ (g.cycleOf x).support
have right : g.SameCycle x x ∧ x ∈ g.support
Tactic: rw [mem_support_cycleOf_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g
have rw : ((∀ (f : Perm α), Membership.mem (γ := Finset (Perm α)) {g} f → f.IsCycle) ∧
    ∃ (h : (↑{g} : Set (Perm α)).Pairwise Disjoint), noncommProd {g} id sorry = f) ↔
  f.IsCycle ∧ f = g
Tactic: rw [cycleFactorsFinset_eq_finset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g
have suffices : f = g → (g.IsCycle ↔ f.IsCycle)
Tactic: suffices f = g → (g.IsCycle ↔ f.IsCycle) by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f = g
have rw : f.cycleFactorsFinset.noncommProd id sorry = g
Tactic: rw [← cycleFactorsFinset_noncommProd f]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
have h₁ : _root_.Disjoint f.support g.support
Tactic: rw [disjoint_iff_disjoint_support] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
have rw : ∀ ⦃a : Perm α⦄, a ∈ f.cycleFactorsFinset → a ∉ g.cycleFactorsFinset
Tactic: rw [Finset.disjoint_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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
⊢ False
have hx₁ : 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
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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 : α)
⊢ False
have hy₁ : 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
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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 : α)
⊢ False
have 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
Tactic: obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
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 : α)
⊢ False
have this : Membership.mem (γ := Finset α) ⊥ a
Tactic: have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset
have 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 sorry = f * g
Tactic: rw [cycleFactorsFinset_eq_finset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
have refine_1 : ∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ (∀ 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
have refine_2 : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
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
⊢ (∀ 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
have refine_3 : (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id sorry = f * g
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset) : Set (Perm α)).Pairwise Disjoint
have 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
Tactic: rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g
have refine_3 : f.cycleFactorsFinset.noncommProd id sorry * g.cycleFactorsFinset.noncommProd id sorry = f * g
Tactic: rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ f.cycleFactorsFinset.noncommProd id ⋯ * g.cycleFactorsFinset.noncommProd id ⋯ = f * g
have refine_3 : f * g.cycleFactorsFinset.noncommProd id sorry = f * g
Tactic: rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
refine_3 : f * g.cycleFactorsFinset.noncommProd id ⋯ = f * g
⊢ f.cycleFactorsFinset.noncommProd id ⋯ * g.cycleFactorsFinset.noncommProd id ⋯ = f * g
have refine_3₁ : f * g = f * g
Tactic: rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹).Disjoint f
have h₁ : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: rw [mem_cycleFactorsFinset_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
have pos : ∀ (hx : (f : (a : α) → α) x = x), (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
pos : ∀ (hx : (f : (a : α) → α) x = x), (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x), (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x ∨ (f : (a : α) → α) x = x
have neg : (g * f⁻¹ : (a : α) → α) x = x
Tactic: left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ (g * f⁻¹ : (a : α) → α) x = x
have neg : (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
Tactic: rw [mul_apply, ← h.right _ (by simpa [eq_symm_apply])]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = f.cycleOf a
have rw : c = c.cycleOf a
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = c.cycleOf a
have a₁ : c.cycleOf a = c
Tactic: apply symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
⊢ c = f.cycleOf a
have suffices : f.cycleOf a = c.cycleOf a
Tactic: suffices f.cycleOf a = c.cycleOf a by
    rw [this]
    apply symm
    exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := ⋯
hfc2 : Commute c (f * c⁻¹) := ⋯
⊢ f.cycleOf a = c.cycleOf a
have rw : f.cycleOf a = (c * (f * c⁻¹)).cycleOf a
Tactic: rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := ⋯
hfc2 : Commute c (f * c⁻¹) := ⋯
rw : f.cycleOf a = (c * (f * c⁻¹)).cycleOf a
⊢ f.cycleOf a = c.cycleOf a
have hx : (f * c⁻¹ : (a : α) → α) a = a
Tactic: rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.IsCycleOn (↑c.support : Set α)
have obtain : ∀ (x : α) (hx : x ∈ c.support), g.IsCycleOn (↑c.support : Set α)
Tactic: obtain ⟨x, hx⟩ := IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp hc).1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn (↑c.support : Set α)
have rw : g.IsCycleOn (↑(g.cycleOf x).support : Set α)
Tactic: rw [cycle_is_cycleOf hx hc]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
⊢ c = g.cycleOf x ↔ x ∈ c.support
have refine : c = g.cycleOf x → x ∈ c.support
Tactic: refine ⟨?_, (cycle_is_cycleOf · hc)⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (g.cycleOf x).support
have rw : ¬g.cycleOf x = 1
Tactic: rw [mem_support, cycleOf_apply_self, ne_eq, ← cycleOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
⊢ Membership.mem (α := α) (↑c : Perm α).support ((g ^ m : (a : α) → α) x : α) ↔ x ∈ (↑c : Perm α).support
have rw : (↑c : Perm α) = g.cycleOf ((g ^ m : (a : α) → α) x) ↔ x ∈ (↑c : Perm α).support
Tactic: rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
    eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
rw : (↑c : Perm α) = g.cycleOf ((g ^ m : (a : α) → α) x) ↔ x ∈ (↑c : Perm α).support
⊢ Membership.mem (α := α) (↑c : Perm α).support ((g ^ m : (a : α) → α) x : α) ↔ x ∈ (↑c : Perm α).support
have rw₁ : (↑c : Perm α) = g.cycleOf x ↔ x ∈ (↑c : Perm α).support
Tactic: rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
    eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
rw : (↑c : Perm α) = g.cycleOf ((g ^ m : (a : α) → α) x) ↔ x ∈ (↑c : Perm α).support
rw₁ : (↑c : Perm α) = g.cycleOf x ↔ x ∈ (↑c : Perm α).support
⊢ Membership.mem (α := α) (↑c : Perm α).support ((g ^ m : (a : α) → α) x : α) ↔ x ∈ (↑c : Perm α).support
have rw₂ : x ∈ (↑c : Perm α).support ↔ x ∈ (↑c : Perm α).support
Tactic: rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
    eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset
have refine : ∀ (h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset), c ∈ g.cycleFactorsFinset
Tactic: refine ⟨fun h ↦ ?_, imp_lemma⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ c ∈ g.cycleFactorsFinset
have aux : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
Tactic: have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
aux : ∀ (h : Perm α), h = k⁻¹ * (k * h * k⁻¹) * k
⊢ c ∈ g.cycleFactorsFinset
have rw : k⁻¹ * (k * c * k⁻¹) * k ∈ (k⁻¹ * (k * g * k⁻¹) * k).cycleFactorsFinset
Tactic: rw [aux g, aux c]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset
have suffices : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
Tactic: suffices imp_lemma : ∀ {g k c : Perm α},
      c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset by
    refine ⟨fun h ↦ ?_, imp_lemma⟩
    have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
    rw [aux g, aux c]
    exact imp_lemma h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
⊢ c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
have simp : (c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
  (k * c * k⁻¹).IsCycle ∧
    ∀ a ∈ (k * c * k⁻¹).support, Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)
Tactic: simp only [mem_cycleFactorsFinset_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
⊢ (c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
    (k * c * k⁻¹).IsCycle ∧
      ∀ a ∈ (k * c * k⁻¹).support, Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)
have apply : (∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
  ∀ a ∈ (k * c * k⁻¹).support, Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)
Tactic: apply And.imp IsCycle.conj