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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ (ϕ i) y * 1 = (ϕ i) y

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ (ϕ i) y * 1 = (ϕ i) y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1)) a = a ↔ ↑(#s) ∣ Int.negSucc n

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1)) a = a ↔ ↑(#s) ∣ Int.negSucc n
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℕ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (↑n - ↑m)) a = a

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℕ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (↑n - ↑m)) a = a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (n - m)) a = a

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (n - m)) a = a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ n * (f ^ ↑(#s)) ^ k) a = (f ^ n) a

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ n * (f ^ ↑(#s)) ^ k) a = (f ^ n) a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle l[idxOf a l] l[idxOf b l]

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle l[idxOf a l] l[idxOf b l]
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l[(idxOf b l + idxOf a l) % l.length] = l[(idxOf b l + idxOf a l) % l.length]

Tactic:
]

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

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ s = Subtype.val '' ⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x}

Tactic:
]

Goal state after:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ s = Subtype.val '' ⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x}
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #s ≤ 1

Tactic:
]

Goal state after:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #s ≤ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
]

Goal state after:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m ∈ ↑(range #s)
n : ℕ
hn : n ∈ ↑(range #s)
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then f⁻¹ y else y) then f (if f⁻¹.SameCycle x y then f⁻¹ y else y)
    else if f⁻¹.SameCycle x y then f⁻¹ y else y

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then f⁻¹ y else y) then f (if f⁻¹.SameCycle x y then f⁻¹ y else y)
    else if f⁻¹.SameCycle x y then f⁻¹ y else y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
]

Goal state after:
case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False
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
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
⊢ (noncommPiCoprod ϕ hcomm).ker ≤ ⊥

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
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
⊢ (noncommPiCoprod ϕ hcomm).ker ≤ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f ((f ^ n) x) = f ((f ^ n) x)

pp: case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)

Tactic:
]

Goal state after:
case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ (f ^ n) a = (f ^ n) a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f⁻¹ ^ (z + 1)) x = (f⁻¹ ^ (z + 1)) x

Tactic:
]

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

Goal state before:
pp: case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
]

Goal state after:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ (if f.SameCycle x z then f z else z) = (f.cycleOf y) z

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ (if f.SameCycle x z then f z else z) = (f.cycleOf y) z
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)
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 : ι
⊢ (fun i ↦ (ϕ i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j ≤ ⊥

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 : ι
⊢ (fun i ↦ (ϕ i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j ≤ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f ((f ^ k) x) = (f ^ (k + 1)) x

pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f ((f ^ k) x) = (f ^ (k + 1)) x

α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f ((f ^ k) x) = f ((f ^ k) x)

Tactic:
]

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

Goal state before:
pp: α : 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
⊢ Multiset.map (Finset.card ∘ support) l.toFinset.val = ↑(List.map (Finset.card ∘ support) l)

pp: case h1
α : 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
⊢ ∀ f ∈ l.toFinset, f.IsCycle

pp: case h2
α : 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).Pairwise Disjoint

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:
α : 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
⊢ Multiset.map (Finset.card ∘ support) l.toFinset.val = ↑(List.map (Finset.card ∘ support) l)

case h1
α : 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
⊢ ∀ f ∈ l.toFinset, f.IsCycle

case h2
α : 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).Pairwise Disjoint

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.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : f.SameCycle x y
⊢ f y = f y

Tactic:
]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : ¬f.SameCycle x y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : f y = y
⊢ y = y

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

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)

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

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 : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f x = x

Tactic:
]

Goal state after:
case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f x = x
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 = f

pp: case neg
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : ¬f x = x
⊢ f x ≠ x

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 x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
⊢ f x ≠ x

Tactic:
]

Goal state after:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
⊢ f x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ y = 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 x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
]

Goal state after:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
n : ℕ
x : α
⊢ (f.cycleOf x ^ n) x = (f.cycleOf x ^ n) x

Tactic:
]

Goal state after:
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
z : ℤ
⊢ ((f * g) ^ (z + 1)) x = (f.cycleOf x) (((f * g) ^ z) x)

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
z : ℤ
⊢ ((f * g) ^ (z + 1)) x = (f.cycleOf x) (((f * g) ^ z) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card { c // #(↑c).support = n }

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    Fintype.card { c // #(↑c).support = n }
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
⊢ y = 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.SameCycle 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.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
]

Goal state after:
case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ (c ^ i) x = g 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 ∈ support 1 ↔ 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 ∈ support 1 ↔ f.SameCycle x y ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({x ∈ σ.cycleFactorsFinset | ∃ (h : x ∈ σ.cycleFactorsFinset), #(↑⟨x, h⟩).support = n})

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({x ∈ σ.cycleFactorsFinset | ∃ (h : x ∈ σ.cycleFactorsFinset), #(↑⟨x, h⟩).support = n})
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a

Tactic:
]

Goal state after:
case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a
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
⊢ (if f.SameCycle x y then f y else 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
⊢ (if f.SameCycle x y then f y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ = 1 ↔ σ = 1

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
x : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
k : ℤ
⊢ ¬(f ^ k) x ∉ f.support ↔ True

Tactic:
]

Goal state after:
case pos
α : Type u_2
f : Perm α
x : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
k : ℤ
⊢ ¬(f ^ k) x ∉ f.support ↔ True