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

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) a ≤ (f * g) b then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
mul_apply,

Goal state after:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ (f * g) b then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ (f ^ i * f) x = (f ^ i) x

Tactic:
mul_apply,

Goal state after:
α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ (f ^ i) (f x) = (f ^ i) x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
h : (f * σ * f⁻¹) (g (τ x)) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))

Tactic:
mul_apply,

Goal state after:
case intro.refine_2.inr.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
h : (f * σ) (f⁻¹ (g (τ x))) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
h : (f * σ) (f⁻¹ (g (τ x))) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))

Tactic:
mul_apply,

Goal state after:
case intro.refine_2.inr.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
h : f (σ (f⁻¹ (g (τ x)))) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ¬(g * τ * g⁻¹) (g (τ x)) = g (τ x)

Tactic:
mul_apply,

Goal state after:
case intro.refine_2.inr.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ¬(g * τ) (g⁻¹ (g (τ x))) = g (τ x)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ¬(g * τ) (g⁻¹ (g (τ x))) = g (τ x)

Tactic:
mul_apply,

Goal state after:
case intro.refine_2.inr.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ¬g (τ (g⁻¹ (g (τ x)))) = g (τ x)
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x ((σ * σ ^ n) x) ∈ H

Tactic:
mul_apply,

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x (σ ((σ ^ n) x)) ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
⊢ ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ (n + 1)) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
intro b

Goal state after:
case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b : α
⊢ ∀ {x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ (n + 1)) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ ((swap x (f x) * f) ^ 1 * (swap x (f x) * f) ^ i) (f x) = b

Tactic:
mul_apply,

Goal state after:
case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ ((swap x (f x) * f) ^ 1) (((swap x (f x) * f) ^ i) (f x)) = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ (swap x (f x) * f) ((Equiv.symm f) b) = b

Tactic:
mul_apply,

Goal state after:
case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ (swap x (f x)) (f ((Equiv.symm f) b)) = b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ (p * g) x = p x ↔ g x = x

Tactic:
mul_apply,

Goal state after:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ p (g x) = p x ↔ g x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b

Tactic:
mul_apply,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (swap x ((Equiv.symm f) x)) (f⁻¹ ((Equiv.symm f) b)) ≠ (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : ¬z = x
h6 : ¬z = y
⊢ swap x y * swap x z * swap x y ∈ H

Tactic:
exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)

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

Goal state before:
pp: case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
· simp only [support_inv, imp_self, implies_true]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
h : Fintype.card α ∣ i
⊢ x = y

Tactic:
obtain ⟨m, hm⟩ := h

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
m : ℕ
hm : i = Fintype.card α * m
⊢ x = y
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: k : ℕ
l : List ℕ
⊢ k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n

Tactic:
simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
hy : ¬f y = y
j : ℤ
hj : (f ^ (j - i) * f ^ i) z = y
⊢ False

Tactic:
mul_apply,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
hy : ¬f y = y
j : ℤ
hj : (f ^ (j - i)) ((f ^ i) z) = y
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ ((f ^ n) ^ m).IsCycle

Tactic:
hm

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ ((f ^ n) ^ m).support

Tactic:
hm

Goal state after:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
⊢ f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_ge hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp [pow_sub _ hab, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
⊢ ⊤ ⊆ l.toFinset

Tactic:
intro b

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
b : α
⊢ b ∈ ⊤ → b ∈ l.toFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
by
  obtain hs | hs := s.subsingleton_or_nontrivial
  · have := hs.coe_sort
    exact isCycleOn_of_subsingleton _ _
  convert! (hf.isCycle_subtypePerm hs).isCycleOn
  rw [eq_comm, Set.eq_univ_iff_forall]
  exact fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)

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

Tactic:
mul_apply,

Goal state after:
case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ (f.cycleOf x) ((f.cycleOf x ^ n) x) = (f ^ (n + 1)) x
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 : ℤ
⊢ (∀ a ∈ c.support, (c ^ k) a = g a) ↔ ∀ (x : α), (c ^ k) x = (ofSubtype (g.subtypePerm ⋯)) x

Tactic:
apply forall_congr'

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 : ℤ
⊢ ∀ (a : α), a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a
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:
apply forall_congr'

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g) x ≠ x
h : y = x
⊢ False

Tactic:
mul_apply,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : (g.cycleOf x)⁻¹ (g x) ≠ x
h : y = x
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g) y ≠ y
h : g y = y
⊢ False

Tactic:
mul_apply,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : (g.cycleOf x)⁻¹ (g y) ≠ y
h : g y = y
⊢ False
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
j : Fin n
⊢ ↑((cycleRange 0) j) = ↑(1 j)

Tactic:
rcases (Fin.zero_le j).eq_or_lt with rfl | hj

Goal state after:
case inl
n : ℕ
inst✝ : NeZero n
⊢ ↑((cycleRange 0) 0) = ↑(1 0)

case inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑((cycleRange 0) j) = ↑(1 j)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ l'.toFinset = l.toFinset → (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset

Tactic:
· intro h
    have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
    have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
    refine ⟨?_, ?_, ?_⟩
    · exact fun _ h => hc' _ (hperm.subset h)
    · rwa [hperm.pairwise_iff symm]
    · rw [← hp', hperm.symm.prod_eq']
      exact hd'.imp Disjoint.commute

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : sign π = π.signAux
⊢ sign (swap i j * π) = (swap i j * π).signAux

Tactic:
rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

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
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
Finset.disjoint_left

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ ∀ ⦃a : Perm α⦄, a ∈ f.cycleFactorsFinset → a ∉ g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : 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
⊢ (g * f⁻¹) x = x

Tactic:
mul_apply,

Goal state after:
case neg
α : 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
⊢ g (f⁻¹ x) = x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ (d * c) x = d x ↔ c x = x

Tactic:
mul_apply,

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ d (c x) = d x ↔ c x = x
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
⊢ ∀ x ∈ (swap a b).support ⊔ (swap a c).support, x ∈ {a, b, c}

Tactic:
simp [ab, ac]

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

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

Tactic:
rw [mem_support]

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : [a, g a, g (g a)].Nodup
⊢ g a ≠ a
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg : g = swap a (g a) * swap (g a) (g (g a))
⊢ a ∈ g.support

Tactic:
rw [mem_support]

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg : g = swap a (g a) * swap (g a) (g (g a))
⊢ g a ≠ a