mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
⊢ n < (bs.insertIdx m x).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ some (l.prev a ha) = l[idxOf a l - 1]?

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ idxOf a l - 1 < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
⊢ (bs.insertIdx m x)[n] = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
⊢ [l.prev a ha, a].length + (idxOf a l - 1) ≤ l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ [l.prev a ha, a] <:+: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
this : x ∈ bs
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.prev a ha = l[(idxOf a l + (l.length - 1)) % l.length]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ 0 < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ l.prev l[i] ⋯ = l[(i + (l.length - 1)) % l.length]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.length - 1 + 1 = l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
h1 : l.length - 1 + 1 = l.length
⊢ l.length - 1 < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.next (l.getLast h) ⋯ = l.head h

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap l.next l ⋯ = l.rotate 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap l.prev l ⋯ = l.rotate (l.length - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev (l.next x hx) ⋯ = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + tl.length + 1) % (tl.length + 1) = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : m < n
this : x ∈ as
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.next (l.prev x hx) ⋯ = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
⊢ l.length - 1 - k < l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ k < (pmap l.next l ⋯).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x y : α
s : List α
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.1 ∈ orbit M y.1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.2 ∈ orbit M y.2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (∀ (m : M), m • a = a) → (orbit M a).Subsingleton

Tactic:
· rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩
    simp only [h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝³ : Monoid M
α : Type v
inst✝² : MulAction M α
β : Type u_1
inst✝¹ : MulAction M β
m : M
inst✝ : DecidableEq β
b : β
⊢ Decidable ((fun b ↦ b ∈ fixedBy β m) b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ fixedPoints G α = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a : α
⊢ ∀ (x y : ↑(orbit G a)), ∃ g, g • x = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.prev x ⋯ = l.next x hx

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l.prev x hx

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ (fun m ↦ m • b✝) ⟨gv, gp⟩ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Tactic:
simp only

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ (fun m ↦ m • b✝) ⟨gv, gp⟩ ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
simp only

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.next x hx = l'.next x ⋯

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
⊢ orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(H ⊓ K)) α

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev x hx = l'.prev x ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ (a :: l).rotate 1 = l ++ [a]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
x✝ : List α
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α)) x✝)).reverse = Quot.mk (⇑(IsRotated.setoid α)) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ s.reverse.Subsingleton ↔ s.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
x : orbitRel.Quotient G α
⊢ ∀ (x_1 y : ↑x.orbit), ∃ g, g • x_1 = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ ∀ (g : Ω), Finite ↑g.orbit

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ Finite α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsCancelSMul G α ↔ ∀ (a : α), stabilizer G a = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
l : List α
hl : l.Nodup
⊢ (↑l).Nontrivial ↔ 2 ≤ l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ s.reverse.Nontrivial ↔ s.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) = stabilizer G b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer hg) x) = (MulAut.conj g) ↑x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G b)
⊢ ↑((stabilizerEquivStabilizer hg).symm x) = (MulAut.conj g⁻¹) ↑x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ stabilizerEquivStabilizer ⋯ = MulEquiv.refl ↥(stabilizer G a)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nontrivial
⊢ 2 ≤ s.length

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (a ∈ S ↔ b ∈ S) → ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ swap a b ∈ MulAction.stabilizer (Perm α) S ↔ (a ∈ S ↔ b ∈ S)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ tl = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ s.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), (toMultiset (Quotient.mk'' a)).card = length (Quotient.mk'' a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), toMultiset (Quotient.mk'' a) = 0 ↔ Quotient.mk'' a = nil

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Cycle α
⊢ ∀ (a : List α), map f (Quotient.mk'' a) = nil ↔ Quotient.mk'' a = nil

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Cycle α
⊢ ∀ (a : List α), b ∈ map f (Quotient.mk'' a) ↔ ∃ a_1 ∈ Quotient.mk'' a, f a_1 = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
⊢ ↑l₁.cyclicPermutations = ↑l₂.cyclicPermutations

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
⊢ nil.lists = {[]}

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ¬(↑[]).Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ ¬(↑[x]).Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x = y
⊢ (↑(x :: y :: l)).Nontrivial ↔ (↑(x :: l)).Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ x ∈ ↑(x :: y :: l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ y ∈ ↑(x :: y :: l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : { l // l.Nodup }
⊢ (↑↑l).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
hs✝ : List α
hs : Nodup (Quotient.mk'' hs✝)
⊢ (fun l ↦ ⟨↑↑l, ⋯⟩) ⟨hs✝, hs⟩ = ⟨Quotient.mk'' hs✝, hs⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
s : Cycle α
hs : s.Nodup
⊢ ∃ a, (fun l ↦ ⟨↑↑l, ⋯⟩) a = ⟨s, hs⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Cycle α),
    x ∈ Finset.filter Nontrivial (Finset.map (Function.Embedding.subtype fun s ↦ s.Nodup) Finset.univ) ↔
      x.Nodup ∧ x.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
⊢ ∀ (a : List α), toFinset (Quotient.mk'' a) = ∅ ↔ Quotient.mk'' a = nil

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ (n ^ k).minFac = n.minFac

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ (p ^ k).minFac = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x hm = l₂.next y hm'

Tactic:
rw [heq_iff_eq] at hxy

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x hm = l₂.next y hm'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x hm = l₂.next y hm'

Tactic:
by

Goal state after: