awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
intro :
  ∀ (val : Fintype β),
    f ^ a = f ^ b ↔
      ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
intro₁ :
  ∀ (val : Fintype β),
    f ^ a = f ^ b →
      ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro₂ : ∀ (val : Fintype β),
  (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) →
    f ^ a = f ^ b
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_ge hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp [pow_sub _ hab, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ (f ^ n).IsCycle
have intro : ∀ (val : Fintype β), (f ^ n).IsCycle
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ n.Coprime (orderOf f)
have refine : (orderOf f).Coprime n
Tactic: refine Nat.Coprime.symm ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ (orderOf f).Coprime n
have rw : ¬orderOf f ∣ n
Tactic: rw [Nat.Prime.coprime_iff_not_dvd hf']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ (f ^ n).IsCycle
have this : n.Coprime (orderOf f)
Tactic: have : n.Coprime (orderOf f) := by
      refine Nat.Coprime.symm ?_
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ (f ^ n).IsCycle
have intro : ∀ (val : Fintype β), (f ^ n).IsCycle
Tactic: classical
    cases nonempty_fintype β
    have : n.Coprime (orderOf f) := by
      refine Nat.Coprime.symm ?_
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
    exact (pow_iff hf).mpr this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
intro : ∀ (val : Fintype β), (f ^ n).IsCycle
⊢ (f ^ n).IsCycle
have intro₁ : ∀ (val : Fintype β) (this : n.Coprime (orderOf f)), (f ^ n).IsCycle
Tactic: classical
    cases nonempty_fintype β
    have : n.Coprime (orderOf f) := by
      refine Nat.Coprime.symm ?_
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
    exact (pow_iff hf).mpr this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ orderOf σ = orderOf τ
have rw : #σ.support = orderOf τ
Tactic: rw [hσ.orderOf, h, hτ.orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
rw : #σ.support = orderOf τ
⊢ orderOf σ = orderOf τ
have rw₁ : #τ.support = orderOf τ
Tactic: rw [hσ.orderOf, h, hτ.orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
rw : #σ.support = orderOf τ
rw₁ : #τ.support = orderOf τ
⊢ orderOf σ = orderOf τ
have rw₂ : #τ.support = #τ.support
Tactic: rw [hσ.orderOf, h, hτ.orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ IsConj σ τ
have by : ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
  Eq (α := α)
    ((↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport) (Equiv.trans (zpowersEquivZPowers sorry) hτ.zpowersEquivSupport) :
              (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) sorry)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport)
                  (Equiv.trans (zpowersEquivZPowers sorry) hτ.zpowersEquivSupport) :
                (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
          α) :
      α)
Tactic: refine
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
x : α
hx : x ∈ (↑σ.support : Set α)
⊢ Eq (α := α)
    ((↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport) (Equiv.trans (zpowersEquivZPowers ⋯) hτ.zpowersEquivSupport) :
              (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport)
                  (Equiv.trans (zpowersEquivZPowers ⋯) hτ.zpowersEquivSupport) :
                (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
          α) :
      α)
have simp : Eq (α := α)
  ((↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
          (((zpowersEquivZPowers sorry : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
              (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
            ((Equiv.symm hσ.zpowersEquivSupport : (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) sorry)))) :
      α) :
    α)
  ((τ : (a : α) → α)
      (↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
            (((zpowersEquivZPowers sorry : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
              ((Equiv.symm hσ.zpowersEquivSupport : (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)))) :
        α) :
    α)
Tactic: simp only [Equiv.trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : IsConj σ τ
⊢ #σ.support = #τ.support
have obtain : ∀ (π : Perm α) (hτ : (π * σ * π⁻¹).IsCycle) (h : IsConj σ (π * σ * π⁻¹)), #σ.support = #(π * σ * π⁻¹).support
Tactic: obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
Cleared hypotheses: τ, hτ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
⊢ f⁻¹.IsCycleOn s ↔ f.IsCycleOn s
have simp : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) →
  (Set.BijOn (⇑f⁻¹ : (a : α) → α) s s ↔ Set.BijOn (⇑f : (a : α) → α) s s)
Tactic: simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑g : (a : α) → α) '' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑g : (a : α) → α) '' s) y
⊢ (g * f * g⁻¹).SameCycle x y
have rw : ∀ (hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x) (y : α)
  (hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y), (g * f * g⁻¹).SameCycle x y
Tactic: rw [Equiv.image_eq_preimage_symm] at hx hy
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y
⊢ (g * f * g⁻¹).SameCycle x y
have h₁ : x = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α)
Tactic: convert! Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y
h₁ : x = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α)
⊢ (g * f * g⁻¹).SameCycle x y
have h₂ : y = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) y : α)
Tactic: convert! Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
x : α
hx : Membership.mem (γ := Set α) {a, b} x
y : α
hy : Membership.mem (γ := Set α) {a, b} y
⊢ (swap a b).SameCycle x y
have rw : ∀ (hx : x = a ∨ x = b) (y : α) (hy : y = a ∨ y = b), (swap a b).SameCycle x y
Tactic: rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y
have inl : ∀ (hab : x ≠ b) (hy : y = x ∨ y = b), (swap x b).SameCycle x y
Tactic: obtain rfl | rfl := hx
Cleared hypotheses: a, hab, hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
inl : ∀ (hab : x ≠ b) (hy : y = x ∨ y = b), (swap x b).SameCycle x y
⊢ (swap a b).SameCycle x y
have inr : ∀ (hab : a ≠ x) (hy : y = a ∨ y = x), (swap a x).SameCycle x y
Tactic: obtain rfl | rfl := hx
Cleared hypotheses: b, hab, hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
b : α
inst : DecidableEq α
x y : α
hab : x ≠ b
hy : y = x ∨ y = b
⊢ (swap x b).SameCycle x y
have inl : ∀ (hab : y ≠ b), (swap y b).SameCycle y y
Tactic: obtain rfl | rfl := hy
Cleared hypotheses: x, hab, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
b : α
inst : DecidableEq α
x y : α
hab : x ≠ b
hy : y = x ∨ y = b
inl : ∀ (hab : y ≠ b), (swap y b).SameCycle y y
⊢ (swap x b).SameCycle x y
have inl₁ : ∀ (hab : x ≠ y), (swap x y).SameCycle x y
Tactic: obtain rfl | rfl := hy
Cleared hypotheses: b, hab, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a : α
inst : DecidableEq α
x y : α
hab : a ≠ x
hy : y = a ∨ y = x
⊢ (swap a x).SameCycle x y
have inr : ∀ (hab : y ≠ x), (swap y x).SameCycle x y
Tactic: obtain rfl | rfl := hy
Cleared hypotheses: a, hab, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a : α
inst : DecidableEq α
x y : α
hab : a ≠ x
hy : y = a ∨ y = x
inr : ∀ (hab : y ≠ x), (swap y x).SameCycle x y
⊢ (swap a x).SameCycle x y
have inr₁ : ∀ (hab : a ≠ y), (swap a y).SameCycle y y
Tactic: obtain rfl | rfl := hy
Cleared hypotheses: x, hab, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
b : α
inst : DecidableEq α
y : α
hab : y ≠ b
⊢ (HPow.hPow (β := ℤ) (swap y b) 0 : (a : α) → α) y = y
have rw : (1 : (a : α) → α) y = y
Tactic: rw [zpow_zero, coe_one, id]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
b : α
inst : DecidableEq α
y : α
hab : y ≠ b
rw : (1 : (a : α) → α) y = y
⊢ (HPow.hPow (β := ℤ) (swap y b) 0 : (a : α) → α) y = y
have rw₁ : id y = y
Tactic: rw [zpow_zero, coe_one, id]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
b : α
inst : DecidableEq α
y : α
hab : y ≠ b
rw : (1 : (a : α) → α) y = y
rw₁ : id y = y
⊢ (HPow.hPow (β := ℤ) (swap y b) 0 : (a : α) → α) y = y
have rw₂ : y = y
Tactic: rw [zpow_zero, coe_one, id]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : x ≠ y
⊢ (HPow.hPow (β := ℤ) (swap x y) 1 : (a : α) → α) x = y
have rw : (swap x y : (a : α) → α) x = y
Tactic: rw [zpow_one, swap_apply_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : x ≠ y
rw : (swap x y : (a : α) → α) x = y
⊢ (HPow.hPow (β := ℤ) (swap x y) 1 : (a : α) → α) x = y
have rw₁ : y = y
Tactic: rw [zpow_one, swap_apply_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : y ≠ x
⊢ (HPow.hPow (β := ℤ) (swap y x) 1 : (a : α) → α) x = y
have rw : (swap y x : (a : α) → α) x = y
Tactic: rw [zpow_one, swap_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : y ≠ x
rw : (swap y x : (a : α) → α) x = y
⊢ (HPow.hPow (β := ℤ) (swap y x) 1 : (a : α) → α) x = y
have rw₁ : y = y
Tactic: rw [zpow_one, swap_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a : α
inst : DecidableEq α
y : α
hab : a ≠ y
⊢ (HPow.hPow (β := ℤ) (swap a y) 0 : (a : α) → α) y = y
have rw : (1 : (a : α) → α) y = y
Tactic: rw [zpow_zero, coe_one, id]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a : α
inst : DecidableEq α
y : α
hab : a ≠ y
rw : (1 : (a : α) → α) y = y
⊢ (HPow.hPow (β := ℤ) (swap a y) 0 : (a : α) → α) y = y
have rw₁ : id y = y
Tactic: rw [zpow_zero, coe_one, id]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
a : α
inst : DecidableEq α
y : α
hab : a ≠ y
rw : (1 : (a : α) → α) y = y
rw₁ : id y = y
⊢ (HPow.hPow (β := ℤ) (swap a y) 0 : (a : α) → α) y = y
have rw₂ : y = y
Tactic: rw [zpow_zero, coe_one, id]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
⊢ (f : (a : α) → α) a ≠ a
have obtain : ∀ (b : α) (hb : b ∈ s) (hba : b ≠ a), (f : (a : α) → α) a ≠ a
Tactic: obtain ⟨b, hb, hba⟩ := hs.exists_ne a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ (f : (a : α) → α) a ≠ a
have obtain : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (hba : (f ^ n : (a : α) → α) a ≠ a),
  (f : (a : α) → α) a ≠ a
Tactic: obtain ⟨n, rfl⟩ := hf.2 ha hb
Cleared hypotheses: b, hb, hba
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
⊢ f.IsCycle ↔ ∃ (s : Set α), s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s
have refine_1 : ∀ (hf : f.IsCycle), Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}
Tactic: refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
refine_1 : ∀ (hf : f.IsCycle), Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}
⊢ f.IsCycle ↔ ∃ (s : Set α), s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s
have refine_2 : (∃ (s : Set α), s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s) → f.IsCycle
Tactic: refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
hf : f.IsCycle
⊢ Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}
have refine_1 : ∀ (a : α) (ha : (f : (a : α) → α) a ≠ a ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle a y),
  Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}
Tactic: obtain ⟨a, ha⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s
⊢ f.IsCycle
have refine_2 : ∀ (a : α) (ha : a ∈ s), f.IsCycle
Tactic: obtain ⟨a, ha⟩ := hs.nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ IsCycle (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯)
have obtain : ∀ (a : α) (ha : a ∈ s), IsCycle (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) sorry)
Tactic: obtain ⟨a, ha⟩ := hs.nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
have inl : ∀ (hs : s.Subsingleton), IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) sorry) _root_.Set.univ
Tactic: obtain hs | hs := s.subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
inl :
  ∀ (hs : s.Subsingleton), IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
have inr : ∀ (hs : s.Nontrivial), IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) sorry) _root_.Set.univ
Tactic: obtain hs | hs := s.subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
have this : Subsingleton.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI := hs.coe_sort
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
have h : Eq.{u_2 + 1} (α := Set { x : α // x ∈ s }) _root_.Set.univ
  {x : { x : α // x ∈ s } |
    (f.subtypePerm (p := Membership.mem s) sorry : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
Tactic: convert! (hf.isCycle_subtypePerm hs).isCycleOn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ Eq.{u_2 + 1} (α := Set { x : α // x ∈ s }) _root_.Set.univ
    {x : { x : α // x ∈ s } |
      (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
have h : ∀ (x : { x : α // x ∈ s }),
  Membership.mem (γ := Set { x : α // x ∈ s })
    {x : { x : α // x ∈ s } |
      (f.subtypePerm (p := Membership.mem s) sorry : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
    x
Tactic: rw [eq_comm, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inl : ∀ (hf : f.IsCycleOn (↑{a} : Set α)) (ha : Membership.mem (γ := Finset α) {a} a),
  (f ^ n : (a : α) → α) a = a ↔ card (α := α) {a} ∣ n
Tactic: obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha
Cleared hypotheses: s, hf, ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
inl :
  ∀ (hf : f.IsCycleOn (↑{a} : Set α)) (ha : Membership.mem (γ := Finset α) {a} a),
    (f ^ n : (a : α) → α) a = a ↔ card (α := α) {a} ∣ n
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inr : ∀ (hs : s.Nontrivial), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
Tactic: obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn (↑{a} : Set α)
ha : Membership.mem (γ := Finset α) {a} a
⊢ (f ^ n : (a : α) → α) a = a ↔ card (α := α) {a} ∣ n
have hf₁ : (f : (a : α) → α) a = a
Tactic: rw [coe_singleton, isCycleOn_singleton] at hf
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
Tactic: have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have this : orderOf (G := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry) =
  card (α := { x : α // x ∈ (↑s : Set α) }) (support (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry))
Tactic: have := (hf.isCycle_subtypePerm hs).orderOf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
this :
  orderOf (G := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) =
    card (α := { x : α // x ∈ (↑s : Set α) }) (support (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯))
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have this₁ : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry) = #s
Tactic: simp only [coe_sort_coe, support_subtypePerm, ne_eq, h, not_false_eq_true, univ_eq_attach,
      mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this
Cleared hypotheses: this