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

Goal state before:
pp: case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n + 1 < (y :: l).length

Tactic:
simpa using

Goal state after:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n < l.length
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x ∈ f.support

Tactic:
simpa using

Goal state after:
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ ¬f x = x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n + 1 < (y :: l).length

Tactic:
simpa [Nat.succ_lt_succ_iff] using hn

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f = 1
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a b : α
⊢ b ∈ f.support ↔ ?m.105 b

Tactic:
← hins,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a b : α
⊢ b ∈ {x, y} ↔ ?m.105 b
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i < xs.length.succ

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i < xs.length + 1
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).Nodup

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ l.Nodup
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ x ∉ l

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ x ∉ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
a b : α
⊢ (x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * Equiv.swap a b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
a b : α
⊢ (y :: (l ++ [a, b])).formPerm = (y :: (l ++ [a])).formPerm * Equiv.swap a b
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
this : x' ∈ {z | (x :: y :: l).formPerm z ≠ z}
⊢ x' ∈ x :: y :: l

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
this : x' ∈ {z | (x :: y :: l).formPerm z ≠ z}
⊢ x' = x ∨ x' = y ∨ x' ∈ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h.zero.e_i
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (0 + n) % (x :: y :: l).length = n

Tactic:
simpa using

Goal state after:
case h.h.zero.e_i
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ n < l.length + 1 + 1
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : ((Equiv.symm g) x :: l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f ((Equiv.symm g) x) = (Equiv.symm g) x
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap ((Equiv.symm g) x) b * f) (permsOfList l)) l
hx' : f ∈ List.map (fun f ↦ Equiv.swap ((Equiv.symm g) x) x * f) (permsOfList l)
hg : g ∈ permsOfList l ∧ Equiv.swap ((Equiv.symm g) x) x * g = f
hxa : x ≠ (Equiv.symm g) x
⊢ g ((Equiv.symm g) x) ≠ (Equiv.symm g) x

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : ((Equiv.symm g) x :: l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f ((Equiv.symm g) x) = (Equiv.symm g) x
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap ((Equiv.symm g) x) b * f) (permsOfList l)) l
hx' : f ∈ List.map (fun f ↦ Equiv.swap ((Equiv.symm g) x) x * f) (permsOfList l)
hg : g ∈ permsOfList l ∧ Equiv.swap ((Equiv.symm g) x) x * g = f
hxa : x ≠ (Equiv.symm g) x
⊢ ¬x = (Equiv.symm g) x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
this : ¬b₁ < b₂
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
split_ifs at h

Goal state after:
case pos
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
this : ¬b₁ < b₂
h✝¹ : f a₂ < f a₁
h✝ : f b₂ < f b₁
h : ⟨f a₁, f a₂⟩ = ⟨f b₁, f b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

case neg
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
this : ¬b₁ < b₂
h✝¹ : f a₂ < f a₁
h✝ : ¬f b₂ < f b₁
h : ⟨f a₁, f a₂⟩ = ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

case pos
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
this : ¬b₁ < b₂
h✝¹ : ¬f a₂ < f a₁
h✝ : f b₂ < f b₁
h : ⟨f a₂, f a₁⟩ = ⟨f b₁, f b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

case neg
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
this : ¬b₁ < b₂
h✝¹ : ¬f a₂ < f a₁
h✝ : ¬f b₂ < f b₁
h : ⟨f a₂, f a₁⟩ = ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k < n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
simpa using

Goal state after:
case succ.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k < n✝
⊢ ¬n✝ = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹) y ≠ y
⊢ (g * f * g⁻¹).SameCycle (g x) y

Tactic:
simpa using

Goal state after:
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹) y ≠ y
⊢ f.SameCycle x ((Equiv.symm g) y)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ x ∈ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | l.formPerm x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | l.formPerm x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
this : x ∉ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
this : x ∉ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ (l.formPerm ^ l.length) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : 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
⊢ (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b

Tactic:
simpa using

Goal state after:
α : 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
⊢ ¬f b = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : 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
⊢ f ((f ^ n) (f x)) = f ((Equiv.symm f) b)

Tactic:
simpa using

Goal state after:
α : 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
⊢ f ((f ^ n) (f x)) = b
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ i < n

Tactic:
simpa using

Goal state after:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ i < n
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: case h
k : ℕ
a✝ : List ℕ
⊢ (Multiset.prod ⟦a✝⟧).Coprime k ↔ ∀ n ∈ ⟦a✝⟧, n.Coprime k

Tactic:
simpa using

Goal state after:
case h
k : ℕ
a✝ : List ℕ
⊢ a✝.prod.Coprime k ↔ ∀ n ∈ a✝, n.Coprime k
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: case h
k : ℕ
a✝ : List ℕ
⊢ k.Coprime (Multiset.prod ⟦a✝⟧) ↔ ∀ n ∈ ⟦a✝⟧, k.Coprime n

Tactic:
simpa using

Goal state after:
case h
k : ℕ
a✝ : List ℕ
⊢ k.Coprime a✝.prod ↔ ∀ n ∈ a✝, k.Coprime n
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: ι : Type u_1
t : Finset ι
s : ι → ℕ
x : ℕ
⊢ (∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x

Tactic:
simpa using

Goal state after:
ι : Type u_1
t : Finset ι
s : ι → ℕ
x : ℕ
⊢ (∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: ι : Type u_1
x : ℕ
t : Finset ι
s : ι → ℕ
⊢ x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
x : ℕ
t : Finset ι
s : ι → ℕ
⊢ x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
this : f.support = g.support
⊢ ∀ x ∈ g.support, f x = g x

Tactic:
simpa using

Goal state after:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
this : f.support = g.support
⊢ ∀ (x : α), ¬f x = x → f x = g x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ n) ((f ^ k) z) = (f ^ k) (1 z)

Tactic:
simpa using

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ n) ((f ^ k) z) = (f ^ k) z
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsCycleOn 1 s ↔ s.Subsingleton

Tactic:
by
  simp [IsCycleOn, Set.bijOn_id, Set.Subsingleton]

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
hab₁ : (prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : (prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)
h : (a₁, b₁).2 = (a₂, b₂).2
⊢ (a₁, b₁) = (a₂, b₂)

Tactic:
simpa using

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
hab₁ : (prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : (prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)
h : (a₁, b₁).2 = (a₂, b₂).2
⊢ b₁ = b₂
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ sign (prodCongrRight σ) = ∏ k, sign (σ k)

Tactic:
obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α

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
⊢ sign (prodCongrRight σ) = ∏ k, sign (σ k)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : f x ∈ s
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : f x ∈ s
⊢ x ∈ s
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (ofSign 1).disjUnion (ofSign (-1)) ⋯ = univ

Tactic:
by
  ext σ
  simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]

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

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ d ≠ 0

Tactic:
simpa using

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ ¬d = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
x : α
hx : x ∈ s.toList.formPerm.support
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
x : α
hx : x ∈ s.toList.formPerm.support
⊢ x ∈ s
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
x : α
hx : x ∈ {x | hs'.toFinset.toList.formPerm x ≠ x}
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
x : α
hx : x ∈ {x | hs'.toFinset.toList.formPerm x ≠ x}
⊢ x ∈ s
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne hx⟩

Goal state after:
case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ hs'.toFinset.toList.formPerm.IsCycleOn s
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
simpa using

Goal state after:
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, f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
simpa using

Goal state after:
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
⊢ List.Pairwise Disjoint l
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:
simpa using

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

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

Tactic:
simpa using

Goal state after:
case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : ¬f.SameCycle x y
⊢ ¬f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x ≠ x
⊢ 2 ≤ #(f.cycleOf x).support

Tactic:
simpa using

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x ≠ x
⊢ 2 ≤ #(f.cycleOf x).support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
simpa using

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype ↥(H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))
⊢ iSupIndep H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype ↥(H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))
⊢ iSupIndep H
Module: Mathlib.GroupTheory.NoncommPiCoprod

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ {f}.val ≤ g.cycleFactorsFinset.val

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ f ∈ g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
this : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)
⊢ (removeNone σ).optionCongr x = (swap none (σ none) * σ) x

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
this : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)
⊢ Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case h
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range ⇑(castLEEmb ⋯)

Tactic:
simpa using

Goal state after:
case h
n : ℕ
i j : Fin n
h : i < j
⊢ i < j
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
⊢ (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j

Tactic:
simpa using

Goal state after:
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
⊢ i.castLT ⋯ = last ↑j
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
i j : Fin 0
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

Tactic:
exact absurd le_rfl j.pos.not_ge

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

Goal state before:
pp: case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ

Tactic:
simpa using

Goal state after:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j < i