[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Monoid M
⊢ ∀ (b : M), 1 • b = b
[PROOFSTEP]
simp only [units_smul_def, ofConjAct_one, Units.val_one, one_mul, inv_one, mul_one, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Monoid M
⊢ ∀ (x y : ConjAct Mˣ) (b : M), (x * y) • b = x • y • b
[PROOFSTEP]
simp only [units_smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Monoid M
⊢ ∀ (x y : ConjAct Mˣ) (b : M),
    ↑(↑ofConjAct (x * y)) * b * ↑(↑ofConjAct (x * y))⁻¹ =
      ↑(↑ofConjAct x) * (↑(↑ofConjAct y) * b * ↑(↑ofConjAct y)⁻¹) * ↑(↑ofConjAct x)⁻¹
[PROOFSTEP]
simp only [map_mul, Units.val_mul, mul_assoc, mul_inv_rev, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ) (x y : M), r • (x * y) = r • x * r • y
[PROOFSTEP]
simp only [units_smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ) (x y : M),
    ↑(↑ofConjAct r) * (x * y) * ↑(↑ofConjAct r)⁻¹ =
      ↑(↑ofConjAct r) * x * ↑(↑ofConjAct r)⁻¹ * (↑(↑ofConjAct r) * y * ↑(↑ofConjAct r)⁻¹)
[PROOFSTEP]
simp only [mul_assoc, Units.inv_mul_cancel_left, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ), r • 1 = 1
[PROOFSTEP]
simp [units_smul_def, mul_one, Units.mul_inv, forall, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
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
[PROOFSTEP]
rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Semiring R
src✝ : MulDistribMulAction (ConjAct Rˣ) R := unitsMulDistribMulAction
⊢ ∀ (a : ConjAct Rˣ), a • 0 = 0
[PROOFSTEP]
simp only [units_smul_def, mul_zero, zero_mul, forall, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Semiring R
src✝ : MulDistribMulAction (ConjAct Rˣ) R := unitsMulDistribMulAction
⊢ ∀ (a : ConjAct Rˣ) (x y : R), a • (x + y) = a • x + a • y
[PROOFSTEP]
simp only [units_smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Semiring R
src✝ : MulDistribMulAction (ConjAct Rˣ) R := unitsMulDistribMulAction
⊢ ∀ (a : ConjAct Rˣ) (x y : R),
    ↑(↑ofConjAct a) * (x + y) * ↑(↑ofConjAct a)⁻¹ =
      ↑(↑ofConjAct a) * x * ↑(↑ofConjAct a)⁻¹ + ↑(↑ofConjAct a) * y * ↑(↑ofConjAct a)⁻¹
[PROOFSTEP]
simp only [mul_add, add_mul, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : GroupWithZero G₀
⊢ ∀ (b : G₀), 1 • b = b
[PROOFSTEP]
simp only [smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : GroupWithZero G₀
⊢ ∀ (b : G₀), ↑ofConjAct 1 * b * (↑ofConjAct 1)⁻¹ = b
[PROOFSTEP]
simp only [map_one, one_mul, inv_one, mul_one, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : GroupWithZero G₀
⊢ ∀ (x y : ConjAct G₀) (b : G₀), (x * y) • b = x • y • b
[PROOFSTEP]
simp only [smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : GroupWithZero G₀
⊢ ∀ (x y : ConjAct G₀) (b : G₀),
    ↑ofConjAct (x * y) * b * (↑ofConjAct (x * y))⁻¹ =
      ↑ofConjAct x * (↑ofConjAct y * b * (↑ofConjAct y)⁻¹) * (↑ofConjAct x)⁻¹
[PROOFSTEP]
simp only [map_mul, mul_assoc, mul_inv_rev, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : SMul α G₀
inst✝¹ : SMulCommClass α G₀ G₀
inst✝ : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
⊢ a • ug • g = ug • a • g
[PROOFSTEP]
rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : DivisionRing K
src✝ : MulAction (ConjAct K) K := mulAction₀
⊢ ∀ (a : ConjAct K), a • 0 = 0
[PROOFSTEP]
simp only [smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : DivisionRing K
src✝ : MulAction (ConjAct K) K := mulAction₀
⊢ ∀ (a : ConjAct K), ↑ofConjAct a * 0 * (↑ofConjAct a)⁻¹ = 0
[PROOFSTEP]
simp only [mul_zero, zero_mul, forall, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : DivisionRing K
src✝ : MulAction (ConjAct K) K := mulAction₀
⊢ ∀ (a : ConjAct K) (x y : K), a • (x + y) = a • x + a • y
[PROOFSTEP]
simp only [smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : DivisionRing K
src✝ : MulAction (ConjAct K) K := mulAction₀
⊢ ∀ (a : ConjAct K) (x y : K),
    ↑ofConjAct a * (x + y) * (↑ofConjAct a)⁻¹ =
      ↑ofConjAct a * x * (↑ofConjAct a)⁻¹ + ↑ofConjAct a * y * (↑ofConjAct a)⁻¹
[PROOFSTEP]
simp only [mul_add, add_mul, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ ∀ (b : G), 1 • b = b
[PROOFSTEP]
simp only [smul_def, ofConjAct_one, one_mul, inv_one, mul_one, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ ∀ (x y : ConjAct G) (b : G), (x * y) • b = x • y • b
[PROOFSTEP]
simp only [smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ ∀ (x y : ConjAct G) (b : G),
    ↑ofConjAct (x * y) * b * (↑ofConjAct (x * y))⁻¹ =
      ↑ofConjAct x * (↑ofConjAct y * b * (↑ofConjAct y)⁻¹) * (↑ofConjAct x)⁻¹
[PROOFSTEP]
simp only [map_mul, mul_assoc, mul_inv_rev, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ ∀ (r : ConjAct G) (x y : G), r • (x * y) = r • x * r • y
[PROOFSTEP]
simp only [smul_def]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ ∀ (r : ConjAct G) (x y : G),
    ↑ofConjAct r * (x * y) * (↑ofConjAct r)⁻¹ =
      ↑ofConjAct r * x * (↑ofConjAct r)⁻¹ * (↑ofConjAct r * y * (↑ofConjAct r)⁻¹)
[PROOFSTEP]
simp only [mul_assoc, inv_mul_cancel_left, forall_const, forall]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ ∀ (r : ConjAct G), r • 1 = 1
[PROOFSTEP]
simp only [smul_def, mul_one, mul_right_inv, forall, forall_const]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
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
[PROOFSTEP]
rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
⊢ fixedPoints (ConjAct G) G = ↑(center G)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
x : G
⊢ x ∈ fixedPoints (ConjAct G) G ↔ x ∈ ↑(center G)
[PROOFSTEP]
simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
g h : G
⊢ g ∈ orbit (ConjAct G) h ↔ IsConj g h
[PROOFSTEP]
rw [isConj_comm, isConj_iff, mem_orbit_iff]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
g h : G
⊢ (∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝ : Group G
g h : G
⊢ Setoid.Rel (orbitRel (ConjAct G) G) g h = IsConj g h
[PROOFSTEP]
rw [orbitRel_apply, mem_orbit_conjAct]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝¹ inst✝ : Group G
g : G
⊢ orbit (ConjAct G) g = ConjClasses.carrier (ConjClasses.mk g)
[PROOFSTEP]
ext h
[GOAL]
case h
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝¹ inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)
[PROOFSTEP]
rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑(↑(MulEquiv.symm (↑MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g
[PROOFSTEP]
change _ * _⁻¹⁻¹ = _
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑ofConjAct (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹ * ↑h * (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹⁻¹ = g⁻¹ * ↑h * g
[PROOFSTEP]
rw [inv_inv]
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑ofConjAct (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹ * ↑h * ↑(MulEquiv.toMonoidHom toConjAct) g = g⁻¹ * ↑h * g
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K✝ : Type u_6
inst✝ : Group G
H : Subgroup G
hH : Normal H
K : Subgroup { x // x ∈ H }
h : Characteristic K
a : G
ha : a ∈ map (Subgroup.subtype H) K
b : G
⊢ b * a * b⁻¹ ∈ map (Subgroup.subtype H) K
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
M : Type u_2
G : Type u_3
G₀ : Type u_4
R : Type u_5
K✝ : Type u_6
inst✝ : Group G
H : Subgroup G
hH : Normal H
K : Subgroup { x // x ∈ H }
h : Characteristic K
b : G
a : { x // x ∈ H }
ha : a ∈ ↑K
⊢ b * ↑(Subgroup.subtype H) a * b⁻¹ ∈ map (Subgroup.subtype H) K
[PROOFSTEP]
exact K.apply_coe_mem_map H.subtype ⟨_, (SetLike.ext_iff.mp (h.fixed (MulAut.conjNormal b)) a).mpr ha⟩
