[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a✝ : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M' M
hf : Injective ↑f
smul : ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
a : R
⊢ ↑f (a • 0) = ↑f 0
[PROOFSTEP]
simp [smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a✝ : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M' M
hf : Injective ↑f
smul : ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
a : M'
⊢ ↑f (0 • a) = ↑f 0
[PROOFSTEP]
simp [smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M M'
hf : Surjective ↑f
smul : ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
c : R
⊢ c • 0 = 0
[PROOFSTEP]
rw [← f.map_zero, ← smul, smul_zero]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M M'
hf : Surjective ↑f
smul : ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
m : M'
⊢ 0 • m = 0
[PROOFSTEP]
rcases hf m with ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom M M'
hf : Surjective ↑f
smul : ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
x : M
⊢ 0 • ↑f x = 0
[PROOFSTEP]
simp [← smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom R' R
m : M
⊢ 0 • m = 0
[PROOFSTEP]
show (f 0) • m = 0
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : SMulWithZero R M
a : R
b : M
inst✝² : Zero R'
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : ZeroHom R' R
m : M
⊢ ↑f 0 • m = 0
[PROOFSTEP]
rw [map_zero, zero_smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero R'
inst✝² : Zero M
inst✝¹ : MulActionWithZero R M
inst✝ : Subsingleton R
x y : M
⊢ x = y
[PROOFSTEP]
rw [← one_smul R x, ← one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
m : M
⊢ 1 • m = m
[PROOFSTEP]
show (f 1) • m = m
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
m : M
⊢ ↑f 1 • m = m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
r s : R'
m : M
⊢ (r * s) • m = r • s • m
[PROOFSTEP]
show f (r * s) • m = (f r) • (f s) • m
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
inst✝⁵ : MonoidWithZero R
inst✝⁴ : MonoidWithZero R'
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Zero M'
inst✝ : SMul R M'
f : R' →*₀ R
src✝ : SMulWithZero R' M := SMulWithZero.compHom M ↑f
r s : R'
m : M
⊢ ↑f (r * s) • m = ↑f r • ↑f s • m
[PROOFSTEP]
simp [mul_smul]
[GOAL]
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
obtain rfl | hc := eq_or_ne c 0
[GOAL]
case inl
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
x : β
⊢ (0 • x)⁻¹ = 0⁻¹ • x⁻¹
[PROOFSTEP]
simp only [inv_zero, zero_smul]
[GOAL]
case inr
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
obtain rfl | hx := eq_or_ne x 0
[GOAL]
case inr.inl
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
hc : c ≠ 0
⊢ (c • 0)⁻¹ = c⁻¹ • 0⁻¹
[PROOFSTEP]
simp only [inv_zero, smul_zero]
[GOAL]
case inr.inr
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
refine' inv_eq_of_mul_eq_one_left _
[GOAL]
case inr.inr
R : Type u_1
R' : Type u_2
M : Type u_3
M' : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1
[PROOFSTEP]
rw [smul_mul_smul, inv_mul_cancel hc, inv_mul_cancel hx, one_smul]
