mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
⊢ orderOf ((ϕ i) g') ∣ Fintype.card (H i)

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
⊢ orderOf ((ϕ i) g') ∣ Fintype.card (H i)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, σ.cycleType = {a}) ↔ σ.IsCycle

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, σ.cycleType = {a}) ↔ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ (c ^ i) (c x) = c ((c ^ i) x)

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ (c ^ i) (c x) = c ((c ^ i) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
hx : f x ≠ x
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ f.SameCycle x y ↔ f.SameCycle x y

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1

Tactic:
]

Goal state after:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g x ∉ c.support

Tactic:
]

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g x ∉ c.support
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf ((noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g) ∣ Fintype.card ((i_1 : { j // j ≠ i }) → H ↑i_1)

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf ((noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g) ∣ Fintype.card ((i_1 : { j // j ≠ i }) → H ↑i_1)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset.val ∪ τ.cycleFactorsFinset.val) =
    Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset.val ∪ τ.cycleFactorsFinset.val)

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ _root_.Disjoint σ.cycleFactorsFinset.val τ.cycleFactorsFinset.val

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ _root_.Disjoint σ.cycleFactorsFinset.val τ.cycleFactorsFinset.val
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : f.SameCycle x a ∧ x ∈ f.support
b : α
hb : f.SameCycle x b ∧ x ∈ f.support
⊢ f.SameCycle a b

Tactic:
]

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : f.SameCycle x a ∧ x ∈ f.support
b : α
hb : f.SameCycle x b ∧ x ∈ f.support
⊢ f.SameCycle a b
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ : Perm α
hσ : σ.IsCycle
⊢ {#σ.support} = {#σ.support}

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ (c ^ k).subtypePerm ⋯ = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ (c ^ k).subtypePerm ⋯ = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y

Tactic:
]

Goal state after:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ f.SameCycle x x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ f.SameCycle x y

Tactic:
]

Goal state after:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
a✝ : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
⊢ σ.cycleType + π.cycleType = σ.cycleType + π.cycleType

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∈ c.support
⊢ (c ^ k) a = g a ↔ (c ^ k) a = g a

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ orderOf f ∣ 1

Tactic:
]

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ orderOf f ∣ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : f x = x
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : f x = x
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ #σ.support = #σ.support

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

pp: case neg.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support

Tactic:
]

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

case neg.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
⊢ #σ.support + #τ.support = #σ.support + #τ.support

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i))

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #(Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ) = #σ.supportᶜ

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #(Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ) = #σ.supportᶜ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) f.cycleType).prod = (-1) ^ (f.cycleType.sum + f.cycleType.card)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) f.cycleType).prod = (-1) ^ (f.cycleType.sum + f.cycleType.card)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ g.SameCycle y y

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (-1) ^ (s.sum + s.card) = (-1) ^ (a + s.sum + (s.card + 1))

Tactic:
]

Goal state after:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (-1) ^ (s.sum + s.card) = (-1) ^ (a + s.sum + (s.card + 1))
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then f y else y) ≠ y
⊢ y ∈ f.support

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then f y else y) ≠ y
⊢ y ∈ f.support
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (a : ι) (b : a ≠ i), (Fintype.card (H ↑⟨a, b⟩)).Coprime (Fintype.card (H i))

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (a : ι) (b : a ≠ i), (Fintype.card (H ↑⟨a, b⟩)).Coprime (Fintype.card (H i))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f.cycleOf x = 1
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f.cycleOf x = 1
⊢ orderOf (f.cycleOf x) ∣ orderOf f
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f x ≠ x

Tactic:
]

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f.cycleOf x ^ n) x = (f.cycleOf x ^ n) x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
]

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
⊢ 2 ∣ 2

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card

pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ σ.cycleType.card

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ σ.cycleType.card
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑⟨(c ^ n) ↑⟨x, hx⟩, ⋯⟩

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos.zero
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc : c ∈ σ.cycleType → c = p
h : c ∈ σ.cycleType
⊢ p ∣ p

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ x ∉ (c ^ n).support

Tactic:
]

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ x ∉ (c ^ n).support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : f x = x
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x

Tactic:
]

Goal state after:
case neg
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : f x = x
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x