awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
inl : ∀ (h : IsEmpty Y), HasFiniteIntegral f μ
inr : ∀ (h : Nonempty Y), HasFiniteIntegral f μ
⊢ HasFiniteIntegral f μ

Tactic:
rcases isEmpty_or_nonempty Y with (h | h)

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : IsEmpty Y
⊢ HasFiniteIntegral f μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
x : X
bound_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
⊢ 0 x ≤ bound x

Tactic:
le_trans (norm_nonneg _) (bound_x h.some)

Premises used: Nonempty.some, norm_nonneg, le_trans
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X)
            {x : X | (fun (x : X) ↦ ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ bound x) x} x}
      a
h₂ h₃ : ∀ (x : X) (bound_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x), 0 x ≤ bound x
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x h.some)
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
have bound_nonneg : 0 ≤ᵐ[μ] bound := by
      filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x h.some)
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
⊢ HasFiniteIntegral f μ

Tactic:
.mono' bound_int ?_

Premises used: MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
inr : ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
⊢ HasFiniteIntegral f μ

Tactic:
refine .mono' bound_int ?_
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
h₁ :
  ∀ (x : X) (bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x)
    (bound_nonneg_x : 0 x ≤ bound x), ‖f x‖ ≤ bound x
⊢ ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a

Tactic:
filter_upwards [bound_ge, bound_nonneg] with x bound_ge_x bound_nonneg_x
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
x : X
bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg_x : 0 x ≤ bound x
⊢ ‖f x‖ ≤ bound x

Tactic:
ContinuousMap.norm_le _ bound_nonneg_x |>.mpr bound_ge_x

Premises used: Iff.mpr, ContinuousMap.norm_le
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
x : X
bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg_x : 0 x ≤ bound x
⊢ ‖f x‖ ≤ bound x

Tactic:
exact ContinuousMap.norm_le _ bound_nonneg_x |>.mpr bound_ge_x

Premises used: Iff.mpr, ContinuousMap.norm_le
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := C(Y, E)) (fun (x : X) ↦ mkD (f x) g) μ

Tactic:
hasFiniteIntegral_of_bound _ bound bound_int ?_

Premises used: ContinuousMap.hasFiniteIntegral_of_bound
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
refine : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
⊢ HasFiniteIntegral (ε := C(Y, E)) (fun (x : X) ↦ mkD (f x) g) μ

Tactic:
refine hasFiniteIntegral_of_bound _ bound bound_int ?_

Premises used: ContinuousMap.hasFiniteIntegral_of_bound
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
h :
  ∀ (x : X) (bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x) (cont_x : Continuous (f x)) (y : Y),
    norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x

Tactic:
filter_upwards [bound_ge, f_ae_cont] with x bound_ge_x cont_x
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
cont_x : Continuous (f x)
⊢ ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x

Tactic:
simpa only [mkD_apply_of_continuous cont_x] using bound_ge_x

Premises used: ContinuousMap.mkD_apply_of_continuous
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := ContinuousMap.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ

Tactic:
hasFiniteIntegral_mkD_of_bound _ _ ?_ bound bound_int ?_

Premises used: ContinuousMap.hasFiniteIntegral_mkD_of_bound
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
refine_1 : ∀ᵐ (x : X) ∂μ, Continuous (s.restrict (π := fun (a : Y) ↦ E) (f x))
refine_2 : ∀ᵐ (x : X) ∂μ, ∀ (y : (↑s : Type u_2)), ‖s.restrict (π := fun (a : Y) ↦ E) (f x) y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := ContinuousMap.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ

Tactic:
refine hasFiniteIntegral_mkD_of_bound _ _ ?_ bound bound_int ?_

Premises used: ContinuousMap.hasFiniteIntegral_mkD_of_bound
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, Continuous (s.restrict (π := fun (a : Y) ↦ E) (f x))

Tactic:
simpa [← continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : (↑s : Type u_2)), ‖s.restrict (π := fun (a : Y) ↦ E) (f x) y‖ ≤ bound x

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
inst_6 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)
f_cont : Continuous (Function.uncurry f)
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ mkD (f x) g) μ

Tactic:
continuous_mkD_of_uncurry _ _ f_cont |>.aestronglyMeasurable

Premises used: Continuous.aestronglyMeasurable, ContinuousMap.continuous_mkD_of_uncurry
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
s : Set X
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
inst_6 : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set Y) s univ)
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ mkD (f x) g) (μ.restrict s)

Tactic:
continuousOn_mkD_of_uncurry _ _ f_cont |>.aestronglyMeasurable hs

Premises used: ContinuousMap.continuousOn_mkD_of_uncurry, ContinuousOn.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
inst_6 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ

Tactic:
continuous_mkD_restrict_of_uncurry _ _ f_cont |>.aestronglyMeasurable

Premises used: ContinuousMap.continuous_mkD_restrict_of_uncurry, Continuous.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
inst_6 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) (μ.restrict s)

Tactic:
continuousOn_mkD_restrict_of_uncurry _ _ f_cont |>.aestronglyMeasurable hs

Premises used: ContinuousOn.aestronglyMeasurable, ContinuousMap.continuousOn_mkD_restrict_of_uncurry
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
x : X
bound_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
⊢ 0 x ≤ bound x

Tactic:
le_trans (norm_nonneg _) (bound_x 0)

Premises used: OfNat.ofNat, norm_nonneg, le_trans
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X)
            {x : X | (fun (x : X) ↦ ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ bound x) x} x}
      a
h₁ h₂ : ∀ (x : X) (bound_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x), 0 x ≤ bound x
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
⊢ 0 ≤ᶠ[ae μ] bound

Tactic:
have bound_nonneg : 0 ≤ᵐ[μ] bound := by
    filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
⊢ HasFiniteIntegral f μ

Tactic:
.mono' bound_int ?_

Premises used: MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
refine : ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
⊢ HasFiniteIntegral f μ

Tactic:
refine .mono' bound_int ?_
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
h :
  ∀ (x : X) (bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x)
    (bound_nonneg_x : 0 x ≤ bound x), ‖f x‖ ≤ bound x
⊢ ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a

Tactic:
filter_upwards [bound_ge, bound_nonneg] with x bound_ge_x bound_nonneg_x
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
x : X
bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg_x : 0 x ≤ bound x
⊢ ‖f x‖ ≤ bound x

Tactic:
ContinuousMap.norm_le _ bound_nonneg_x |>.mpr bound_ge_x

Premises used: Iff.mpr, ContinuousMap.norm_le
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
x : X
bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg_x : 0 x ≤ bound x
⊢ ‖f x‖ ≤ bound x

Tactic:
exact ContinuousMap.norm_le _ bound_nonneg_x |>.mpr bound_ge_x

Premises used: Iff.mpr, ContinuousMap.norm_le
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) μ

Tactic:
hasFiniteIntegral_of_bound _ bound bound_int ?_

Premises used: ContinuousMapZero.hasFiniteIntegral_of_bound
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
refine : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
⊢ HasFiniteIntegral (ε := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) μ

Tactic:
refine hasFiniteIntegral_of_bound _ bound bound_int ?_

Premises used: ContinuousMapZero.hasFiniteIntegral_of_bound
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
h :
  ∀ (x : X) (bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x) (cont_x : Continuous (f x)) (zero_x : f x 0 = 0) (y : Y),
    norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x

Tactic:
filter_upwards [bound_ge, f_ae_cont, f_ae_zero] with x bound_ge_x cont_x zero_x
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
cont_x : Continuous (f x)
zero_x : f x 0 = 0
⊢ ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x

Tactic:
simpa only [mkD_apply_of_continuous cont_x zero_x] using bound_ge_x

Premises used: ContinuousMapZero.mkD_apply_of_continuous
-- Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
inst_4 : Zero (↑s : Type u_2)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := ContinuousMapZero.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ

Tactic:
hasFiniteIntegral_mkD_of_bound _ _ ?_ f_ae_zero bound bound_int ?_

Premises used: ContinuousMapZero.hasFiniteIntegral_mkD_of_bound