[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N β
f : α → β
hf : Injective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ f (c₁ • c₂ • x) = f (c₂ • c₁ • x)
[PROOFSTEP]
simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N α
f : α → β
hf : Surjective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ c₁ • c₂ • f x = c₂ • c₁ • f x
[PROOFSTEP]
simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]
[GOAL]
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α✝ : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
α : Type u_11
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ a • a' • b = a' • a • b
[PROOFSTEP]
rw [← mul_smul, mul_comm, mul_smul]
[GOAL]
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α✝ : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
α : Type u_11
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
m : Mᵐᵒᵖ
a : α
⊢ MulOpposite.unop m • a = m • a
[PROOFSTEP]
induction m using MulOpposite.rec'
[GOAL]
case h
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α✝ : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
α : Type u_11
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : α
X✝ : M
⊢ MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a
[PROOFSTEP]
exact (IsCentralScalar.op_smul_eq_smul _ a).symm
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ m • n • a = n • m • a
[PROOFSTEP]
rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = n • m • a
[PROOFSTEP]
rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = m • n • a
[PROOFSTEP]
rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁵ : SMul M α
inst✝⁴ : SMul M N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • n) • a = m • n • a
[PROOFSTEP]
rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
⊢ Sort ?u.10323
[PROOFSTEP]
haveI := comp α g
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Sort ?u.10323
[PROOFSTEP]
haveI := comp β g
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.10323
[PROOFSTEP]
exact IsScalarTower N α β
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d
[PROOFSTEP]
rw [smul_assoc, smul_assoc, smul_comm b]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a₁ a₂ : M
b : α
⊢ (if p then a₁ else a₂) • b = if p then a₁ • b else a₂ • b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a₁ a₂ : M
b : α
h✝ : p
⊢ a₁ • b = a₁ • b
[PROOFSTEP]
rfl
[GOAL]
case neg
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a₁ a₂ : M
b : α
h✝ : ¬p
⊢ a₂ • b = a₂ • b
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a : M
b₁ b₂ : α
⊢ (a • if p then b₁ else b₂) = if p then a • b₁ else a • b₂
[PROOFSTEP]
split_ifs
[GOAL]
case pos
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a : M
b₁ b₂ : α
h✝ : p
⊢ a • b₁ = a • b₁
[PROOFSTEP]
rfl
[GOAL]
case neg
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a : M
b₁ b₂ : α
h✝ : ¬p
⊢ a • b₂ = a • b₂
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : SMul M β
f : β → α
hf : Injective f
smul : ∀ (c : M) (x : β), f (c • x) = c • f x
c₁ c₂ : M
x : β
⊢ f ((c₁ * c₂) • x) = f (c₁ • c₂ • x)
[PROOFSTEP]
simp only [smul, mul_smul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
y : β
⊢ 1 • y = y
[PROOFSTEP]
rcases hf y with ⟨x, rfl⟩
[GOAL]
case intro
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
x : α
⊢ 1 • f x = f x
[PROOFSTEP]
rw [← smul, one_smul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
c₁ c₂ : M
y : β
⊢ (c₁ * c₂) • y = c₁ • c₂ • y
[PROOFSTEP]
rcases hf y with ⟨x, rfl⟩
[GOAL]
case intro
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
c₁ c₂ : M
x : α
⊢ (c₁ * c₂) • f x = c₁ • c₂ • f x
[PROOFSTEP]
simp only [← smul, mul_smul]
[GOAL]
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_10
S : Type u_11
M : Type u_12
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ↑f
hsmul : ∀ (c : R) (x : M), ↑f c • x = c • x
b : M
⊢ 1 • b = b
[PROOFSTEP]
rw [← f.map_one, hsmul, one_smul]
[GOAL]
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_10
S : Type u_11
M : Type u_12
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ↑f
hsmul : ∀ (c : R) (x : M), ↑f c • x = c • x
a b : R
x : M
⊢ (↑f a * ↑f b) • x = ↑f a • ↑f b • x
[PROOFSTEP]
simp only [← f.map_mul, hsmul, mul_smul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : MulAction M α
inst✝² : Mul α
r s : M
x y : α
inst✝¹ : IsScalarTower M α α
inst✝ : SMulCommClass M α α
⊢ r • x * s • y = (r * s) • (x * y)
[PROOFSTEP]
rw [smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝¹ : Monoid M
inst✝ : MulAction M α
y₁ y₂ : α
H : (fun y x => x • y) y₁ = (fun y x => x • y) y₂
⊢ 1 • y₁ = 1 • y₂
[PROOFSTEP]
convert congr_fun H 1
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ 1 • x✝ = x✝
[PROOFSTEP]
simp [(· • ·)]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ SMul.smul 1 x✝ = x✝
[PROOFSTEP]
apply MulAction.one_smul
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝
[PROOFSTEP]
simp [(· • ·)]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ SMul.smul (↑g x✝² * ↑g x✝¹) x✝ = SMul.smul (↑g x✝²) (SMul.smul (↑g x✝¹) x✝)
[PROOFSTEP]
apply MulAction.mul_smul
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
N : Type u_11
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ (x • 1) • y = x • y
[PROOFSTEP]
rw [smul_assoc, one_smul]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
N : Type u_11
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • 1 * y = x • y
[PROOFSTEP]
rw [smul_mul_assoc, one_mul]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
N : Type u_11
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ y * x • 1 = x • y
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
N : Type u_11
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type u_10
N : Type u_11
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • x • z
[PROOFSTEP]
rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
M : Type ?u.30564
N : Type ?u.30567
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ OneHom.toFun { toFun := fun x => x • 1, map_one' := (_ : 1 • 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => x • 1, map_one' := (_ : 1 • 1 = 1) } x *
      OneHom.toFun { toFun := fun x => x • 1, map_one' := (_ : 1 • 1 = 1) } y
[PROOFSTEP]
rw [smul_one_mul, smul_smul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : Zero A
inst✝² : SMulZeroClass M A
inst✝¹ : Zero B
inst✝ : SMul M B
f : ZeroHom B A
hf : Injective ↑f
smul : ∀ (c : M) (x : B), ↑f (c • x) = c • ↑f x
c : M
⊢ ↑f (c • 0) = ↑f 0
[PROOFSTEP]
simp only [smul, map_zero, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : Zero A
inst✝² : SMulZeroClass M A
inst✝¹ : Zero B
inst✝ : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
c : M
⊢ c • 0 = 0
[PROOFSTEP]
rw [← map_zero f, ← smul, smul_zero]
[GOAL]
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Zero A
inst✝³ : SMulZeroClass M✝ A
R : Type u_10
S : Type u_11
M : Type u_12
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
⊢ f c • 0 = 0
[PROOFSTEP]
rw [hsmul, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : AddZeroClass A
inst✝¹ : DistribSMul M A
inst✝ : AddZeroClass B
r : M
f : B →+ A
⊢ (fun a => r • ↑f a) 0 = 0
[PROOFSTEP]
simp only [map_zero, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : AddZeroClass A
inst✝¹ : DistribSMul M A
inst✝ : AddZeroClass B
r : M
f : B →+ A
x y : B
⊢ ZeroHom.toFun { toFun := fun a => r • ↑f a, map_zero' := (_ : r • ↑f 0 = 0) } (x + y) =
    ZeroHom.toFun { toFun := fun a => r • ↑f a, map_zero' := (_ : r • ↑f 0 = 0) } x +
      ZeroHom.toFun { toFun := fun a => r • ↑f a, map_zero' := (_ : r • ↑f 0 = 0) } y
[PROOFSTEP]
simp only [map_add, smul_add]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : B →+ A
hf : Injective ↑f
smul : ∀ (c : M) (x : B), ↑f (c • x) = c • ↑f x
src✝ : SMulZeroClass M B := Injective.smulZeroClass (↑f) hf smul
c : M
x y : B
⊢ ↑f (c • (x + y)) = ↑f (c • x + c • y)
[PROOFSTEP]
simp only [smul, map_add, smul_add]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : SMulZeroClass M B := ZeroHom.smulZeroClass (↑f) smul
c : M
x y : B
⊢ c • (x + y) = c • x + c • y
[PROOFSTEP]
rcases hf x with ⟨x, rfl⟩
[GOAL]
case intro
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : SMulZeroClass M B := ZeroHom.smulZeroClass (↑f) smul
c : M
y : B
x : A
⊢ c • (↑f x + y) = c • ↑f x + c • y
[PROOFSTEP]
rcases hf y with ⟨y, rfl⟩
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : SMulZeroClass M B := ZeroHom.smulZeroClass (↑f) smul
c : M
x y : A
⊢ c • (↑f x + ↑f y) = c • ↑f x + c • ↑f y
[PROOFSTEP]
simp only [smul_add, ← smul, ← map_add]
[GOAL]
M✝ : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : AddZeroClass A
inst✝³ : DistribSMul M✝ A
R : Type u_10
S : Type u_11
M : Type u_12
inst✝² : AddZeroClass M
inst✝¹ : DistribSMul R M
inst✝ : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
src✝ : SMulZeroClass S M := smulZeroClassLeft f hf hsmul
c : R
x y : M
⊢ f c • (x + y) = f c • x + f c • y
[PROOFSTEP]
simp only [hsmul, smul_add]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : AddGroup A
inst✝ : DistribMulAction M A
r : M
x : A
⊢ r • -x + r • x = 0
[PROOFSTEP]
rw [← smul_add, neg_add_self, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝² : Monoid M
inst✝¹ : AddGroup A
inst✝ : DistribMulAction M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ↑f
smul : ∀ (c : M) (x : B), ↑f (c • x) = c • ↑f x
src✝ : MulAction M B := Injective.mulAction (↑f) hf smul
c : M
x y : B
⊢ ↑f (c • (x * y)) = ↑f (c • x * c • y)
[PROOFSTEP]
simp only [smul, f.map_mul, smul_mul']
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ↑f
smul : ∀ (c : M) (x : B), ↑f (c • x) = c • ↑f x
src✝ : MulAction M B := Injective.mulAction (↑f) hf smul
c : M
⊢ ↑f (c • 1) = ↑f 1
[PROOFSTEP]
simp only [smul, f.map_one, smul_one]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : MulAction M B := Surjective.mulAction (↑f) hf smul
c : M
x y : B
⊢ c • (x * y) = c • x * c • y
[PROOFSTEP]
rcases hf x with ⟨x, rfl⟩
[GOAL]
case intro
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : MulAction M B := Surjective.mulAction (↑f) hf smul
c : M
y : B
x : A
⊢ c • (↑f x * y) = c • ↑f x * c • y
[PROOFSTEP]
rcases hf y with ⟨y, rfl⟩
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : MulAction M B := Surjective.mulAction (↑f) hf smul
c : M
x y : A
⊢ c • (↑f x * ↑f y) = c • ↑f x * c • ↑f y
[PROOFSTEP]
simp only [smul_mul', ← smul, ← f.map_mul]
[GOAL]
M : Type u_1
N : Type u_2
G : Type u_3
A : Type u_4
B : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ↑f
smul : ∀ (c : M) (x : A), ↑f (c • x) = c • ↑f x
src✝ : MulAction M B := Surjective.mulAction (↑f) hf smul
c : M
⊢ c • 1 = 1
[PROOFSTEP]
rw [← f.map_one, ← smul, smul_one]


[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⟩


[GOAL]
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ (x * y) • ↑z = ↑z
[PROOFSTEP]
rw [mul_smul, hy z, hx z]
[GOAL]
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
src✝ : Submonoid M := fixingSubmonoid M s
x✝ : M
hx : x✝ ∈ { toSubsemigroup := src✝.toSubsemigroup, one_mem' := (_ : 1 ∈ src✝.carrier) }.toSubsemigroup.carrier
z : ↑s
⊢ x✝⁻¹ • ↑z = ↑z
[PROOFSTEP]
rw [inv_smul_eq_iff, hx z]


[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a b c : N ⋊[φ] G
⊢ (a * b * c).left = (a * (b * c)).left
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a b c : N ⋊[φ] G
⊢ (a * b * c).right = (a * (b * c)).right
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (1 * a).left = a.left
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (a * 1).left = a.left
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (a⁻¹ * a).left = 1.left
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (a⁻¹ * a).right = 1.right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : N),
    OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          x *
        OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ OneHom.toFun
      { toFun := fun n => { left := n, right := 1 },
        map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        y✝
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ (OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        (x✝ * y✝)).left =
    (OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          y✝).left
[PROOFSTEP]
simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ (OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        (x✝ * y✝)).right =
    (OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          y✝).right
[PROOFSTEP]
simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : G),
    OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          x *
        OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ OneHom.toFun
      { toFun := fun g => { left := 1, right := g },
        map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        y✝
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ (OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        (x✝ * y✝)).left =
    (OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          y✝).left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ (OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        (x✝ * y✝)).right =
    (OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          y✝).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ ↑inl (↑(↑φ g) n) = ↑inr g * ↑inl n * ↑inr g⁻¹
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ (↑inl (↑(↑φ g) n)).left = (↑inr g * ↑inl n * ↑inr g⁻¹).left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ (↑inl (↑(↑φ g) n)).right = (↑inr g * ↑inl n * ↑inr g⁻¹).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ ↑inl (↑(↑φ g)⁻¹ n) = ↑inr g⁻¹ * ↑inl n * ↑inr g
[PROOFSTEP]
rw [← MonoidHom.map_inv, inl_aut, inv_inv]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g } = ↑inl n * ↑inr g
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g }.left = (↑inl n * ↑inr g).left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g }.right = (↑inl n * ↑inr g).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ ↑inl x.left * ↑inr x.right = x
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (↑inl x.left * ↑inr x.right).left = x.left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (↑inl x.left * ↑inr x.right).right = x.right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ MonoidHom.comp rightHom inl = 1
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N
⊢ ↑(MonoidHom.comp rightHom inl) x✝ = ↑1 x✝
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ MonoidHom.comp rightHom inr = MonoidHom.id G
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : G
⊢ ↑(MonoidHom.comp rightHom inr) x✝ = ↑(MonoidHom.id G) x✝
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
n : N
⊢ ↑rightHom (↑inl n) = 1
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
⊢ ↑rightHom (↑inr g) = g
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N ⋊[φ] G
⊢ x✝ ∈ MonoidHom.range inl → x✝ ∈ MonoidHom.ker rightHom
[PROOFSTEP]
simp (config := { contextual := true }) [MonoidHom.mem_ker, eq_comm]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ ↑inl x.left = x
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ (↑inl x.left).left = x.left
[PROOFSTEP]
simp_all [MonoidHom.mem_ker]
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ (↑inl x.left).right = x.right
[PROOFSTEP]
simp_all [MonoidHom.mem_ker]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
⊢ (fun a => ↑f₁ a.left * ↑f₂ a.right) 1 = 1
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
a b : N ⋊[φ] G
⊢ OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } a *
      OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } b
[PROOFSTEP]
have := fun n g ↦ FunLike.ext_iff.1 (h n) g
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
a b : N ⋊[φ] G
this :
  ∀ (n : G) (g : N),
    ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ n))) g =
      ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ n))) f₁) g
⊢ OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } a *
      OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } b
[PROOFSTEP]
simp only [MulAut.conj_apply, MonoidHom.comp_apply, MulEquiv.coe_toMonoidHom] at this
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
a b : N ⋊[φ] G
this : ∀ (n : G) (g : N), ↑f₁ (↑(↑φ n) g) = ↑f₂ n * ↑f₁ g * (↑f₂ n)⁻¹
⊢ OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } a *
      OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } b
[PROOFSTEP]
simp only [mul_left, mul_right, map_mul, this, mul_assoc, inv_mul_cancel_left]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
n : N
⊢ ↑(lift f₁ f₂ h) (↑inl n) = ↑f₁ n
[PROOFSTEP]
simp [lift]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
⊢ MonoidHom.comp (lift f₁ f₂ h) inl = f₁
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
x✝ : N
⊢ ↑(MonoidHom.comp (lift f₁ f₂ h) inl) x✝ = ↑f₁ x✝
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
g : G
⊢ ↑(lift f₁ f₂ h) (↑inr g) = ↑f₂ g
[PROOFSTEP]
simp [lift]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
⊢ MonoidHom.comp (lift f₁ f₂ h) inr = f₂
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
x✝ : G
⊢ ↑(MonoidHom.comp (lift f₁ f₂ h) inr) x✝ = ↑f₂ x✝
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝ : G
⊢ MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝)) =
    MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝))) (MonoidHom.comp F inl)
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ↑(MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝¹))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝¹))) (MonoidHom.comp F inl)) x✝
[PROOFSTEP]
simp [inl_aut]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ F =
    lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x))) (MonoidHom.comp F inl))
[PROOFSTEP]
rw [FunLike.ext_iff]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G),
    ↑F x =
      ↑(lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
            (_ :
              ∀ (x : G),
                MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
                  MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x)))
                    (MonoidHom.comp F inl)))
        x
[PROOFSTEP]
simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul, inl_left_mul_inr_right, forall_const]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
f g : N ⋊[φ] G →* H
hl : MonoidHom.comp f inl = MonoidHom.comp g inl
hr : MonoidHom.comp f inr = MonoidHom.comp g inr
⊢ f = g
[PROOFSTEP]
rw [lift_unique f, lift_unique g]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
f g : N ⋊[φ] G →* H
hl : MonoidHom.comp f inl = MonoidHom.comp g inl
hr : MonoidHom.comp f inr = MonoidHom.comp g inr
⊢ lift (MonoidHom.comp f inl) (MonoidHom.comp f inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp f inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp f inr) x))) (MonoidHom.comp f inl)) =
    lift (MonoidHom.comp g inl) (MonoidHom.comp g inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp g inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp g inr) x))) (MonoidHom.comp g inl))
[PROOFSTEP]
simp only [*]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
⊢ (fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right }) 1 = 1
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x y : N ⋊[φ] G
⊢ OneHom.toFun
      { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
        map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        y
[PROOFSTEP]
replace h := FunLike.ext_iff.1 (h x.right) y.left
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
x y : N ⋊[φ] G
h :
  ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ x.right))) y.left =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ x.right))) f₁) y.left
⊢ OneHom.toFun
      { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
        map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        y
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
x y : N ⋊[φ] G
h :
  ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ x.right))) y.left =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ x.right))) f₁) y.left
⊢ (OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        (x * y)).left =
    (OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          x *
        OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          y).left
[PROOFSTEP]
simp_all
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
x y : N ⋊[φ] G
h :
  ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ x.right))) y.left =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ x.right))) f₁) y.left
⊢ (OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        (x * y)).right =
    (OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          x *
        OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          y).right
[PROOFSTEP]
simp_all
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
n : N
⊢ ↑(map f₁ f₂ h) (↑inl n) = ↑inl (↑f₁ n)
[PROOFSTEP]
simp [map]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
⊢ MonoidHom.comp (map f₁ f₂ h) inl = MonoidHom.comp inl f₁
[PROOFSTEP]
ext
[GOAL]
case h.left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : N
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inl) x✝).left = (↑(MonoidHom.comp inl f₁) x✝).left
[PROOFSTEP]
simp
[GOAL]
case h.right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : N
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inl) x✝).right = (↑(MonoidHom.comp inl f₁) x✝).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
g : G
⊢ ↑(map f₁ f₂ h) (↑inr g) = ↑inr (↑f₂ g)
[PROOFSTEP]
simp [map]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
⊢ MonoidHom.comp (map f₁ f₂ h) inr = MonoidHom.comp inr f₂
[PROOFSTEP]
ext
[GOAL]
case h.left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : G
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inr) x✝).left = (↑(MonoidHom.comp inr f₂) x✝).left
[PROOFSTEP]
simp [map]
[GOAL]
case h.right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : G
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inr) x✝).right = (↑(MonoidHom.comp inr f₂) x✝).right
[PROOFSTEP]
simp [map]


[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : (i : I) → SMul α (f i)
inst✝¹ : ∀ (i : I), Nonempty (f i)
i : I
inst✝ : FaithfulSMul α (f i)
m₁✝ m₂✝ : α
h : ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
a : f i
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
classical
have := congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (f i)› j)) i a) i
simpa using this
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : (i : I) → SMul α (f i)
inst✝¹ : ∀ (i : I), Nonempty (f i)
i : I
inst✝ : FaithfulSMul α (f i)
m₁✝ m₂✝ : α
h : ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
a : f i
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
have := congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (f i)› j)) i a) i
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : (i : I) → SMul α (f i)
inst✝¹ : ∀ (i : I), Nonempty (f i)
i : I
inst✝ : FaithfulSMul α (f i)
m₁✝ m₂✝ : α
h : ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
a : f i
this :
  (m₁✝ • Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i =
    (m₂✝ • Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
simpa using this
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
a✝ : (i : I) → f i
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
a✝ : (i : I) → f i
x : I
⊢ (a✝ • 0) x = OfNat.ofNat 0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x : I
⊢ (a✝ • 0) x = OfNat.ofNat 0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝¹ y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
x : I
⊢ (a✝ • (x✝ + y✝)) x = (a✝ • x✝ + a✝ • y✝) x
[PROOFSTEP]
exact smul_add _ _ _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • y
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
⊢ r✝ • (x✝ * y✝) = r✝ • x✝ * r✝ • y✝
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝¹ y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
x : I
⊢ (r✝ • (x✝ * y✝)) x = (r✝ • x✝ * r✝ • y✝) x
[PROOFSTEP]
apply smul_mul'
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i), r • 1 = 1
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
⊢ r✝ • 1 = 1
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x : I
⊢ (r✝ • 1) x = OfNat.ofNat 1 x
[PROOFSTEP]
apply smul_one
[GOAL]
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x
[PROOFSTEP]
haveI : Decidable (∃ a : α, f a = x) := Classical.propDecidable _
[GOAL]
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x
[PROOFSTEP]
rw [extend_def, Pi.smul_apply, Pi.smul_apply, extend_def]
[GOAL]
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
⊢ (if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) =
    r • if h : ∃ a, f a = x then g (Classical.choose h) else e x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
h✝ : ∃ a, f a = x
⊢ (r • g) (Classical.choose h✝) = r • g (Classical.choose h✝)
[PROOFSTEP]
rfl
  -- convert (apply_dite (fun c : γ => r • c) _ _ _).symm
[GOAL]
case neg
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
h✝ : ¬∃ a, f a = x
⊢ r • e x = r • e x
[PROOFSTEP]
rfl
  -- convert (apply_dite (fun c : γ => r • c) _ _ _).symm


[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s t : Set α
b : β
g : H
h : Supports G s b
⊢ Supports G (g • s) (g • b)
[PROOFSTEP]
rintro g' hg'
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s t : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
⊢ g' • g • b = g • b
[PROOFSTEP]
rw [smul_comm, h]
[GOAL]
case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s t : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
⊢ ∀ ⦃a : α⦄, a ∈ s → g' • a = a
[PROOFSTEP]
rintro a ha
[GOAL]
case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s t : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
⊢ g' • a = a
[PROOFSTEP]
have := Set.ball_image_iff.1 hg' a ha
[GOAL]
case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s t : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
this : g' • g • a = g • a
⊢ g' • a = a
[PROOFSTEP]
rwa [smul_comm, smul_left_cancel_iff] at this


[GOAL]
M : Type u
α : Type v
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
⊢ (fun m => m • a) 1 = a
[PROOFSTEP]
simp [MulAction.one_smul]
[GOAL]
M : Type u
α : Type v
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ (m * m') • a = a
[PROOFSTEP]
rw [← smul_smul, hb, ha]
[GOAL]
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1
[PROOFSTEP]
rw [Fintype.card_eq_one_iff, mem_fixedPoints]
[GOAL]
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ (∀ (m : M), m • a = a) ↔ ∃ x, ∀ (y : ↑(orbit M a)), y = x
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ (∀ (m : M), m • a = a) → ∃ x, ∀ (y : ↑(orbit M a)), y = x
[PROOFSTEP]
exact fun h => ⟨⟨a, mem_orbit_self _⟩, fun ⟨a, ⟨x, hx⟩⟩ => Subtype.eq <| by simp [h x, hx.symm]⟩
[GOAL]
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a✝ : α
inst✝ : Fintype ↑(orbit M a✝)
h : ∀ (m : M), m • a✝ = a✝
x✝ : ↑(orbit M a✝)
a : α
x : M
hx : (fun m => m • a✝) x = a
⊢ ↑{ val := a, property := (_ : ∃ y, (fun m => m • a✝) y = a) } = ↑{ val := a✝, property := (_ : a✝ ∈ orbit M a✝) }
[PROOFSTEP]
simp [h x, hx.symm]
[GOAL]
case mpr
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ (∃ x, ∀ (y : ↑(orbit M a)), y = x) → ∀ (m : M), m • a = a
[PROOFSTEP]
intro h x
[GOAL]
case mpr
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
h : ∃ x, ∀ (y : ↑(orbit M a)), y = x
x : M
⊢ x • a = a
[PROOFSTEP]
rcases h with ⟨⟨z, hz⟩, hz₁⟩
[GOAL]
case mpr.intro.mk
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
x : M
z : α
hz : z ∈ orbit M a
hz₁ : ∀ (y : ↑(orbit M a)), y = { val := z, property := hz }
⊢ x • a = a
[PROOFSTEP]
calc
  x • a = z := Subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
  _ = a := (Subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
src✝ : Submonoid G := Stabilizer.submonoid G a
m : G
ha : m • a = a
⊢ m⁻¹ • a = a
[PROOFSTEP]
rw [inv_smul_eq_iff, ha]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)
[PROOFSTEP]
rw [inv_smul_smul]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ∀ (x y : ↑(orbit G a)), ∃ g, g • x = y
[PROOFSTEP]
rintro ⟨_, g, rfl⟩ ⟨_, h, rfl⟩
[GOAL]
case mk.intro.mk.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g h : G
⊢ ∃ g_1,
    g_1 • { val := (fun m => m • a) g, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) g) } =
      { val := (fun m => m • a) h, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) h) }
[PROOFSTEP]
use h * g⁻¹
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g h : G
⊢ (h * g⁻¹) • { val := (fun m => m • a) g, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) g) } =
    { val := (fun m => m • a) h, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) h) }
[PROOFSTEP]
ext1
[GOAL]
case h.a
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g h : G
⊢ ↑((h * g⁻¹) • { val := (fun m => m • a) g, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) g) }) =
    ↑{ val := (fun m => m • a) h, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) h) }
[PROOFSTEP]
simp [mul_smul]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ a ∈ orbit G (g • a)
[PROOFSTEP]
simp only [orbit_smul, mem_orbit_self]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)
[PROOFSTEP]
simp only [orbit_smul, mem_orbit]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ a ∈ orbit G b → b ∈ orbit G a
[PROOFSTEP]
simp [orbit_eq_iff.symm, eq_comm]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ ∀ {z : α}, a ∈ orbit G b → b ∈ orbit G z → a ∈ orbit G z
[PROOFSTEP]
simp (config := { contextual := true }) [orbit_eq_iff.symm, eq_comm]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
letI := orbitRel G α
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ f ⁻¹' (f '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
ext a
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) ↔ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) → a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
rintro ⟨b, hb, hab⟩
[GOAL]
case h.mp.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a b : α
hb : b ∈ U
hab : f b = f a
⊢ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
obtain ⟨g, rfl⟩ := Quotient.exact hab
[GOAL]
case h.mp.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
rw [Set.mem_iUnion]
[GOAL]
case h.mp.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ ∃ i, a ∈ (fun x x_1 => x • x_1) i '' U
[PROOFSTEP]
exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
[GOAL]
case h.mpr
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U → a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
⊢ a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
rw [Set.mem_iUnion] at hx
[GOAL]
case h.mpr
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : ∃ i, a ∈ (fun x x_1 => x • x_1) i '' U
⊢ a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
obtain ⟨g, u, hu₁, hu₂⟩ := hx
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
rw [Set.mem_preimage, Set.mem_image_iff_bex]
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ ∃ x x_1, f x = f a
[PROOFSTEP]
refine' ⟨g⁻¹ • a, _, by simp only [Quotient.eq']; use g⁻¹⟩
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ f (g⁻¹ • a) = f a
[PROOFSTEP]
simp only [Quotient.eq']
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ Setoid.r (g⁻¹ • a) a
[PROOFSTEP]
use g⁻¹
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ g⁻¹ • a ∈ U
[PROOFSTEP]
rw [← hu₂]
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ g⁻¹ • (fun x x_1 => x • x_1) g u ∈ U
[PROOFSTEP]
convert hu₁
[GOAL]
case h.e'_4
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ g⁻¹ • (fun x x_1 => x • x_1) g u = u
[PROOFSTEP]
simp only [inv_smul_smul]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
[PROOFSTEP]
letI := orbitRel G α
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
[PROOFSTEP]
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
[PROOFSTEP]
refine' ⟨fun h a a_in_U g g_in_V => h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, _⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, _⟩
[GOAL]
case refine'_1
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
a : α
a_in_U : a ∈ U
g : G
g_in_V : g • a ∈ V
⊢ (fun m => m • g • a) g⁻¹ = a
[PROOFSTEP]
simp
[GOAL]
case refine'_2
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ (∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V) → Disjoint (f '' U) (f '' V)
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
⊢ Disjoint (f '' U) (f '' V)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
case refine'_2
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
⊢ ∀ ⦃a : Quotient (orbitRel G α)⦄, a ∈ f '' U → ¬a ∈ f '' V
[PROOFSTEP]
rintro _ ⟨b, hb₁, hb₂⟩ ⟨c, hc₁, hc₂⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
a✝ : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a✝
c : α
hc₁ : c ∈ V
hc₂ : f c = a✝
⊢ False
[PROOFSTEP]
obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
a✝ : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a✝
g : G
hc₁ : (fun m => m • b) g ∈ V
hc₂ : f ((fun m => m • b) g) = a✝
⊢ False
[PROOFSTEP]
exact h b hb₁ g hc₁
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
x : Quotient G α
⊢ a ∈ orbit x ↔ Quotient.mk'' a = x
[PROOFSTEP]
induction x using Quotient.inductionOn'
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' a = Quotient.mk'' a✝
[PROOFSTEP]
rw [Quotient.eq'']
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Setoid.r a a✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
⊢ orbit x = MulAction.orbit G (φ x)
[PROOFSTEP]
conv_lhs => rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
| orbit x
[PROOFSTEP]
rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
| orbit x
[PROOFSTEP]
rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
| orbit x
[PROOFSTEP]
rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer G a)
[PROOFSTEP]
ext h
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer G a)
[PROOFSTEP]
rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul, mul_left_inv, one_smul, ←
  mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : Setoid.Rel (orbitRel G α) a b
g : G := Classical.choose h
hg : g • b = a
⊢ stabilizer G a = Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer G b)
[PROOFSTEP]
rw [← hg, stabilizer_smul_eq_stabilizer_map_conj]
[GOAL]
G : Type u
α : Type v
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
⊢ stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer G a)
[PROOFSTEP]
ext h
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g +ᵥ a) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer G a)
[PROOFSTEP]
rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd, add_left_neg, zero_vadd, ←
  mem_stabilizer_iff, AddSubgroup.mem_map_equiv, AddAut.conj_symm_apply]
[GOAL]
G : Type u
α : Type v
inst✝¹ : AddGroup G
inst✝ : AddAction G α
a b : α
h : Setoid.Rel (orbitRel G α) a b
g : G := Classical.choose h
hg : g +ᵥ b = a
⊢ stabilizer G a = AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer G b)
[PROOFSTEP]
rw [← hg, stabilizer_vadd_eq_stabilizer_map_conj]
[GOAL]
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a = b
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a - b = 0
[PROOFSTEP]
refine' h _ _
[GOAL]
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ k • (a - b) = 0
[PROOFSTEP]
rw [smul_sub, h', sub_self]