awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one : (cycleType.{u_1} (α := α) 1).sum = Finset.card.{u_1} (α := α) (support 1)
⊢ σ.cycleType.sum = #σ.support
have base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ.cycleType.sum = #σ.support
Tactic: induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one : (cycleType.{u_1} (α := α) 1).sum = Finset.card.{u_1} (α := α) (support 1)
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ.cycleType.sum = #σ.support
⊢ σ.cycleType.sum = #σ.support
have induction_disjoint : ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
  σ.IsCycle →
    ∀ (hσ : σ.cycleType.sum = #σ.support) (hτ : τ.cycleType.sum = #τ.support), (σ * τ).cycleType.sum = #(σ * τ).support
Tactic: induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1) = Fintype.card α - σ.cycleType.sum
have rw : #(Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ) = #σ.supportᶜ
Tactic: rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl, Fintype.card_ofFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ #(Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ) = #σ.supportᶜ
have e_s : Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ = σ.supportᶜ
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
have base_one : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1)
  (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (cycleType.{u_1} (α := α) 1)))
Tactic: 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_mul]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (cycleType.{u_1} (α := α) 1)))
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
have base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle),
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
Tactic: 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_mul]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (cycleType.{u_1} (α := α) 1)))
base_cycles :
  ∀ (σ : Perm α) (hσ : σ.IsCycle),
    Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
      (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
have induction_disjoint : ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
  σ.IsCycle →
    ∀
      (hσ :
        Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
          (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ))
      (hτ :
        Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) τ : ℤˣ)
          (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) τ.cycleType) : ℤˣ)),
      Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (σ * τ) : ℤˣ)
        (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (σ * τ).cycleType) : ℤˣ)
Tactic: 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_mul]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f = HPow.hPow (α := ℤˣ) (-1) (f.cycleType.sum + f.cycleType.card)
have rw : Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) f.cycleType) =
  HPow.hPow (α := ℤˣ) (-1) (f.cycleType.sum + f.cycleType.card)
Tactic: rw [sign_of_cycleType']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs :
  Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) s) = HPow.hPow (α := ℤˣ) (-1) (s.sum + s.card)
⊢ Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (a ::ₘ s)) =
    HPow.hPow (α := ℤˣ) (-1) ((a ::ₘ s).sum + (a ::ₘ s).card)
have cons : -HPow.hPow (α := ℤˣ) (-1) a * HPow.hPow (α := ℤˣ) (-1) (s.sum + s.card) =
  HPow.hPow (α := ℤˣ) (-1) (a + s.sum + (s.card + 1))
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
⊢ Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) f.cycleType) =
    HPow.hPow (α := ℤˣ) (-1) (f.cycleType.sum + f.cycleType.card)
have induction : ∀ (x : Multiset ℕ),
  Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) x) = HPow.hPow (α := ℤˣ) (-1) (x.sum + x.card)
Tactic: induction f.cycleType using Multiset.induction_on with
  | empty => rfl
  | cons a s ihs =>
    rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType.lcm = orderOf σ
have base_one : (cycleType.{u_1} (α := α) 1).lcm = orderOf.{u_1} (G := Perm α) 1
Tactic: 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_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one : (cycleType.{u_1} (α := α) 1).lcm = orderOf.{u_1} (G := Perm α) 1
⊢ σ.cycleType.lcm = orderOf σ
have base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ.cycleType.lcm = orderOf σ
Tactic: 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_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one : (cycleType.{u_1} (α := α) 1).lcm = orderOf.{u_1} (G := Perm α) 1
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ.cycleType.lcm = orderOf σ
⊢ σ.cycleType.lcm = orderOf σ
have induction_disjoint : ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
  σ.IsCycle →
    ∀ (hσ : σ.cycleType.lcm = orderOf σ) (hτ : τ.cycleType.lcm = orderOf τ), (σ * τ).cycleType.lcm = orderOf (σ * τ)
Tactic: 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_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ orderOf σ
have rw : n ∣ σ.cycleType.lcm
Tactic: rw [← lcm_cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
⊢ orderOf (f.cycleOf x) ∣ orderOf f
have pos : ∀ (hx : (f : (a : α) → α) x = x), orderOf (f.cycleOf x) ∣ orderOf f
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
pos : ∀ (hx : (f : (a : α) → α) x = x), orderOf (f.cycleOf x) ∣ orderOf f
⊢ orderOf (f.cycleOf x) ∣ orderOf f
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x), orderOf (f.cycleOf x) ∣ orderOf f
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : (f : (a : α) → α) x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f
have hx₁ : f.cycleOf x = 1
Tactic: rw [← cycleOf_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f
have neg : orderOf (f.cycleOf x) ∈ f.cycleType
Tactic: refine dvd_of_mem_cycleType ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ orderOf (f.cycleOf x) ∈ f.cycleType
have neg : ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)
Tactic: rw [cycleType, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)
have neg : f.cycleOf x ∈ f.cycleFactorsFinset.val
Tactic: refine ⟨f.cycleOf x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x ∈ f.cycleFactorsFinset.val
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)
have neg₁ : (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)
Tactic: refine ⟨f.cycleOf x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val
have neg : f.cycleOf x ∈ f.cycleFactorsFinset
Tactic: rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x ∈ f.cycleFactorsFinset
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val
have neg₁ : x ∈ f.support
Tactic: rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x ∈ f.cycleFactorsFinset
neg₁ : x ∈ f.support
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val
have neg₂ : (f : (a : α) → α) x ≠ x
Tactic: rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : HPow.hPow (β := ℕ) σ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
⊢ 2 ∣ n
have rw : Dvd.dvd (α := ℕ) 2 2
Tactic: rw [_root_.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)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ∃ (n : ℕ), σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
have refine_1 : σ.cycleType.card = σ.cycleType.card - 1 + 1
Tactic: refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
refine_1 : σ.cycleType.card = σ.cycleType.card - 1 + 1
⊢ ∃ (n : ℕ), σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
have refine_2 : ∀ (n : ℕ) (hn : n ∈ σ.cycleType), n = orderOf σ
Tactic: refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1
have refine_1 : 1 ≤ σ.cycleType.card
Tactic: rw [tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ σ.cycleType.card
have refine_1 : ¬orderOf σ = 1
Tactic: rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p
have rw : (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, ← lcm_cycleType, Multiset.lcm_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p
have h : ∀ (a : ℕ), a ∈ σ.cycleType → a ∣ p ↔ a ∈ σ.cycleType → a = p
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc : c ∈ σ.cycleType → c = p
h : c ∈ σ.cycleType
⊢ c ∣ p
have rw : p ∣ p
Tactic: rw [hc h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
⊢ σ.IsCycle
have obtain : ∀ (n : ℕ) (hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)), σ.IsCycle
Tactic: obtain ⟨n, hn⟩ := cycleType_prime_order h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
have rw : ∀ (n : ℕ) (h2 : n = 0) (hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)), σ.IsCycle
Tactic: rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id,
    mul_lt_mul_iff_left₀ (orderOf_pos σ), Nat.succ_lt_succ_iff, Nat.lt_succ_iff, Nat.le_zero] at h2
Cleared hypotheses: h2, n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
have rw : σ.cycleType.card = 1
Tactic: rw [← card_cycleType_eq_one, hn, card_replicate, h2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
rw : σ.cycleType.card = 1
⊢ σ.IsCycle
have rw₁ : (Multiset.replicate (n + 1) (orderOf σ)).card = 1
Tactic: rw [← card_cycleType_eq_one, hn, card_replicate, h2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
rw : σ.cycleType.card = 1
rw₁ : (Multiset.replicate (n + 1) (orderOf σ)).card = 1
⊢ σ.IsCycle
have rw₂ : n + 1 = 1
Tactic: rw [← card_cycleType_eq_one, hn, card_replicate, h2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
rw : σ.cycleType.card = 1
rw₁ : (Multiset.replicate (n + 1) (orderOf σ)).card = 1
rw₂ : n + 1 = 1
⊢ σ.IsCycle
have rw₃ : HAdd.hAdd (α := ℕ) 0 1 = 1
Tactic: rw [← card_cycleType_eq_one, hn, card_replicate, h2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ f.cycleType ≤ g.cycleType
have hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: have hf' := mem_cycleFactorsFinset_iff.1 hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ f.cycleType ≤ g.cycleType
have rw : Multiset.map (α := Perm α) (Finset.card ∘ support) (Finset.val {f}) ≤
  Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val
Tactic: rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ Multiset.map (α := Perm α) (Finset.card ∘ support) (Finset.val {f}) ≤
    Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val
have refine : Finset.val {f} ≤ g.cycleFactorsFinset.val
Tactic: refine map_le_map ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
⊢ ((insert i s).noncommProd k hs').cycleType = ∑ i ∈ insert i s, (k i).cycleType
have hs'₁ : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
Tactic: have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k hs'_1).cycleType = ∑ i ∈ insert i s, (k i).cycleType
have insert : (k i * s.noncommProd k sorry).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType
have insert : (k i).Disjoint (s.noncommProd k sorry)
Tactic: rw [Disjoint.cycleType_mul, hrec hs']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (k i).Disjoint (s.noncommProd k ⋯)
have insert : ∀ i_1 ∈ s, (k i).Disjoint (k i_1)
Tactic: apply disjoint_noncommProd_right
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ (k i).Disjoint (k j)
have apply : i ∈ (↑(insert i s) : Set ι)
Tactic: apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j))
    (hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs'_1 : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
apply : i ∈ (↑(insert i s) : Set ι)
⊢ (k i).Disjoint (k j)
have apply₁ : j ∈ (↑(insert i s) : Set ι)
Tactic: apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm