[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
⊢ ∀ (f g : { x // x ∈ Lp E p }), c • (f + g) = c • f + c • g
[PROOFSTEP]
rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk Setoid.r a✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk Setoid.r a✝ ∈ Lp E p
⊢ c •
      ({ val := Quot.mk Setoid.r a✝¹, property := property✝¹ } +
        { val := Quot.mk Setoid.r a✝, property := property✝ }) =
    c • { val := Quot.mk Setoid.r a✝¹, property := property✝¹ } +
      c • { val := Quot.mk Setoid.r a✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
f : { x // x ∈ Lp E p }
⊢ c • -f = -(c • f)
[PROOFSTEP]
rcases f with ⟨⟨_⟩, _⟩
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk Setoid.r a✝ ∈ Lp E p
⊢ c • -{ val := Quot.mk Setoid.r a✝, property := property✝ } =
    -(c • { val := Quot.mk Setoid.r a✝, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
⊢ ∀ (f g : { x // x ∈ Lp E p }), c • (f - g) = c • f - c • g
[PROOFSTEP]
rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk Setoid.r a✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk Setoid.r a✝ ∈ Lp E p
⊢ c •
      ({ val := Quot.mk Setoid.r a✝¹, property := property✝¹ } -
        { val := Quot.mk Setoid.r a✝, property := property✝ }) =
    c • { val := Quot.mk Setoid.r a✝¹, property := property✝¹ } -
      c • { val := Quot.mk Setoid.r a✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
⊢ ∀ (a : Mᵈᵐᵃ) (x y : { x // x ∈ Lp E p }), a • (x + y) = a • x + a • y
[PROOFSTEP]
rintro _ ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
a✝² : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk Setoid.r a✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk Setoid.r a✝ ∈ Lp E p
⊢ a✝² •
      ({ val := Quot.mk Setoid.r a✝¹, property := property✝¹ } +
        { val := Quot.mk Setoid.r a✝, property := property✝ }) =
    a✝² • { val := Quot.mk Setoid.r a✝¹, property := property✝¹ } +
      a✝² • { val := Quot.mk Setoid.r a✝, property := property✝ }
[PROOFSTEP]
rfl
  -- The next few lemmas follow from the `IsometricSMul` instance if `1 ≤ p`
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
f g : { x // x ∈ Lp E p }
⊢ dist (c • f) (c • g) = dist f g
[PROOFSTEP]
simp only [dist, ← smul_Lp_sub, norm_smul_Lp]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
f g : { x // x ∈ Lp E p }
⊢ edist (c • f) (c • g) = edist f g
[PROOFSTEP]
simp only [Lp.edist_dist, dist_smul_Lp]