case refine_1
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝¹ y : α
f : Perm α
x x✝ : α
h : ↑f x✝ ∈ ↑(support (cycleOf f x))
⊢ SameCycle f x x✝ ∧ x ∈ support f

case refine_2
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝¹ y : α
f : Perm α
x x✝ : α
h : x✝ ∈ ↑(support (cycleOf f x))
⊢ SameCycle f x (↑f x✝) ∧ x ∈ support f
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ ∀ (a : α), ↑f a ∈ ↑(support (cycleOf f x)) ↔ a ∈ ↑(support (cycleOf f x))
refine fun _ ↦ ⟨fun h ↦ mem_support_cycleOf_iff.2 ?_, fun h ↦ mem_support_cycleOf_iff.2 ?_⟩
no goals
case refine_1
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝¹ y : α
f : Perm α
x x✝ : α
h : ↑f x✝ ∈ ↑(support (cycleOf f x))
⊢ SameCycle f x x✝ ∧ x ∈ support f
exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff.1 h).1,
(mem_support_cycleOf_iff.1 h).2⟩
no goals
case refine_2
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝¹ y : α
f : Perm α
x x✝ : α
h : x✝ ∈ ↑(support (cycleOf f x))
⊢ SameCycle f x (↑f x✝) ∧ x ∈ support f
exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff.1 h).1,
(mem_support_cycleOf_iff.1 h).2⟩
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x a : α
ha : SameCycle f x a ∧ x ∈ support f
b : α
hb : SameCycle f x b ∧ x ∈ support f
⊢ SameCycle f a b
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x a : α
ha : a ∈ ↑(support (cycleOf f x))
b : α
hb : b ∈ ↑(support (cycleOf f x))
⊢ SameCycle f a b
rw [mem_coe, mem_support_cycleOf_iff] at ha hb
no goals
ι : Type ?u.2583510
α : Type u_1
β : Type ?u.2583516
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x a : α
ha : SameCycle f x a ∧ x ∈ support f
b : α
hb : SameCycle f x b ∧ x ∈ support f
⊢ SameCycle f a b
exact ha.1.symm.trans hb.1