awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α) ↔
    (f ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ) : (a : α) → α) a = a

Tactic:
simp [sub_eq_neg_add, zpow_add, eq_symm_apply, eq_comm]

Premises used: zpow_add, sub_eq_neg_add, eq_comm, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
m n : ℤ
rw : Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔ (f ^ (n - m) : (a : α) → α) a = a
⊢ Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔ m ≡ n [ZMOD (↑(#s) : ℤ)]

Tactic:
rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]

Premises used: Int.modEq_iff_dvd, Equiv.Perm.IsCycleOn.zpow_apply_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α) ↔ (f ^ (n - m) : (a : α) → α) a = a

Tactic:
simp [sub_eq_neg_add, zpow_add, eq_symm_apply, eq_comm]

Premises used: zpow_add, sub_eq_neg_add, eq_comm, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
⊢ (f ^ #s : (a : α) → α) a = a

Tactic:
(hf.pow_apply_eq ha).2 dvd_rfl

Premises used: Iff.mpr, dvd_rfl, Equiv.Perm.IsCycleOn.pow_apply_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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

Tactic:
obtain ⟨n, rfl⟩ := hf.2 ha hb

Premises used: And.right, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
obtain :
  ∀ (k : ℤ) (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k),
    ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)

Tactic:
obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd

Premises used: Int.ModEq.symm, Int.ModEq.dvd, Nat.cast, Finset.card, Int.mod_modEq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)

Tactic:
⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩

Premises used: Int.natMod_lt, Finset.Nonempty.card_pos, Nat.cast, LT.lt.ne', And.intro, Exists.intro, Finset.card, Int.natMod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
refine : Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ ∃ n_1 < #s, Eq (α := α) ((f ^ n_1 : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)

Tactic:
refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
rw : Eq (α := α) ((f ^ n * HPow.hPow (β := ℤ) f (↑(#s) : ℤ) ^ k : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ Eq (α := α) ((f ^ n.natMod (↑(#s) : ℤ) : (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]

Premises used: zpow_natCast, Iff.mpr, zpow_add, Int.toNat_of_nonneg, zpow_mul, Finset.Nonempty.card_pos, LT.lt.ne', Exists.intro, Iff.mp, Int.emod_nonneg, sub_eq_iff_eq_add', Nat.cast_ne_zero, Int.natMod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
simp : ((f ^ #s) ^ k : (a : α) → α) a = a
⊢ Eq (α := α) ((f ^ n * HPow.hPow (β := ℤ) f (↑(#s) : ℤ) ^ k : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)

Tactic:
simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: zpow_natCast, Equiv.Perm.coe_mul, EmbeddingLike.apply_eq_iff_eq, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ ((f ^ #s) ^ k : (a : α) → α) a = a

Tactic:
IsFixedPt.perm_zpow (hf.pow_card_apply ha) _

Premises used: Function.IsFixedPt.perm_zpow, Equiv.Perm.IsCycleOn.pow_card_apply, Function.IsFixedPt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ ((f ^ #s) ^ k : (a : α) → α) a = a

Tactic:
exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _

Premises used: Function.IsFixedPt.perm_zpow, Equiv.Perm.IsCycleOn.pow_card_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
obtain₄ :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (k : ℤ)
    (hk : n % (↑(#s) : ℤ) - n = (↑(#s) : ℤ) * k), ((f ^ #s) ^ k : (a : α) → α) a = a
⊢ ∃ n < #s, (f ^ n : (a : α) → α) a = b

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) _

Premises used: zpow_natCast, Iff.mpr, zpow_add, Equiv.Perm.coe_mul, Int.toNat_of_nonneg, zpow_mul, Function.IsFixedPt.perm_zpow, Finset.Nonempty.card_pos, Equiv.Perm.IsCycleOn.pow_card_apply, EmbeddingLike.apply_eq_iff_eq, LT.lt.ne', And.right, Exists.intro, Function.comp_apply, Int.emod_nonneg, rfl, Nat.cast_ne_zero, Int.natMod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a b : α
hs : s.Finite
hf : f.IsCycleOn s
ha : a ∈ s
hb : b ∈ s
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a b : α
hs : s.Finite
hf : f.IsCycleOn s
ha : a ∈ s
hb : b ∈ s
lift :
  ∀ (s : Finset α) (hf : f.IsCycleOn (↑s : Set α)) (ha : a ∈ (↑s : Set α)) (hb : b ∈ (↑s : Set α)),
    ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b
⊢ ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ (↑s : Set α)
hb : b ∈ (↑s : Set α)
obtain : ∀ (n : ℕ) (hn : (f ^ n : (a : α) → α) a = b), ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b
⊢ ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b

Tactic:
obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb

Premises used: Equiv.Perm.IsCycleOn.exists_pow_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ (↑s : Set α)
hb : b ∈ (↑s : Set α)
n : ℕ
hn : (f ^ n : (a : α) → α) a = b
⊢ ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b

Tactic:
⟨n, hn⟩

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ (↑s : Set α)
hb : b ∈ (↑s : Set α)
n : ℕ
hn : (f ^ n : (a : α) → α) a = b
⊢ ∃ (n : ℕ), (f ^ n : (a : α) → α) a = b

Tactic:
exact ⟨n, hn⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hs : s.Finite
h : f.IsCycleOn s
ha : a ∈ s
⊢ (Set.range fun (n : ℕ) ↦ (f ^ n : (a : α) → α) a) = s

Tactic:
Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => h.1.mapsTo.perm_pow _ ha) fun _ =>
    h.exists_pow_eq' hs ha

Premises used: Set.Subset.antisymm, Iff.mpr, Equiv.Perm.IsCycleOn.exists_pow_eq', Set.MapsTo.perm_pow, And.left, Set.BijOn.mapsTo, Set.range_subset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
h : f.IsCycleOn s
ha : a ∈ s
⊢ (Set.range fun (n : ℤ) ↦ (f ^ n : (a : α) → α) a) = s

Tactic:
Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => (h.1.perm_zpow _).mapsTo ha) <| h.2 ha

Premises used: Set.Subset.antisymm, Iff.mpr, Set.BijOn.perm_zpow, And.right, And.left, Set.BijOn.mapsTo, Set.range_subset_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
n : ℕ
hf : (f ^ n).IsCycleOn s
h : Set.BijOn (⇑f : (a : α) → α) s s
⊢ f.IsCycleOn s

Tactic:
⟨h, fun _ hx _ hy => (hf.2 hx hy).of_pow⟩

Premises used: Equiv.Perm.SameCycle.of_pow, And.right, And.intro, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
n : ℤ
hf : (f ^ n).IsCycleOn s
h : Set.BijOn (⇑f : (a : α) → α) s s
⊢ f.IsCycleOn s

Tactic:
⟨h, fun _ hx _ hy => (hf.2 hx hy).of_zpow⟩

Premises used: Equiv.Perm.SameCycle.of_zpow, And.right, And.intro, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
h : g.IsCycleOn s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ (g.extendDomain (p := p) f).SameCycle (comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a)
    (comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) b)

Tactic:
(h.2 ha hb).extendDomain

Premises used: And.right, Equiv.Perm.SameCycle.extendDomain
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
h : g.IsCycleOn s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ (g.extendDomain (p := p) f).SameCycle (comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a)
    (comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) b)

Tactic:
exact (h.2 ha hb).extendDomain

Premises used: And.right, Equiv.Perm.SameCycle.extendDomain
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
inl : ∀ (hs : f.IsCycleOn ∅), Set.Countable.{u_2} (α := α) ∅
inr : ∀ (a : α) (ha : a ∈ s), s.Countable
⊢ s.Countable

Tactic:
obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ Set.Countable.{u_2} (α := α) ∅

Tactic:
Set.countable_empty

Premises used: Set.countable_empty
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ Set.Countable.{u_2} (α := α) ∅

Tactic:
exact Set.countable_empty

Premises used: Set.countable_empty
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable

Tactic:
(Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)

Premises used: Set.countable_range, HPow.hPow, And.right, Set.Countable.mono, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable

Tactic:
exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)

Premises used: Set.countable_range, HPow.hPow, And.right, Set.Countable.mono, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ l.formPerm.IsCycleOn {a : α | a ∈ l}

Tactic:
⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩

Premises used: List.formPerm, Equiv.bijOn, List.formPerm_mem_iff_mem, And.intro, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
h : l.Nodup
refine :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) {a : α | a ∈ l} a) (b : α)
    (hb : Membership.mem (γ := Set α) {a : α | a ∈ l} b), l.formPerm.SameCycle a b
⊢ l.formPerm.IsCycleOn {a : α | a ∈ l}

Tactic:
refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
rw : ∀ (ha : idxOf a l < l.length) (b : α) (hb : idxOf b l < l.length), l.formPerm.SameCycle a b
⊢ l.formPerm.SameCycle a b

Tactic:
rw [Set.mem_setOf, ← List.idxOf_lt_length_iff] at ha hb

Premises used: List.idxOf_lt_length_iff, Set.mem_setOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
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)
⊢ l.formPerm.SameCycle a b

Tactic:
rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]

Premises used: List.getElem_idxOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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)

Tactic:
⟨l.idxOf b - l.idxOf a, ?_⟩

Premises used: HSub.hSub, Equiv.Perm.SameCycle, Nat.cast, Exists.intro, List.idxOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
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
⊢ 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:
refine ⟨l.idxOf b - l.idxOf a, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
simp :
  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) ⋯
⊢ (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:
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]

Premises used: zpow_natCast, zpow_add, Equiv.Perm.coe_mul, sub_eq_neg_add, Equiv.Perm.inv_eq_iff_eq, Function.comp, List.formPerm_pow_apply_getElem, zpow_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
rw rw₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf b l + idxOf a l) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf b l + idxOf a 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) ⋯

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
x : α
hx : x ∈ s.toList.formPerm.support
⊢ x ∈ s

Tactic:
simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)

Premises used: Equiv.Perm.mem_support, Iff.mp, List.mem_of_formPerm_apply_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
refine : s.toList.formPerm.IsCycleOn (↑s : Set α)
⊢ ∃ (f : Perm α), f.IsCycleOn (↑s : Set α) ∧ f.support ⊆ s

Tactic:
refine ⟨s.toList.formPerm, ?_, fun x hx => by
    simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ s.toList.formPerm.IsCycleOn {a : α | a ∈ s.toList}

Tactic:
s.nodup_toList.isCycleOn_formPerm

Premises used: Finset.nodup_toList, List.Nodup.isCycleOn_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
h : (↑s : Set α) = {a : α | a ∈ s.toList}
⊢ s.toList.formPerm.IsCycleOn (↑s : Set α)

Tactic:
convert! s.nodup_toList.isCycleOn_formPerm

Premises used: Finset.nodup_toList, List.Nodup.isCycleOn_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ (↑s : Set α) = {a : α | a ∈ s.toList}

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
inl : ∀ (hs' : s.Finite), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
inr : ∀ (hs' : s.Infinite), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s

Tactic:
obtain hs' | hs' := s.finite_or_infinite

Premises used: Set.finite_or_infinite
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
x : α
hx : Membership.mem (γ := Set α) {x : α | (hs'.toFinset (s := s).toList.formPerm : (a : α) → α) x ≠ x} x
⊢ x ∈ s

Tactic:
simpa using List.mem_of_formPerm_apply_ne hx

Premises used: List.mem_of_formPerm_apply_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
inl : hs'.toFinset (s := s).toList.formPerm.IsCycleOn s
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s

Tactic:
refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ hs'.toFinset (s := s).toList.formPerm.IsCycleOn {a : α | a ∈ hs'.toFinset (s := s).toList}

Tactic:
hs'.toFinset.nodup_toList.isCycleOn_formPerm

Premises used: Finset.nodup_toList, List.Nodup.isCycleOn_formPerm, Set.Finite.toFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ s = {a : α | a ∈ hs'.toFinset (s := s).toList}

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
⊢ Countable.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI := hs.to_subtype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this : Countable.{u_2 + 1} (↑s : Type u_2)
⊢ Infinite.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI := hs'.to_subtype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this_1 : Countable.{u_2 + 1} (↑s : Type u_2)
this : Infinite.{u_2 + 1} (↑s : Type u_2)
⊢ Nonempty.{max 1 (u_2 + 1)} (ℤ ≃ (↑s : Type u_2))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this_1 : Countable.{u_2 + 1} (↑s : Type u_2)
this : Infinite.{u_2 + 1} (↑s : Type u_2)
inr : ∀ (f : ℤ ≃ (↑s : Type u_2)), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s

Tactic:
obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance

Premises used: Set.Elem, Equiv, Int, Nonempty
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this_1 : Countable.{u_2 + 1} (↑s : Type u_2)
this : Infinite.{u_2 + 1} (↑s : Type u_2)
f : ℤ ≃ (↑s : Type u_2)
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s

Tactic:
⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩

Premises used: Equiv.addRight, Equiv.Perm.extendDomain, Equiv.Perm.extendDomain_apply_not_subtype, And.intro, Exists.intro, of_not_not, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this_1 : Countable.{u_2 + 1} (↑s : Type u_2)
this : Infinite.{u_2 + 1} (↑s : Type u_2)
f : ℤ ≃ (↑s : Type u_2)
inr : (Perm.extendDomain (Equiv.addRight 1) (p := fun (x : α) ↦ x ∈ s) f).IsCycleOn s
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s

Tactic:
refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this_1 : Countable.{u_2 + 1} (↑s : Type u_2)
this : Infinite.{u_2 + 1} (↑s : Type u_2)
f : ℤ ≃ (↑s : Type u_2)
⊢ (Perm.extendDomain (Equiv.addRight 1) (p := fun (x : α) ↦ x ∈ s) f).IsCycleOn
    (Set.image (α := ℤ)
      (comp (β := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑f : (a : ℤ) → { x : α // x ∈ s }))
      {x : ℤ | (Equiv.addRight 1 : (a : ℤ) → ℤ) x ≠ x})

Tactic:
Int.addRight_one_isCycle.isCycleOn.extendDomain f

Premises used: Int.addRight_one_isCycle, Equiv.Perm.IsCycle.isCycleOn, Equiv.Perm.IsCycleOn.extendDomain