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

Goal state before:
pp: case refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
⊢ (List.replicate p g).prod = 1

Tactic:
← v.1.2,

Goal state after:
case refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
⊢ (List.replicate (↑↑v).length g).prod = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
⊢ Commute g1 g2

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : ¬x = k
⊢ ↑x + 1 < n

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ ∃ x, orderOf x = p

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝² : AddGroup G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card (Multiplicative G)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
⊢ ⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k) = ⇑(i.cycleIcc k)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
⊢ ⇑(j.cycleIcc i) ∘ ⇑(i.cycleIcc k) = ⇑(i.cycleIcc k)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hjk : j ≤ k
⊢ ⇑(i.cycleIcc k) ∘ ⇑(k.cycleIcc j) = ⇑(i.cycleIcc k)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p ∈ f.cycleFactorsFinset
⊢ p.support ⊆ f.support

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
v : ↥(Subgroup.zpowers ↑c)
⊢ (↑v).support ⊆ g.support

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
⊢ ∃ x, orderOf x = p

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
hx : x ∈ Subgroup.zpowers ↑c
hy : y ∈ Subgroup.zpowers ↑d
⊢ x.Disjoint y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
h : sign σ = σ.signAux
⊢ sign σ = ∏ j, ∏ i < j, if σ i < σ j then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign 1 = signAux 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign σ = ∏ j, ∏ i < j, if σ i < σ j then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ ∀ (x y : Fin n), x ∈ Finset.univ ∧ y ∈ Finset.Iio x ↔ x ∈ Finset.Ioi y ∧ y ∈ Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign σ = ∏ i, ∏ j > i, if σ i < σ j then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
this : (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) ↔ x2 < x1
⊢ ⟨x1, x2⟩ ∈ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D ↔ ⟨x1, x2⟩ ∈ D

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
⊢ H = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
i j : Fin n
hij : j < i
⊢ min (σ i) (σ j) ≠ max (σ i) (σ j)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint ((Subgroup.noncommPiCoprod ⋯) v)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
⊢ 0 < n

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.cycleFactorsFinset = ∅ ↔ f = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ cycleFactorsFinset 1 = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.cycleFactorsFinset = {f} ↔ f.IsCycle

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hlt' : (Equiv.symm σ) x1 < (Equiv.symm σ) x2
⊢ max (σ ((Equiv.symm σ) x2)) (σ ((Equiv.symm σ) x1)) = x1 ∧ min (σ ((Equiv.symm σ) x2)) (σ ((Equiv.symm σ) x1)) = x2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ (Equiv.symm σ) x2 ≠ (Equiv.symm σ) x1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Injective cycleFactorsFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.filter (fun n ↦ 2 ≤ n) σ.partition.parts = σ.cycleType

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ max (σ ((Equiv.symm σ) x1)) (σ ((Equiv.symm σ) x2)) = x1 ∧ min (σ ((Equiv.symm σ) x1)) (σ ((Equiv.symm σ) x2)) = x2

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
⊢ a ∈ f.support ∩ g.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
⊢ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ σ.partition = τ.partition

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsSwap ↔ σ.cycleType = {2}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
σ : Perm α
h : σ.IsSwap
⊢ _root_.orderOf σ = 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ ≠ 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x : (_ : Fin n) × Fin n
hx : x ∈ ↑D
y : (_ : Fin n) × Fin n
hy : y ∈ ↑D
⊢ (Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D).card = D.card

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ f⁻¹ x ∈ f.support

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹).Disjoint f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = f.cycleOf a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
⊢ c = f.cycleOf a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.IsCycleOn ↑c.support

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
⊢ c = g.cycleOf x ↔ x ∈ c.support

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
⊢ (g ^ m) x ∈ (↑c).support ↔ x ∈ (↑c).support

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
x✝ : Perm α
⊢ x✝ = k⁻¹ * (k * x✝ * k⁻¹) * k

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3
hm : m ∈ σ.cycleType.erase n
⊢ ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support = 3 ↔ σ.IsThreeCycle

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : ⟨x₁, x₂⟩ ∈ D
⊢ x₂ < x₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.IsCycle

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ Perm.sign σ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute c g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
h : f.IsThreeCycle
⊢ f⁻¹.IsThreeCycle

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹.IsThreeCycle → f.IsThreeCycle

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ _root_.orderOf g = 3

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
⊢ ∀ (x : α), d x ∈ c.support ↔ x ∈ c.support

Tactic:
by

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
this : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ P σ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ (g * g).IsThreeCycle

Tactic:
by

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

Goal state before:
pp: case intro.cons
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ (∀ τ ∈ σ :: l, τ.IsCycle) → List.Pairwise Disjoint (σ :: l) → P (σ :: l).prod

Tactic:
intro h1 h2

Goal state after:
case intro.cons
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ :: l).prod
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
by

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
⊢ P σ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = g (g a)
this : (g ^ 3) a = a
⊢ g a = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g.support = {a, g a, g (g a)} ↔ a ∈ g.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∀ (x y : Fin n), x ∈ Finset.univ ∧ y ∈ Finset.Ioi x ↔ x ∈ Finset.Iio y ∧ y ∈ Finset.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : g.support = {a, g a, g (g a)}
this : #g.support = 3
⊢ [a, g a, g (g a)].Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ [a, g a, g (g a)].Nodup ↔ a ∈ g.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∀ (x y : Fin n), x ∈ Finset.univ ∧ y ∈ Finset.Iio x ↔ x ∈ Finset.Ioi y ∧ y ∈ Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ i, ∏ j > i, f (σ i) (σ j) = ↑↑(sign σ) * ∏ i, ∏ j > i, f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
⊢ f = g

Tactic:
by

Goal state after: