awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf f = 0 ∨ (orderOf f).gcd n = 1
intro : ∀ (h : orderOf f = 0), n.Coprime (orderOf f)
⊢ n.Coprime (orderOf f)
have intro₁ : (orderOf f).gcd n = 1 → n.Coprime (orderOf f)
Tactic: rcases this with h | _
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h_1 : (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)
have intro : n.gcd (orderOf f) = 1
Tactic: rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle
have intro : ∀ (m : ℕ) (hm : (f ^ n) ^ m = f), (f ^ n).IsCycle
Tactic: obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ (f ^ n).IsCycle
have hf' : ((f ^ n) ^ m).IsCycle
Tactic: have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle
have intro : ∀ (x : β) (hx : x ∈ (f ^ n).support), x ∈ ((f ^ n) ^ m).support
Tactic: refine hf'.of_pow fun x hx => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ ((f ^ n) ^ m).support
have intro : x ∈ f.support
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
have intro : ∀ (val : Fintype β), (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine hf'.of_pow fun x hx => ?_
      rw [hm]
      exact support_pow_le _ n hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
have intro₁ : ∀ (val : Fintype β), (f ^ n).IsCycle → n.Coprime (orderOf f)
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine hf'.of_pow fun x hx => ?_
      rw [hm]
      exact support_pow_le _ n hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
intro₁ : ∀ (val : Fintype β), (f ^ n).IsCycle → n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
have intro₂ : ∀ (val : Fintype β), n.Coprime (orderOf f) → (f ^ n).IsCycle
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine hf'.of_pow fun x hx => ?_
      rw [hm]
      exact support_pow_le _ n hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro : ∀ (val : Fintype β), f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro : f ^ n = 1 → ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
intro : f ^ n = 1 → ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro₁ : (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x) → f ^ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : f ^ n = 1
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro : ∀ (x : β) (hx : (f : (a : β) → β) x ≠ x), ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
Tactic: obtain ⟨x, hx, -⟩ := id hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
⊢ f ^ n = 1
have pos : ∀ (h : (f ^ n).support = f.support), f ^ n = 1
Tactic: by_cases h : support (f ^ n) = support f
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
pos : ∀ (h : (f ^ n).support = f.support), f ^ n = 1
⊢ f ^ n = 1
have neg : ∀ (h : ¬(f ^ n).support = f.support), f ^ n = 1
Tactic: by_cases h : support (f ^ n) = support f
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1
have hx₁ : (f ^ n : (a : β) → β) x ≠ x
Tactic: rw [← mem_support, ← h, mem_support] at hx
Cleared hypotheses: hx, hx', h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : ¬(f ^ n).support = f.support
⊢ f ^ n = 1
have h₁ : orderOf f ∣ n
Tactic: rw [hf.support_pow_eq_iff, Classical.not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1
have neg : ∀ (k : ℕ) (hx' : (f ^ (orderOf f * k) : (a : β) → β) x = x), f ^ (orderOf f * k) = 1
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: n, hx', h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k) : (a : β) → β) x = x
⊢ f ^ (orderOf f * k) = 1
have neg : (f ^ orderOf f) ^ k = 1
Tactic: rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k) : (a : β) → β) x = x
neg : (f ^ orderOf f) ^ k = 1
⊢ f ^ (orderOf f * k) = 1
have neg₁ : HPow.hPow (α := Perm β) 1 k = 1
Tactic: rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k) : (a : β) → β) x = x
neg : (f ^ orderOf f) ^ k = 1
neg₁ : HPow.hPow (α := Perm β) 1 k = 1
⊢ f ^ (orderOf f * k) = 1
have neg₂ : Eq.{u_3 + 1} (α := Perm β) 1 1
Tactic: rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro : ∀ (val : Fintype β), f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro₁ : ∀ (val : Fintype β), f ^ n = 1 → ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
intro₁ : ∀ (val : Fintype β), f ^ n = 1 → ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
have intro₂ : ∀ (val : Fintype β), (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x) → f ^ n = 1
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro : ∀ (val : Fintype β),
  f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro : f ^ a = f ^ b →
  ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
intro :
  f ^ a = f ^ b →
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro₁ : (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) →
  f ^ a = f ^ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
h : f ^ a = f ^ b
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro : ∀ (x : β) (hx : (f : (a : β) → β) x ≠ x),
  ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
Tactic: obtain ⟨x, hx, -⟩ := id hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
⊢ f ^ a = f ^ b
have intro : ∀
  (this :
    ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b),
      f ^ a = f ^ b)
  (hab : ¬a ≤ b), f ^ a = f ^ b
Tactic: wlog hab : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
intro :
  ∀
    (this :
      ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b),
        f ^ a = f ^ b)
    (hab : ¬a ≤ b), f ^ a = f ^ b
⊢ f ^ a = f ^ b
have wlog : ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b), f ^ a = f ^ b
Tactic: wlog hab : a ≤ b generalizing a b
Cleared hypotheses: a, b, hx'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
this : f ^ (b - a) = 1
⊢ f ^ a = f ^ b
have this₁ : f ^ b = f ^ a
Tactic: rw [pow_sub _ hab, mul_inv_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b
have rw : f ^ a = f ^ a
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
⊢ f ^ a = f ^ b
have suffices : f ^ (b - a) = 1
Tactic: suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
⊢ f ^ (b - a) = 1
have rw : ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
Tactic: rw [hf.pow_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
have pos : ∀ (hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)),
  ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
Tactic: by_cases hfa : (f ^ a) x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
pos :
  ∀ (hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)),
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
have neg : ∀ (hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support),
  ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
Tactic: by_cases hfa : (f ^ a) x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
have pos : Eq (α := β) ((f ^ (b - a) : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β) ((f ^ a : (a : β) → β) x : β)
Tactic: refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
have h : Eq (α := β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) x : β) : β)
  ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) x : β) : β)
Tactic: have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
h :
  Eq (α := β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) x : β) : β)
    ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) x : β) : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
have h₁ : Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β) ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)
Tactic: simp only [zpow_one, zpow_natCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
h :
  Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β)
    ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
have hfa₁ : (f : (a : β) → β) x = x
Tactic: rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
Cleared hypotheses: hfa, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro : ∀ (val : Fintype β),
  f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_ge hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp [pow_sub _ hab, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
intro :
  ∀ (val : Fintype β),
    f ^ a = f ^ b ↔
      ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
have intro₁ : ∀ (val : Fintype β),
  f ^ a = f ^ b →
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
Tactic: classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_ge hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp [pow_sub _ hab, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction