case inl
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
hs : Set.Subsingleton ↑s
⊢ Set.PairwiseDisjoint ↑(range (card s)) fun k =>
    map
      { toFun := fun i => (i, ↑(f ^ k) i),
        inj' :=
          (_ :
            ∀ (i j : α),
              (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
      s

case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
⊢ Set.PairwiseDisjoint ↑(range (card s)) fun k =>
    map
      { toFun := fun i => (i, ↑(f ^ k) i),
        inj' :=
          (_ :
            ∀ (i j : α),
              (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
      s
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
⊢ Set.PairwiseDisjoint ↑(range (card s)) fun k =>
    map
      { toFun := fun i => (i, ↑(f ^ k) i),
        inj' :=
          (_ :
            ∀ (i j : α),
              (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
      s
obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
no goals
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
⊢ Set.PairwiseDisjoint ↑(range (card s)) fun k =>
    map
      { toFun := fun i => (i, ↑(f ^ k) i),
        inj' :=
          (_ :
            ∀ (i j : α),
              (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
      s
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)
case inl
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
hs : Set.Subsingleton ↑s
⊢ Set.Subsingleton ↑(range (card s))
case inl
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
hs : Set.Subsingleton ↑s
⊢ Set.PairwiseDisjoint ↑(range (card s)) fun k =>
    map
      { toFun := fun i => (i, ↑(f ^ k) i),
        inj' :=
          (_ :
            ∀ (i j : α),
              (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
      s
refine' Set.Subsingleton.pairwise _ _
case inl
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
hs : card s ≤ 1
⊢ card (range (card s)) ≤ 1
case inl
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
hs : Set.Subsingleton ↑s
⊢ Set.Subsingleton ↑(range (card s))
simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs⊢
no goals
case inl
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
hs : card s ≤ 1
⊢ card (range (card s)) ≤ 1
rwa [card_range]
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
⊢ (_root_.Disjoint on fun k =>
      map
        { toFun := fun i => (i, ↑(f ^ k) i),
          inj' :=
            (_ :
              ∀ (i j : α),
                (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                  ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
        s)
    m n
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
⊢ Set.PairwiseDisjoint ↑(range (card s)) fun k =>
    map
      { toFun := fun i => (i, ↑(f ^ k) i),
        inj' :=
          (_ :
            ∀ (i j : α),
              (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
      s
rintro m hm n hn hmn
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
⊢ ∀ (a b x : α), x ∈ s → x = a → ↑(f ^ m) x = b → ∀ (x : α), x ∈ s → x = a → ¬↑(f ^ n) x = b
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
⊢ (_root_.Disjoint on fun k =>
      map
        { toFun := fun i => (i, ↑(f ^ k) i),
          inj' :=
            (_ :
              ∀ (i j : α),
                (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j →
                  ((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) }
        s)
    m n
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]
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
a : α
ha : a ∈ s
h : ↑(f ^ n) a = ↑(f ^ m) a
⊢ False
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
⊢ ∀ (a b x : α), x ∈ s → x = a → ↑(f ^ m) x = b → ∀ (x : α), x ∈ s → x = a → ¬↑(f ^ n) x = b
rintro _ _ _ - rfl rfl a ha rfl h
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD card s]
⊢ False
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
a : α
ha : a ∈ s
h : ↑(f ^ n) a = ↑(f ^ m) a
⊢ False
rw [hf.pow_apply_eq_pow_apply ha] at h
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m < card s
n : ℕ
hn : n < card s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD card s]
⊢ False
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m ∈ ↑(range (card s))
n : ℕ
hn : n ∈ ↑(range (card s))
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD card s]
⊢ False
rw [mem_coe, mem_range] at hm hn
no goals
case inr
ι : Type ?u.3115870
α : Type u_1
β : Type ?u.3115876
inst✝ : DecidableEq α
f : Perm α
s : Finset α
hf : IsCycleOn f ↑s
h✝ : Set.Nontrivial ↑s
m : ℕ
hm : m < card s
n : ℕ
hn : n < card s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD card s]
⊢ False
exact hmn.symm (h.eq_of_lt_of_lt hn hm)