-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem product_self_eq_disjiUnion_perm (hf : f.IsCycleOn s) :
    s ×ˢ s =
      (range #s).disjiUnion
        (fun k => s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩)
        (product_self_eq_disjiUnion_perm_aux hf)

Proof state:
case h.mk.refine_1
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b

Tactic:
obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2

Result:
case h.mk.refine_1.intro.intro
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = (f ^ n) a

Proof state:
case h.mk.refine_1.intro.intro
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = (f ^ n) a

Tactic:
exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩

Result:
no goals

Proof state:
case h.mk.refine_2.intro.intro.intro.intro.intro
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
n : ℕ
a : α
ha : a ∈ s
⊢ a ∈ s ∧ (⇑f)^[n] a ∈ s

Tactic:
exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩

Result:
no goals

Proof state:
case h.mk
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔ (a, b) ∈ (range #s).disjiUnion (fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯

Tactic:
simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
  Function.Embedding.coeFn_mk, Prod.mk.inj_iff, exists_prop]

Result:
case h.mk
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b

Proof state:
case h.mk
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b

Tactic:
refine ⟨fun hx => ?_, ?_⟩

Result:
case h.mk.refine_1
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b

case h.mk.refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s

Proof state:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ (⇑f)^[n] a = (f ^ n) a

Tactic:
rw [f.iterate_eq_pow]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
⊢ s ×ˢ s = (range #s).disjiUnion (fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔ (a, b) ∈ (range #s).disjiUnion (fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯

Proof state:
case h.mk.refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s

Tactic:
rintro ⟨n, -, a, ha, rfl, rfl⟩

Result:
case h.mk.refine_2.intro.intro.intro.intro.intro
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
n : ℕ
a : α
ha : a ∈ s
⊢ a ∈ s ∧ (⇑f)^[n] a ∈ s