awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l_1 : Multiset (α → M)
l : List (α → M)
hl :
  ∀ (f : α → M),
    Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
        f →
      AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)) μ

Tactic:
simpa using l.aestronglyMeasurable_prod (by simpa using hl)

Premises used: List.aestronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
s : Multiset (α → M)
hs : ∀ f ∈ s, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_5} (β := M) (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (f : α → M) ↦ f x) s)) μ

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.aestronglyMeasurable_prod hs

Premises used: Pi.multiset_prod_apply, Multiset.aestronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
ι : Type u_6
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable.{u_1, u_5} (β := M) (∏ i ∈ s, f i) μ

Tactic:
Multiset.aestronglyMeasurable_prod _ fun _g hg =>
    let ⟨_i, hi, hg⟩ := Multiset.mem_map.1 hg
    hg ▸ hf _ hi

Premises used: Multiset.mem_map, Eq.rec, Finset.prod, _private.0.Finset.aestronglyMeasurable_prod.match_1, Iff.mp, Multiset.aestronglyMeasurable_prod, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
ι : Type u_6
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable.{u_1, u_5} (β := M) (fun (a : α) ↦ ∏ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.prod_apply] using s.aestronglyMeasurable_prod hf

Premises used: Finset.prod_apply, Finset.aestronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : MeasurableSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : OpensMeasurableSpace β
inst_4 : SecondCountableTopology β
hf : AEMeasurable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
⟨hf.mk f, hf.measurable_mk.stronglyMeasurable, hf.ae_eq_mk⟩

Premises used: Measurable.stronglyMeasurable, AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
x : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
⊢ AEStronglyMeasurable id μ

Tactic:
aemeasurable_id.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, aemeasurable_id
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : MeasurableSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : BorelSpace β
inst_4 : SecondCountableTopology β
⊢ AEStronglyMeasurable f μ ↔ AEMeasurable f μ

Tactic:
⟨fun h => h.aemeasurable, fun h => h.aestronglyMeasurable⟩

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : PseudoMetricSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ dist (f x) (g x)) μ

Tactic:
continuous_dist.comp_aestronglyMeasurable (hf.prodMk hg)

Premises used: Continuous.comp_aestronglyMeasurable, continuous_dist, MeasureTheory.AEStronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : SeminormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
continuous_norm.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, continuous_norm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : SeminormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ≥0) (fun (x : α) ↦ ‖f x‖₊) μ

Tactic:
continuous_nnnorm.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, continuous_nnnorm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : ContinuousENorm β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
(continuous_enorm.comp_aestronglyMeasurable hf).aemeasurable

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, continuous_enorm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : PseudoMetricSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ edist (f a) (g a)) μ

Tactic:
(continuous_edist.comp_aestronglyMeasurable (hf.prodMk hg)).aemeasurable

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, continuous_edist, MeasureTheory.AEStronglyMeasurable.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ

Tactic:
continuous_real_toNNReal.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, continuous_real_toNNReal
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
mp : AEStronglyMeasurable (s.indicator f) μ → AEStronglyMeasurable f (μ.restrict s)
mpr : AEStronglyMeasurable f (μ.restrict s) → AEStronglyMeasurable (s.indicator f) μ
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable (s.indicator f) μ
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
(h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.restrict_le_self, indicator_ae_eq_restrict
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable (s.indicator f) μ
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.restrict_le_self, indicator_ae_eq_restrict
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ

Tactic:
⟨indicator s (h.mk f), h.stronglyMeasurable_mk.indicator hs, ?_⟩

Premises used: Set.indicator, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.StronglyMeasurable.indicator, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
mpr : s.indicator f =ᶠ[ae μ] s.indicator (AEStronglyMeasurable.mk f h)
⊢ AEStronglyMeasurable (s.indicator f) μ

Tactic:
refine ⟨indicator s (h.mk f), h.stronglyMeasurable_mk.indicator hs, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEStronglyMeasurable.mk f h)

Tactic:
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (h.mk f) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEStronglyMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEStronglyMeasurable.mk f h)

Tactic:
have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (h.mk f) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEStronglyMeasurable.mk f h)
B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEStronglyMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEStronglyMeasurable.mk f h)

Tactic:
ae_of_ae_restrict_of_ae_restrict_compl _ A B

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEStronglyMeasurable.mk f h)
B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEStronglyMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEStronglyMeasurable.mk f h)

Tactic:
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : NullMeasurableSet s μ
rw : AEStronglyMeasurable ((toMeasurable μ s).indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
rw₁ : AEStronglyMeasurable f (μ.restrict (toMeasurable μ s)) ↔ AEStronglyMeasurable f (μ.restrict s)
rw₂ rw₃ : AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)

Tactic:
rw [← aestronglyMeasurable_congr (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    aestronglyMeasurable_indicator_iff (measurableSet_toMeasurable ..),
    restrict_congr_set hs.toMeasurable_ae_eq]

Premises used: aestronglyMeasurable_congr, MeasureTheory.Measure.restrict_congr_set, indicator_ae_eq_of_ae_eq_set, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, aestronglyMeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
hfm : AEStronglyMeasurable f μ
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable (s.indicator f) μ

Tactic:
(aestronglyMeasurable_indicator_iff hs).mpr hfm.restrict

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.restrict, aestronglyMeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
hfm : AEStronglyMeasurable f μ
s : Set α
hs : NullMeasurableSet s μ
⊢ AEStronglyMeasurable (s.indicator f) μ

Tactic:
(aestronglyMeasurable_indicator_iff₀ hs).2 hfm.restrict

Premises used: Iff.mpr, aestronglyMeasurable_indicator_iff₀, MeasureTheory.AEStronglyMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
this : {a : α | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {x : α | f x = g x}
⊢ NullMeasurableSet {x : α | f x = g x} μ

Tactic:
apply
    (hf.stronglyMeasurable_mk.measurableSet_eq_fun
          hg.stronglyMeasurable_mk).nullMeasurableSet.congr

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.measurableSet_eq_fun, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h :
  ∀ (x : α) (hfx : f x = AEStronglyMeasurable.mk f hf x) (hgx : g x = AEStronglyMeasurable.mk g hg x),
    {a : α | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} x = {x : α | f x = g x} x
⊢ {a : α | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {x : α | f x = g x}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x) = (f x = g x)

Tactic:
simp only [hfx, hgx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
inst_2 : One E
f : α → E
hf : AEStronglyMeasurable f μ
⊢ NullMeasurableSet (mulSupport f) μ

Tactic:
(hf.nullMeasurableSet_eq_fun stronglyMeasurable_const.aestronglyMeasurable).compl

Premises used: MeasureTheory.stronglyMeasurable_const, Set.Mem, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.NullMeasurableSet.compl, setOf, Function.mulSupport, MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
this : {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a < g a}
⊢ NullMeasurableSet {a : α | f a < g a} μ

Tactic:
apply
    (hf.stronglyMeasurable_mk.measurableSet_lt hg.stronglyMeasurable_mk).nullMeasurableSet.congr

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.StronglyMeasurable.measurableSet_lt, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h :
  ∀ (x : α) (hfx : f x = AEStronglyMeasurable.mk f hf x) (hgx : g x = AEStronglyMeasurable.mk g hg x),
    {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a : α | f a < g a} x
⊢ {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a < g a}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
h : (AEStronglyMeasurable.mk f hf x < AEStronglyMeasurable.mk g hg x) = (f x < g x)
⊢ {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a : α | f a < g a} x

Tactic:
change (hf.mk f x < hg.mk g x) = (f x < g x)

Premises used: MeasureTheory.AEStronglyMeasurable.mk, LT.lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x < AEStronglyMeasurable.mk g hg x) = (f x < g x)

Tactic:
simp only [hfx, hgx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
this : {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a ≤ g a}
⊢ NullMeasurableSet {a : α | f a ≤ g a} μ

Tactic:
apply
    (hf.stronglyMeasurable_mk.measurableSet_le hg.stronglyMeasurable_mk).nullMeasurableSet.congr

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h :
  ∀ (x : α) (hfx : f x = AEStronglyMeasurable.mk f hf x) (hgx : g x = AEStronglyMeasurable.mk g hg x),
    {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a : α | f a ≤ g a} x
⊢ {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a ≤ g a}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
h : (AEStronglyMeasurable.mk f hf x ≤ AEStronglyMeasurable.mk g hg x) = (f x ≤ g x)
⊢ {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a : α | f a ≤ g a} x

Tactic:
change (hf.mk f x ≤ hg.mk g x) = (f x ≤ g x)

Premises used: LE.le, MeasureTheory.AEStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x ≤ AEStronglyMeasurable.mk g hg x) = (f x ≤ g x)

Tactic:
simp only [hfx, hgx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
β : Type u_2
inst : TopologicalSpace β
α : Type u_5
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → β
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ AEStronglyMeasurable f μ

Tactic:
⟨hf.mk f, StronglyMeasurable.mono hf.stronglyMeasurable_mk hm, ae_eq_of_ae_eq_trim hf.ae_eq_mk⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.ae_eq_of_ae_eq_trim, MeasureTheory.StronglyMeasurable.mono, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
g : α → β
γ : Type u_5
x : MeasurableSpace γ
x_1 : MeasurableSpace α
f : γ → α
μ : Measure γ
hg : AEStronglyMeasurable (m₀ := x_1) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ AEStronglyMeasurable (g ∘ f) μ

Tactic:
⟨hg.mk g ∘ hf.mk f, hg.stronglyMeasurable_mk.comp_measurable hf.measurable_mk,
    (ae_eq_comp hf hg.ae_eq_mk).trans (hf.ae_eq_mk.fun_comp (hg.mk g))⟩

Premises used: Filter.EventuallyEq.trans, Function.comp, AEMeasurable.mk, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.ae_eq_comp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.fun_comp, MeasureTheory.AEStronglyMeasurable, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
g : α → β
γ : Type u_5
x : MeasurableSpace γ
x_1 : MeasurableSpace α
f : γ → α
μ : Measure γ
hg : AEStronglyMeasurable (m₀ := x_1) g (Measure.map f μ)
hf : Measurable f
⊢ AEStronglyMeasurable (g ∘ f) μ

Tactic:
hg.comp_aemeasurable hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable