[GOAL]
M : Type ?u.4198
N : Type ?u.4201
α : Type ?u.4204
β : Type ?u.4214
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
⊢ ∀ (m : Mᵈᵐᵃ) (n : N) (a : α →ₘ[μ] β), m • n • a = n • m • a
[PROOFSTEP]
rintro _ _ ⟨_⟩
[GOAL]
case mk
M : Type ?u.4198
N : Type ?u.4201
α : Type ?u.4204
β : Type ?u.4214
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
m✝ : Mᵈᵐᵃ
n✝ : N
a✝¹ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ m✝ • n✝ • Quot.mk Setoid.r a✝ = n✝ • m✝ • Quot.mk Setoid.r a✝
[PROOFSTEP]
rfl
[GOAL]
M : Type ?u.8732
N : Type ?u.8735
α : Type ?u.8738
β : Type ?u.8748
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
⊢ ∀ (a : Mᵈᵐᵃ) (x y : α →ₘ[μ] β), a • (x + y) = a • x + a • y
[PROOFSTEP]
rintro _ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
M : Type ?u.8732
N : Type ?u.8735
α : Type ?u.8738
β : Type ?u.8748
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
a✝² : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ a✝² • (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) = a✝² • Quot.mk Setoid.r a✝¹ + a✝² • Quot.mk Setoid.r a✝
[PROOFSTEP]
rfl
[GOAL]
M : Type ?u.19747
N : Type ?u.19750
α : Type ?u.19753
β : Type ?u.19763
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace N
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : Monoid M
inst✝⁴ : MulAction M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : Monoid β
inst✝ : ContinuousMul β
⊢ ∀ (r : Mᵈᵐᵃ) (x y : α →ₘ[μ] β), r • (x * y) = r • x * r • y
[PROOFSTEP]
rintro _ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
M : Type ?u.19747
N : Type ?u.19750
α : Type ?u.19753
β : Type ?u.19763
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace N
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : Monoid M
inst✝⁴ : MulAction M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : Monoid β
inst✝ : ContinuousMul β
r✝ : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ r✝ • (Quot.mk Setoid.r a✝¹ * Quot.mk Setoid.r a✝) = r✝ • Quot.mk Setoid.r a✝¹ * r✝ • Quot.mk Setoid.r a✝
[PROOFSTEP]
rfl
