mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ x ∈ orbitRel.Quotient.orbit (Quotient.mk'' x)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ Set.univ = ⋃ x, x.orbit

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
⊢ f a < f b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ stabilizer G a ≤ stabilizer G (a • b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m n : ℕ
mn : m ≤ n
⊢ ↑(fs m) m = ↑(fs n) m

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ stabilizer G' b ≤ stabilizer G' (a • b)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
h : Injective fun x ↦ x • b
⊢ stabilizer G (a • b) = stabilizer G a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G β
α : Type u_4
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : SMulCommClass G α β
a : α
b : β
⊢ stabilizer G (a⁻¹ • a • b) = stabilizer G b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subsemigroup.Center

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ ∀ (g : G), g * z = z * g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : G
⊢ h * g = g * h

Tactic:
← ϕ.injective.eq_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : G
⊢ ϕ (h * g) = ϕ (g * h)
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (center G).Characteristic

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : center G = ⊤
⊢ ∀ (a b : G), a * b = b * a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∈ center G
b : G
⊢ b * a * b⁻¹ ∈ center G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ center G ≤ normalizer s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
g h : M
H : IsConj g h
Hg : g ∈ Set.center M
⊢ g = h

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
⊢ c • r • v = r • c • v

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
n : ℕ
x : α
hx : x ∈ if n < g 0 then f n else (f (g (n - g 0))).tail
⊢ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ center.commMonoid.toMonoid = (center M).toMonoid

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ SMulCommClass (↥(center M)) (↥(center M)) M

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑(r * (Units.map (Submonoid.center M).subtype) u) = ↑((Units.map (Submonoid.center M).subtype) u * r)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
hx : x ∈ Set.center M
⊢ e x ∈ Set.center N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
x✝ : e x ∈ Set.center N
⊢ x ∈ Set.center M

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * (z * c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
a : M
inst✝ : Mul M
h : IsMulCentral a
b c : M
⊢ a * (b * c) = b * (a * c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
c : M
inst✝ : Mul M
h : IsMulCentral c
a b : M
⊢ a * b * c = a * c * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
⊢ z₁ * z₂ ∈ center M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S T : Set M
inst✝ : Mul M
⊢ (S ∪ T).centralizer = S.centralizer ∩ T.centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer = S.centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
⊢ ∅.centralizer = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
⊢ (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
⊢ S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
⊢ center (M × N) = center M ×ˢ center N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Centralizer

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ centralizer s.centralizer.centralizer = centralizer s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ (∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)) →
    (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a : A i
⊢ x i * a = a * x i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
b c : A i
⊢ x i * (b * c) = x i * b * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a b : A i
⊢ a * b * x i = a * (b * x i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
⊢ center ((i : ι) → A i) = univ.pi fun i ↦ center (A i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
z : M
a : z ∈ center M
g : M
⊢ g * z = z * g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * (a * b) = a * b * g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
h : ⊤ ⊆ S.centralizer
x✝¹ : M
hx : x✝¹ ∈ S
x✝ : M
⊢ x✝ * x✝¹ = x✝¹ * x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝ : M
⊢ Commute 1 x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ 1 * (x✝¹ * x✝) = 1 * x✝¹ * x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * 1 = x✝¹ * (x✝ * 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : MulOneClass M
⊢ 1 ∈ S.centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ x✝ ∈ center Mˣ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ↑a ∈ center M
⊢ ↑a⁻¹ ∈ center M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : a ∈ center M
⊢ ⅟a ∈ center M

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (x y : ConjAct Mˣ) (b : M), (x * y) • b = x • y • b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (b : M), 1 • b = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ), r • 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ) (x y : M), r • (x * y) = r • x * r • y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • um • m = um • a • m

Tactic:
by

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

Goal state before:
pp: G : Type u_4
inst✝ : Group G
H : Subgroup G
g h : ↥H
⊢ ↑(toConjAct g • h) = toConjAct ↑g • ↑h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ toConjAct g⁻¹ • h = g⁻¹ * h * g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (x y : ConjAct G) (b : G), (x * y) • b = x • y • b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (b : G), 1 • b = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (r : ConjAct G), r • 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (r : ConjAct G) (x y : G), r • (x * y) = r • x * r • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a / b ∈ S.centralizer

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • ug • g = ug • a • g

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ fixedPoints (ConjAct G) G = ↑(center G)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
⊢ ∃ g', Monotone fun n ↦ (ofLex f (g (g' n))).2

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ g ∈ orbit (ConjAct G) h ↔ IsConj g h

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ (orbitRel (ConjAct G) G) g h = IsConj g h

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
⊢ orbit (ConjAct G) g = (ConjClasses.mk g).carrier

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
⊢ centralizer {g} = comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
g' : ℕ ↪o ℕ
hg' : Monotone fun n ↦ (ofLex f (g (g' n))).2
this : f (g (g' 0)) ≤ f (g (g' 1))
⊢ g (g' 0) < g (g' 1) ∧ f (g (g' 0)) ≤ f (g (g' 1))

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
a : G
ha : a ∈ map H.subtype K
b : G
⊢ b * a * b⁻¹ ∈ map H.subtype K

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
⊢ ↑(ConjAct.ofConjAct ↑u) ∈ Submonoid.centralizer {↑x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {↑x}))ˣ
⊢ ConjAct.toConjAct ((Units.map (Submonoid.centralizer {↑x}).subtype) u) ∈ MulAction.stabilizer (ConjAct Mˣ) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x ↦ f x ^ n) ⊆ mulSupport f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝ : DivisionMonoid G
f g : α → G
⊢ 1 * 1⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
⊢ g ∈ centralizer s ↔ ∀ h ∈ s, ⁅h, g⁆ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ s.IsPWO

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
⊢ g ∈ centralizer s ↔ ∀ h ∈ s, ⁅g, h⁆ = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k * g = g * k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
⊢ map f (centralizer s) ≤ centralizer (⇑f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
⊢ {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})

Tactic:
by

Goal state after: