awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
refine_1 : MeasurableSet (α := ℝ≥0 × ℝ) {a : ℝ≥0 × ℝ | a.1 = 0 ∧ a.2 < 0}
⊢ Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ) ↦ if p.1 = 0 ∧ p.2 < 0 then ∞ else (↑(p.1 ^ p.2) : ℝ≥0∞)

Tactic:
refine Measurable.ite ?_ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal

Premises used: Measurable.coe_nnreal_ennreal, Measurable.ite, measurable_snd, measurable_const, Measurable.pow, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ MeasurableSet (α := ℝ≥0 × ℝ) {a : ℝ≥0 × ℝ | a.1 = 0 ∧ a.2 < 0}

Tactic:
MeasurableSet.inter (measurable_fst (measurableSet_singleton 0))
        (measurable_snd measurableSet_Iio)

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, measurableSet_Iio, setOf, Set.inter, measurable_snd, OfNat.ofNat, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ MeasurableSet (α := ℝ≥0 × ℝ) {a : ℝ≥0 × ℝ | a.1 = 0 ∧ a.2 < 0}

Tactic:
exact
      MeasurableSet.inter (measurable_fst (measurableSet_singleton 0))
        (measurable_snd measurableSet_Iio)

Premises used: MeasurableSingletonClass.measurableSet_singleton, measurableSet_Iio, measurable_snd, OfNat.ofNat, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if 0 < x then ∞ else if x = 0 then 1 else 0

Tactic:
Measurable.ite measurableSet_Ioi measurable_const ?_

Premises used: Measurable.ite, measurableSet_Ioi, measurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
refine_2 : Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if x = 0 then 1 else 0
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if 0 < x then ∞ else if x = 0 then 1 else 0

Tactic:
refine Measurable.ite measurableSet_Ioi measurable_const ?_

Premises used: Measurable.ite, measurableSet_Ioi, measurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if x = 0 then 1 else 0

Tactic:
Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const

Premises used: MeasurableSingletonClass.measurableSet_singleton, Measurable.ite, measurable_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ if x = 0 then 1 else 0

Tactic:
exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const

Premises used: MeasurableSingletonClass.measurableSet_singleton, Measurable.ite, measurable_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : MeasurableSpace α
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SecondCountableTopology E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (t : α) ↦ ⟪f t, g t⟫

Tactic:
Continuous.measurable2 continuous_inner hf hg

Premises used: continuous_inner, Continuous.measurable2
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : MeasurableSpace α
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SecondCountableTopology E
c : E
f : α → E
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (t : α) ↦ ⟪c, f t⟫

Tactic:
Measurable.inner measurable_const hf

Premises used: Measurable.inner, measurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : MeasurableSpace α
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SecondCountableTopology E
c : E
f : α → E
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (t : α) ↦ ⟪f t, c⟫

Tactic:
Measurable.inner hf measurable_const

Premises used: Measurable.inner, measurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_1, u_2} (β := 𝕜) (fun (x : α) ↦ ⟪f x, g x⟫) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SecondCountableTopology E
μ : MeasureTheory.Measure α
f : α → E
c : E
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_1, u_2} (β := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) μ

Tactic:
AEMeasurable.inner aemeasurable_const hf

Premises used: AEMeasurable.inner, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SecondCountableTopology E
μ : MeasureTheory.Measure α
f : α → E
c : E
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_1, u_2} (β := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) μ

Tactic:
AEMeasurable.inner hf aemeasurable_const

Premises used: AEMeasurable.inner, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Measurable.{u_1, 0} (α := 𝕜) (β := ℝ) (⇑re : (a : 𝕜) → ℝ)

Tactic:
continuous_re.measurable

Premises used: RCLike.continuous_re, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Measurable.{u_1, 0} (α := 𝕜) (β := ℝ) (⇑im : (a : 𝕜) → ℝ)

Tactic:
continuous_im.measurable

Premises used: Continuous.measurable, RCLike.continuous_im
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
m : MeasurableSpace α
f : α → 𝕜
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)

Tactic:
RCLike.measurable_re.comp hf

Premises used: Measurable.comp, RCLike.measurable_re
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
m : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
RCLike.measurable_re.comp_aemeasurable hf

Premises used: RCLike.measurable_re, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
m : MeasurableSpace α
f : α → 𝕜
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)

Tactic:
RCLike.measurable_im.comp hf

Premises used: Measurable.comp, RCLike.measurable_im
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
m : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
RCLike.measurable_im.comp_aemeasurable hf

Premises used: RCLike.measurable_im, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
⊢ Measurable.{0, u_2} (β := 𝕜) ofReal

Tactic:
RCLike.continuous_ofReal.measurable

Premises used: RCLike.continuous_ofReal, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
hre : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)
him : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)
⊢ Measurable.{u_1, u_2} (β := 𝕜) fun (a : α) ↦
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) a +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) a) RCLike.I

Tactic:
Measurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp hre)
      ((RCLike.measurable_ofReal.comp him).mul_const RCLike.I)

Premises used: RCLike.measurable_ofReal, Measurable.comp, Measurable.add, RCLike.I, Measurable.mul_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
hre : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)
him : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)
h :
  ∀ (x : α),
    f x =
      (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
        HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I
⊢ Measurable f

Tactic:
convert!
    Measurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp hre)
      ((RCLike.measurable_ofReal.comp him).mul_const RCLike.I)

Premises used: RCLike.measurable_ofReal, Measurable.comp, Measurable.add, RCLike.I, Measurable.mul_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
hre : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)
him : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)
x : α
⊢ f x =
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I

Tactic:
(RCLike.re_add_im _).symm

Premises used: RCLike.re_add_im, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
hre : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)
him : Measurable (β := ℝ) fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)
x : α
⊢ f x =
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I

Tactic:
exact (RCLike.re_add_im _).symm

Premises used: RCLike.re_add_im, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
him : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
⊢ AEMeasurable.{u_1, u_2} (β := 𝕜)
    (fun (a : α) ↦
      (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) a +
        HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) a) RCLike.I)
    μ

Tactic:
AEMeasurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp_aemeasurable hre)
      ((RCLike.measurable_ofReal.comp_aemeasurable him).mul_const RCLike.I)

Premises used: RCLike.measurable_ofReal, AEMeasurable.add, AEMeasurable.mul_const, RCLike.I, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
him : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
h :
  ∀ (x : α),
    f x =
      (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
        HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I
⊢ AEMeasurable f μ

Tactic:
convert!
    AEMeasurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp_aemeasurable hre)
      ((RCLike.measurable_ofReal.comp_aemeasurable him).mul_const RCLike.I)

Premises used: RCLike.measurable_ofReal, AEMeasurable.add, AEMeasurable.mul_const, RCLike.I, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
him : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
x : α
⊢ f x =
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I

Tactic:
(RCLike.re_add_im _).symm

Premises used: RCLike.re_add_im, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
Goal:
α : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
him : AEMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
x : α
⊢ f x =
    (RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) x +
      HMul.hMul (α := 𝕜) ((RCLike.ofReal ∘ fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) x) RCLike.I

Tactic:
exact (RCLike.re_add_im _).symm

Premises used: RCLike.re_add_im, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
⊢ Measurable sinc

Tactic:
continuous_sinc.measurable

Premises used: Real.continuous_sinc, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
⊢ StronglyMeasurable sinc

Tactic:
measurable_sinc.stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, Real.measurable_sinc
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
funProp : enorm (E := ℝ) 1 ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ 1) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
⊢ AEStronglyMeasurable sinc μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
refine : ∀ (x : ℝ), ‖sinc x‖ ≤ (fun (x : ℝ) ↦ (1 : ℝ)) x
⊢ Integrable sinc μ

Tactic:
refine Integrable.mono' (g := fun _ ↦ 1) (by fun_prop) (by fun_prop) <| ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.Integrable.mono', MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x : ℝ
⊢ |sinc x| ≤ (fun (x : ℝ) ↦ (1 : ℝ)) x

Tactic:
abs_sinc_le_one x

Premises used: Real.abs_sinc_le_one
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x : ℝ
⊢ |sinc x| ≤ (fun (x : ℝ) ↦ (1 : ℝ)) x

Tactic:
exact abs_sinc_le_one x

Premises used: Real.abs_sinc_le_one
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ sinc (f x)

Tactic:
Real.measurable_sinc.comp hf

Premises used: Measurable.comp, Real.measurable_sinc, Real.sinc, ite
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ

Tactic:
Real.measurable_sinc.comp_aemeasurable hf

Premises used: Real.measurable_sinc, Real.sinc, Measurable.comp_aemeasurable, ite
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := ℝ) fun (x : α) ↦ sinc (f x)

Tactic:
Real.stronglyMeasurable_sinc.comp_measurable hf.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, Real.sinc, MeasureTheory.StronglyMeasurable.comp_measurable, Real.stronglyMeasurable_sinc, ite
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEStronglyMeasurable f μ
rw : ∀ (hf : AEMeasurable f μ), AEMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ

Tactic:
rw [aestronglyMeasurable_iff_aemeasurable] at hf ⊢

Premises used: aestronglyMeasurable_iff_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ

Tactic:
hf.sinc

Premises used: AEMeasurable.sinc
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ sinc (f x)) μ

Tactic:
exact hf.sinc

Premises used: AEMeasurable.sinc
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
hf : FinStronglyMeasurable f μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
⟨f, hf, ae_eq_refl f⟩

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.AEFinStronglyMeasurable, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
x : MeasurableSpace α
μ : Measure α
inst : Zero β
inst_1 : TopologicalSpace β
⊢ AEFinStronglyMeasurable.{u_5, u_6} (β := β) 0 μ

Tactic:
⟨0, finStronglyMeasurable_zero, EventuallyEq.rfl⟩

Premises used: MeasureTheory.finStronglyMeasurable_zero, MeasureTheory.AEFinStronglyMeasurable, And.intro, Exists.intro, Filter.EventuallyEq.rfl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : StronglyMeasurable f
⊢ AEStronglyMeasurable f μ

Tactic:
⟨f, hf, EventuallyEq.refl _ _⟩

Premises used: Filter.EventuallyEq.refl, 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 α
b : β
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ b) μ

Tactic:
stronglyMeasurable_const.aestronglyMeasurable

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
inst_1 : One β
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) 1 μ

Tactic:
stronglyMeasurable_one.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Subsingleton α
⊢ AEStronglyMeasurable f μ

Tactic:
StronglyMeasurable.of_subsingleton_dom.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.of_subsingleton_dom
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Subsingleton β
⊢ AEStronglyMeasurable f μ

Tactic:
StronglyMeasurable.of_subsingleton_cod.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.of_subsingleton_cod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
h : Nontrivial α
inhabit : ∀ (inhabited_h : Inhabited α), AEStronglyMeasurable (m₀ := m₀) f 0
⊢ AEStronglyMeasurable (m₀ := m₀) f 0

Tactic:
inhabit α
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
h : Nontrivial α
inhabited_h : Inhabited α
⊢ AEStronglyMeasurable (m₀ := m₀) f 0

Tactic:
⟨fun _ => f default, stronglyMeasurable_const, rfl⟩

Premises used: MeasureTheory.stronglyMeasurable_const, Inhabited.default, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable, rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
h : Nontrivial α
inhabited_h : Inhabited α
⊢ AEStronglyMeasurable (m₀ := m₀) f 0

Tactic:
exact ⟨fun _ => f default, stronglyMeasurable_const, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α →ₛ β
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (⇑f : (a : α) → β) μ

Tactic:
f.stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
obtain : ∀ (a : α), AEStronglyMeasurable id μ
⊢ AEStronglyMeasurable id μ

Tactic:
obtain ⟨a, -⟩ := exists_pair_ne α

Premises used: exists_pair_ne
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set α)
    {x : α | (fun (x : α) ↦ id x = (closure[inst] s).piecewise (β := fun (a : α) ↦ α) id (fun (x : α) ↦ a) x) x} x

Tactic:
simp [subset_closure hx]

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
refine : StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
⊢ AEStronglyMeasurable id μ

Tactic:
refine ⟨(closure s).piecewise id (fun _ ↦ a), ?_,
    Filter.mem_of_superset h2 (fun x hx ↦ by simp [subset_closure hx])⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
⊢ SecondCountableTopology.{u_1} (↑(closure[inst] s) : Type u_1)

Tactic:
have := h1.closure.secondCountableTopology