awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜' : Type u_5
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' E
f : C(α, E)
this : MemLp.{u_1, u_2} (ε := E) (↑(↑((toLp p μ 𝕜' : (a : C(α, E)) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E) p μ
rwa : ∀ (this : MemLp (↑(toAEEqFun μ f) : α → E) p μ), MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ), MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
⊢ MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
rwa [coe_toLp, memLp_congr_ae (coeFn_toAEEqFun _ _)] at this

Premises used: ContinuousMap.coeFn_toAEEqFun, MeasureTheory.memLp_congr_ae, ContinuousMap.coe_toLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
⊢ (↑(c • f) : α →ₘ[μ] E) = c • (↑f : α →ₘ[μ] E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
⊢ (↑(↑(c • f) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fun (x : α) ↦
    (↑(↑f : α →ₘ[μ] E) : α → E) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) x)

Tactic:
Lp.coeFn_compMeasurePreserving _ _

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.Lp.coeFn_compMeasurePreserving, dite
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : M
f : α → E
hf : MemLp f p μ
⊢ HSMul.hSMul (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) (MemLp.toLp f hf) = MemLp.toLp (fun (x : α) ↦ f (c • x)) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.MemLp.toLp, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, MulOpposite.unop, rfl, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
inst_5 : IsFiniteMeasure μ
c : Mᵈᵐᵃ
a : E
⊢ HSMul.hSMul (β := ↥(Lp E p μ)) c ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) a : ↥(Lp E p μ)) =
    (Lp.const p μ : (a : E) → ↥(Lp E p μ)) a

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.compMeasurePreserving, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : M
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
b : E
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [SMulInvariantMeasure.measure_preimage_smul c hs]

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : M
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
b : E
⊢ HSMul.hSMul (α := Mᵈᵐᵃ) (β := ↥(Lp E p μ)) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) (indicatorConstLp (s := s) p hs hμs b) =
    indicatorConstLp (s := (fun (x : α) ↦ c • x) ⁻¹' s) p ⋯ ⋯ b

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Set.indicator, MeasureTheory.indicatorConstLp, setOf, MeasureTheory.AEEqFun.compMeasurePreserving, Set.preimage, MeasureTheory.MemLp.toLp, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, MulOpposite.unop, rfl, MeasureTheory.AEEqFun.mk, ite
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
inst_5 : SMul N α
inst_6 : SMulCommClass M N α
inst_7 : SMulInvariantMeasure N α μ
inst_8 : MeasurableConstSMul N α
⊢ SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ ↥(Lp E p μ)

Tactic:
Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl

Premises used: Function.Injective.smulCommClass, Subtype.val_injective, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
𝕜 : Type u_5
inst_5 : NormedRing 𝕜
inst_6 : Module 𝕜 E
inst_7 : IsBoundedSMul 𝕜 E
⊢ SMulCommClass Mᵈᵐᵃ 𝕜 ↥(Lp E p μ)

Tactic:
Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl

Premises used: Function.Injective.smulCommClass, Subtype.val_injective, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
𝕜 : Type u_5
inst_5 : NormedRing 𝕜
inst_6 : Module 𝕜 E
inst_7 : IsBoundedSMul 𝕜 E
⊢ SMulCommClass 𝕜 Mᵈᵐᵃ ↥(Lp E p μ)

Tactic:
.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
val : α →ₘ[μ] E
a : { f : α → E // AEStronglyMeasurable f μ }
property :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a)
val_1 : α →ₘ[μ] E
a_1 : { f : α → E // AEStronglyMeasurable f μ }
property_1 :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a_1)
⊢ c •
      (Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property +
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_1)
          property_1) =
    c •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property +
      c •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_1)
          property_1

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
⊢ HSMul.hSMul (β := ↥(Lp E p μ)) c 0 = 0

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
mk :
  ∀ (val : α →ₘ[μ] E) (a : { f : α → E // AEStronglyMeasurable f μ })
    (property :
      Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
        (Quot.mk
          (⇑(Measure.aeEqSetoid E μ) :
            { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
          a)),
    c •
        -Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
            (Quot.mk
              (⇑(Measure.aeEqSetoid E μ) :
                { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
              a)
            property =
      -(c •
          Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
            (Quot.mk
              (⇑(Measure.aeEqSetoid E μ) :
                { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
              a)
            property)
⊢ c • -f = -(c • f)

Tactic:
rcases f with ⟨⟨_⟩, _⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
val : α →ₘ[μ] E
a : { f : α → E // AEStronglyMeasurable f μ }
property :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a)
⊢ c •
      -Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property =
    -(c •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
val : α →ₘ[μ] E
a : { f : α → E // AEStronglyMeasurable f μ }
property :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a)
val_1 : α →ₘ[μ] E
a_1 : { f : α → E // AEStronglyMeasurable f μ }
property_1 :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a_1)
⊢ c •
      (Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property -
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_1)
          property_1) =
    c •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property -
      c •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_1)
          property_1

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
a : Mᵈᵐᵃ
val : α →ₘ[μ] E
a_1 : { f : α → E // AEStronglyMeasurable f μ }
property :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a_1)
val_1 : α →ₘ[μ] E
a_2 : { f : α → E // AEStronglyMeasurable f μ }
property_1 :
  Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (Quot.mk
      (⇑(Measure.aeEqSetoid E μ) :
        { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
      a_2)
⊢ a •
      (Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_1)
          property +
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_2)
          property_1) =
    a •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_1)
          property +
      a •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a_2)
          property_1

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
⊢ ‖c • f‖ = ‖f‖

Tactic:
Lp.norm_compMeasurePreserving _ _

Premises used: MeasureTheory.Lp.norm_compMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
⊢ ‖c • f‖₊ = ‖f‖₊

Tactic:
NNReal.eq <| Lp.norm_compMeasurePreserving _ _

Premises used: NNReal.eq, MeasureTheory.Lp.norm_compMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f g : ↥(Lp E p μ)
⊢ dist (c • f) (c • g) = dist f g

Tactic:
simp only [dist, ← smul_Lp_neg, ← smul_Lp_add, norm_smul_Lp]

Premises used: DomMulAct.smul_Lp_neg, DomMulAct.norm_smul_Lp, Dist.dist, DomMulAct.smul_Lp_add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f g : ↥(Lp E p μ)
⊢ edist (c • f) (c • g) = edist f g

Tactic:
simp only [Lp.edist_dist, dist_smul_Lp]

Premises used: DomMulAct.dist_smul_Lp, MeasureTheory.Lp.edist_dist
-- Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
inst_5 : Fact (1 ≤ p)
⊢ IsIsometricSMul Mᵈᵐᵃ ↥(Lp E p μ)

Tactic:
⟨edist_smul_Lp⟩

Premises used: DomMulAct.edist_smul_Lp, IsIsometricSMul.mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
inl :
  ∀ (hp : Ne (α := ℝ≥0∞) 0 ∞),
    ∃ (η : ℝ≥0),
      0 < η ∧
        ∀ (s : Set α),
          (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) 0 μ ≤ ε
inr :
  ∀ (h'p : p ≠ 0),
    ∃ (η : ℝ≥0),
      0 < η ∧
        ∀ (s : Set α),
          (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε

Tactic:
rcases eq_or_ne p 0 with (rfl | h'p)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : Ne (α := ℝ≥0∞) 0 ∞
s : Set α
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑1 : ℝ≥0∞)
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) 0 μ ≤ ε

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : Ne (α := ℝ≥0∞) 0 ∞
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) 0 μ ≤ ε

Tactic:
exact ⟨1, zero_lt_one, fun s _ => by simp⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
⊢ 0 < p

Tactic:
have hp₀ : 0 < p := bot_lt_iff_ne_bot.2 h'p
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
⊢ 0 ≤ 1 / p.toReal

Tactic:
have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
⊢ 0 < p.toReal

Tactic:
have hp₀'' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
rw : Tendsto (β := ℝ≥0) (fun (x : ℝ≥0) ↦ ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 0)
⊢ Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))

Tactic:
rw [ENNReal.tendsto_coe]

Premises used: ENNReal.tendsto_coe
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun (x : ℝ≥0) ↦ ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 (‖c‖₊ * HPow.hPow (α := ℝ≥0) 0 (1 / p.toReal)))

Tactic:
(NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _

Premises used: Filter.Tendsto.const_mul, NNReal.continuousAt_rpow_const, ContinuousAt.tendsto, Or.inr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
h : 0 = ‖c‖₊ * HPow.hPow (α := ℝ≥0) 0 (1 / p.toReal)
⊢ Tendsto (β := ℝ≥0) (fun (x : ℝ≥0) ↦ ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 0)

Tactic:
convert! (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _

Premises used: Filter.Tendsto.const_mul, NNReal.continuousAt_rpow_const, ContinuousAt.tendsto, Or.inr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ 0 = ‖c‖₊ * HPow.hPow (α := ℝ≥0) 0 (1 / p.toReal)

Tactic:
simp [hp₀''.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))

Tactic:
have :
      Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
        (𝓝 (0 : ℝ≥0)) := by
      rw [ENNReal.tendsto_coe]
      convert! (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
      simp [hp₀''.ne']
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
⊢ 0 < ε

Tactic:
have hε' : 0 < ε := hε.bot_lt