-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
    IsCycle f

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle

Tactic:
have key : ∀ x : α, (f ^ n) x ≠ x ↔ f x ≠ x := by
  simp_rw [← mem_support, ← Finset.ext_iff]
  exact (support_pow_le _ n).antisymm h2

Result:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
⊢ f.IsCycle

Proof state:
case intro.intro
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : f y ≠ y
⊢ f.SameCycle x y

Tactic:
obtain ⟨i, _⟩ := hx2 ((key y).mpr hy)

Result:
case intro.intro.intro
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : f y ≠ y
i : ℤ
h✝ : ((f ^ n) ^ i) x = y
⊢ f.SameCycle x y

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : f y ≠ y
i : ℤ
h✝ : ((f ^ n) ^ i) x = y
⊢ (f ^ (↑n * i)) x = y

Tactic:
rwa [zpow_mul]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
⊢ f.IsCycle

Tactic:
obtain ⟨x, hx1, hx2⟩ := h1

Result:
case intro.intro
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
⊢ f.IsCycle

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ (f ^ n).support = f.support

Tactic:
exact (support_pow_le _ n).antisymm h2

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
⊢ f.IsCycle

Tactic:
refine ⟨x, (key x).mp hx1, fun y hy => ?_⟩

Result:
case intro.intro
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : f y ≠ y
⊢ f.SameCycle x y

Proof state:
case intro.intro.intro
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : f y ≠ y
i : ℤ
h✝ : ((f ^ n) ^ i) x = y
⊢ f.SameCycle x y

Tactic:
exact ⟨n * i, by rwa [zpow_mul]⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x

Tactic:
simp_rw [← mem_support, ← Finset.ext_iff]

Result:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ (f ^ n).support = f.support