awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inr : (f ^ n : (a : α) → α) a = a ↔
  (HPow.hPow (α := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry) n :
        (a : { x : α // x ∈ (↑s : Set α) }) → { x : α // x ∈ (↑s : Set α) })
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
Tactic: rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
-- 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 : ℕ
hs : s.Nontrivial
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inr : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
Tactic: classical
    have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    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
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-SetLike.coe_sort_coe]
-- 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 : ℕ
hs : s.Nontrivial
inr inr₁ inr₂ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inr₃ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
  (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))),
  (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
Tactic: classical
    have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    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
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-SetLike.coe_sort_coe]
-- 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 : ℕ
hs : s.Nontrivial
inr inr₁ inr₂ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
inr₃ :
  ∀ (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
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inr₄ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
  (this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry) = #s),
  (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
Tactic: classical
    have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    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
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-SetLike.coe_sort_coe]
-- 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 : ℕ
hs : s.Nontrivial
inr inr₁ inr₂ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
inr₃ :
  ∀ (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
inr₄ :
  ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
    (this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s),
    (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
have inr₅ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
  (this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry) = #s),
  (f ^ n : (a : α) → α) a = a ↔
    (HPow.hPow (α := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) sorry) n :
          (a : { x : α // x ∈ (↑s : Set α) }) → { x : α // x ∈ (↑s : Set α) })
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
Tactic: classical
    have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    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
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-SetLike.coe_sort_coe]
-- 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 ^ Int.negSucc n : (a : α) → α) a = a ↔ (↑(#s) : ℤ) ∣ Int.negSucc n
have rw : (f⁻¹ ^ (n + 1) : (a : α) → α) a = a ↔ (↑(#s) : ℤ) ∣ Int.negSucc n
Tactic: rw [zpow_negSucc, ← inv_pow]
-- 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
m n : ℕ
⊢ Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔ m ≡ n [MOD #s]
have rw : Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔
  (f ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ) : (a : α) → α) a = a
Tactic: rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq 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
m n : ℤ
⊢ Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔ m ≡ n [ZMOD (↑(#s) : ℤ)]
have rw : Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔ (f ^ (n - m) : (a : α) → α) a = a
Tactic: rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b
have obtain : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
  ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: obtain ⟨n, rfl⟩ := hf.2 ha hb
Cleared hypotheses: b, hb
-- 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 : ℤ
hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
have obtain : ∀ (k : ℤ) (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
  ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
-- 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 : ℤ
hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
k : ℤ
hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k
⊢ ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
have refine : Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
-- 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 : ℤ
hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
k : ℤ
hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k
⊢ Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
have rw : Eq (α := α) ((f ^ n * HPow.hPow (β := ℤ) f (↑(#s) : ℤ) ^ k : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
-- 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 : ℤ
hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
k : ℤ
hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k
⊢ Eq (α := α) ((f ^ n * HPow.hPow (β := ℤ) f (↑(#s) : ℤ) ^ k : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
have simp : ((f ^ #s) ^ k : (a : α) → α) a = a
Tactic: simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b
have obtain : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
  ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
    refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
    rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
hb : b ∈ s
obtain :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b
have obtain₁ : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
  (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
  ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
    refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
    rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
hb : b ∈ s
obtain :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
obtain₁ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b
have obtain₂ : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
  (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
  Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
    refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
    rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
hb : b ∈ s
obtain :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
obtain₁ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
obtain₂ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b
have obtain₃ : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
  (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
  Eq (α := α) ((f ^ n * HPow.hPow (β := ℤ) f (↑(#s) : ℤ) ^ k : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
    refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
    rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
hb : b ∈ s
obtain :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
obtain₁ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
obtain₂ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
obtain₃ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    Eq (α := α) ((f ^ n * HPow.hPow (β := ℤ) f (↑(#s) : ℤ) ^ k : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b
have obtain₄ : ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
  (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k), ((f ^ #s) ^ k : (a : α) → α) a = a
Tactic: classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
    refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
    rw [← zpow_natCast, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
a b : α
hs : s.Finite
hf : f.IsCycleOn s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b
have lift : ∀ (s : Finset α) (hf : f.IsCycleOn (↑s : Set α)) (ha : a ∈ (↑s : Set α)) (hb : b ∈ (↑s : Set α)),
  ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs, hf, ha, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ (↑s : Set α)
hb : b ∈ (↑s : Set α)
⊢ ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b
have obtain : ∀ (n : ℕ) (hn : (f ^ n : (a : α) → α) a = b), ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b
Tactic: obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
⊢ s.Countable
have inl : ∀ (hs : f.IsCycleOn ∅), Set.Countable.{u_2} (α := α) ∅
Tactic: obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
inl : ∀ (hs : f.IsCycleOn ∅), Set.Countable.{u_2} (α := α) ∅
⊢ s.Countable
have inr : ∀ (a : α) (ha : a ∈ s), s.Countable
Tactic: obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ l.formPerm.IsCycleOn {a : α | a ∈ l}
have refine : ∀ (a : α) (ha : Membership.mem (γ := Set α) {a : α | a ∈ l} a) (b : α)
  (hb : Membership.mem (γ := Set α) {a : α | a ∈ l} b), l.formPerm.SameCycle a b
Tactic: refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : Membership.mem (γ := Set α) {a : α | a ∈ l} a
b : α
hb : Membership.mem (γ := Set α) {a : α | a ∈ l} b
⊢ l.formPerm.SameCycle a b
have rw : ∀ (ha : idxOf a l < l.length) (b : α) (hb : idxOf b l < l.length), l.formPerm.SameCycle a b
Tactic: rw [Set.mem_setOf, ← List.idxOf_lt_length_iff] at ha hb
Cleared hypotheses: ha, b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b
have rw : l.formPerm.SameCycle (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) ha)
  (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf b l) hb)
Tactic: rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) ha)
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf b l) hb)
have refine : (l.formPerm ^ HSub.hSub (α := ℤ) (↑(idxOf b l) : ℤ) (↑(idxOf a l) : ℤ) : (a : α) → α)
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) ha) =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf b l) hb
Tactic: refine ⟨l.idxOf b - l.idxOf a, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ (l.formPerm ^ HSub.hSub (α := ℤ) (↑(idxOf b l) : ℤ) (↑(idxOf a l) : ℤ) : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) ha) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf b l) hb
have simp : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + idxOf b l) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf b l + idxOf a l) % l.length) sorry
Tactic: simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast,
    Equiv.Perm.coe_mul, List.formPerm_pow_apply_getElem _ h, Function.comp]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + idxOf b l) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf b l + idxOf a l) % l.length) ⋯
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf b l + idxOf a l) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf b l + idxOf a l) % l.length) sorry
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ ∃ (f : Perm α), f.IsCycleOn (↑s : Set α) ∧ f.support ⊆ s
have refine : s.toList.formPerm.IsCycleOn (↑s : Set α)
Tactic: refine ⟨s.toList.formPerm, ?_, fun x hx => by
    simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ s.toList.formPerm.IsCycleOn (↑s : Set α)
have h : (↑s : Set α) = {a : α | a ∈ s.toList}
Tactic: convert! s.nodup_toList.isCycleOn_formPerm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Countable
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
have inl : ∀ (hs' : s.Finite), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
Tactic: obtain hs' | hs' := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Countable
inl : ∀ (hs' : s.Finite), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
have inr : ∀ (hs' : s.Infinite), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
Tactic: obtain hs' | hs' := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
have inl : hs'.toFinset (s := s).toList.formPerm.IsCycleOn s
Tactic: refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
have this : Countable.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI := hs.to_subtype