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

Goal state before:
pp: case cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)

Tactic:
]

Goal state after:
case cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mp.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h✝ : (orderOf f).gcd n = 1
⊢ (orderOf f).gcd n = 1

Tactic:
]

Goal state after:
case intro.mp.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h✝ : (orderOf f).gcd n = 1
⊢ (orderOf f).gcd n = 1
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.IsCycle

Tactic:
]

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.support

Tactic:
]

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.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * b ^ (n + m) = a * b ^ (n + m)

Tactic:
]

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

Goal state before:
pp: case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : (f ^ n) x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
]

Goal state after:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : (f ^ n) x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * b ^ (m + 1) = a * b ^ (m + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * b ^ (n + 1) = a * b ^ (n + 1)

Tactic:
]

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

Goal state before:
pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1

Tactic:
]

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : orderOf f ∣ n
⊢ f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k)) x = x
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, b)

Tactic:
]

Goal state after:
case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b

Tactic:
]

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ a

Tactic:
]

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
]

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case cons.inr
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
]

Goal state after:
case cons.inr
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : f x = x
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
]

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : f x = x
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1

Tactic:
]

Goal state after:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n

Tactic:
]

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ ¬orderOf f ∣ n
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
]

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

Goal state before:
pp: case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ (a, (σ a) b) = (a, (σ a) b)

Tactic:
]

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

Goal state before:
pp: α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑(Equiv.symm g) ⁻¹' s
y : α
hy : y ∈ ⇑(Equiv.symm g) ⁻¹' s
⊢ (g * f * g⁻¹).SameCycle x y

Tactic:
]

Goal state after:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑(Equiv.symm g) ⁻¹' s
y : α
hy : y ∈ ⇑(Equiv.symm g) ⁻¹' s
⊢ (g * f * g⁻¹).SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y

Tactic:
]

Goal state after:
α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ y = y

Tactic:
]

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

Goal state before:
pp: case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a
⊢ a ∈ a :: l ∧ (prodExtendRight a (σ a)) (a, b) = (a, (σ a) b) ∨ a ∉ a :: l ∧ (prodExtendRight a (σ a)) (a, b) = (a, b)

Tactic:
]

Goal state after:
case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a
⊢ a ∈ a :: l ∧ (prodExtendRight a (σ a)) (a, b) = (a, (σ a) b) ∨ a ∉ a :: l ∧ (prodExtendRight a (σ a)) (a, b) = (a, b)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a
⊢ (a, (σ a) b) = (a, (σ a) b)

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ y = y

Tactic:
]

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

Goal state before:
pp: α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ (a, b) = (a, b)

Tactic:
]

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_to_finset : l.toFinset = univ
⊢ (List.map (⇑sign ∘ fun a ↦ prodExtendRight a (σ a)) l).prod = (List.map (fun k ↦ sign (σ k)) l).prod

Tactic:
]

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
l_to_finset : l.toFinset = univ
⊢ (List.map (⇑sign ∘ fun a ↦ prodExtendRight a (σ a)) l).prod = (List.map (fun k ↦ sign (σ k)) l).prod
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
⊢ sign (f.trans (Equiv.trans p g)) = sign (g.permCongr p * f.trans g)

Tactic:
]

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
⊢ sign (f.trans (Equiv.trans p g)) = sign (g.permCongr p * f.trans g)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}

Tactic:
]

Goal state after:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
this : sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb
⊢ sign (σa.sumCongr σb) = sign (σa.sumCongr σb)

Tactic:
]

Goal state after:
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
⊢ (insert i (Finset.univ.erase i)).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ 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
⊢ (insert i (Finset.univ.erase i)).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f a = a
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

Tactic:
]

Goal state after:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f a = a
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ -1 * sign σa' = -1 * sign σa'

Tactic:
]

Goal state after:
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) (Pi.mulSingle i y i) * (Finset.univ.erase i).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ 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) (Pi.mulSingle i y i) * (Finset.univ.erase i).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
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 * (Finset.univ.erase i).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ 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 * (Finset.univ.erase i).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case right.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ -1 * sign σb' = -1 * sign σb'

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ℤˣ
σ : Perm α
⊢ sign σ = s ↔ sign σ = s

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ a ∈ ofSign 1, ∀ b ∈ ofSign (-1), a ≠ b

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ a ∈ ofSign 1, ∀ b ∈ ofSign (-1), a ≠ b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
⊢ False

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
⊢ False
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 * ?m ^ (Finset.univ.erase i).card = (ϕ i) y

pp: case m
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
⊢ M

pp: case h
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
⊢ ∀ x ∈ Finset.univ.erase i, (ϕ x) (Pi.mulSingle i y x) = ?m

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 * ?m ^ (Finset.univ.erase i).card = (ϕ i) y

case m
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
⊢ M

case h
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
⊢ ∀ x ∈ Finset.univ.erase i, (ϕ x) (Pi.mulSingle i y x) = ?m
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ (f.subtypePerm ⋯ ^ n) ⟨a, ha⟩ = ⟨a, ha⟩

Tactic:
]

Goal state after:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ (f.subtypePerm ⋯ ^ n) ⟨a, ha⟩ = ⟨a, ha⟩
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a + y * b

Tactic:
]

Goal state after:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a + y * b
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ (↑x).gcd ↑y = d

Tactic:
]

Goal state after:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ (↑x).gcd ↑y = d
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d

Tactic:
]

Goal state after:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ x * y = x * y

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y : ℤ
⊢ x.natAbs.gcd y.natAbs = x.natAbs.gcd y.natAbs

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y : ℤ
⊢ x.natAbs.lcm y.natAbs = x.natAbs.lcm y.natAbs

Tactic:
]

Goal state after: