awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this : Countable.{u_2 + 1} (↑s : Type u_2)
⊢ ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
have this₁ : Infinite.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI := hs'.to_subtype
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
have inr : ∀ (f : ℤ ≃ (↑s : Type u_2)), ∃ (f : Perm α), f.IsCycleOn s ∧ {x : α | (f : (a : α) → α) x ≠ x} ⊆ s
Tactic: obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
have inr : (Perm.extendDomain (Equiv.addRight 1) (p := fun (x : α) ↦ x ∈ s) f).IsCycleOn s
Tactic: refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 s
have 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}
Tactic: convert! Int.addRight_one_isCycle.isCycleOn.extendDomain f
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)
⊢ 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}
have 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})
Tactic: rw [Set.image_comp, Equiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)
⊢ 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})
have 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
Tactic: ext
-- 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: 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
-- 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: 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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
⊢ s ×ˢ s = ⋃ (n : ℤ), (fun (a : α) ↦ (a, (f ^ n : (a : α) → α) a)) '' s
have h : ∀ (a b : α),
  (a, b) ∈ s ×ˢ s ↔
    Membership.mem (γ := Set (α × α)) (⋃ (n : ℤ), (fun (a : α) ↦ (a, (f ^ n : (a : α) → α) a)) '' s) (a, b)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔
    Membership.mem (γ := Set (α × α)) (⋃ (n : ℤ), (fun (a : α) ↦ (a, (f ^ n : (a : α) → α) a)) '' s) (a, b)
have h : a ∈ s ∧ b ∈ s ↔ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)
Tactic: simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)
have h : ∀ (hx : a ∈ s ∧ b ∈ s), ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)
Tactic: refine ⟨fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)
⊢ a ∈ s ∧ b ∈ s ↔ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)
have h₁ : (∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)) → a ∈ s ∧ b ∈ s
Tactic: refine ⟨fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ (i : ℤ), ∃ x ∈ s, (x, (f ^ i : (a : α) → α) x) = (a, b)
have 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) : α × α)
Tactic: obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
Cleared hypotheses: b, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
have 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' := sorry } s
Tactic: obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
have 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' := sorry } s
Tactic: obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
have inl : (↑(range #s) : Set ℕ).Subsingleton
Tactic: refine Set.Subsingleton.pairwise ?_ _
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
hs : (↑s : Set α).Subsingleton
⊢ (↑(range #s) : Set ℕ).Subsingleton
have inl : ∀ (hs : #s ≤ 1), #(range #s) ≤ 1
Tactic: simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ onFun.{1, u_2 + 1, 1} (β := Finset (α × α)) Disjoint
    (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s) m n
have inr : ∀ (a b x : α), x ∈ s → x = a → (f ^ m : (a : α) → α) x = b → ∀ x ∈ s, x = a → ¬(f ^ n : (a : α) → α) x = b
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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 : α)
⊢ False
have h₁ : n ≡ m [MOD #s]
Tactic: rw [hf.pow_apply_eq_pow_apply ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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]
⊢ False
have inr : ∀ (hm : m < #s) ⦃n : ℕ⦄ (hn : n < #s) (hmn : m ≠ n) (a : α) (ha : a ∈ s) (h : n ≡ m [MOD #s]), False
Tactic: rw [mem_coe, mem_range] at hm hn
Cleared hypotheses: hm, n, hn, hmn, a, ha, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
h : (↑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
have 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' := sorry } s) m n
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset (α × α)) (↑(range #s) : Set ℕ) fun (k : ℕ) ↦
    map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s
have inr₄ : ∀ ⦃m : ℕ⦄ (hm : m < #s) ⦃n : ℕ⦄ (hn : n < #s) (hmn : m ≠ n) (a : α) (ha : a ∈ s) (h : n ≡ m [MOD #s]), False
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
⊢ s ×ˢ s =
    (range #s).disjiUnion (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ } s) ⋯
have h : ∀ (a b : α),
  (a, b) ∈ s ×ˢ s ↔
    (a, b) ∈
      (range #s).disjiUnion
        (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := sorry : α ↪ α × α } s) sorry
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔
    (a, b) ∈
      (range #s).disjiUnion
        (fun (k : ℕ) ↦ map { toFun := fun (i : α) ↦ (i, (f ^ k : (a : α) → α) i), inj' := ⋯ : α ↪ α × α } s) ⋯
have h : a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b
Tactic: simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
    Function.Embedding.coeFn_mk, Prod.mk_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
have h : ∀ (hx : a ∈ s ∧ b ∈ s), ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b
Tactic: refine ⟨fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b
have h₁ : (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s
Tactic: refine ⟨fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f : (a : α) → α)^[a_1] a_2 = b
have 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
Tactic: obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
Cleared hypotheses: b, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α)
⊢ (⇑f : (a : α) → α)^[n] a = (f ^ n : (a : α) → α) a
have rw : Eq (α := α) ((f ^ n : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α)
Tactic: rw [f.iterate_eq_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : ι → β
⊢ 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)
have 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))
Tactic: rw [sum_smul_sum, ← sum_product']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : ι → β
⊢ Eq.{u_3 + 1} (α := β) (∑ x ∈ s ×ˢ s, f x.1 • g x.2) (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
have simp_rw : Eq.{u_3 + 1} (α := β)
  (∑
    x ∈
      (range #s).disjiUnion
        (fun (k : ℕ) ↦ map { toFun := fun (i : ι) ↦ (i, (σ ^ k : (a : ι) → ι) i), inj' := sorry : ι ↪ ι × ι } s) sorry,
    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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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))
⊢ Eq.{u_3 + 1} (α := β) (∑ x ∈ s ×ˢ s, f x.1 • g x.2) (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
have simp_rw₁ : Eq.{u_3 + 1} (α := β)
  (∑ i ∈ range #s, ∑ x ∈ map { toFun := fun (i_1 : ι) ↦ (i_1, (σ ^ i : (a : ι) → ι) i_1), inj' := sorry } 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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))
⊢ Eq.{u_3 + 1} (α := β) (∑ x ∈ s ×ˢ s, f x.1 • g x.2) (∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i))
have simp_rw₂ : Eq.{u_3 + 1} (α := β)
  (∑ x ∈ range #s,
    ∑ x_1 ∈ s,
      f (({ toFun := fun (i : ι) ↦ (i, (σ ^ x : (a : ι) → ι) i), inj' := sorry : ι ↪ ι × ι } : (a : ι) → ι × ι) x_1).1 •
        g (({ toFun := fun (i : ι) ↦ (i, (σ ^ x : (a : ι) → ι) i), inj' := sorry : ι ↪ ι × ι } : (a : ι) → ι × ι) x_1).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]