awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : (f : (a : α) → α) y ≠ y
i : ℤ
h : ((f ^ n) ^ i : (a : α) → α) x = y
⊢ (f ^ ((↑n : ℤ) * i) : (a : α) → α) x = y
have rwa : (HPow.hPow (β := ℤ) f (↑n : ℤ) ^ i : (a : α) → α) x = y
Tactic: rwa [zpow_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle
have ofNat : ∀ (a : ℕ) (h1 : (f ^ Int.ofNat a).IsCycle) (h2 : f.support ⊆ (f ^ Int.ofNat a).support), f.IsCycle
Tactic: cases n
Cleared hypotheses: n, h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
ofNat : ∀ (a : ℕ) (h1 : (f ^ Int.ofNat a).IsCycle) (h2 : f.support ⊆ (f ^ Int.ofNat a).support), f.IsCycle
⊢ f.IsCycle
have negSucc : ∀ (a : ℕ) (h1 : (f ^ Int.negSucc a).IsCycle) (h2 : f.support ⊆ (f ^ Int.negSucc a).support), f.IsCycle
Tactic: cases n
Cleared hypotheses: n, h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ Int.negSucc a).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a).support
⊢ f.IsCycle
have h1₁ : (f ^ (a + 1))⁻¹.IsCycle
Tactic: simp only [zpow_negSucc, Perm.support_inv] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ Int.negSucc a).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a).support
h1₁ : (f ^ (a + 1))⁻¹.IsCycle
⊢ f.IsCycle
have h2₁ : f.support ⊆ (f ^ (a + 1)).support
Tactic: simp only [zpow_negSucc, Perm.support_inv] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ f.support = g.support
have refine : g.support ≤ f.support
Tactic: refine le_antisymm h ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
⊢ z ∈ f.support
have obtain : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), (∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y) → z ∈ f.support
Tactic: obtain ⟨x, hx, _⟩ := id hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ z ∈ f.support
have hx' : (g : (a : α) → α) x ≠ x
Tactic: have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
⊢ z ∈ f.support
have obtain : ∀ (m : ℕ) (hm : (g ^ m : (a : α) → α) x = z), z ∈ f.support
Tactic: obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
m : ℕ
hm : (g ^ m : (a : α) → α) x = z
⊢ z ∈ f.support
have h'' : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
m : ℕ
hm : (g ^ m : (a : α) → α) x = z
h'' : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ z ∈ f.support
have rwa : Membership.mem (α := α) f.support ((g ^ m : (a : α) → α) x : α)
Tactic: rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
m : ℕ
hm : (g ^ m : (a : α) → α) x = z
h'' : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
rwa : Membership.mem (α := α) f.support ((g ^ m : (a : α) → α) x : α)
⊢ z ∈ f.support
have rwa₁ : Membership.mem (α := α) f.support ((f ^ m : (a : α) → α) x : α)
Tactic: rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
m : ℕ
hm : (g ^ m : (a : α) → α) x = z
h'' : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
rwa : Membership.mem (α := α) f.support ((g ^ m : (a : α) → α) x : α)
rwa₁ : Membership.mem (α := α) f.support ((f ^ m : (a : α) → α) x : α)
⊢ z ∈ f.support
have rwa₂ : x ∈ f.support
Tactic: rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ f = g
have this : f.support = g.support
Tactic: have : f.support = g.support := by
    refine le_antisymm h ?_
    intro z hz
    obtain ⟨x, hx, _⟩ := id hf
    have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
    obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
    have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
    rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
this : f.support = g.support
⊢ f = g
have refine : ∀ x ∈ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: refine Equiv.Perm.support_congr h ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
⊢ x ∈ g.support
have rwa : (g : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
rwa : (g : (a : α) → α) x ≠ x
⊢ x ∈ g.support
have rwa₁ : (f : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
⊢ f = g
have hx'' : x ∈ g.support
Tactic: have hx'' : x ∈ g.support := by rwa [mem_support, ← hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
y : α
hy : y ∈ f.support
⊢ y ∈ g.support
have obtain : ∀ (k : ℕ) (hy : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) x : α)),
  Membership.mem (α := α) g.support ((f ^ k : (a : α) → α) x : α)
Tactic: obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
k : ℕ
hy : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) x : α)
⊢ Membership.mem (α := α) g.support ((f ^ k : (a : α) → α) x : α)
have rwa : Membership.mem (α := α) g.support ((g ^ k : (a : α) → α) x : α)
Tactic: rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
⊢ f = g
have this : f.support ⊆ g.support
Tactic: have : f.support ⊆ g.support := by
    intro y hy
    obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
    rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g
have h₁ : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: rw [inter_eq_left.mpr this] at h
Cleared hypotheses: h, hx, hx', hx'', this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support ↔ ¬orderOf f ∣ n
have rw : (f ^ n).support = f.support ↔ ¬f ^ n = 1
Tactic: rw [orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support ↔ ¬f ^ n = 1
have mp : (f ^ n).support = f.support → ¬f ^ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
mp : (f ^ n).support = f.support → ¬f ^ n = 1
⊢ (f ^ n).support = f.support ↔ ¬f ^ n = 1
have mpr : ¬f ^ n = 1 → (f ^ n).support = f.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
⊢ False
have mp : f = 1
Tactic: refine hf.ne_one ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
⊢ f = 1
have mp : f.support = ∅
Tactic: rw [← support_eq_empty_iff, ← h, H, support_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
mp : f.support = ∅
⊢ f = 1
have mp₁ : (f ^ n).support = ∅
Tactic: rw [← support_eq_empty_iff, ← h, H, support_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
mp : f.support = ∅
mp₁ : (f ^ n).support = ∅
⊢ f = 1
have mp₂ : Eq.{u_2 + 1} (α := Finset α) (support 1) ∅
Tactic: rw [← support_eq_empty_iff, ← h, H, support_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
mp : f.support = ∅
mp₁ : (f ^ n).support = ∅
mp₂ : Eq.{u_2 + 1} (α := Finset α) (support 1) ∅
⊢ f = 1
have mp₃ : Eq.{u_2 + 1} (α := Finset α) ∅ ∅
Tactic: rw [← support_eq_empty_iff, ← h, H, support_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
H : ¬f ^ n = 1
⊢ (f ^ n).support = f.support
have apply : f.support ≤ (f ^ n).support
Tactic: apply le_antisymm (support_pow_le _ n) _
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
H : ¬f ^ n = 1
x : α
hx : x ∈ f.support
⊢ x ∈ (f ^ n).support
have contrapose : ∀ (H : x ∉ (f ^ n).support), f ^ n = 1
Tactic: contrapose H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
⊢ f ^ n = 1
have H₁ : ∀ (z : α), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
Tactic: ext z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
have pos : ∀ (hz : (f : (a : α) → α) z = z), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
Tactic: by_cases hz : f z = z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
pos : ∀ (hz : (f : (a : α) → α) z = z), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
have neg : ∀ (hz : ¬(f : (a : α) → α) z = z), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
Tactic: by_cases hz : f z = z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : (f : (a : α) → α) z = z
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
have pos : z = (1 : (a : α) → α) z
Tactic: rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : (f : (a : α) → α) z = z
pos : z = (1 : (a : α) → α) z
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
have pos₁ : z = z
Tactic: rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬(f : (a : α) → α) z = z
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
have neg : ∀ (k : ℕ) (hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α))
  (H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support),
  Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
Tactic: obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
Cleared hypotheses: x, hx, H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬(f : (a : α) → α) z = z
k : ℕ
hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α)
H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
have neg : Eq (α := α) ((f ^ k : (a : α) → α) ((f ^ n : (a : α) → α) z : α) : α)
  ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)
Tactic: apply (f ^ k).injective
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬(f : (a : α) → α) z = z
k : ℕ
hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α)
H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support
⊢ Eq (α := α) ((f ^ k : (a : α) → α) ((f ^ n : (a : α) → α) z : α) : α)
    ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)
have neg : Eq (α := α) ((f ^ n : (a : α) → α) ((f ^ k : (a : α) → α) z : α) : α)
  ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)
Tactic: rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
-- 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: 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).IsCycle ↔ n.Coprime (orderOf f)
have intro : (f ^ n).IsCycle → n.Coprime (orderOf f)
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).IsCycle → n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
have intro₁ : n.Coprime (orderOf f) → (f ^ n).IsCycle
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).IsCycle
⊢ (f ^ n).support = f.support
have rw : ¬orderOf f ∣ n
Tactic: rw [hf.support_pow_eq_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 β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
⊢ False
have refine : f ^ (orderOf f * k) = 1
Tactic: refine h.ne_one ?_
-- 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 : (f ^ n).IsCycle
⊢ n.Coprime (orderOf f)
have hr : (f ^ n).support = f.support
Tactic: 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]
-- 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
⊢ orderOf (f ^ n) = orderOf f
have rw : #(f ^ n).support = orderOf f
Tactic: rw [h.orderOf, hr, hf.orderOf]
-- 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
rw : #(f ^ n).support = orderOf f
⊢ orderOf (f ^ n) = orderOf f
have rw₁ : #f.support = orderOf f
Tactic: rw [h.orderOf, hr, hf.orderOf]
-- 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
rw : #(f ^ n).support = orderOf f
rw₁ : #f.support = orderOf f
⊢ orderOf (f ^ n) = orderOf f
have rw₂ : #f.support = #f.support
Tactic: rw [h.orderOf, hr, hf.orderOf]
-- 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 : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ n.Coprime (orderOf f)
have this : orderOf (f ^ n) = orderOf f
Tactic: have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
-- 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 : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf (f ^ n) = orderOf f
⊢ n.Coprime (orderOf f)
have this₁ : orderOf f = 0 ∨ (orderOf f).gcd n = 1
Tactic: rw [orderOf_pow, Nat.div_eq_self] 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
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf f = 0 ∨ (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)
have intro : ∀ (h : orderOf f = 0), n.Coprime (orderOf f)
Tactic: rcases this with h | _
Cleared hypotheses: this