[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
c : α
x : β
⊢ c⁻¹ • c • x = x
[PROOFSTEP]
rw [smul_smul, mul_left_inv, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
c : α
x : β
⊢ c • c⁻¹ • x = x
[PROOFSTEP]
rw [smul_smul, mul_right_inv, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
rw [inv_eq_iff_mul_eq_one, smul_mul_smul, mul_right_inv, mul_right_inv, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
p : ℤ
⊢ (c • x) ^ p = c ^ p • x ^ p
[PROOFSTEP]
cases p
[GOAL]
case ofNat
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
a✝ : ℕ
⊢ (c • x) ^ Int.ofNat a✝ = c ^ Int.ofNat a✝ • x ^ Int.ofNat a✝
[PROOFSTEP]
simp [smul_pow, smul_inv]
[GOAL]
case negSucc
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
a✝ : ℕ
⊢ (c • x) ^ Int.negSucc a✝ = c ^ Int.negSucc a✝ • x ^ Int.negSucc a✝
[PROOFSTEP]
simp [smul_pow, smul_inv]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Mul β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
a b : β
r : α
⊢ Commute (r • a) b ↔ Commute a b
[PROOFSTEP]
rw [Commute.symm_iff, Commute.smul_right_iff, Commute.symm_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
a✝ a : α
ha : a ≠ 0
x y : β
h : a⁻¹ • x = y
⊢ x = a • y
[PROOFSTEP]
rw [← h, smul_inv_smul₀ ha]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
a✝ a : α
ha : a ≠ 0
x y : β
h : x = a • y
⊢ a⁻¹ • x = y
[PROOFSTEP]
rw [h, inv_smul_smul₀ ha]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0
[PROOFSTEP]
rw [← inv_smul_smul a x, h, smul_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
⊢ ∀ (b : A → B), 1 • b = b
[PROOFSTEP]
intro f
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ 1 • f = f
[PROOFSTEP]
show (fun x => f ((1 : G)⁻¹ • x)) = f
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ (fun x => f (1⁻¹ • x)) = f
[PROOFSTEP]
simp only [inv_one, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
⊢ ∀ (x y : G) (b : A → B), (x * y) • b = x • y • b
[PROOFSTEP]
intros x y f
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (x * y) • f = x • y • f
[PROOFSTEP]
show (fun a => f ((x * y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (fun a => f ((x * y)⁻¹ • a)) = fun a => f (y⁻¹ • x⁻¹ • a)
[PROOFSTEP]
simp only [mul_smul, mul_inv_rev]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁵ : Group α
inst✝⁴ : Monoid β
inst✝³ : AddGroup β
inst✝² : DistribMulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
r : α
a : β
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
[PROOFSTEP]
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]
