[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ cycleType σ = map (Finset.card ∘ support) s.val
[PROOFSTEP]
rw [cycleType_def]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ map (Finset.card ∘ support) (cycleFactorsFinset σ).val = map (Finset.card ∘ support) s.val
[PROOFSTEP]
congr
[GOAL]
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ cycleFactorsFinset σ = s
[PROOFSTEP]
rw [cycleFactorsFinset_eq_finset]
[GOAL]
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ (f : Perm α), f ∈ s → IsCycle f
h2 : Set.Pairwise (↑s) Disjoint
h0 : Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
⊢ (∀ (f : Perm α), f ∈ s → IsCycle f) ∧
    ∃ h, Finset.noncommProd s id (_ : Set.Pairwise ↑s fun a b => Commute (id a) (id b)) = σ
[PROOFSTEP]
exact ⟨h1, h2, h0⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
⊢ cycleType σ = ↑(List.map (Finset.card ∘ support) l)
[PROOFSTEP]
have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ cycleType σ = ↑(List.map (Finset.card ∘ support) l)
[PROOFSTEP]
rw [cycleType_eq' l.toFinset]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ map (Finset.card ∘ support) (List.toFinset l).val = ↑(List.map (Finset.card ∘ support) l)
[PROOFSTEP]
simp [List.dedup_eq_self.mpr hl, (· ∘ ·)]
[GOAL]
case h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ ∀ (f : Perm α), f ∈ List.toFinset l → IsCycle f
[PROOFSTEP]
simpa using h1
[GOAL]
case h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ Set.Pairwise (↑(List.toFinset l)) Disjoint
[PROOFSTEP]
simpa [hl] using h2
[GOAL]
case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : List.prod l = σ
h1 : ∀ (σ : Perm α), σ ∈ l → IsCycle σ
h2 : List.Pairwise Disjoint l
hl : List.Nodup l
⊢ Finset.noncommProd (List.toFinset l) id (_ : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (id a) (id b)) = σ
[PROOFSTEP]
simp [hl, h0]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ cycleType σ = 0 ↔ σ = 1
[PROOFSTEP]
simp [cycleType_def, cycleFactorsFinset_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ ↑card (cycleType σ) = 0 ↔ σ = 1
[PROOFSTEP]
rw [card_eq_zero, cycleType_eq_zero]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ 2 ≤ n
[PROOFSTEP]
simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map, mem_cycleFactorsFinset_iff] at h
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : ∃ a, (IsCycle a ∧ ∀ (a_1 : α), a_1 ∈ support a → ↑a a_1 = ↑σ a_1) ∧ Finset.card (support a) = n
⊢ 2 ≤ n
[PROOFSTEP]
obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : IsCycle w✝
⊢ 2 ≤ Finset.card (support w✝)
[PROOFSTEP]
exact hc.two_le_card_support
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ ↑card (cycleType σ) = 1 ↔ IsCycle σ
[PROOFSTEP]
rw [card_eq_one]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, cycleType σ = {a}) ↔ IsCycle σ
[PROOFSTEP]
simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
  cycleFactorsFinset_eq_singleton_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ IsCycle σ
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) → IsCycle σ
[PROOFSTEP]
rintro ⟨_, _, ⟨h, -⟩, -⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
w✝¹ : ℕ
w✝ : Perm α
h : IsCycle σ
⊢ IsCycle σ
[PROOFSTEP]
exact h
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ IsCycle σ → ∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsCycle σ
⊢ ∃ a a_1, (IsCycle σ ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
[PROOFSTEP]
use σ.support.card, σ
[GOAL]
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsCycle σ
⊢ (IsCycle σ ∧ σ = σ) ∧ (Finset.card ∘ support) σ = Finset.card (support σ)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : Disjoint σ τ
⊢ Perm.cycleType (σ * τ) = Perm.cycleType σ + Perm.cycleType τ
[PROOFSTEP]
rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ← Multiset.map_add,
  Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : Disjoint σ τ
⊢ Multiset.Disjoint (cycleFactorsFinset σ).val (cycleFactorsFinset τ).val
[PROOFSTEP]
exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ : Perm α
hσ : IsCycle σ
⊢ (fun τ => cycleType τ⁻¹ = cycleType τ) σ
[PROOFSTEP]
simp only [hσ.cycleType, hσ.inv.cycleType, support_inv]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ τ : Perm α
hστ : Disjoint σ τ
x✝ : IsCycle σ
hσ : (fun τ => cycleType τ⁻¹ = cycleType τ) σ
hτ : (fun τ => cycleType τ⁻¹ = cycleType τ) τ
⊢ (fun τ => cycleType τ⁻¹ = cycleType τ) (σ * τ)
[PROOFSTEP]
simp only [mul_inv_rev, hστ.cycleType, hστ.symm.inv_left.inv_right.cycleType, hσ, hτ, add_comm]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ cycleType (τ * σ * τ⁻¹) = cycleType σ
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
| induction_disjoint σ π hd _ hσ hπ => rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ cycleType (τ * σ * τ⁻¹) = cycleType σ
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
| induction_disjoint σ π hd _ hσ hπ => rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
⊢ cycleType (τ * 1 * τ⁻¹) = cycleType 1
[PROOFSTEP]

| base_one => simp
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
⊢ cycleType (τ * 1 * τ⁻¹) = cycleType 1
[PROOFSTEP]
simp
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ : Perm α
hσ : IsCycle σ
⊢ cycleType (τ * σ * τ⁻¹) = cycleType σ
[PROOFSTEP]

| base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ : Perm α
hσ : IsCycle σ
⊢ cycleType (τ * σ * τ⁻¹) = cycleType σ
[PROOFSTEP]
rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : Disjoint σ π
a✝ : IsCycle σ
hσ : cycleType (τ * σ * τ⁻¹) = cycleType σ
hπ : cycleType (τ * π * τ⁻¹) = cycleType π
⊢ cycleType (τ * (σ * π) * τ⁻¹) = cycleType (σ * π)
[PROOFSTEP]

| induction_disjoint σ π hd _ hσ hπ => rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : Disjoint σ π
a✝ : IsCycle σ
hσ : cycleType (τ * σ * τ⁻¹) = cycleType σ
hπ : cycleType (τ * π * τ⁻¹) = cycleType π
⊢ cycleType (τ * (σ * π) * τ⁻¹) = cycleType (σ * π)
[PROOFSTEP]
rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ sum (cycleType σ) = Finset.card (support σ)
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, coe_sum, List.sum_singleton]
| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ sum (cycleType σ) = Finset.card (support σ)
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, coe_sum, List.sum_singleton]
| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sum (cycleType 1) = Finset.card (support 1)
[PROOFSTEP]

| base_one => simp
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sum (cycleType 1) = Finset.card (support 1)
[PROOFSTEP]
simp
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ sum (cycleType σ) = Finset.card (support σ)
[PROOFSTEP]

| base_cycles σ hσ => rw [hσ.cycleType, coe_sum, List.sum_singleton]
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ sum (cycleType σ) = Finset.card (support σ)
[PROOFSTEP]
rw [hσ.cycleType, coe_sum, List.sum_singleton]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : sum (cycleType σ) = Finset.card (support σ)
hτ : sum (cycleType τ) = Finset.card (support τ)
⊢ sum (cycleType (σ * τ)) = Finset.card (support (σ * τ))
[PROOFSTEP]

| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : sum (cycleType σ) = Finset.card (support σ)
hτ : sum (cycleType τ) = Finset.card (support τ)
⊢ sum (cycleType (σ * τ)) = Finset.card (support (σ * τ))
[PROOFSTEP]
rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
| induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
| induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType]
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign 1 = prod (map (fun n => -(-1) ^ n) (cycleType 1))
[PROOFSTEP]

| base_one => simp
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign 1 = prod (map (fun n => -(-1) ^ n) (cycleType 1))
[PROOFSTEP]
simp
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
[PROOFSTEP]

| base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
[PROOFSTEP]
simp [hσ.cycleType, hσ.sign]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
hτ : ↑sign τ = prod (map (fun n => -(-1) ^ n) (cycleType τ))
⊢ ↑sign (σ * τ) = prod (map (fun n => -(-1) ^ n) (cycleType (σ * τ)))
[PROOFSTEP]

| induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
hτ : ↑sign τ = prod (map (fun n => -(-1) ^ n) (cycleType τ))
⊢ ↑sign (σ * τ) = prod (map (fun n => -(-1) ^ n) (cycleType (σ * τ)))
[PROOFSTEP]
simp [hσ, hτ, hd.cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ ↑sign f = (-1) ^ (sum (cycleType f) + ↑card (cycleType f))
[PROOFSTEP]
rw [sign_of_cycleType']
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ prod (map (fun n => -(-1) ^ n) (cycleType f)) = (-1) ^ (sum (cycleType f) + ↑card (cycleType f))
[PROOFSTEP]
induction' f.cycleType using Multiset.induction_on with a s ihs
[GOAL]
case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ prod (map (fun n => -(-1) ^ n) 0) = (-1) ^ (sum 0 + ↑card 0)
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : prod (map (fun n => -(-1) ^ n) s) = (-1) ^ (sum s + ↑card s)
⊢ prod (map (fun n => -(-1) ^ n) (a ::ₘ s)) = (-1) ^ (sum (a ::ₘ s) + ↑card (a ::ₘ s))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
[GOAL]
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : prod (map (fun n => -(-1) ^ n) s) = (-1) ^ (sum s + ↑card s)
⊢ -(-1) ^ a * (-1) ^ (sum s + ↑card s) = (-1) ^ (a + sum s + (↑card s + 1))
[PROOFSTEP]
simp only [pow_add, pow_one, mul_neg_one, neg_mul, mul_neg, mul_assoc, mul_one]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.lcm (cycleType σ) = orderOf σ
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
| induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.lcm (cycleType σ) = orderOf σ
[PROOFSTEP]
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
| induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Multiset.lcm (cycleType 1) = orderOf 1
[PROOFSTEP]

| base_one => simp
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Multiset.lcm (cycleType 1) = orderOf 1
[PROOFSTEP]
simp
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ Multiset.lcm (cycleType σ) = orderOf σ
[PROOFSTEP]

| base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ Multiset.lcm (cycleType σ) = orderOf σ
[PROOFSTEP]
simp [hσ.cycleType, hσ.orderOf]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : Multiset.lcm (cycleType σ) = orderOf σ
hτ : Multiset.lcm (cycleType τ) = orderOf τ
⊢ Multiset.lcm (cycleType (σ * τ)) = orderOf (σ * τ)
[PROOFSTEP]

| induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : Multiset.lcm (cycleType σ) = orderOf σ
hτ : Multiset.lcm (cycleType τ) = orderOf τ
⊢ Multiset.lcm (cycleType (σ * τ)) = orderOf (σ * τ)
[PROOFSTEP]
simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ n ∣ orderOf σ
[PROOFSTEP]
rw [← lcm_cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ n ∣ Multiset.lcm (cycleType σ)
[PROOFSTEP]
exact dvd_lcm h
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
⊢ orderOf (cycleOf f x) ∣ orderOf f
[PROOFSTEP]
by_cases hx : f x = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ↑f x = x
⊢ orderOf (cycleOf f x) ∣ orderOf f
[PROOFSTEP]
rw [← cycleOf_eq_one_iff] at hx
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx✝ : ↑f x = x
hx : cycleOf f x = 1
⊢ orderOf (cycleOf f x) ∣ orderOf f
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ orderOf (cycleOf f x) ∣ orderOf f
[PROOFSTEP]
refine dvd_of_mem_cycleType ?_
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ orderOf (cycleOf f x) ∈ cycleType f
[PROOFSTEP]
rw [cycleType, Multiset.mem_map]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ ∃ a, a ∈ (cycleFactorsFinset f).val ∧ (Finset.card ∘ support) a = orderOf (cycleOf f x)
[PROOFSTEP]
refine' ⟨f.cycleOf x, _, _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ cycleOf f x ∈ (cycleFactorsFinset f).val
[PROOFSTEP]
rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬↑f x = x
⊢ (Finset.card ∘ support) (cycleOf f x) = orderOf (cycleOf f x)
[PROOFSTEP]
simp [(isCycle_cycleOf _ hx).orderOf]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ cycleType σ
⊢ 2 ∣ n
[PROOFSTEP]
rw [le_antisymm (Nat.le_of_dvd zero_lt_two <| (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
    (two_le_of_mem_cycleType hn)]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ∃ n, cycleType σ = replicate (n + 1) (orderOf σ)
[PROOFSTEP]
refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
[GOAL]
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ↑card (cycleType σ) = ↑card (cycleType σ) - 1 + 1
[PROOFSTEP]
rw [tsub_add_cancel_of_le]
[GOAL]
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ ↑card (cycleType σ)
[PROOFSTEP]
rw [Nat.succ_le_iff, card_cycleType_pos, Ne.def, ← orderOf_eq_one_iff]
[GOAL]
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1
[PROOFSTEP]
exact hσ.ne_one
[GOAL]
case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ cycleType σ
⊢ n = orderOf σ
[PROOFSTEP]
exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left (one_lt_of_mem_cycleType hn).ne'
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Finset.card (support σ) < 2 * orderOf σ
⊢ IsCycle σ
[PROOFSTEP]
obtain ⟨n, hn⟩ := cycleType_prime_order h1
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Finset.card (support σ) < 2 * orderOf σ
n : ℕ
hn : cycleType σ = replicate (n + 1) (orderOf σ)
⊢ IsCycle σ
[PROOFSTEP]
rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_lt_mul_right (orderOf_pos σ),
  Nat.succ_lt_succ_iff, Nat.lt_succ_iff, le_zero_iff] at h2
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : cycleType σ = replicate (n + 1) (orderOf σ)
⊢ IsCycle σ
[PROOFSTEP]
rw [← card_cycleType_eq_one, hn, card_replicate, h2]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
⊢ cycleType f ≤ cycleType g
[PROOFSTEP]
have hf' := mem_cycleFactorsFinset_iff.1 hf
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ cycleType f ≤ cycleType g
[PROOFSTEP]
rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ map (Finset.card ∘ support) {f}.val ≤ map (Finset.card ∘ support) (cycleFactorsFinset g).val
[PROOFSTEP]
refine map_le_map ?_
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ {f}.val ≤ (cycleFactorsFinset g).val
[PROOFSTEP]
simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
⊢ cycleType (g * f⁻¹) + cycleType f = cycleType g - cycleType f + cycleType f
[PROOFSTEP]
rw [← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType, inv_mul_cancel_right,
  tsub_add_cancel_of_le (cycleType_le_of_mem_cycleFactorsFinset hf)]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : cycleType σ = cycleType τ
⊢ IsConj σ τ
[PROOFSTEP]
induction σ using cycle_induction_on generalizing τ with
| base_one =>
  rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
  rw [h]
| base_cycles σ hσ =>
  have hτ := card_cycleType_eq_one.2 hσ
  rw [h, card_cycleType_eq_one] at hτ
  apply hσ.isConj hτ
  rw [hσ.cycleType, hτ.cycleType, coe_eq_coe, List.singleton_perm] at h
  exact List.singleton_injective h
| induction_disjoint σ π hd hc hσ hπ =>
  rw [hd.cycleType] at h
  have h' : σ.support.card ∈ τ.cycleType := by simp [← h, hc.cycleType]
  obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
  have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
  refine' IsConj.trans _ key
  rw [mul_assoc]
  have hs : σ.cycleType = σ'.cycleType :=
    by
    rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
    rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
  refine' hd.isConj_mul (hσ hs) (hπ _) _
  · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs, add_tsub_cancel_right]
    rwa [Finset.mem_def]
  · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : cycleType σ = cycleType τ
⊢ IsConj σ τ
[PROOFSTEP]
induction σ using cycle_induction_on generalizing τ with
| base_one =>
  rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
  rw [h]
| base_cycles σ hσ =>
  have hτ := card_cycleType_eq_one.2 hσ
  rw [h, card_cycleType_eq_one] at hτ
  apply hσ.isConj hτ
  rw [hσ.cycleType, hτ.cycleType, coe_eq_coe, List.singleton_perm] at h
  exact List.singleton_injective h
| induction_disjoint σ π hd hc hσ hπ =>
  rw [hd.cycleType] at h
  have h' : σ.support.card ∈ τ.cycleType := by simp [← h, hc.cycleType]
  obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
  have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
  refine' IsConj.trans _ key
  rw [mul_assoc]
  have hs : σ.cycleType = σ'.cycleType :=
    by
    rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
    rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
  refine' hd.isConj_mul (hσ hs) (hπ _) _
  · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs, add_tsub_cancel_right]
    rwa [Finset.mem_def]
  · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : cycleType 1 = cycleType τ
⊢ IsConj 1 τ
[PROOFSTEP]

| base_one =>
  rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
  rw [h]
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : cycleType 1 = cycleType τ
⊢ IsConj 1 τ
[PROOFSTEP]
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
[GOAL]
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ
[PROOFSTEP]
rw [h]
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
⊢ IsConj σ τ
[PROOFSTEP]

| base_cycles σ hσ =>
  have hτ := card_cycleType_eq_one.2 hσ
  rw [h, card_cycleType_eq_one] at hτ
  apply hσ.isConj hτ
  rw [hσ.cycleType, hτ.cycleType, coe_eq_coe, List.singleton_perm] at h
  exact List.singleton_injective h
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
⊢ IsConj σ τ
[PROOFSTEP]
have hτ := card_cycleType_eq_one.2 hσ
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : ↑card (cycleType σ) = 1
⊢ IsConj σ τ
[PROOFSTEP]
rw [h, card_cycleType_eq_one] at hτ
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : IsCycle τ
⊢ IsConj σ τ
[PROOFSTEP]
apply hσ.isConj hτ
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : IsCycle τ
⊢ Finset.card (support σ) = Finset.card (support τ)
[PROOFSTEP]
rw [hσ.cycleType, hτ.cycleType, coe_eq_coe, List.singleton_perm] at h
[GOAL]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : [Finset.card (support σ)] = [Finset.card (support τ)]
hτ : IsCycle τ
⊢ Finset.card (support σ) = Finset.card (support τ)
[PROOFSTEP]
exact List.singleton_injective h
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType (σ * π) = cycleType τ
⊢ IsConj (σ * π) τ
[PROOFSTEP]

| induction_disjoint σ π hd hc hσ hπ =>
  rw [hd.cycleType] at h
  have h' : σ.support.card ∈ τ.cycleType := by simp [← h, hc.cycleType]
  obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
  have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
  refine' IsConj.trans _ key
  rw [mul_assoc]
  have hs : σ.cycleType = σ'.cycleType :=
    by
    rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
    rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
  refine' hd.isConj_mul (hσ hs) (hπ _) _
  · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs, add_tsub_cancel_right]
    rwa [Finset.mem_def]
  · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType (σ * π) = cycleType τ
⊢ IsConj (σ * π) τ
[PROOFSTEP]
rw [hd.cycleType] at h
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
⊢ IsConj (σ * π) τ
[PROOFSTEP]
have h' : σ.support.card ∈ τ.cycleType := by simp [← h, hc.cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
⊢ Finset.card (support σ) ∈ cycleType τ
[PROOFSTEP]
simp [← h, hc.cycleType]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
⊢ IsConj (σ * π) τ
[PROOFSTEP]
obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
[GOAL]
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
⊢ IsConj (σ * π) τ
[PROOFSTEP]
have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
[GOAL]
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ
[PROOFSTEP]
refine' IsConj.trans _ key
[GOAL]
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
[PROOFSTEP]
have hs : σ.cycleType = σ'.cycleType :=
  by
  rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
  rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ cycleType σ = cycleType σ'
[PROOFSTEP]
rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : IsCycle σ' ∧ ∀ (a : α), a ∈ support σ' → ↑σ' a = ↑τ a
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ cycleType σ = cycleType σ'
[PROOFSTEP]
rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : IsCycle σ' ∧ ∀ (a : α), a ∈ support σ' → ↑σ' a = ↑τ a
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ ↑[(Finset.card ∘ support) σ'] = ↑[Finset.card (support σ')]
[PROOFSTEP]
rfl
[GOAL]
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
[PROOFSTEP]
refine' hd.isConj_mul (hσ hs) (hπ _) _
[GOAL]
case induction_disjoint.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ cycleType π = cycleType (τ * σ'⁻¹)
[PROOFSTEP]
rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs, add_tsub_cancel_right]
[GOAL]
case induction_disjoint.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ σ' ∈ cycleFactorsFinset τ
[PROOFSTEP]
rwa [Finset.mem_def]
[GOAL]
case induction_disjoint.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : Disjoint σ π
hc : IsCycle σ
hσ : ∀ {τ : Perm α}, cycleType σ = cycleType τ → IsConj σ τ
hπ : ∀ {τ : Perm α}, cycleType π = cycleType τ → IsConj π τ
τ : Perm α
h : cycleType σ + cycleType π = cycleType τ
h' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ Disjoint σ' (τ * σ'⁻¹)
[PROOFSTEP]
exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : IsConj σ τ
⊢ cycleType σ = cycleType τ
[PROOFSTEP]
obtain ⟨π, rfl⟩ := isConj_iff.1 h
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ cycleType σ = cycleType (π * σ * π⁻¹)
[PROOFSTEP]
rw [cycleType_conj]
[GOAL]
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ cycleType (extendDomain g f) = cycleType g
[PROOFSTEP]
induction g using cycle_induction_on with
| base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
| base_cycles σ hσ => rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]
[GOAL]
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ cycleType (extendDomain g f) = cycleType g
[PROOFSTEP]
induction g using cycle_induction_on with
| base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
| base_cycles σ hσ => rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]
[GOAL]
case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ cycleType (extendDomain 1 f) = cycleType 1
[PROOFSTEP]

| base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
[GOAL]
case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ cycleType (extendDomain 1 f) = cycleType 1
[PROOFSTEP]
rw [extendDomain_one, cycleType_one, cycleType_one]
[GOAL]
case base_cycles
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ : Perm α
hσ : IsCycle σ
⊢ cycleType (extendDomain σ f) = cycleType σ
[PROOFSTEP]

| base_cycles σ hσ => rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
[GOAL]
case base_cycles
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ : Perm α
hσ : IsCycle σ
⊢ cycleType (extendDomain σ f) = cycleType σ
[PROOFSTEP]
rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : cycleType (extendDomain σ f) = cycleType σ
hτ : cycleType (extendDomain τ f) = cycleType τ
⊢ cycleType (extendDomain (σ * τ) f) = cycleType (σ * τ)
[PROOFSTEP]

| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]
[GOAL]
case induction_disjoint
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : cycleType (extendDomain σ f) = cycleType σ
hτ : cycleType (extendDomain τ f) = cycleType τ
⊢ cycleType (extendDomain (σ * τ) f) = cycleType (σ * τ)
[PROOFSTEP]
rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ cycleType σ ↔ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ cycleType σ → ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ cycleType σ
⊢ ∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
[PROOFSTEP]
obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
[GOAL]
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ cycleType (List.prod l)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, List.prod l = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
[PROOFSTEP]
rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
[GOAL]
case mp.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a, a ∈ l ∧ (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, List.prod l = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n
[PROOFSTEP]
obtain ⟨c, cl, rfl⟩ := h
[GOAL]
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ c_1 τ, List.prod l = c_1 * τ ∧ Disjoint c_1 τ ∧ IsCycle c_1 ∧ Finset.card (support c_1) = (Finset.card ∘ support) c
[PROOFSTEP]
rw [(List.perm_cons_erase cl).pairwise_iff Disjoint.symmetric] at hld
[GOAL]
case mp.mk.mk.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ ∃ c_1 τ, List.prod l = c_1 * τ ∧ Disjoint c_1 τ ∧ IsCycle c_1 ∧ Finset.card (support c_1) = (Finset.card ∘ support) c
[PROOFSTEP]
refine' ⟨c, (l.erase c).prod, _, _, hlc _ cl, rfl⟩
[GOAL]
case mp.mk.mk.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ List.prod l = c * List.prod (List.erase l c)
[PROOFSTEP]
rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
[GOAL]
case mp.mk.mk.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ (∀ (g : Perm α), g ∈ l_1 → IsCycle g) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ (g : Perm α), g ∈ l → IsCycle g
c : Perm α
hld : List.Pairwise Disjoint (c :: List.erase l c)
cl : c ∈ l
⊢ Disjoint c (List.prod (List.erase l c))
[PROOFSTEP]
exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ Disjoint c τ ∧ IsCycle c ∧ Finset.card (support c) = n) → n ∈ cycleType σ
[PROOFSTEP]
rintro ⟨c, t, rfl, hd, hc, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : Disjoint c t
hc : IsCycle c
⊢ Finset.card (support c) ∈ cycleType (c * t)
[PROOFSTEP]
simp [hd.cycleType, hc.cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
g : Perm α
hn2 : Fintype.card α < n + 2
hng : n ∈ cycleType g
⊢ cycleType g = {n}
[PROOFSTEP]
obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
⊢ cycleType (c * g') = {Finset.card (support c)}
[PROOFSTEP]
by_cases g'1 : g' = 1
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : g' = 1
⊢ cycleType (c * g') = {Finset.card (support c)}
[PROOFSTEP]
rw [hd.cycleType, hc.cycleType, coe_singleton, g'1, cycleType_one, add_zero]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hn2 : Fintype.card α < Finset.card (support c) + 2
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
⊢ cycleType (c * g') = {Finset.card (support c)}
[PROOFSTEP]
contrapose! hn2
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Fintype.card α
[PROOFSTEP]
apply le_trans _ (c * g').support.card_le_univ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Finset.card (support (c * g'))
[PROOFSTEP]
rw [hd.card_support_mul]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : Disjoint c g'
hc : IsCycle c
hng : Finset.card (support c) ∈ cycleType (c * g')
g'1 : ¬g' = 1
hn2 : cycleType (c * g') ≠ {Finset.card (support c)}
⊢ Finset.card (support c) + 2 ≤ Finset.card (support c) + Finset.card (support g')
[PROOFSTEP]
exact add_le_add_left (two_le_card_support_of_ne_one g'1) _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ Finset.card (support σ)ᶜ ≡ Fintype.card α [MOD p]
[PROOFSTEP]
rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ sum (cycleType σ)
[PROOFSTEP]
refine Multiset.dvd_sum fun k hk => ?_
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ cycleType σ
⊢ p ∣ k
[PROOFSTEP]
obtain ⟨m, -, hm⟩ := (Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hσ)
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ cycleType σ
m : ℕ
hm : orderOf σ = p ^ m
⊢ p ∣ k
[PROOFSTEP]
obtain ⟨l, -, rfl⟩ := (Nat.dvd_prime_pow hp.out).mp ((congr_arg _ hm).mp (dvd_of_mem_cycleType hk))
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ cycleType σ
⊢ p ∣ p ^ l
[PROOFSTEP]
exact dvd_pow_self _ fun h => (one_lt_of_mem_cycleType hk).ne <| by rw [h, pow_zero]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ cycleType σ
h : l = 0
⊢ 1 = p ^ l
[PROOFSTEP]
rw [h, pow_zero]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ Finset.card (support σ)ᶜ ≤ Fintype.card α
[PROOFSTEP]
exact Finset.card_le_univ _
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, ↑σ a = a
[PROOFSTEP]
classical
contrapose! hα
simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
exact
  Nat.modEq_zero_iff_dvd.1
    ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp (card_compl_support_modEq hσ).symm)
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, ↑σ a = a
[PROOFSTEP]
contrapose! hα
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), ↑σ a ≠ a
⊢ p ∣ Fintype.card α
[PROOFSTEP]
simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : support σ = Finset.univ
⊢ p ∣ Fintype.card α
[PROOFSTEP]
exact
  Nat.modEq_zero_iff_dvd.1
    ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp (card_compl_support_modEq hσ).symm)
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : ↑σ a = a
⊢ ∃ b, ↑σ b = b ∧ b ≠ a
[PROOFSTEP]
classical
have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by rw [Finset.mem_compl, mem_support, Classical.not_not]
obtain ⟨b, hb1, hb2⟩ :=
  Finset.exists_ne_of_one_lt_card
    (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩)
        (Nat.modEq_zero_iff_dvd.mp ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα)))))
    a
exact ⟨b, (h b).mp hb1, hb2⟩
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : ↑σ a = a
⊢ ∃ b, ↑σ b = b ∧ b ≠ a
[PROOFSTEP]
have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by rw [Finset.mem_compl, mem_support, Classical.not_not]
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : ↑σ a = a
b : α
⊢ b ∈ (support σ)ᶜ ↔ ↑σ b = b
[PROOFSTEP]
rw [Finset.mem_compl, mem_support, Classical.not_not]
[GOAL]
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : ↑σ a = a
h : ∀ (b : α), b ∈ (support σ)ᶜ ↔ ↑σ b = b
⊢ ∃ b, ↑σ b = b ∧ b ≠ a
[PROOFSTEP]
obtain ⟨b, hb1, hb2⟩ :=
  Finset.exists_ne_of_one_lt_card
    (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩)
        (Nat.modEq_zero_iff_dvd.mp ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα)))))
    a
[GOAL]
case intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : ↑σ a = a
h : ∀ (b : α), b ∈ (support σ)ᶜ ↔ ↑σ b = b
b : α
hb1 : b ∈ (support σ)ᶜ
hb2 : b ≠ a
⊢ ∃ b, ↑σ b = b ∧ b ≠ a
[PROOFSTEP]
exact ⟨b, (h b).mp hb1, hb2⟩
[GOAL]
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ IsCycle σ
[PROOFSTEP]
classical exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)
[GOAL]
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ IsCycle σ
[PROOFSTEP]
exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)
[GOAL]
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ Fintype.card α < 2 * orderOf σ
[PROOFSTEP]
rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_right (orderOf_pos σ)]
[GOAL]
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 < 2
[PROOFSTEP]
exact one_lt_two
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}
[PROOFSTEP]
simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, Vector.toList_singleton, List.prod_singleton, Vector.head_cons,
  true_and]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ ∀ (x : Vector G 1), Vector.head x = 1 → x = 1 ::ᵥ Vector.nil
[PROOFSTEP]
exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑(vectorsProdEqOne G 0)
[PROOFSTEP]
rw [zero_eq]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑{Vector.nil}
[PROOFSTEP]
exact Set.uniqueSingleton Vector.nil
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑(vectorsProdEqOne G 1)
[PROOFSTEP]
rw [one_eq]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑{1 ::ᵥ Vector.nil}
[PROOFSTEP]
exact Set.uniqueSingleton (Vector.nil.cons 1)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : Vector G n
⊢ (List.prod (Vector.toList v))⁻¹ ::ᵥ v ∈ vectorsProdEqOne G (n + 1)
[PROOFSTEP]
rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_self]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ Vector.head ↑v * List.prod (Vector.toList (Vector.tail ↑v)) = 1
[PROOFSTEP]
rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ List.prod (Vector.toList ↑v) = 1
[PROOFSTEP]
exact v.2
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_lt hp.out.one_lt)
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have Scard :=
  calc
    p ∣ Fintype.card G ^ (p - 1) := hdvd.trans (dvd_pow (dvd_refl _) hp')
    _ = Fintype.card (vectorsProdEqOne G p) := (VectorsProdEqOne.card G p).symm
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
let f : ℕ → vectorsProdEqOne G p → vectorsProdEqOne G p := fun k v => VectorsProdEqOne.rotate v k
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have hf1 : ∀ v, f 0 v = v := VectorsProdEqOne.rotate_zero
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have hf2 : ∀ j k v, f k (f j v) = f (j + k) v := fun j k v => VectorsProdEqOne.rotate_rotate v j k
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have hf3 : ∀ v, f p v = v := VectorsProdEqOne.rotate_length
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
let σ :=
  Equiv.mk (f 1) (f (p - 1)) (fun s => by rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]) fun s => by
    rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
s : ↑(vectorsProdEqOne G p)
⊢ f (p - 1) (f 1 s) = s
[PROOFSTEP]
rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
s : ↑(vectorsProdEqOne G p)
⊢ f 1 (f (p - 1) s) = s
[PROOFSTEP]
rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have hσ : ∀ k v, (σ ^ k) v = f k v := fun k v =>
  Nat.rec (hf1 v).symm (fun k hk => Eq.trans (congr_arg σ hk) (hf2 k 1 v)) k
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : ∀ (k : ℕ) (v : ↑(vectorsProdEqOne G p)), ↑(σ ^ k) v = f k v
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
replace hσ : σ ^ p ^ 1 = 1 := Perm.ext fun v => by rw [pow_one, hσ, hf3, one_apply]
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : ∀ (k : ℕ) (v : ↑(vectorsProdEqOne G p)), ↑(σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ ↑(σ ^ p ^ 1) v = ↑1 v
[PROOFSTEP]
rw [pow_one, hσ, hf3, one_apply]
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
let v₀ : vectorsProdEqOne G p := ⟨Vector.replicate p 1, (List.prod_replicate p 1).trans (one_pow p)⟩
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := { val := Vector.replicate p 1, property := (_ : List.prod (List.replicate p 1) = 1) }
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
have hv₀ : σ v₀ = v₀ := Subtype.ext (Subtype.ext (List.rotate_replicate (1 : G) p 1))
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := { val := Vector.replicate p 1, property := (_ : List.prod (List.replicate p 1) = 1) }
hv₀ : ↑σ v₀ = v₀
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀
[GOAL]
case intro.intro
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := { val := Vector.replicate p 1, property := (_ : List.prod (List.replicate p 1) = 1) }
hv₀ : ↑σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : ↑σ v = v
hv2 : v ≠ v₀
⊢ ∃ x, orderOf x = p
[PROOFSTEP]
refine'
  Exists.imp (fun g hg => orderOf_eq_prime _ fun hg' => hv2 _)
    (List.rotate_one_eq_self_iff_eq_replicate.mp (Subtype.ext_iff.mp (Subtype.ext_iff.mp hv1)))
[GOAL]
case intro.intro.refine'_1
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := { val := Vector.replicate p 1, property := (_ : List.prod (List.replicate p 1) = 1) }
hv₀ : ↑σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : ↑σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (List.length ↑↑v) g
⊢ g ^ p = 1
[PROOFSTEP]
rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
[GOAL]
case intro.intro.refine'_2
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := { val := Vector.replicate p 1, property := (_ : List.prod (List.replicate p 1) = 1) }
hv₀ : ↑σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : ↑σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (List.length ↑↑v) g
hg' : g = 1
⊢ v = v₀
[PROOFSTEP]
rw [Subtype.ext_iff_val, Subtype.ext_iff_val, hg, hg', v.1.2]
[GOAL]
case intro.intro.refine'_2
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f (p - 1) (f 1 s) = s),
    right_inv := (_ : ∀ (s : ↑(vectorsProdEqOne G p)), f 1 (f (p - 1) s) = s) }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := { val := Vector.replicate p 1, property := (_ : List.prod (List.replicate p 1) = 1) }
hv₀ : ↑σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : ↑σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (List.length ↑↑v) g
hg' : g = 1
⊢ List.replicate p 1 = ↑↑v₀
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : Fintype α
G✝ : Type u_2
inst✝² : Group G✝
n : ℕ
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card (Multiplicative G)
[PROOFSTEP]
convert hdvd
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
⊢ H = ⊤
[PROOFSTEP]
haveI : Fact (Fintype.card α).Prime := ⟨h0⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
⊢ H = ⊤
[PROOFSTEP]
obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
⊢ H = ⊤
[PROOFSTEP]
have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (orderOf_subgroup σ).trans hσ
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
⊢ H = ⊤
[PROOFSTEP]
have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
⊢ H = ⊤
[PROOFSTEP]
have hσ3 : (σ : Perm α).support = ⊤ := Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
⊢ H = ⊤
[PROOFSTEP]
have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ H = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ ↑σ ∈ ↑H ∧ τ ∈ ↑H
[PROOFSTEP]
exact ⟨Subtype.mem σ, h2⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : n ∈ cycleType σ + replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ 0 < n
[PROOFSTEP]
cases' mem_add.mp hn with hn hn
[GOAL]
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn✝ : n ∈ cycleType σ + replicate (Fintype.card α - Finset.card (support σ)) 1
hn : n ∈ cycleType σ
⊢ 0 < n
[PROOFSTEP]
exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)
[GOAL]
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn✝ : n ∈ cycleType σ + replicate (Fintype.card α - Finset.card (support σ)) 1
hn : n ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ 0 < n
[PROOFSTEP]
exact lt_of_lt_of_le zero_lt_one (ge_of_eq (Multiset.eq_of_mem_replicate hn))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ sum (cycleType σ + replicate (Fintype.card α - Finset.card (support σ)) 1) = Fintype.card α
[PROOFSTEP]
rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
  add_tsub_cancel_of_le σ.support.card_le_univ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ filter (fun n => 2 ≤ n) (partition σ).parts = cycleType σ
[PROOFSTEP]
rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
  Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ ¬2 ≤ a
[PROOFSTEP]
rw [Multiset.eq_of_mem_replicate h]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ replicate (Fintype.card α - Finset.card (support σ)) 1
⊢ ¬2 ≤ 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ partition σ = partition τ
[PROOFSTEP]
rw [isConj_iff_cycleType_eq]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ cycleType σ = cycleType τ ↔ partition σ = partition τ
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : cycleType σ = cycleType τ
⊢ partition σ = partition τ
[PROOFSTEP]
rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType, h]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : partition σ = partition τ
⊢ cycleType σ = cycleType τ
[PROOFSTEP]
rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ Finset.card (support σ) = 3
[PROOFSTEP]
rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Finset.card (support σ) = 3 ↔ IsThreeCycle σ
[PROOFSTEP]
refine' ⟨fun h => _, IsThreeCycle.card_support⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
⊢ IsThreeCycle σ
[PROOFSTEP]
by_cases h0 : σ.cycleType = 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : Perm.cycleType σ = 0
⊢ IsThreeCycle σ
[PROOFSTEP]
rw [← sum_cycleType, h0, sum_zero] at h
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : 0 = 3
h0 : Perm.cycleType σ = 0
⊢ IsThreeCycle σ
[PROOFSTEP]
exact (ne_of_lt zero_lt_three h).elim
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
⊢ IsThreeCycle σ
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0
[GOAL]
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
⊢ IsThreeCycle σ
[PROOFSTEP]
by_cases h1 : σ.cycleType.erase n = 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
[PROOFSTEP]
rw [← sum_cycleType, ← cons_erase hn, h1, cons_zero, Multiset.sum_singleton] at h
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
h : n = 3
hn : n ∈ Perm.cycleType σ
h1 : erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
[PROOFSTEP]
rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1
[GOAL]
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
hm : m ∈ erase (Perm.cycleType σ) n
⊢ IsThreeCycle σ
[PROOFSTEP]
rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h
[GOAL]
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
⊢ IsThreeCycle σ
[PROOFSTEP]
have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False :=
  by
  intros
  linarith
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
⊢ ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
k✝ : ℕ
a✝² : 2 ≤ m
a✝¹ : 2 ≤ n
a✝ : n + (m + k✝) = 3
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
⊢ IsThreeCycle σ
[PROOFSTEP]
cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ IsCycle σ
[PROOFSTEP]
rw [← card_cycleType_eq_one, h.cycleType, card_singleton]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ ↑Perm.sign σ = 1
[PROOFSTEP]
rw [Equiv.Perm.sign_of_cycleType, h.cycleType]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ (-1) ^ (sum {3} + ↑card {3}) = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ f : Perm α
h : IsThreeCycle f
⊢ IsThreeCycle f⁻¹
[PROOFSTEP]
rwa [IsThreeCycle, cycleType_inv]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ f : Perm α
⊢ IsThreeCycle f⁻¹ → IsThreeCycle f
[PROOFSTEP]
rw [← inv_inv f]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ f : Perm α
⊢ IsThreeCycle f⁻¹⁻¹⁻¹ → IsThreeCycle f⁻¹⁻¹
[PROOFSTEP]
apply inv
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ _root_.orderOf g = 3
[PROOFSTEP]
rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ IsThreeCycle (g * g)
[PROOFSTEP]
rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ Nat.coprime 2 (_root_.orderOf g)
[PROOFSTEP]
rw [ht.orderOf]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ Nat.coprime 2 3
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ IsThreeCycle (swap a b * swap a c)
[PROOFSTEP]
suffices h : support (swap a b * swap a c) = { a, b, c }
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : support (swap a b * swap a c) = {a, b, c}
⊢ IsThreeCycle (swap a b * swap a c)
[PROOFSTEP]
rw [← card_support_eq_three_iff, h]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : support (swap a b * swap a c) = {a, b, c}
⊢ Finset.card {a, b, c} = 3
[PROOFSTEP]
simp [ab, ac, bc]
[GOAL]
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ support (swap a b * swap a c) = {a, b, c}
[PROOFSTEP]
apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ ∀ (x : α), x ∈ support (swap a b) ⊔ support (swap a c) → x ∈ {a, b, c}
[PROOFSTEP]
simp [ab, ac, bc]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x ∈ {a, b, c}
⊢ x ∈ support (swap a b * swap a c)
[PROOFSTEP]
simp only [Finset.mem_insert, Finset.mem_singleton] at hx
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ x ∈ support (swap a b * swap a c)
[PROOFSTEP]
rw [mem_support]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ ↑(swap a b * swap a c) x ≠ x
[PROOFSTEP]
simp only [Perm.coe_mul, Function.comp_apply, Ne.def]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ ¬↑(swap a b) (↑(swap a c) x) = x
[PROOFSTEP]
obtain rfl | rfl | rfl := hx
[GOAL]
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬↑(swap x b) (↑(swap x c) x) = x
[PROOFSTEP]
rw [swap_apply_left, swap_apply_of_ne_of_ne ac.symm bc.symm]
[GOAL]
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬c = x
[PROOFSTEP]
exact ac.symm
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬↑(swap a x) (↑(swap a c) x) = x
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne ab.symm bc, swap_apply_right]
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬a = x
[PROOFSTEP]
exact ab
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬↑(swap a b) (↑(swap a x) x) = x
[PROOFSTEP]
rw [swap_apply_right, swap_apply_left]
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬b = x
[PROOFSTEP]
exact bc
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
⊢ swap a b * swap a c ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
by_cases bc : b = c
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b = c
⊢ swap a b * swap a c ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
subst bc
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab ac : a ≠ b
⊢ swap a b * swap a b ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
simp [one_mem]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : ¬b = c
⊢ swap a b * swap a c ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact subset_closure (isThreeCycle_swap_mul_swap_same ab ac bc)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : IsSwap σ
hτ : IsSwap τ
⊢ σ * τ ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨a, b, ab, rfl⟩ := hσ
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
hτ : IsSwap τ
a b : α
ab : a ≠ b
⊢ swap a b * τ ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨c, d, cd, rfl⟩ := hτ
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
by_cases ac : a = c
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : a = c
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
subst ac
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
d : α
cd : a ≠ d
⊢ swap a b * swap a d ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact swap_mul_swap_same_mem_closure_three_cycles ab cd
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d) := by simp [swap_comm c a, mul_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
[PROOFSTEP]
simp [swap_comm c a, mul_assoc]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [h']
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap a c * (swap c a * swap c d) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact
  mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
    (swap_mul_swap_same_mem_closure_three_cycles (Ne.symm ac) cd)


[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
⊢ ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑(p ^ (Nat.zero + 1)) ∣ a ^ p ^ Nat.zero - b ^ p ^ Nat.zero
[PROOFSTEP]
rwa [pow_one, pow_zero, pow_one, pow_one]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑(p ^ (Nat.succ k + 1)) ∣ a ^ p ^ Nat.succ k - b ^ p ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ' p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ, Nat.cast_mul]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑p * ↑(p ^ (k + 1)) ∣
    (Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)
[PROOFSTEP]
refine' mul_dvd_mul _ ih
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)})
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
r : R
⊢ ↑p ∣ r ↔ ↑f r = 0
[PROOFSTEP]
rw [eq_zero_iff_mem, mem_span_singleton]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
hf : ∀ (r : R), ↑p ∣ r ↔ ↑f r = 0
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
rw [hf, map_sub, sub_eq_zero] at h
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : ↑f a = ↑f b
hf : ∀ (r : R), ↑p ∣ r ↔ ↑f r = 0
⊢ ↑p ∣ Finset.sum (Finset.range p) fun i => (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
[PROOFSTEP]
rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
[GOAL]
case succ.h
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑(p ^ (k + 1)) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : ↑f a = ↑f b
hf : ∀ (r : R), ↑p ∣ r ↔ ↑f r = 0
⊢ ↑p = 0
[PROOFSTEP]
rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]


[GOAL]
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
⊢ FrobeniusNumber (m * n - m - n) {m, n}
[PROOFSTEP]
simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]
[GOAL]
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)
[PROOFSTEP]
have hmn : m + n ≤ m * n := add_le_mul hm hn
[GOAL]
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)
[PROOFSTEP]
constructor
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
[PROOFSTEP]
push_neg
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k}
[PROOFSTEP]
intro a b h
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False
[PROOFSTEP]
apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ (a + 1) * m + (b + 1) * n = m * n
[PROOFSTEP]
simp only [Nat.sub_sub, smul_eq_mul] at h
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a * m + b * n = m * n - (m + n)
⊢ (a + 1) * m + (b + 1) * n = m * n
[PROOFSTEP]
zify [hmn] at h ⊢
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n = ↑m * ↑n
[PROOFSTEP]
rw [← sub_eq_zero] at h ⊢
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h✝ : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0
[PROOFSTEP]
rw [← h]
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h✝ : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n))
[PROOFSTEP]
ring
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ upperBounds {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
[PROOFSTEP]
intro k hk
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : k ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
⊢ k ≤ m * n - m - n
[PROOFSTEP]
dsimp at hk
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : ¬∃ m_1 n_1, m_1 * m + n_1 * n = k
⊢ k ≤ m * n - m - n
[PROOFSTEP]
contrapose! hk
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
let x := chineseRemainder cop 0 k
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
have hx : x.val < m * n := chineseRemainder_lt_mul cop 0 k (ne_bot_of_gt hm) (ne_bot_of_gt hn)
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
suffices key : x.1 ≤ k
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1
[GOAL]
case right.intro
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2
[GOAL]
case right.intro.intro
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩
[GOAL]
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ a * m + b * n = k
[PROOFSTEP]
rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]
[GOAL]
case key
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ k
[PROOFSTEP]
refine' ModEq.le_of_lt_add x.2.2 (lt_of_le_of_lt _ (add_lt_add_right hk n))
[GOAL]
case key
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m - n + n
[PROOFSTEP]
rw [Nat.sub_add_cancel (le_tsub_of_add_le_left hmn)]
[GOAL]
case key
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m
[PROOFSTEP]
exact
  ModEq.le_of_lt_add (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub' (dvd_mul_right m n) dvd_rfl)).symm)
    (lt_of_lt_of_le hx le_tsub_add)