awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 (ε := ContinuousMapZero.{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 _ _ ?_ f_ae_zero bound bound_int ?_

Premises used: ContinuousMapZero.hasFiniteIntegral_mkD_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
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
⊢ ∀ᵐ (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.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
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : (↑s : Type u_2)), ‖s.restrict (π := fun (a : Y) ↦ E) (f x) y‖ ≤ bound x

Tactic:
simpa
-- 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
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
rw : AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) μ
⊢ AEStronglyMeasurable (β := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) μ

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.aestronglyMeasurable_comp_iff
-- 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
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) μ

Tactic:
aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry f g f_cont

Premises used: aestronglyMeasurable_congr, toContinuousMap, Iff.mp, ContinuousMap.aeStronglyMeasurable_mkD_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
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
refine :
  (ae μ).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
    (↑(mkD (f x) g) : C(Y, E))
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) μ

Tactic:
refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry f g f_cont

Premises used: aestronglyMeasurable_congr, toContinuousMap, Iff.mp, ContinuousMap.aeStronglyMeasurable_mkD_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
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
h :
  ∀ (x : X) (zero_x : f x 0 = 0), Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))
⊢ (ae μ).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
    (↑(mkD (f x) g) : C(Y, E))

Tactic:
filter_upwards [f_zero] with 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
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
x : X
zero_x : f x 0 = 0
h h₁ : Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (ContinuousMap.mkD (f x) (↑g : C(Y, E)))
⊢ Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))

Tactic:
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]

Premises used: ContinuousMapZero.mkD_eq_mkD_of_map_zero
-- 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
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : 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)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
rw : AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) (μ.restrict s)
⊢ AEStronglyMeasurable (β := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) (μ.restrict s)

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.aestronglyMeasurable_comp_iff
-- 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
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : 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)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) (μ.restrict s)

Tactic:
aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry hs f g f_cont

Premises used: aestronglyMeasurable_congr, toContinuousMap, ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry, Iff.mp
-- 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
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : 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)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
refine :
  (ae (μ.restrict s)).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
    (↑(mkD (f x) g) : C(Y, E))
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) (μ.restrict s)

Tactic:
refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry hs f g f_cont

Premises used: aestronglyMeasurable_congr, toContinuousMap, ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry, Iff.mp
-- 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
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : 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)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
h :
  ∀ (x : X) (zero_x : f x 0 = 0), Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))
⊢ (ae (μ.restrict s)).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
    (↑(mkD (f x) g) : C(Y, E))

Tactic:
filter_upwards [f_zero] with 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
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : 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)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
x : X
zero_x : f x 0 = 0
h h₁ : Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (ContinuousMap.mkD (f x) (↑g : C(Y, E)))
⊢ Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))

Tactic:
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]

Premises used: ContinuousMapZero.mkD_eq_mkD_of_map_zero
-- 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
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
rw :
  AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) μ
⊢ AEStronglyMeasurable (β := ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.aestronglyMeasurable_comp_iff
-- 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
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) μ

Tactic:
aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry f g f_cont

Premises used: aestronglyMeasurable_congr, ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry, Iff.mp
-- 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
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
refine :
  (ae μ).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) μ

Tactic:
refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry f g f_cont

Premises used: aestronglyMeasurable_congr, ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry, Iff.mp
-- 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
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
h :
  ∀ (x : X) (zero_x : f x (↑0 : Y) = 0),
    Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
      (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
      (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
⊢ (ae μ).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))

Tactic:
filter_upwards [f_zero] with 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
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
x : X
zero_x : f x (↑0 : Y) = 0
h h₁ :
  Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
⊢ Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))

Tactic:
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]

Premises used: ContinuousMapZero.mkD_eq_mkD_of_map_zero
-- 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 X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
rw :
  AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) (μ.restrict s)
⊢ AEStronglyMeasurable (β := ContinuousMapZero.{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:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.aestronglyMeasurable_comp_iff
-- 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 X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) (μ.restrict s)

Tactic:
aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs f g f_cont

Premises used: aestronglyMeasurable_congr, ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, Iff.mp
-- 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 X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
refine :
  (ae (μ.restrict s)).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
⊢ AEStronglyMeasurable (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))) (μ.restrict s)

Tactic:
refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs f g f_cont

Premises used: aestronglyMeasurable_congr, ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, Iff.mp
-- 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 X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
h :
  ∀ (x : X) (zero_x : f x (↑0 : Y) = 0),
    Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
      (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
      (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))
⊢ (ae (μ.restrict s)).EventuallyEq (β := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (fun (x : X) ↦ ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    fun (x : X) ↦ (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))

Tactic:
filter_upwards [f_zero] with 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
s : Set X
t : Set Y
inst_3 : CompactSpace.{u_2} (↑t : Type u_2)
inst_4 : Zero (↑t : Type u_2)
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X (ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
hs : MeasurableSet s
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑t : Type u_2) E
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x (↑0 : Y) = 0
x : X
zero_x : f x (↑0 : Y) = 0
h h₁ :
  Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
⊢ Eq (α := ContinuousMap.{u_2, u_3} (↑t : Type u_2) E)
    (ContinuousMap.mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) (↑g : C((↑t : Type u_2), E)))
    (↑(mkD (t.restrict (π := fun (a : Y) ↦ E) (f x)) g) : C((↑t : Type u_2), E))

Tactic:
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]

Premises used: ContinuousMapZero.mkD_eq_mkD_of_map_zero
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
h : ∀ (x : X) (x_1 : ι), f x x_1 = (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) x x_1
⊢ f = ∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i

Tactic:
ext
-- Module: Mathlib.MeasureTheory.SpecificCodomains.Pi
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp.{u_1, u_3} (ε := E i) (fun (x : X) ↦ f x i) p μ
x : X
x_1 : ι
⊢ f x x_1 = (∑ i : ι, Pi.single (M := E) i ∘ fun (x : X) ↦ f x i) x x_1

Tactic:
simp