mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : ¬f x = x
⊢ f.cycleOf x = if f x = x then 1 else f

Tactic:
·

Goal state after:
case neg
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : ¬f x = x
⊢ f.cycleOf x = if f x = x then 1 else f
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ

Tactic:
·

Goal state after:
case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro.hcomm
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
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
⊢ Pairwise fun i_1 j ↦ ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)

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
hxi : f ∈ Set.range ⇑(ϕ i)
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
hxp : f ∈ ↑(noncommPiCoprod (fun x ↦ ϕ ↑x) ?intro.hcomm).range
⊢ f ∈ ⊥

Tactic:
·

Goal state after:
case intro.hcomm
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
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
⊢ Pairwise fun i_1 j ↦ ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : (f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y

pp: case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y

Tactic:
·

Goal state after:
case pos
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : (f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y

Tactic:
·

Goal state after:
case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case inl
α : Type u_2
f g : Perm α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableRel g.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hfx : f x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

pp: case inr
α : Type u_2
f g : Perm α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableRel g.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hgx : g x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
·

Goal state after:
case inl
α : Type u_2
f g : Perm α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableRel g.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hfx : f x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case inl
α : Type u_2
f g : Perm α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableRel g.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hfx : f x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]

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

Goal state before:
pp: case inr
α : Type u_2
f g : Perm α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableRel g.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hgx : g x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
·

Goal state after:
case inr
α : Type u_2
f g : Perm α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableRel g.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hgx : g x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : f x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
·

Goal state after:
case pos
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : f x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
·

Goal state after:
case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
⊢ (∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport) →
    Commute g c

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
⊢ (∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport) →
    Commute g c
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : f.SameCycle x y
⊢ f y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : ¬f.SameCycle x y
⊢ y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
·

Goal state after:
case pos
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : f.SameCycle x y
⊢ f y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
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
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
⊢ g (c x) = c (g x)

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 (c x) = c (g x)

Tactic:
·

Goal state after:
case pos
α : 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 (c x) = c (g x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : ¬f.SameCycle x y
⊢ y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
·

Goal state after:
case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : ¬f.SameCycle x y
⊢ y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
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 (c x) = c (g x)

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 (c x) = c (g x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : f x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x x✝ ∧ x ∈ f.support

pp: case refine_2
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x (f x✝) ∧ x ∈ f.support

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : f x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x x✝ ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x (f x✝) ∧ x ∈ f.support

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x (f x✝) ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

pp: case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ f.SameCycle x y → ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
·

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

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

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ f.SameCycle x y → ∃ m < Fintype.card α, (f ^ m) x = y
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
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

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.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
·

Goal state after:
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
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a
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.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

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.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a
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
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
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.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.Basic

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

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 : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
·

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : f.SameCycle x y
hy : f y ≠ y
⊢ y ∈ f.support

pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : f.SameCycle x y
hy : f y ≠ y
⊢ y ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f
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
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ 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
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

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

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) 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 ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x
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 : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

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 : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)
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.cycleOf x ∈ f.cycleFactorsFinset.val

pp: case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

pp: case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
·

Goal state after:
case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y
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 - 1 + 1

pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
·

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

Goal state before:
pp: case pos.zero
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

pp: case pos.succ
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
·

Goal state after:
case pos.zero
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (f ^ 0) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y
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 = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

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
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
·

Goal state after:
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 = (ofSubtype (c.subtypePerm ⋯ ^ n)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case hind
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep fun i ↦ (H i).subtype.range

pp: case hinj
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ ∀ (i : ι), Function.Injective ⇑(H i).subtype

Tactic:
·

Goal state after:
case hind
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep fun i ↦ (H i).subtype.range