awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
y : α
pos :
  ∀ (hy : (σ : (a : α) → α) y = y),
    Eq (α := α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
have neg : ∀ (hy : ¬(σ : (a : α) → α) y = y),
  Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
Tactic: by_cases hy : σ y = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
y : α
hy : (σ : (a : α) → α) y = y
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
have pos : Eq (α := α) ((σ ^ m : (a : α) → α) y : α) ((σ ^ n : (a : α) → α) y : α)
Tactic: simp_rw [zpow_apply_eq_self_of_apply_eq_self hy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
y : α
hy : ¬(σ : (a : α) → α) y = y
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
have neg : ∀ (i : ℤ)
  (hy :
    ¬Eq (α := α)
        ((σ : (a : α) → α)
            ((σ ^ i : (a : α) → α)
                (Classical.choose (p := fun (x : α) ↦
                  (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
              α) :
          α)
        ((σ ^ i : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α)),
  Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) sorry) :
            Perm α) :
          (a : α) → α)
        ((σ ^ i : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) sorry) :
            Perm α) :
          (a : α) → α)
        ((σ ^ i : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
Tactic: obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
i : ℤ
hy :
  ¬Eq (α := α)
      ((σ : (a : α) → α)
          ((σ ^ i : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
            α) :
        α)
      ((σ ^ i : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦
            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
        α)
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        ((σ ^ i : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        ((σ ^ i : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
have neg : Eq (α := α)
  ((σ ^ i : (a : α) → α)
      ((σ ^ m : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦
            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
        α) :
    α)
  ((σ ^ i : (a : α) → α)
      ((σ ^ n : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦
            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
        α) :
    α)
Tactic: rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
y : α
hy : y ∈ σ.support
⊢ ∃ (a : ↥(Subgroup.zpowers σ)),
    (fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
              (((↑τ : Perm α) : (a : α) → α)
                (Classical.choose (p := fun (x : α) ↦
                  (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
              ⋯ :
            ↥σ.support))
        a =
      Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support) y hy
have hy₁ : (σ : (a : α) → α) y ≠ y
Tactic: rw [mem_support] at hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
y : α
hy_1 : y ∈ σ.support
hy : (σ : (a : α) → α) y ≠ y
⊢ ∃ (a : ↥(Subgroup.zpowers σ)),
    (fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
              (((↑τ : Perm α) : (a : α) → α)
                (Classical.choose (p := fun (x : α) ↦
                  (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
              ⋯ :
            ↥σ.support))
        a =
      Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support) y hy_1
have right : ∀ (n : ℤ)
  (hy :
    Membership.mem (α := α) σ.support
      ((σ ^ n : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦
            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
        α))
  (hy_2 :
    Ne (α := α)
      ((σ : (a : α) → α)
          ((σ ^ n : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
            α) :
        α)
      ((σ ^ n : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦
            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
        α)),
  ∃ (a : ↥(Subgroup.zpowers σ)),
    Eq (α := ↥σ.support)
      ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
                (((↑τ : Perm α) : (a : α) → α)
                  (Classical.choose (p := fun (x : α) ↦
                    (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
                sorry :
              ↥σ.support))
          a :
        ↥σ.support)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
          ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
          hy :
        ↥σ.support)
Tactic: obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy
Cleared hypotheses: y, hy_1, hy
-- 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
⊢ orderOf f = #f.support
have rw : Fintype.card.{u_2} ↥(Subgroup.zpowers f) = Fintype.card.{u_2} ↥f.support
Tactic: rw [← Fintype.card_zpowers, ← Fintype.card_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ : ∀ (hfbx : (f : (a : α) → α) x = b),
  ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
Tactic: obtain hfbx | hfbx := eq_or_ne (f x) b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
succ :
  ∀ (hfbx : (f : (a : α) → α) x = b),
    ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₁ : ∀ (hfbx : (f : (a : α) → α) x ≠ b),
  ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
Tactic: obtain hfbx | hfbx := eq_or_ne (f x) b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
Tactic: have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have hb' : Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
  ((Equiv.symm f : (a : α) → α) b : α)
Tactic: have hb' : (swap x (f x) * f) (f.symm b) ≠ f.symm b := by
      simpa [swap_apply_of_ne_of_ne this.2 hfbx.symm, eq_symm_apply, f.injective.eq_iff]
        using this.1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ : ∀ (i : ℤ)
  (hi :
    Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
      ((Equiv.symm f : (a : α) → α) b : α)),
  ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
Tactic: obtain ⟨i, hi⟩ := hn hb' <| f.injective <| by simpa [pow_succ'] using h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ : ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
Tactic: refine ⟨i + 1, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ : ((swap x ((f : (a : α) → α) x) * f) ^ (1 + i) : (a : α) → α) ((f : (a : α) → α) x : α) = b
Tactic: rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
succ : ((swap x ((f : (a : α) → α) x) * f) ^ (1 + i) : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₁ : (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 * (swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α)
    ((f : (a : α) → α) x : α) =
  b
Tactic: rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
succ : ((swap x ((f : (a : α) → α) x) * f) ^ (1 + i) : (a : α) → α) ((f : (a : α) → α) x : α) = b
succ₁ :
  (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 * (swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α)
      ((f : (a : α) → α) x : α) =
    b
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₂ : (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 : (a : α) → α)
    (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α) =
  b
Tactic: rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]