ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ (IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a) ↔ x ∈ support f
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ support f
rw [mem_cycleFactorsFinset_iff]
case mp
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ (IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a) → x ∈ support f

case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ x ∈ support f → IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ (IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a) ↔ x ∈ support f
constructor
case mp.intro
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hc : IsCycle (cycleOf f x)
right✝ : ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
⊢ x ∈ support f
case mp
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ (IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a) → x ∈ support f
rintro ⟨hc, _⟩
case mp.intro
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
right✝ : ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
hc : ¬x ∈ support f
⊢ ¬IsCycle (cycleOf f x)
case mp.intro
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hc : IsCycle (cycleOf f x)
right✝ : ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
⊢ x ∈ support f
contrapose! hc
case mp.intro
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
right✝ : ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
hc✝ : ↑f x = x
hc : cycleOf f x = 1
⊢ ¬IsCycle (cycleOf f x)
case mp.intro
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
right✝ : ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
hc : ¬x ∈ support f
⊢ ¬IsCycle (cycleOf f x)
rw [not_mem_support, ← cycleOf_eq_one_iff] at hc
no goals
case mp.intro
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
right✝ : ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
hc✝ : ↑f x = x
hc : cycleOf f x = 1
⊢ ¬IsCycle (cycleOf f x)
simp [hc]
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
⊢ IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
⊢ x ∈ support f → IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
intro hx
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
⊢ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
⊢ IsCycle (cycleOf f x) ∧ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
refine' ⟨isCycle_cycleOf _ (mem_support.mp hx), _⟩
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : y ∈ support (cycleOf f x)
⊢ ↑(cycleOf f x) y = ↑f y
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
⊢ ∀ (a : α), a ∈ support (cycleOf f x) → ↑(cycleOf f x) a = ↑f a
intro y hy
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
⊢ ↑(cycleOf f x) y = ↑f y
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : y ∈ support (cycleOf f x)
⊢ ↑(cycleOf f x) y = ↑f y
rw [mem_support] at hy
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
⊢ (if SameCycle f x y then ↑f y else y) = ↑f y
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
⊢ ↑(cycleOf f x) y = ↑f y
rw [cycleOf_apply]
case mpr.inl
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
H : SameCycle f x y
⊢ ↑f y = ↑f y

case mpr.inr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
H : ¬SameCycle f x y
⊢ y = ↑f y
case mpr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
⊢ (if SameCycle f x y then ↑f y else y) = ↑f y
split_ifs with H
no goals
case mpr.inl
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
H : SameCycle f x y
⊢ ↑f y = ↑f y
rfl
case mpr.inr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : y ≠ y
H : ¬SameCycle f x y
⊢ y = ↑f y
case mpr.inr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : ↑(cycleOf f x) y ≠ y
H : ¬SameCycle f x y
⊢ y = ↑f y
rw [cycleOf_apply_of_not_sameCycle H] at hy
no goals
case mpr.inr
ι : Type ?u.2742928
α : Type u_1
β : Type ?u.2742934
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f : Perm α
x : α
hx : x ∈ support f
y : α
hy : y ≠ y
H : ¬SameCycle f x y
⊢ y = ↑f y
contradiction