case h.mk
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔ (a, b) ∈ ⋃ (n : ℤ), (fun a => (a, ↑(f ^ n) a)) '' s
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
⊢ s ×ˢ s = ⋃ (n : ℤ), (fun a => (a, ↑(f ^ n) a)) '' s
ext ⟨a, b⟩
case h.mk
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, b)
case h.mk
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔ (a, b) ∈ ⋃ (n : ℤ), (fun a => (a, ↑(f ^ n) a)) '' s
simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
case h.mk.refine'_1
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, b)

case h.mk.refine'_2
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
⊢ (∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s
case h.mk
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, b)
refine' ⟨fun hx => _, _⟩
case h.mk.refine'_1.intro
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a : α
n : ℤ
hx : a ∈ s ∧ ↑(f ^ n) a ∈ s
⊢ ∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, ↑(f ^ n) a)
case h.mk.refine'_1
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, b)
obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
no goals
case h.mk.refine'_1.intro
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a : α
n : ℤ
hx : a ∈ s ∧ ↑(f ^ n) a ∈ s
⊢ ∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, ↑(f ^ n) a)
exact ⟨_, _, hx.1, rfl⟩
case h.mk.refine'_2.intro.intro.intro.refl
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ ↑(f ^ n) a ∈ s
case h.mk.refine'_2
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a b : α
⊢ (∃ i x, x ∈ s ∧ (x, ↑(f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s
rintro ⟨n, a, ha, ⟨⟩⟩
no goals
case h.mk.refine'_2.intro.intro.intro.refl
ι : Type ?u.3084179
α : Type u_1
β : Type ?u.3084185
inst✝ : DecidableEq α
f : Perm α
s : Set α
hf : IsCycleOn f s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ ↑(f ^ n) a ∈ s
exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩