awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
hg : HPow.hPow (α := ℝ) (∫ (a : α), ‖HSub.hSub (β := α → E) f (⇑g : (a : α) → E) a‖ ^ p ∂μ) p⁻¹ ≤ ε ^ p⁻¹
⊢ LE.le (α := ℝ) 0 (∫ (a : α), ‖HSub.hSub (β := α → E) f (⇑g : (a : α) → E) a‖ ^ p ∂μ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
simp :
  ∀ (hf : MemLp f 1 μ),
    ∃ (g : α →ᵇ E),
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)) 1 μ ≤ ε ∧
        MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) 1 μ
⊢ ∃ (g : α →ᵇ E),
    ∫⁻ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ₑ ∂μ ≤ ε ∧
      Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ

Tactic:
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ (g : α →ᵇ E),
    eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)) 1 μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) 1 μ

Tactic:
hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top hε

Premises used: MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ (g : α →ᵇ E),
    eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)) 1 μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) 1 μ

Tactic:
exact hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top hε

Premises used: MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
simp :
  ∀ (hf : MemLp f (ENNReal.ofReal 1) μ),
    ∃ (g : α →ᵇ E),
      ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ∂μ ≤ ε ∧
        MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal 1) μ
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ∂μ ≤ ε ∧
      Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ

Tactic:
simp only [← memLp_one_iff_integrable, ← ENNReal.ofReal_one]
    at hf ⊢

Premises used: ENNReal.ofReal_one, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal 1) μ

Tactic:
simpa using hf.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one hε

Premises used: MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le, zero_lt_one
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
⊢ f ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))

Tactic:
(mem_closure_iff_nhds_basis Metric.nhds_basis_closedEBall).2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Set.Mem, Metric.nhds_basis_closedEBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
refine :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε
⊢ f ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))

Tactic:
refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedEBall).2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedEBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (g : α →ᵇ E),
    eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ

Tactic:
(Lp.memLp f).exists_boundedContinuous_eLpNorm_sub_le hp hε.ne'

Premises used: MeasureTheory.Lp.memLp, LT.lt.ne', MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
obtain :
  ∀ (g : α →ᵇ E) (hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε)
    (g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ),
    ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε
⊢ ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε

Tactic:
obtain ⟨g, hg, g_mem⟩ :
      ∃ g : α →ᵇ E, eLpNorm ((f : α → E) - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ :=
    (Lp.memLp f).exists_boundedContinuous_eLpNorm_sub_le hp hε.ne'

Premises used: MeasureTheory.Lp.memLp, LT.lt.ne', MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ
⊢ ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε

Tactic:
⟨g_mem.toLp _, ⟨g, rfl⟩, ?_⟩

Premises used: And.intro, MeasureTheory.MemLp.toLp, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ
refine : MemLp.toLp (⇑g : (a : α) → E) g_mem ∈ Metric.closedEBall f ε
⊢ ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε

Tactic:
refine ⟨g_mem.toLp _, ⟨g, rfl⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ
rwa : edist f (MemLp.toLp (⇑g : (a : α) → E) g_mem) ≤ ε
rwa₁ : edist (MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) (MemLp.toLp (⇑g : (a : α) → E) g_mem) ≤ ε
rwa₂ rwa₃ rwa₄ rwa₅ : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
⊢ MemLp.toLp (⇑g : (a : α) → E) g_mem ∈ Metric.closedEBall f ε

Tactic:
rwa [Metric.mem_closedEBall', ← Lp.toLp_coeFn f (Lp.memLp f), Lp.edist_toLp_toLp]

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.Lp.edist_toLp_toLp, Metric.mem_closedEBall', MeasureTheory.Lp.toLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
⊢ Eq (α := AddSubgroup ↥(Lp E p μ)) (AddSubgroup.topologicalClosure (boundedContinuousFunction E p μ)) ⊤

Tactic:
SetLike.ext' <| (boundedContinuousFunction_dense E μ hp).closure_eq

Premises used: MeasureTheory.Lp.boundedContinuousFunction_dense, Dense.closure_eq, SetLike.ext'
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : μ.WeaklyRegular
inst_11 : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ DenseRange (X := ↥(Lp E p μ)) (α := α →ᵇ E) (⇑(toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))

Tactic:
simpa only [← range_toLp p μ (𝕜 := 𝕜)]
    using MeasureTheory.Lp.boundedContinuousFunction_dense E μ hp

Premises used: MeasureTheory.Lp.boundedContinuousFunction_dense, BoundedContinuousFunction.range_toLp
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ DenseRange (X := ↥(Lp E p μ)) (α := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ))

Tactic:
(BoundedContinuousFunction.toLp_denseRange _ _ 𝕜 hp).mono ?_

Premises used: Dense.mono, DenseRange, BoundedContinuousFunction.toLp_denseRange
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
refine :
  Subset (α := Set ↥(Lp E p μ))
    (range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
⊢ DenseRange (X := ↥(Lp E p μ)) (α := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ))

Tactic:
refine (BoundedContinuousFunction.toLp_denseRange _ _ 𝕜 hp).mono ?_

Premises used: Dense.mono, BoundedContinuousFunction.toLp_denseRange
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ Subset (α := Set ↥(Lp E p μ))
    (range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))

Tactic:
range_subset_iff.2 fun f ↦ ?_

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
refine :
  ∀ (f : α →ᵇ E),
    Membership.mem (α := ↥(Lp E p μ)) (γ := Set ↥(Lp E p μ))
      (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
      ((BoundedContinuousFunction.toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
⊢ Subset (α := Set ↥(Lp E p μ))
    (range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))

Tactic:
refine range_subset_iff.2 fun f ↦ ?_

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
f : α →ᵇ E
⊢ Membership.mem (α := ↥(Lp E p μ)) (γ := Set ↥(Lp E p μ))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
    ((BoundedContinuousFunction.toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))

Tactic:
⟨f.toContinuousMap, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl, BoundedContinuousFunction.toContinuousMap
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
f : α →ᵇ E
⊢ Membership.mem (α := ↥(Lp E p μ)) (γ := Set ↥(Lp E p μ))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
    ((BoundedContinuousFunction.toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))

Tactic:
exact ⟨f.toContinuousMap, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst_1 : TopologicalSpace E
inst_2 : OpensMeasurableSpace E
hZ : AEMeasurable Z μ'
x : ι
⊢ AEMeasurable Z μ'

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
⊢ Tendsto (fun (x : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
h : ∀ (j : ι), Eq (α := Measure E) (Measure.map (X j) (μ j)) (Measure.map Z μ')
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
convert! tendsto_const_nhds with j

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
j : ι
⊢ Eq (α := Measure E) (Measure.map (X j) (μ j)) (Measure.map Z μ')

Tactic:
(hX j).map_eq.symm.trans hZ.map_eq

Premises used: ProbabilityTheory.IdentDistrib.map_eq, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
j : ι
⊢ Eq (α := Measure E) (Measure.map (X j) (μ j)) (Measure.map Z μ')

Tactic:
exact (hX j).map_eq.symm.trans hZ.map_eq

Premises used: ProbabilityTheory.IdentDistrib.map_eq, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
h.tendsto

Premises used: MeasureTheory.TendstoInDistribution.tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h₁ :
  ∀ (n : ι),
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) ⋯ =
      Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯
h₂ :
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯))

Tactic:
convert! h.tendsto using 2 with n

Premises used: MeasureTheory.TendstoInDistribution.tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
n : ι
⊢ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯

Tactic:
simpa using Measure.map_congr (hXY n).symm

Premises used: MeasureTheory.Measure.map_congr, Filter.EventuallyEq.symm