[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b : R
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : ((fun m => a • m) ∘ fun x => s • x) c = ((fun m => a • m) ∘ fun x => s • x) d
⊢ c = d
[PROOFSTEP]
dsimp only [Function.comp] at cd 
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b : R
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : a • s • c = a • s • d
⊢ c = d
[PROOFSTEP]
rw [← smul_assoc, ← smul_assoc] at cd 
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b : R
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd✝¹ : a • s • c = a • s • d
cd✝ : (a • s) • c = a • s • d
cd : (a • s) • c = (a • s) • d
⊢ c = d
[PROOFSTEP]
exact ab cd
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b
[PROOFSTEP]
rw [← smul_eq_mul] at ab 
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b
[PROOFSTEP]
exact ab.of_smul _
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
rintro ⟨ab, ba⟩
[GOAL]
case refine'_1.intro
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
refine' ⟨ba.of_mul, ab.of_mul⟩
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case refine'_2.intro
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁵ : SMul R M
inst✝⁴ : SMul R S
inst✝³ : SMul S M
inst✝² : IsScalarTower R S M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
[PROOFSTEP]
exact ⟨ha.mul hb, hb.mul ha⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : (fun x => 1 • x) a = (fun x => 1 • x) b
⊢ a = b
[PROOFSTEP]
dsimp only [Function.comp] at ab 
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b
[PROOFSTEP]
rw [one_smul, one_smul] at ab 
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b
[PROOFSTEP]
assumption
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (?m.10326 h * b)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
[PROOFSTEP]
exact one M
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ Nat.zero)
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1
[PROOFSTEP]
simp only [one]
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ Nat.succ n)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)
[PROOFSTEP]
exact (ra.smul_iff (a ^ n)).mpr hn
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a
[PROOFSTEP]
refine' ⟨_, pow n⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ', ← smul_eq_mul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ Nat.pred n • a) → IsSMulRegular M a
[PROOFSTEP]
exact of_smul _
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
[PROOFSTEP]
exact one M
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ (fun x => 0 • x) a = (fun x => 0 • x) b
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
[PROOFSTEP]
repeat' rw [MulActionWithZero.zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
[PROOFSTEP]
rw [MulActionWithZero.zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a✝ b✝ : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b
[PROOFSTEP]
rw [MulActionWithZero.zero_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M
[PROOFSTEP]
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
[PROOFSTEP]
rw [← mul_and_mul_iff]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
[PROOFSTEP]
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g
[PROOFSTEP]
intro x y h
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ x = y
[PROOFSTEP]
convert congr_arg (g⁻¹ • ·) h using 1
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ x = g⁻¹ • (fun x => g • x) x
[PROOFSTEP]
simp [← smul_assoc]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x => g • x) x = (fun x => g • x) y
⊢ y = g⁻¹ • (fun x => g • x) y
[PROOFSTEP]
simp [← smul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ua : IsUnit a
⊢ IsSMulRegular M a
[PROOFSTEP]
rcases ua with ⟨a, rfl⟩
[GOAL]
case intro
R : Type u_1
S : Type u_2
M : Type u_3
b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a
[PROOFSTEP]
exact a.isSMulRegular M
