awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a) : (a : X) → Y) μ ν
hgm₀ : MeasurePreserving (⇑g₀ : (a : X) → Y) μ ν
hp : p ≠ ∞
this :
  Tendsto (β := ↥(Lp E p μ))
    (fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      ((Lp.compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1 :
        ↥(Lp E p μ)))
    (𝓝 (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀))
    (𝓝
        ((Lp.compMeasurePreserving
              (⇑(↑(f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).2 :
                    C(X, Y)) :
                (a : X) → Y)
              ⋯ :
            (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
          (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).1) :
      Filter ↥(Lp E p μ))
hg :
  Tendsto (β := { g : C(X, Y) // MeasurePreserving (⇑g : (a : X) → Y) μ ν })
    (fun (a : α) ↦ Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) (g a) ⋯) l
    (𝓝 (Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) g₀ hgm₀))
⊢ Tendsto (β := ↥(Lp E p μ))
    ((fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
          (Lp.compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1) ∘
        fun (c : α) ↦ (f c, Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) (g c) ⋯) :
      α → ↥(Lp E p μ))
    l
    (𝓝
        ((Lp.compMeasurePreserving
              (⇑(↑(f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).2 :
                    C(X, Y)) :
                (a : X) → Y)
              ⋯ :
            (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
          (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).1) :
      Filter ↥(Lp E p μ))

Tactic:
this.comp (hf.prodMk_nhds hg)

Premises used: Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a) : (a : X) → Y) μ ν
hgm₀ : MeasurePreserving (⇑g₀ : (a : X) → Y) μ ν
hp : p ≠ ∞
this :
  Tendsto (β := ↥(Lp E p μ))
    (fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      ((Lp.compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1 :
        ↥(Lp E p μ)))
    (𝓝 (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀))
    (𝓝
        ((Lp.compMeasurePreserving
              (⇑(↑(f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).2 :
                    C(X, Y)) :
                (a : X) → Y)
              ⋯ :
            (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
          (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).1) :
      Filter ↥(Lp E p μ))
hg :
  Tendsto (β := { g : C(X, Y) // MeasurePreserving (⇑g : (a : X) → Y) μ ν })
    (fun (a : α) ↦ Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) (g a) ⋯) l
    (𝓝 (Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) g₀ hgm₀))
⊢ Tendsto (β := ↥(Lp E p μ))
    (fun (a : α) ↦
      ((Lp.compMeasurePreserving (⇑(g a) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f a) : ↥(Lp E p μ)))
    l
    (𝓝 ((Lp.compMeasurePreserving (⇑g₀ : (a : X) → Y) hgm₀ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) f₀) : Filter ↥(Lp E p μ))

Tactic:
convert! this.comp (hf.prodMk_nhds hg)

Premises used: Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
Z : Type u_4
inst_12 : TopologicalSpace Z
f : Z → ↥(Lp E p ν)
g : Z → C(X, Y)
s : Set Z
z : Z
hf : ContinuousWithinAt f s z
hg : ContinuousWithinAt g s z
hgm : ∀ (z : Z), MeasurePreserving (⇑(g z) : (a : X) → Y) μ ν
hp : p ≠ ∞
⊢ ContinuousWithinAt (Y := ↥(Lp E p μ))
    (fun (z : Z) ↦ (Lp.compMeasurePreserving (⇑(g z) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f z)) s z

Tactic:
Tendsto.compMeasurePreservingLp hf hg _ _ hp

Premises used: ContinuousWithinAt, Filter.Tendsto.compMeasurePreservingLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
Z : Type u_4
inst_12 : TopologicalSpace Z
f : Z → ↥(Lp E p ν)
g : Z → C(X, Y)
z : Z
hf : ContinuousAt f z
hg : ContinuousAt g z
hgm : ∀ (z : Z), MeasurePreserving (⇑(g z) : (a : X) → Y) μ ν
hp : p ≠ ∞
⊢ ContinuousAt (Y := ↥(Lp E p μ))
    (fun (z : Z) ↦ (Lp.compMeasurePreserving (⇑(g z) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f z)) z

Tactic:
Tendsto.compMeasurePreservingLp hf hg _ _ hp

Premises used: ContinuousAt, Filter.Tendsto.compMeasurePreservingLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
Z : Type u_4
inst_12 : TopologicalSpace Z
f : Z → ↥(Lp E p ν)
g : Z → C(X, Y)
s : Set Z
hf : ContinuousOn f s
hg : ContinuousOn g s
hgm : ∀ (z : Z), MeasurePreserving (⇑(g z) : (a : X) → Y) μ ν
hp : p ≠ ∞
⊢ ContinuousOn (Y := ↥(Lp E p μ))
    (fun (z : Z) ↦ (Lp.compMeasurePreserving (⇑(g z) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f z)) s

Tactic:
fun z hz ↦
  (hf z hz).compMeasurePreservingLp (hg z hz) hgm hp

Premises used: ContinuousWithinAt.compMeasurePreservingLp, ContinuousOn
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
Z : Type u_4
inst_12 : TopologicalSpace Z
f : Z → ↥(Lp E p ν)
g : Z → C(X, Y)
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst_12, _] g
hgm : ∀ (z : Z), MeasurePreserving (⇑(g z) : (a : X) → Y) μ ν
hp : p ≠ ∞
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (z : Z) ↦
    (Lp.compMeasurePreserving (⇑(g z) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f z)

Tactic:
continuous_iff_continuousAt.mpr fun _ ↦
    hf.continuousAt.compMeasurePreservingLp hg.continuousAt hgm hp

Premises used: Iff.mpr, ContinuousAt.compMeasurePreservingLp, Continuous.continuousAt, continuous_iff_continuousAt
-- 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
f : ↥(Lp E p μ)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (boundedContinuousFunction E p μ) f ↔
    ∃ (f₀ : α →ᵇ E), ContinuousMap.toAEEqFun μ f₀.toContinuousMap = (↑f : α →ₘ[μ] E)

Tactic:
AddSubgroup.mem_addSubgroupOf

Premises used: ContinuousMap.toAEEqFun, Set.Mem, setOf, AddSubgroup.mem_addSubgroupOf, Set.range, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
f : α →ᵇ E
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) (⇑f : (a : α) → E) μ

Tactic:
fun_prop
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (ContinuousMap.toAEEqFun μ f.toContinuousMap)

Tactic:
Lp.mem_Lp_of_ae_bound ‖f‖ ?_

Premises used: Norm.norm, MeasureTheory.Lp.mem_Lp_of_ae_bound
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
refine : ∀ᵐ (x : α) ∂μ, ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (ContinuousMap.toAEEqFun μ f.toContinuousMap)

Tactic:
refine Lp.mem_Lp_of_ae_bound ‖f‖ ?_

Premises used: Norm.norm, MeasureTheory.Lp.mem_Lp_of_ae_bound
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
h :
  (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x →
    ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖
⊢ (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x →
    ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖

Tactic:
_
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
h :
  ∀ (x : α),
    (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x →
      ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖
⊢ ∀ᵐ (x : α) ∂μ, ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖

Tactic:
filter_upwards [f.toContinuousMap.coeFn_toAEEqFun μ] with x _

Premises used: ContinuousMap.coeFn_toAEEqFun, BoundedContinuousFunction.toContinuousMap
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
h : (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x
⊢ norm.{u_2} (E := E) ((f : (a : α) → E) x : E) ≤ ‖f‖

Tactic:
f.norm_coe_le_norm x

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
h : (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x
⊢ ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖

Tactic:
convert! f.norm_coe_le_norm x using 2

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
hfC :
  ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                    (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
                α →ₘ[μ] E) :
            α → E)
          x‖₊ ≤
      ‖f‖₊
⊢ NNNorm.nnnorm (E := ↥(Lp E p μ))
      (Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
        (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) ≤
    measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊

Tactic:
apply Lp.nnnorm_le_of_ae_bound

Premises used: MeasureTheory.Lp.nnnorm_le_of_ae_bound
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                    (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
                α →ₘ[μ] E) :
            α → E)
          x‖₊ ≤
      ‖f‖₊

Tactic:
(f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_

Premises used: ContinuousMap.coeFn_toAEEqFun, Filter.Eventually.mono, BoundedContinuousFunction.toContinuousMap
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
hfC :
  ∀ (x : α),
    (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x →
      ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                      (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
                  α →ₘ[μ] E) :
              α → E)
            x‖₊ ≤
        ‖f‖₊
⊢ ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                    (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
                α →ₘ[μ] E) :
            α → E)
          x‖₊ ≤
      ‖f‖₊

Tactic:
refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_

Premises used: ContinuousMap.coeFn_toAEEqFun, Filter.Eventually.mono, BoundedContinuousFunction.toContinuousMap
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x
hfC :
  ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                  (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
              α →ₘ[μ] E) :
          α → E)
        x‖ ≤
    ‖f‖
⊢ ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                  (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
              α →ₘ[μ] E) :
          α → E)
        x‖₊ ≤
    ‖f‖₊

Tactic:
rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]

Premises used: coe_nnnorm, NNReal.coe_le_coe
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x
⊢ norm.{u_2} (E := E) ((f : (a : α) → E) x : E) ≤ ‖f‖

Tactic:
f.norm_coe_le_norm x

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x
⊢ ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                  (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
              α →ₘ[μ] E) :
          α → E)
        x‖ ≤
    ‖f‖

Tactic:
convert! f.norm_coe_le_norm x using 2

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- 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 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ norm (E := ↥(Lp E p μ))
      (Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
        (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) ≤
    (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹ * ‖f‖

Tactic:
Lp_nnnorm_le f

Premises used: BoundedContinuousFunction.Lp_nnnorm_le
-- 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 : IsFiniteMeasure μ
inst_5 : Fact (1 ≤ p)
symm :
  Eq (α := AddSubgroup ↥(Lp E p μ)) (Lp.boundedContinuousFunction E p μ)
    (NormedAddGroupHom.range (V₁ := α →ᵇ E) (toLpHom p μ))
⊢ Eq (α := AddSubgroup ↥(Lp E p μ)) (NormedAddGroupHom.range (V₁ := α →ᵇ E) (toLpHom p μ))
    (Lp.boundedContinuousFunction E p μ)

Tactic:
symm
-- 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 : IsFiniteMeasure μ
inst_5 : Fact (1 ≤ p)
f : α →ᵇ E
⊢ Membership.mem (α := α →ₘ[μ] E) (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (((AddMonoidHom.comp (ContinuousMap.toAEEqFunAddHom μ : C(α, E) →+ α →ₘ[μ] E)
              (toContinuousMapAddMonoidHom α E : (α →ᵇ E) →+ C(α, E)) :
            (α →ᵇ E) →+ α →ₘ[μ] E) :
          (a : α →ᵇ E) → α →ₘ[μ] E)
        f :
      α →ₘ[μ] E)

Tactic:
mem_Lp f

Premises used: ContinuousMap.toAEEqFun, Set.Mem, setOf, BoundedContinuousFunction.mem_Lp, MeasureTheory.AEEqFun.mk
-- 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 : IsFiniteMeasure μ
inst_5 : Fact (1 ≤ p)
f : α →ᵇ E
⊢ Membership.mem (α := α →ₘ[μ] E) (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
    (((AddMonoidHom.comp (ContinuousMap.toAEEqFunAddHom μ : C(α, E) →+ α →ₘ[μ] E)
              (toContinuousMapAddMonoidHom α E : (α →ᵇ E) →+ C(α, E)) :
            (α →ᵇ E) →+ α →ₘ[μ] E) :
          (a : α →ᵇ E) → α →ₘ[μ] E)
        f :
      α →ₘ[μ] E)

Tactic:
exact mem_Lp f

Premises used: BoundedContinuousFunction.mem_Lp
-- 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 : IsFiniteMeasure μ
inst_5 : Fact (1 ≤ p)
⊢ Eq (α := AddSubgroup ↥(Lp E p μ)) (Lp.boundedContinuousFunction E p μ)
    (NormedAddGroupHom.range (V₁ := α →ᵇ E) (toLpHom p μ))

Tactic:
exact AddMonoidHom.addSubgroupOf_range_eq_of_le
      ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddMonoidHom α E))
      (by rintro - ⟨f, rfl⟩; exact mem_Lp f : _ ≤ Lp E p μ)

Premises used: BoundedContinuousFunction.toContinuousMapAddMonoidHom, AddMonoidHom.addSubgroupOf_range_eq_of_le, ContinuousMap.toAEEqFunAddHom, AddMonoidHom.comp
-- 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 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f : α →ᵇ E
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E)
    (⇑f : (a : α) → E)

Tactic:
AEEqFun.coeFn_mk f _

Premises used: ContinuousMap.toAEEqFun, MeasureTheory.AEEqFun.coeFn_mk, DFunLike.coe, MeasureTheory.AEEqFun.mk
-- 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 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
⊢ Eq (α := AddSubgroup ↥(Lp E p μ))
    (Submodule.toAddSubgroup (module_M := Lp.instModule)
      (LinearMap.range (M := α →ᵇ E) (↑(toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ))))
    (Lp.boundedContinuousFunction E p μ)

Tactic:
range_toLpHom p μ

Premises used: ContinuousMap.toAEEqFun, Set.Mem, AddMonoidHom.range, BoundedContinuousFunction.range_toLpHom, NormedAddGroupHom.range, AddSubgroup.copy, MeasureTheory.AEEqFun.mk