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

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
⊢ (↑(range #s)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s

Tactic:
rintro m hm n hn hmn

Result:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
⊢ (Disjoint on fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) m n

Proof state:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : (↑s).Subsingleton
⊢ (↑(range #s)).Subsingleton

Tactic:
simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢

Result:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #(range #s) ≤ 1

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

Tactic:
obtain hs | _ := (s : Set α).subsingleton_or_nontrivial

Result:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : (↑s).Subsingleton
⊢ (↑(range #s)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s

case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
⊢ (↑(range #s)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
⊢ (↑(range #s)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s

Tactic:
classical
  rintro m hm n hn hmn
  simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk, exists_prop,
    not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk.inj_iff]
  rintro _ _ _ - rfl rfl a ha rfl h
  rw [hf.pow_apply_eq_pow_apply ha] at h
  rw [mem_coe, mem_range] at hm hn
  exact hmn.symm (h.eq_of_lt_of_lt hn hm)

Result:
no goals

Proof state:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #(range #s) ≤ 1

Tactic:
rwa [card_range]

Result:
no goals

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
exact hmn.symm (h.eq_of_lt_of_lt hn hm)

Result:
no goals

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
⊢ (Disjoint on fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) m n

Tactic:
simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk, exists_prop,
  not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk.inj_iff]

Result:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
⊢ ∀ (a b x : α), x ∈ s → x = a → (f ^ m) x = b → ∀ x ∈ s, x = a → ¬(f ^ n) x = b

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

Tactic:
refine Set.Subsingleton.pairwise ?_ _

Result:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : (↑s).Subsingleton
⊢ (↑(range #s)).Subsingleton

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
rw [mem_coe, mem_range] at hm hn

Result:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
⊢ ∀ (a b x : α), x ∈ s → x = a → (f ^ m) x = b → ∀ x ∈ s, x = a → ¬(f ^ n) x = b

Tactic:
rintro _ _ _ - rfl rfl a ha rfl h

Result:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
a : α
ha : a ∈ s
h : (f ^ n) a = (f ^ m) a
⊢ False

Proof state:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
a : α
ha : a ∈ s
h : (f ^ n) a = (f ^ m) a
⊢ False

Tactic:
rw [hf.pow_apply_eq_pow_apply ha] at h

Result:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False