case refine'_1
R : Type u_1
S : Type ?u.7631
M : Type u_2
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

case refine'_2
R : Type u_1
S : Type ?u.7631
M : Type u_2
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)
R : Type u_1
S : Type ?u.7631
M : Type u_2
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
refine' ⟨_, _⟩
case refine'_1.intro
R : Type u_1
S : Type ?u.7631
M : Type u_2
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
case refine'_1
R : Type u_1
S : Type ?u.7631
M : Type u_2
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
rintro ⟨ab, ba⟩
no goals
case refine'_1.intro
R : Type u_1
S : Type ?u.7631
M : Type u_2
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
refine' ⟨ba.of_mul, ab.of_mul⟩
case refine'_2.intro
R : Type u_1
S : Type ?u.7631
M : Type u_2
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)
case refine'_2
R : Type u_1
S : Type ?u.7631
M : Type u_2
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)
rintro ⟨ha, hb⟩
no goals
case refine'_2.intro
R : Type u_1
S : Type ?u.7631
M : Type u_2
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)
exact ⟨ha.mul hb, hb.mul ha⟩