-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} :
    cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support

Proof state:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : x ∉ f.support
⊢ ¬(f.cycleOf x).IsCycle

Tactic:
rw [not_mem_support, ← cycleOf_eq_one_iff] at hc

Result:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : f.cycleOf x = 1
⊢ ¬(f.cycleOf x).IsCycle

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support → (f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Tactic:
intro hx

Result:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
⊢ (f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Proof state:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : f.cycleOf x = 1
⊢ ¬(f.cycleOf x).IsCycle

Tactic:
simp [hc]

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
⊢ (if f.SameCycle x y then f y else y) = f y

Tactic:
split_ifs with H

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
H : f.SameCycle x y
⊢ f y = f y

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
H : ¬f.SameCycle x y
⊢ y = f y

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
⊢ (f.cycleOf x) y = f y

Tactic:
rw [cycleOf_apply]

Result:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
⊢ (if f.SameCycle x y then f y else y) = f y

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
H : ¬f.SameCycle x y
⊢ y = f y

Tactic:
rw [cycleOf_apply_of_not_sameCycle H] at hy

Result:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ≠ y
H : ¬f.SameCycle x y
⊢ y = f y

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
⊢ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Tactic:
intro y hy

Result:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ∈ (f.cycleOf x).support
⊢ (f.cycleOf x) y = f y

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
⊢ (f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Tactic:
refine ⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩

Result:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
⊢ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
H : f.SameCycle x y
⊢ f y = f y

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) ↔ x ∈ f.support

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) → x ∈ f.support

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support → (f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ≠ y
H : ¬f.SameCycle x y
⊢ y = f y

Tactic:
contradiction

Result:
no goals

Proof state:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hc : (f.cycleOf x).IsCycle
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
⊢ x ∈ f.support

Tactic:
contrapose! hc

Result:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : x ∉ f.support
⊢ ¬(f.cycleOf x).IsCycle

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) → x ∈ f.support

Tactic:
rintro ⟨hc, _⟩

Result:
case mp.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hc : (f.cycleOf x).IsCycle
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
⊢ x ∈ f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support

Tactic:
rw [mem_cycleFactorsFinset_iff]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) ↔ x ∈ f.support

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ∈ (f.cycleOf x).support
⊢ (f.cycleOf x) y = f y

Tactic:
rw [mem_support] at hy

Result:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
⊢ (f.cycleOf x) y = f y