awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h :
  s =
    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}
⊢ (Perm.extendDomain (Equiv.addRight 1) (p := fun (x : α) ↦ x ∈ s) f).IsCycleOn s

Tactic:
convert! Int.addRight_one_isCycle.isCycleOn.extendDomain f

Premises used: Int.addRight_one_isCycle, Equiv.Perm.IsCycle.isCycleOn, Equiv.Perm.IsCycleOn.extendDomain
-- 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)
h :
  s =
    Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := ℤ) (⇑f.symm : (a : { x : α // x ∈ s }) → ℤ) {x : ℤ | (Equiv.addRight 1 : (a : ℤ) → ℤ) x ≠ x})
⊢ s =
    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:
rw [Set.image_comp, Equiv.image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm, Set.image_comp
-- 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)
h :
  ∀ (x : α),
    x ∈ s ↔
      Membership.mem (γ := Set α)
        (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
          (preimage (β := ℤ) (⇑f.symm : (a : { x : α // x ∈ s }) → ℤ) {x : ℤ | (Equiv.addRight 1 : (a : ℤ) → ℤ) x ≠ x}))
        x
⊢ s =
    Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := ℤ) (⇑f.symm : (a : { x : α // x ∈ s }) → ℤ) {x : ℤ | (Equiv.addRight 1 : (a : ℤ) → ℤ) x ≠ x})

Tactic:
ext
-- 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)
x : α
⊢ x ∈ s ↔
    Membership.mem (γ := Set α)
      (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (preimage (β := ℤ) (⇑f.symm : (a : { x : α // x ∈ s }) → ℤ) {x : ℤ | (Equiv.addRight 1 : (a : ℤ) → ℤ) x ≠ x}))
      x

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 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:
classical
  obtain hs' | hs' := s.finite_or_infinite
  · refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne hx⟩
    convert! hs'.toFinset.nodup_toList.isCycleOn_formPerm
    simp
  · haveI := hs.to_subtype
    haveI := hs'.to_subtype
    obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
    refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
    convert! Int.addRight_one_isCycle.isCycleOn.extendDomain f
    rw [Set.image_comp, Equiv.image_eq_preimage_symm]
    ext
    simp

Premises used: Set.finite_or_infinite, Set.Elem, Equiv, Int, Equiv.image_eq_preimage_symm, Set.image_comp, Nonempty
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
h :
  ∀ (a b : α),
    (a, b) ∈ s ×ˢ s ↔
      Membership.mem (γ := Set (α × α)) (⋃ (n : ℤ), (fun (a : α) ↦ (a, (f ^ n : (a : α) → α) a)) '' s) (a, b)
⊢ s ×ˢ s = ⋃ (n : ℤ), (fun (a : α) ↦ (a, (f ^ n : (a : α) → α) a)) '' s

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
h : a ∈ s ∧ b ∈ s ↔ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)
⊢ (a, b) ∈ s ×ˢ s ↔
    Membership.mem (γ := Set (α × α)) (⋃ (n : ℤ), (fun (a : α) ↦ (a, (f ^ n : (a : α) → α) a)) '' s) (a, b)

Tactic:
simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)

Tactic:
⟨fun hx => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
h : ∀ (hx : a ∈ s ∧ b ∈ s), ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)
h₁ : (∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)) → a ∈ s ∧ b ∈ s
⊢ a ∈ s ∧ b ∈ s ↔ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)

Tactic:
refine ⟨fun hx => ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
hx : a ∈ s ∧ b ∈ s
h :
  ∀ (n : ℤ) (hx : a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
    ∃ (i : ℤ), ∃ x ∈ s, Eq (α := α × α) ((x, (f ^ i : (a : α) → α) x) : α × α) ((a, (f ^ n : (a : α) → α) a) : α × α)
⊢ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)

Tactic:
obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2

Premises used: And.right, And.left, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
hx : a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
⊢ ∃ (i : ℤ), ∃ x ∈ s, Eq (α := α × α) ((x, (f ^ i : (a : α) → α) x) : α × α) ((a, (f ^ n : (a : α) → α) a) : α × α)

Tactic:
⟨_, _, hx.1, rfl⟩

Premises used: And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
hx : a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
⊢ ∃ (i : ℤ), ∃ x ∈ s, Eq (α := α × α) ((x, (f ^ i : (a : α) → α) x) : α × α) ((a, (f ^ n : (a : α) → α) a) : α × α)

Tactic:
exact ⟨_, _, hx.1, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)

Tactic:
⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩

Premises used: Set.BijOn.perm_zpow, And.left, And.intro, Set.BijOn.mapsTo
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)

Tactic:
exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
inl :
  ∀ (hs : (↑s : Set α).Subsingleton),
    Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
      map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
inr :
  (↑s : Set α).Nontrivial →
    Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
      map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s

Tactic:
obtain hs | _ := (s : Set α).subsingleton_or_nontrivial

Premises used: Set.subsingleton_or_nontrivial, SetLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
hs : (↑s : Set α).Subsingleton
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s

Tactic:
Set.Subsingleton.pairwise ?_ _

Premises used: Set.PairwiseDisjoint, Set.Subsingleton.pairwise
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
hs : (↑s : Set α).Subsingleton
inl : (↑(range #s) : Set ℕ).Subsingleton
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s

Tactic:
refine Set.Subsingleton.pairwise ?_ _

Premises used: Set.Subsingleton.pairwise
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
hs : (↑s : Set α).Subsingleton
inl : ∀ (hs : #s ≤ 1), #(range #s) ≤ 1
⊢ (↑(range #s) : Set ℕ).Subsingleton

Tactic:
simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢

Premises used: Finset.card_le_one, Set.Subsingleton, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
hs inl inl₁ inl₂ inl₃ : #s ≤ 1
⊢ #(range #s) ≤ 1

Tactic:
rwa [card_range]

Premises used: Finset.card_range
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h : (↑s : Set α).Nontrivial
m : ℕ
hm : m ∈ (↑(range #s) : Set ℕ)
n : ℕ
hn : n ∈ (↑(range #s) : Set ℕ)
hmn : m ≠ n
inr : ∀ (a b x : α), x ∈ s → x = a → (f ^ m : (a : α) → α) x = b → ∀ x ∈ s, x = a → ¬(f ^ n : (a : α) → α) x = b
⊢ onFun.{1, u_2 + 1, 1} (β := Finset (α × α)) Disjoint
    (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s) m n

Tactic:
simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk,
      not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk_inj]

Premises used: Function.onFun, and_imp, Prod.mk_inj, forall_exists_index, not_exists, Function.Embedding.coeFn_mk, Prod.forall, Finset.disjoint_left, Finset.mem_map, not_and
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h_1 : (↑s : Set α).Nontrivial
m : ℕ
hm : m ∈ (↑(range #s) : Set ℕ)
n : ℕ
hn : n ∈ (↑(range #s) : Set ℕ)
hmn : m ≠ n
a : α
ha : a ∈ s
h : Eq (α := α) ((f ^ n : (a : α) → α) a : α) ((f ^ m : (a : α) → α) a : α)
⊢ n ≡ m [MOD #s]

Tactic:
rw [hf.pow_apply_eq_pow_apply ha] at h

Premises used: Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h_1 : (↑s : Set α).Nontrivial
m : ℕ
hm : m ∈ (↑(range #s) : Set ℕ)
n : ℕ
hn : n ∈ (↑(range #s) : Set ℕ)
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
inr : ∀ (hm : m < #s) ⦃n : ℕ⦄ (hn : n < #s) (hmn : m ≠ n) (a : α) (ha : a ∈ s) (h : n ≡ m [MOD #s]), False
⊢ False

Tactic:
rw [mem_coe, mem_range] at hm hn

Premises used: Finset.mem_range, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h_1 : (↑s : Set α).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
hmn.symm (h.eq_of_lt_of_lt hn hm)

Premises used: Ne.symm, Nat.ModEq.eq_of_lt_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h_1 : (↑s : Set α).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
exact hmn.symm (h.eq_of_lt_of_lt hn hm)

Premises used: Ne.symm, Nat.ModEq.eq_of_lt_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h : (↑s : Set α).Nontrivial
inr :
  ∀ ⦃m : ℕ⦄ (hm : m ∈ (↑(range #s) : Set ℕ)) ⦃n : ℕ⦄ (hn : n ∈ (↑(range #s) : Set ℕ)) (hmn : m ≠ n),
    onFun.{1, u_2 + 1, 1} (β := Finset (α × α)) Disjoint
      (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s) m n
inr₁ :
  ∀ ⦃m : ℕ⦄ (hm : m ∈ (↑(range #s) : Set ℕ)) ⦃n : ℕ⦄ (hn : n ∈ (↑(range #s) : Set ℕ)) (hmn : m ≠ n) (a b x : α),
    x ∈ s → x = a → (f ^ m : (a : α) → α) x = b → ∀ x ∈ s, x = a → ¬(f ^ n : (a : α) → α) x = b
inr₂ :
  ∀ ⦃m : ℕ⦄ (hm : m ∈ (↑(range #s) : Set ℕ)) ⦃n : ℕ⦄ (hn : n ∈ (↑(range #s) : Set ℕ)) (hmn : m ≠ n) (a : α) (ha : a ∈ s)
    (h : Eq (α := α) ((f ^ n : (a : α) → α) a : α) ((f ^ m : (a : α) → α) a : α)), False
inr₃ :
  ∀ ⦃m : ℕ⦄ (hm : m ∈ (↑(range #s) : Set ℕ)) ⦃n : ℕ⦄ (hn : n ∈ (↑(range #s) : Set ℕ)) (hmn : m ≠ n) (a : α) (ha : a ∈ s)
    (h : n ≡ m [MOD #s]), False
inr₄ : ∀ ⦃m : ℕ⦄ (hm : m < #s) ⦃n : ℕ⦄ (hn : n < #s) (hmn : m ≠ n) (a : α) (ha : a ∈ s) (h : n ≡ m [MOD #s]), False
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s

Tactic:
classical
    rintro m hm n hn hmn
    simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk,
      not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk_inj]
    rintro _ _ _ - rfl rfl a ha rfl h
    rw [hf.pow_apply_eq_pow_apply ha] at h
    rw [mem_coe, mem_range] at hm hn
    exact hmn.symm (h.eq_of_lt_of_lt hn hm)

Premises used: Function.onFun, and_imp, Prod.mk_inj, forall_exists_index, not_exists, Finset.mem_range, Function.Embedding.coeFn_mk, Prod.forall, Finset.disjoint_left, Finset.mem_map, not_and, Finset.mem_coe, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h :
  ∀ (a b : α),
    (a, b) ∈ s ×ˢ s ↔
      (a, b) ∈
        (range #s).disjiUnion
          (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ : α ↪ α × α } s) ⋯
⊢ s ×ˢ s =
    (range #s).disjiUnion (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s) ⋯

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a b : α
h : a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b
⊢ (a, b) ∈ s ×ˢ s ↔
    (a, b) ∈
      (range #s).disjiUnion
        (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ : α ↪ α × α } s) ⋯

Tactic:
simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
    Function.Embedding.coeFn_mk, Prod.mk_inj]

Premises used: Prod.mk_inj, Finset.mem_range, Finset.mem_disjiUnion, Function.Embedding.coeFn_mk, Finset.mem_map, Finset.mem_product, Equiv.Perm.coe_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b

Tactic:
⟨fun hx => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a b : α
h : ∀ (hx : a ∈ s ∧ b ∈ s), ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b
h₁ : (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b

Tactic:
refine ⟨fun hx => ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a b : α
hx : a ∈ s ∧ b ∈ s
h :
  ∀ (n : ℕ) (hn : n < #s) (hx : a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)),
    ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = (f ^ n : (a : α) → α) a
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b

Tactic:
obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2

Premises used: Equiv.Perm.IsCycleOn.exists_pow_eq, And.right, And.left, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
rw rw₁ : Eq (α := α) ((f ^ n : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
⊢ (⇑f : (a : α) → α)^[n] a = (f ^ n : (a : α) → α) a

Tactic:
rw [f.iterate_eq_pow]

Premises used: Equiv.Perm.iterate_eq_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = (f ^ n : (a : α) → α) a

Tactic:
exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
n : ℕ
a : α
ha : a ∈ s
⊢ a ∈ s ∧ (⇑f : (a : α) → α)^[n] a ∈ s

Tactic:
⟨ha, (hf.1.iterate _).mapsTo ha⟩

Premises used: And.left, And.intro, Set.BijOn.mapsTo, Set.BijOn.iterate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
n : ℕ
a : α
ha : a ∈ s
⊢ a ∈ s ∧ (⇑f : (a : α) → α)^[n] a ∈ s

Tactic:
exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn (↑s : Set ι)
f : ι → α
g : ι → β
rw : Eq.{u_3 + 1} (α := β) (∑ x ∈ s ×ˢ s, f x.1 • g x.2) (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) =
    ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i)

Tactic:
rw [sum_smul_sum, ← sum_product']

Premises used: Finset.sum_product', Finset.sum_smul_sum
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn (↑s : Set ι)
f : ι → α
g : ι → β
simp_rw :
  Eq.{u_3 + 1} (α := β)
    (∑
      x ∈
        (range #s).disjiUnion
          (fun (k : ℕ) ↦ map { toFun := fun (i : ι) ↦ (i, (σ ^ k : (a : ι) → ι) i), inj' := ⋯ : ι ↪ ι × ι } s) ⋯,
      f x.1 • g x.2)
    (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
simp_rw₁ :
  Eq.{u_3 + 1} (α := β)
    (∑ i ∈ range #s,
      ∑ x ∈ map { toFun := fun (i_1 : ι) ↦ (i_1, (σ ^ i : (a : ι) → ι) i_1), inj' := ⋯ } s, f x.1 • g x.2)
    (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
simp_rw₂ :
  Eq.{u_3 + 1} (α := β)
    (∑ x ∈ range #s,
      ∑ x_1 ∈ s,
        f (({ toFun := fun (i : ι) ↦ (i, (σ ^ x : (a : ι) → ι) i), inj' := ⋯ : ι ↪ ι × ι } : (a : ι) → ι × ι) x_1).1 •
          g (({ toFun := fun (i : ι) ↦ (i, (σ ^ x : (a : ι) → ι) i), inj' := ⋯ : ι ↪ ι × ι } : (a : ι) → ι × ι) x_1).2)
    (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
⊢ Eq.{u_3 + 1} (α := β) (∑ x ∈ s ×ˢ s, f x.1 • g x.2) (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))

Tactic:
simp_rw [product_self_eq_disjiUnion_perm hσ, sum_disjiUnion, sum_map, Embedding.coeFn_mk]

Premises used: Finset.sum_map, Function.Embedding.coeFn_mk, Finset.sum_disjiUnion, Finset.product_self_eq_disjiUnion_perm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn (↑s : Set ι)
f g : ι → α
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) = ∑ k ∈ range #s, ∑ i ∈ s, f i * g ((σ ^ k : (a : ι) → ι) i)

Tactic:
sum_smul_sum_eq_sum_perm hσ f g

Premises used: Finset.sum_smul_sum_eq_sum_perm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
n : ℕ
x : α
hx : x ∈ s
⊢ Eq (α := α)
    ((↑((g.subtypePerm (p := Membership.mem s) hs ^ n : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) :
        α) :
      α)
    ((g ^ n : (a : α) → α) x : α)

Tactic:
simp only [subtypePerm_pow, subtypePerm_apply]

Premises used: Equiv.Perm.subtypePerm_apply, Equiv.Perm.subtypePerm_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
i : ℤ
x : α
hx : x ∈ s
⊢ Eq (α := α)
    ((↑((g.subtypePerm (p := Membership.mem s) hs ^ i : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) :
        α) :
      α)
    ((g ^ i : (a : α) → α) x : α)

Tactic:
simp only [subtypePerm_zpow, subtypePerm_apply]

Premises used: Equiv.Perm.subtypePerm_zpow, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
rw : ¬g = 1
⊢ g.support.Nonempty

Tactic:
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty_iff]

Premises used: Equiv.Perm.support_eq_empty_iff, Finset.nonempty_iff_ne_empty, ne_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1

Tactic:
IsCycle.ne_one hg

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1

Tactic:
exact IsCycle.ne_one hg

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
mp :
  Commute g c →
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (g.subtypePerm (p := Membership.mem c.support) hc')
mpr :
  (∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (g.subtypePerm (p := Membership.mem c.support) hc')) →
    Commute g c
⊢ Commute g c ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (g.subtypePerm (p := Membership.mem c.support) hc')

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
⊢ ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support

Tactic:
have hgc' := mem_support_iff_of_commute hgc
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
h :
  Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')
⊢ ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hc')

Tactic:
use hgc'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
h :
  ∀ (a : α) (ha : a ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hgc')
⊢ Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')

Tactic:
obtain ⟨a, ha⟩ := IsCycle.nonempty_support hc

Premises used: Equiv.Perm.IsCycle.nonempty_support