awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
hx : (f : (a : α) → α) x ≠ x
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
rw : f.SameCycle x y ∧ x ∈ f.support ↔ f.SameCycle x y
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
have rw₁ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [mem_support_cycleOf_iff_aux, and_iff_left (mem_support.2 hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
⊢ (f.cycleOf x).IsCycle ↔ (f : (a : α) → α) x ≠ x
have refine : ∀ (hx : (f.cycleOf x).IsCycle), (f : (a : α) → α) x ≠ x
Tactic: refine ⟨fun hx => ?_, f.isCycle_cycleOf⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ (f : (a : α) → α) x ≠ x
have rw : ¬f.cycleOf x = 1
Tactic: rw [Ne, ← cycleOf_eq_one_iff f]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x : α
⊢ ∀ (a : α),
    Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) a : α) ↔
      a ∈ (↑(f.cycleOf x).support : Set α)
have refine_1 : ∀ (x_1 : α) (h : Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) x_1 : α)),
  f.SameCycle x x_1 ∧ x ∈ f.support
Tactic: refine fun _ ↦
        ⟨fun h ↦ mem_support_cycleOf_iff_aux.2 ?_, fun h ↦ mem_support_cycleOf_iff_aux.2 ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x : α
refine_1 :
  ∀ (x_1 : α) (h : Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) x_1 : α)),
    f.SameCycle x x_1 ∧ x ∈ f.support
⊢ ∀ (a : α),
    Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) a : α) ↔
      a ∈ (↑(f.cycleOf x).support : Set α)
have refine_2 : ∀ (x_1 : α) (h : x_1 ∈ (↑(f.cycleOf x).support : Set α)), f.SameCycle x ((f : (a : α) → α) x_1) ∧ x ∈ f.support
Tactic: refine fun _ ↦
        ⟨fun h ↦ mem_support_cycleOf_iff_aux.2 ?_, fun h ↦ mem_support_cycleOf_iff_aux.2 ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x a : α
ha : a ∈ (↑(f.cycleOf x).support : Set α)
b : α
hb : b ∈ (↑(f.cycleOf x).support : Set α)
⊢ f.SameCycle a b
have rw : ∀ (ha : f.SameCycle x a ∧ x ∈ f.support) (b : α) (hb : f.SameCycle x b ∧ x ∈ f.support), f.SameCycle a b
Tactic: rw [mem_coe, mem_support_cycleOf_iff_aux] at ha hb
Cleared hypotheses: ha, b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i : (a : α) → α) x = y
have hx₁ : (f : (a : α) → α) x ≠ x
Tactic: rw [mem_support] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : (f : (a : α) → α) x ≠ x
⊢ x ∈ (f.cycleOf x).support
have rw : f.SameCycle x x
Tactic: rw [mem_support_cycleOf_iff'_aux hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
⊢ y ∈ List.iterate (⇑f : (a : α) → α) x (Fintype.card α) ↔ f.SameCycle x y
have simp : (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) ↔ f.SameCycle x y
Tactic: simp only [List.mem_iterate, iterate_eq_pow, eq_comm (a := y)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
⊢ (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) ↔ f.SameCycle x y
have mp : (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) → f.SameCycle x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
mp : (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) → f.SameCycle x y
⊢ (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) ↔ f.SameCycle x y
have mpr : f.SameCycle x y → ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have by_cases : ∀ (hx : x ∈ f.support), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
Tactic: by_cases hx : x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
by_cases : ∀ (hx : x ∈ f.support), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have by_cases₁ : ∀ (hx : x ∉ f.support), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
Tactic: by_cases hx : x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∈ f.support
_inst : (f : Perm α) → DecidableRel f.SameCycle := fun (f : Perm α) ↦ Classical.decRel f.SameCycle
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have rcases : ∀ (i : ℕ) (hixy : i < #(f.cycleOf x).support) (hi : (f ^ i : (a : α) → α) x = y),
  ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
Tactic: rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨x⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have hx₁ : (f : (a : α) → α) x = x
Tactic: rw [notMem_support] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have case : ∀ (this : Nonempty α), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
Tactic: case neg =>
        haveI : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
case case₁ case₂ : ∀ (this : Nonempty α), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
have case₃ : ∀ (hx : (f : (a : α) → α) x = x) (this : Nonempty α), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
Tactic: case neg =>
        haveI : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
⊢ 2 ≤ #(f.cycleOf x).support ↔ (f : (a : α) → α) x ≠ x
have refine : ∀ (h : 2 ≤ #(f.cycleOf x).support), (f : (a : α) → α) x ≠ x
Tactic: refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
h : 2 ≤ #(f.cycleOf x).support
⊢ (f : (a : α) → α) x ≠ x
have contrapose! : ∀ (h : (f : (a : α) → α) x = x), #(f.cycleOf x).support < 2
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
h : (f : (a : α) → α) x = x
⊢ #(f.cycleOf x).support < 2
have h₁ : f.cycleOf x = 1
Tactic: rw [← cycleOf_eq_one_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
⊢ (f.cycleOf x).support.Nonempty ↔ (f : (a : α) → α) x ≠ x
have rw : Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support
Tactic: rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
⊢ g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y
have refine : ∀ (h : g.cycleOf x = g.cycleOf y), g.SameCycle x y
Tactic: refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ g.SameCycle x y
have rw : y ∈ (g.cycleOf x).support
Tactic: rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
    mem_support_cycleOf_iff' (mem_support.mp hy)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
rw : y ∈ (g.cycleOf x).support
⊢ g.SameCycle x y
have rw₁ : y ∈ (g.cycleOf y).support
Tactic: rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
    mem_support_cycleOf_iff' (mem_support.mp hy)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
rw : y ∈ (g.cycleOf x).support
rw₁ : y ∈ (g.cycleOf y).support
⊢ g.SameCycle x y
have rw₂ : g.SameCycle y y
Tactic: rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
    mem_support_cycleOf_iff' (mem_support.mp hy)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : y ∈ (f.cycleOf x).support
⊢ y ∈ f.support
have hy₁ : (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y
Tactic: rw [mem_support, cycleOf_apply] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y
⊢ y ∈ f.support
have pos : f.SameCycle x y → ∀ (hy : (f : (a : α) → α) y ≠ y), y ∈ f.support
Tactic: split_ifs at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y
pos : f.SameCycle x y → ∀ (hy : (f : (a : α) → α) y ≠ y), y ∈ f.support
⊢ y ∈ f.support
have neg : ¬f.SameCycle x y → ∀ (hy : y ≠ y), y ∈ f.support
Tactic: split_ifs at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have pos : ∀ (hx : (f : (a : α) → α) x = x),
  Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
pos :
  ∀ (hx : (f : (a : α) → α) x = x),
    Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x),
  Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have pos : x = (f ^ n : (a : α) → α) x
Tactic: rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : (f : (a : α) → α) x = x
pos : x = (f ^ n : (a : α) → α) x
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have pos₁ : x = x
Tactic: rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have neg : Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬(f : (a : α) → α) x = x
neg : Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have neg₁ : Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬(f : (a : α) → α) x = x
neg : Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
neg₁ :
  Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have neg₂ : Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬(f : (a : α) → α) x = x
neg : Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
neg₁ :
  Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
neg₂ :
  Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have neg₃ : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have pos : ∀ (hx : x ∈ f.support), ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
Tactic: by_cases hx : x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
pos : ∀ (hx : x ∈ f.support), ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have neg : ∀ (hx : x ∉ f.support), ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
Tactic: by_cases hx : x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have pos : ∀ (k : ℕ) (hk : k < #(f.cycleOf x).support) (hk' : (f ^ k : (a : α) → α) x = y),
  ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
Tactic: obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k < #(f.cycleOf x).support
hk' : (f ^ k : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have pos : ∀ (hk : 0 < #(f.cycleOf x).support) (hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y),
  ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
Tactic: rcases k with - | k
Cleared hypotheses: k, hk, hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k < #(f.cycleOf x).support
hk' : (f ^ k : (a : α) → α) x = y
pos :
  ∀ (hk : 0 < #(f.cycleOf x).support) (hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y),
    ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have pos₁ : ∀ (k : ℕ) (hk : k + 1 < #(f.cycleOf x).support) (hk' : (f ^ (k + 1) : (a : α) → α) x = y),
  ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
Tactic: rcases k with - | k
Cleared hypotheses: k, hk, hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have pos : (f ^ #(f.cycleOf x).support : (a : α) → α) x = y
Tactic: refine ⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = y
have hk'₁ : x = y
Tactic: simp only [pow_zero, coe_one, id_eq] at hk'
Cleared hypotheses: hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : x = y
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = y
have pos : ∀ (h : f.SameCycle x x), (f ^ #(f.cycleOf x).support : (a : α) → α) x = x
Tactic: subst hk'
Cleared hypotheses: y, h, hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = x
have pos : (f ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
Tactic: rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
pos : (f ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = x
have pos₁ : (f.cycleOf x ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
Tactic: rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
pos : (f ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
pos₁ : (f.cycleOf x ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = x
have pos₂ : (1 : (a : α) → α) x = x
Tactic: rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
pos : (f ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
pos₁ : (f.cycleOf x ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
pos₂ : (1 : (a : α) → α) x = x
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = x
have pos₃ : x = x
Tactic: rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
have neg : (HPow.hPow (β := ℕ) f 1 : (a : α) → α) x = y
Tactic: refine ⟨1, zero_lt_one, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ (HPow.hPow (β := ℕ) f 1 : (a : α) → α) x = y
have neg : ∀ (k : ℤ), Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∉ f.support
k : ℤ
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have neg : ∀ (hx : (f : (a : α) → α) x = x) (k : ℤ),
  Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
Tactic: rw [notMem_support] at hx
Cleared hypotheses: hx, k