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 : IsFiniteMeasure μ
inst_5 : Fact (1 ≤ p)
𝕜 : Type u_4
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NormedSpace 𝕜 E
⊢ norm (E := (α →ᵇ E) →L[𝕜] ↥(Lp E p μ)) (toLp p μ 𝕜) ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹

Tactic:
LinearMap.mkContinuous_norm_le _ (measureUnivNNReal μ ^ p.toReal⁻¹).coe_nonneg _

Premises used: Set.Mem, BoundedContinuousFunction.toLp, ENNReal.toReal, Inv.inv, HPow.hPow, LinearMap.mkContinuous_norm_le, NNReal.coe_nonneg, MeasureTheory.measureUnivNNReal, NNReal.toReal
-- 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 g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  f = g →
    Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
      ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
⊢ f = g →
    Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
      ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))

Tactic:
tauto
-- 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 g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
refine :
  ∀
    (h :
      Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
        ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))),
    f = g
⊢ Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
      ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ)) ↔
    f = g

Tactic:
refine ⟨fun h => ?_, by tauto⟩
-- 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 g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
rw : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
⊢ f = g

Tactic:
rw [← DFunLike.coe_fn_eq, ← (map_continuous f).ae_eq_iff_eq μ (map_continuous g)]

Premises used: Continuous.ae_eq_iff_eq, DFunLike.coe_fn_eq, ContinuousMapClass.map_continuous
-- 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 g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)

Tactic:
(coeFn_toLp p μ 𝕜 f).symm.trans (EventuallyEq.trans ?_ <| coeFn_toLp p μ 𝕜 g)

Premises used: Filter.EventuallyEq.trans, BoundedContinuousFunction.coeFn_toLp, Filter.EventuallyEq.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 μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
refine :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E)
    (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)

Tactic:
refine (coeFn_toLp p μ 𝕜 f).symm.trans (EventuallyEq.trans ?_ <| coeFn_toLp p μ 𝕜 g)

Premises used: Filter.EventuallyEq.trans, BoundedContinuousFunction.coeFn_toLp, Filter.EventuallyEq.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 μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
rw rw₁ :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
    (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E)
    (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)

Tactic:
rw [h]
-- 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
inst_9 : μ.IsOpenPosMeasure
⊢ Function.Injective (α := α →ᵇ E) (β := ↥(Lp E p μ)) (⇑(toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))

Tactic:
fun _f _g hfg => (toLp_inj μ).mp hfg

Premises used: BoundedContinuousFunction.toLp_inj, Iff.mp, Function.Injective
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
⊢ Eq (α := AddSubgroup ↥(Lp E p μ))
    (Submodule.toAddSubgroup (module_M := Lp.instModule)
      (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ))))
    (Lp.boundedContinuousFunction E p μ)

Tactic:
SetLike.ext' ?_

Premises used: SetLike.ext'
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
refine :
  (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))
⊢ Eq (α := AddSubgroup ↥(Lp E p μ))
    (Submodule.toAddSubgroup (module_M := Lp.instModule)
      (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ))))
    (Lp.boundedContinuousFunction E p μ)

Tactic:
refine SetLike.ext' ?_

Premises used: SetLike.ext'
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
⊢ Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)

Tactic:
have := (linearIsometryBoundedOfCompact α E 𝕜).surjective
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
⊢ Eq (α := Set ↥(Lp E p μ))
    (Set.range (ι := C(α, E))
      (Function.comp (β := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
        (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)))
    (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))

Tactic:
Function.Surjective.range_comp this (BoundedContinuousFunction.toLp (E := E) p μ 𝕜)

Premises used: BoundedContinuousFunction.toLp, Function.Surjective.range_comp, DFunLike.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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
h :
  (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
⊢ (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))

Tactic:
convert! Function.Surjective.range_comp this (BoundedContinuousFunction.toLp (E := E) p μ 𝕜)

Premises used: BoundedContinuousFunction.toLp, Function.Surjective.range_comp, DFunLike.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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
h :
  (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
h₁ :
  (↑(LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
h₂ :
  Eq (α := Set ↥(Lp E p μ))
    (Set.range (ι := α →ᵇ E)
      (⇑(↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
h₃ h₄ :
  Eq (α := Set ↥(Lp E p μ))
    (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
⊢ (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))

Tactic:
rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,
    LinearMap.coe_range, ContinuousLinearMap.coe_coe]

Premises used: ContinuousLinearMap.coe_coe, LinearMap.coe_range, BoundedContinuousFunction.range_toLp, Submodule.coe_toAddSubgroup
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
f : C(α, E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : C(α, 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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
f : C(α, E)
⊢ Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((BoundedContinuousFunction.toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ))
        ((linearIsometryBoundedOfCompact α E 𝕜 : (a : C(α, E)) → α →ᵇ E) f) :
      ↥(Lp E p μ))

Tactic:
rfl

Premises used: rfl
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
f : α →ᵇ E
⊢ Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f.toContinuousMap : ↥(Lp E p μ))
    ((BoundedContinuousFunction.toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))

Tactic:
rfl

Premises used: rfl
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
f : C(α, E)
⊢ (↑((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) = toAEEqFun μ f

Tactic:
rfl

Premises used: ContinuousMap.toAEEqFun, rfl, 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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
inst_10 : μ.IsOpenPosMeasure
⊢ Function.Injective (α := C(α, E)) (β := ↥(Lp E p μ)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ))

Tactic:
(BoundedContinuousFunction.toLp_injective _).comp (linearIsometryBoundedOfCompact α E 𝕜).injective

Premises used: BoundedContinuousFunction.toLp_injective, LinearIsometryEquiv.injective, Function.Injective.comp, ContinuousMap.linearIsometryBoundedOfCompact
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
f g : C(α, E)
inst_10 : μ.IsOpenPosMeasure
⊢ Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
      ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) g : ↥(Lp E p μ)) ↔
    f = g

Tactic:
(toLp_injective μ).eq_iff

Premises used: Function.Injective.eq_iff, ContinuousMap.toLp_injective
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
β : Type u_4
inst_10 : μ.IsOpenPosMeasure
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 :
  HasSum (α := ↥(Lp E p μ)) ((⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)) ∘ g : β → ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
⊢ HasSum g (∑' (b : β), g b)

Tactic:
Summable.hasSum hg

Premises used: Summable.hasSum
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
β : Type u_4
inst_10 : μ.IsOpenPosMeasure
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 :
  HasSum (α := ↥(Lp E p μ)) ((⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)) ∘ g : β → ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
h : f = ∑' (b : β), g b
⊢ HasSum g f

Tactic:
convert! Summable.hasSum hg

Premises used: Summable.hasSum
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
β : Type u_4
inst_10 : μ.IsOpenPosMeasure
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 :
  HasSum (α := ↥(Lp E p μ)) ((⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)) ∘ g : β → ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
⊢ f = ∑' (b : β), g b

Tactic:
toLp_injective μ (hg2.unique ((toLp p μ 𝕜).hasSum <| Summable.hasSum hg))

Premises used: ContinuousMap.toLp, ContinuousLinearMap.hasSum, ContinuousMap.toLp_injective, Summable.hasSum, HasSum.unique
-- 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 μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
β : Type u_4
inst_10 : μ.IsOpenPosMeasure
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 :
  HasSum (α := ↥(Lp E p μ)) ((⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)) ∘ g : β → ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
⊢ f = ∑' (b : β), g b

Tactic:
exact toLp_injective μ (hg2.unique ((toLp p μ 𝕜).hasSum <| Summable.hasSum hg))

Premises used: ContinuousMap.toLp, ContinuousLinearMap.hasSum, ContinuousMap.toLp_injective, Summable.hasSum, HasSum.unique
-- 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_4
inst_7 : NontriviallyNormedField 𝕜
inst_8 : NormedSpace 𝕜 E
⊢ norm (E := C(α, E) →L[𝕜] ↥(Lp E p μ)) (toLp p μ 𝕜) =
    norm (E := (α →ᵇ E) →L[𝕜] ↥(Lp E p μ)) (BoundedContinuousFunction.toLp p μ 𝕜)

Tactic:
ContinuousLinearMap.opNorm_comp_linearIsometryEquiv _ _

Premises used: ContinuousLinearMap.opNorm_comp_linearIsometryEquiv, ContinuousMap.toLp, Set.Mem
-- 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_4
inst_7 : NontriviallyNormedField 𝕜
inst_8 : NormedSpace 𝕜 E
rw :
  norm (E := (α →ᵇ E) →L[𝕜] ↥(Lp E p μ)) (BoundedContinuousFunction.toLp p μ 𝕜) ≤
    (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹
⊢ norm (E := C(α, E) →L[𝕜] ↥(Lp E p μ)) (toLp p μ 𝕜) ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹

Tactic:
rw [toLp_norm_eq_toLp_norm_coe]

Premises used: ContinuousMap.toLp_norm_eq_toLp_norm_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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜 : Type u_4
inst_7 : NontriviallyNormedField 𝕜
inst_8 : NormedSpace 𝕜 E
⊢ norm (E := (α →ᵇ E) →L[𝕜] ↥(Lp E p μ)) (BoundedContinuousFunction.toLp p μ 𝕜) ≤
    (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹

Tactic:
BoundedContinuousFunction.toLp_norm_le μ

Premises used: BoundedContinuousFunction.toLp_norm_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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜 : Type u_4
inst_7 : NontriviallyNormedField 𝕜
inst_8 : NormedSpace 𝕜 E
⊢ norm (E := (α →ᵇ E) →L[𝕜] ↥(Lp E p μ)) (BoundedContinuousFunction.toLp p μ 𝕜) ≤
    (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹

Tactic:
exact BoundedContinuousFunction.toLp_norm_le μ

Premises used: BoundedContinuousFunction.toLp_norm_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 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜' : Type u_5
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' E
f : C(α, E)
⊢ MemLp.{u_1, u_2} (ε := E) (↑(↑((toLp p μ 𝕜' : (a : C(α, E)) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E) p μ

Tactic:
have := Lp.mem_Lp_iff_memLp.mp (Subtype.val_prop (f.toLp p μ 𝕜'))