awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m m₀ : MeasurableSpace α
μ : Measure α
β' : Type u_5
inst_2 : TopologicalSpace β'
g : β → β' → γ
f : α → β
f' : α → β'
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
hf : AEStronglyMeasurable f μ
h'f : AEStronglyMeasurable f' μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x) (f' x)) μ

Tactic:
hg.comp_aestronglyMeasurable (hf.prodMk h'f)

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

Tactic:
hf.stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Measurable.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f

Tactic:
Filter.EventuallyEq.trans ?_ <|
      indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero

Premises used: Filter.EventuallyEq.trans, indicator_ae_eq_of_restrict_compl_ae_eq_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
refine : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] s.indicator f
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f

Tactic:
refine Filter.EventuallyEq.trans ?_ <|
      indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero

Premises used: Filter.EventuallyEq.trans, indicator_ae_eq_of_restrict_compl_ae_eq_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h :
  ∀ (x : α) (hx : f x = AEStronglyMeasurable.mk f hf x), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] s.indicator f

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
pos : ∀ (hxs : x ∈ s), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
neg : ∀ (hxs : x ∉ s), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∈ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
simp [hxs, hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∉ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
simp [hxs]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f

Tactic:
have h_ind_eq : s.indicator (hf.mk f) =ᵐ[μ] f := by
    refine Filter.EventuallyEq.trans ?_ <|
      indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero
    filter_upwards [hf.ae_eq_mk] with x hx
    by_cases hxs : x ∈ s
    · simp [hxs, hx]
    · simp [hxs]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
suffices : StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))
⊢ AEStronglyMeasurable f μ

Tactic:
suffices StronglyMeasurable[m'] (s.indicator (hf.mk f)) from
    this.aestronglyMeasurable.congr h_ind_eq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
⊢ StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))

Tactic:
(hf.stronglyMeasurable_mk.indicator hs_m).stronglyMeasurable_of_measurableSpace_le_on hs_m
    hs fun x hxs => Set.indicator_of_notMem hxs _

Premises used: MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.StronglyMeasurable.indicator, Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
⊢ StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))

Tactic:
exact (hf.stronglyMeasurable_mk.indicator hs_m).stronglyMeasurable_of_measurableSpace_le_on hs_m
    hs fun x hxs => Set.indicator_of_notMem hxs _

Premises used: MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.StronglyMeasurable.indicator, Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst_1 : Mul β
inst_2 : ContinuousMul β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ StronglyMeasurable (AEStronglyMeasurable.mk f hf * AEStronglyMeasurable.mk g hg)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Mul β
inst_2 : ContinuousMul β
hf : AEStronglyMeasurable f μ
c : β
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ f x * c) μ

Tactic:
hf.mul aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Mul β
inst_2 : ContinuousMul β
hf : AEStronglyMeasurable f μ
c : β
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ c * f x) μ

Tactic:
aestronglyMeasurable_const.mul hf

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Inv β
inst_2 : ContinuousInv β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f⁻¹ μ

Tactic:
⟨(hf.mk f)⁻¹, hf.stronglyMeasurable_mk.inv, hf.ae_eq_mk.inv⟩

Premises used: MeasureTheory.StronglyMeasurable.inv, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Inv.inv, MeasureTheory.AEStronglyMeasurable.mk, Filter.EventuallyEq.inv, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst_1 : Group β
inst_2 : IsTopologicalGroup β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (f / g) μ

Tactic:
⟨hf.mk f / hg.mk g, hf.stronglyMeasurable_mk.div' hg.stronglyMeasurable_mk,
    hf.ae_eq_mk.div hg.ae_eq_mk⟩

Premises used: Filter.EventuallyEq.div, HDiv.hDiv, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.StronglyMeasurable.div', And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (f / g) μ

Tactic:
⟨hf.mk f / hg.mk g, hf.stronglyMeasurable_mk.div hg.stronglyMeasurable_mk,
    hf.ae_eq_mk.div hg.ae_eq_mk⟩

Premises used: Filter.EventuallyEq.div, HDiv.hDiv, MeasureTheory.StronglyMeasurable.div, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst_1 : CommGroup β
inst_2 : IsTopologicalGroup β
hf : AEStronglyMeasurable f μ
h : AEStronglyMeasurable (f * g) μ
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Premises used: mul_inv_cancel_comm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst_1 : CommGroup β
inst_2 : IsTopologicalGroup β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (g * f) μ ↔ AEStronglyMeasurable g μ

Tactic:
mul_comm g f ▸ AEStronglyMeasurable.mul_iff_right hf

Premises used: Eq.rec, MeasureTheory.AEStronglyMeasurable.mul_iff_right, mul_comm, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : SMul 𝕜 β
inst_3 : ContinuousSMul 𝕜 β
f : α → 𝕜
g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ f x • g x) μ

Tactic:
continuous_smul.comp_aestronglyMeasurable (hf.prodMk hg)

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.prodMk, ContinuousSMul.continuous_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Monoid β
inst_2 : ContinuousMul β
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ AEStronglyMeasurable (f ^ n) μ

Tactic:
⟨hf.mk f ^ n, hf.stronglyMeasurable_mk.pow _, hf.ae_eq_mk.pow_const _⟩

Premises used: Filter.EventuallyEq.pow_const, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, HPow.hPow, MeasureTheory.StronglyMeasurable.pow, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
𝕜 : Type u_5
inst_1 : SMul 𝕜 β
inst_2 : ContinuousConstSMul 𝕜 β
hf : AEStronglyMeasurable f μ
c : 𝕜
⊢ AEStronglyMeasurable (c • f) μ

Tactic:
⟨c • hf.mk f, hf.stronglyMeasurable_mk.const_smul c, hf.ae_eq_mk.const_smul c⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, MeasureTheory.StronglyMeasurable.const_smul, Exists.intro, HSMul.hSMul, Filter.EventuallyEq.const_smul, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
𝕜 : Type u_5
inst_1 : SMul 𝕜 β
inst_2 : ContinuousConstSMul 𝕜 β
hf : AEStronglyMeasurable f μ
c : 𝕜
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ c • f x) μ

Tactic:
hf.const_smul c

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : SMul 𝕜 β
inst_3 : ContinuousSMul 𝕜 β
f : α → 𝕜
hf : AEStronglyMeasurable f μ
c : β
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ f x • c) μ

Tactic:
continuous_smul.comp_aestronglyMeasurable (hf.prodMk aestronglyMeasurable_const)

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.prodMk, ContinuousSMul.continuous_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
R : Type u_5
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
f : α → R
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (star f) μ

Tactic:
⟨star (hf.mk f), hf.stronglyMeasurable_mk.star, hf.ae_eq_mk.star⟩

Premises used: Filter.EventuallyEq.star, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.StronglyMeasurable.star, Star.star
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst_1 : SemilatticeSup β
inst_2 : ContinuousSup β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (f ⊔ g) μ

Tactic:
⟨hf.mk f ⊔ hg.mk g, hf.stronglyMeasurable_mk.sup hg.stronglyMeasurable_mk,
    hf.ae_eq_mk.sup hg.ae_eq_mk⟩

Premises used: MeasureTheory.StronglyMeasurable.sup, Filter.EventuallyEq.sup, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, Max.max, 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 g : α → β
inst_1 : SemilatticeInf β
inst_2 : ContinuousInf β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (f ⊓ g) μ

Tactic:
⟨hf.mk f ⊓ hg.mk g, hf.stronglyMeasurable_mk.inf hg.stronglyMeasurable_mk,
    hf.ae_eq_mk.inf hg.ae_eq_mk⟩

Premises used: MeasureTheory.StronglyMeasurable.inf, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable, Min.min, Filter.EventuallyEq.inf
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_5} (β := M) (List.prod []) μ

Tactic:
aestronglyMeasurable_one

Premises used: List.foldr, MeasureTheory.aestronglyMeasurable_one, List.prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_5} (β := M) (List.prod []) μ

Tactic:
exact aestronglyMeasurable_one

Premises used: MeasureTheory.aestronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ
⊢ AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ

Tactic:
rw [List.forall_mem_cons] at hl

Premises used: List.forall_mem_cons
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
cons : AEStronglyMeasurable (f * l.prod) μ
⊢ AEStronglyMeasurable (f :: l).prod μ

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * l.prod) μ

Tactic:
hl.1.mul (ihl hl.2)

Premises used: And.right, And.left, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * l.prod) μ

Tactic:
exact hl.1.mul (ihl hl.2)

Premises used: And.right, And.left, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
nil :
  ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEStronglyMeasurable f μ),
    AEStronglyMeasurable.{u_1, u_5} (β := M) (List.prod []) μ
cons :
  ∀ (f : α → M) (l : List (α → M)) (ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ)
    (hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ), AEStronglyMeasurable (f :: l).prod μ
⊢ AEStronglyMeasurable l.prod μ

Tactic:
induction l with
  | nil => exact aestronglyMeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)

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

Tactic:
simpa only [← Pi.list_prod_apply] using l.aestronglyMeasurable_prod hl

Premises used: List.aestronglyMeasurable_prod, Pi.list_prod_apply
-- 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 : Multiset (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
mk :
  ∀ (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)) μ
⊢ AEStronglyMeasurable l.prod μ

Tactic:
rcases l with ⟨l⟩
-- 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 μ
⊢ ∀ f ∈ l, AEStronglyMeasurable f μ

Tactic:
simpa using hl