awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
⊢ MemLp.{u_1, u_4} (ε := E) (⇑(Lp.simpleFunc.toSimpleFunc f) : (a : α) → E) 1 μ

Tactic:
Lp.simpleFunc.memLp f

Premises used: MeasureTheory.Lp.simpleFunc.memLp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
⊢ MemLp.{u_1, u_4} (ε := E) (⇑(Lp.simpleFunc.toSimpleFunc f) : (a : α) → E) 1 μ

Tactic:
exact Lp.simpleFunc.memLp f

Premises used: MeasureTheory.Lp.simpleFunc.memLp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g)
h_closed : IsClosed (X := ↥(Lp E 1 μ)) {f : ↥(Lp E 1 μ) | P (↑(↑f : α →ₘ[μ] E) : α → E)}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Integrable f μ → P f → P g
simp :
  ∀ (h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f 1 μ → MemLp g 1 μ → P f → P g → P (f + g))
    (h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f 1 μ → P f → P g) ⦃f : α → E⦄, MemLp f 1 μ → P f
⊢ ∀ ⦃f : α → E⦄, Integrable f μ → P f

Tactic:
simp only [← memLp_one_iff_integrable] at *

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_closed : IsClosed (X := ↥(Lp E 1 μ)) {f : ↥(Lp E 1 μ) | P (↑(↑f : α →ₘ[μ] E) : α → E)}
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f 1 μ → MemLp g 1 μ → P f → P g → P (f + g)
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f 1 μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, MemLp f 1 μ → P f

Tactic:
MemLp.induction one_ne_top (motive := P) h_ind h_add h_closed h_ae

Premises used: MeasureTheory.MemLp.induction, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_closed : IsClosed (X := ↥(Lp E 1 μ)) {f : ↥(Lp E 1 μ) | P (↑(↑f : α →ₘ[μ] E) : α → E)}
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f 1 μ → MemLp g 1 μ → P f → P g → P (f + g)
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f 1 μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, MemLp f 1 μ → P f

Tactic:
exact MemLp.induction one_ne_top (motive := P) h_ind h_add h_closed h_ae

Premises used: MeasureTheory.MemLp.induction, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan
Goal:
⊢ Measurable arctan

Tactic:
continuous_arctan.measurable

Premises used: Real.continuous_arctan, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ Real.arctan (f x)

Tactic:
measurable_arctan.comp hf

Premises used: Real.arctan, Measurable.comp, Real.measurable_arctan
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable rexp

Tactic:
continuous_exp.measurable

Premises used: Real.continuous_exp, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable log

Tactic:
measurable_of_measurable_on_compl_singleton 0 <|
    Continuous.measurable <| continuousOn_iff_continuous_restrict.1 continuousOn_log

Premises used: Real.continuousOn_log, continuousOn_iff_continuous_restrict, measurable_of_measurable_on_compl_singleton, Continuous.measurable, Iff.mp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
h : ∀ (x : α), f x = log (rexp (f x))
⊢ f = fun (x : α) ↦ log (rexp (f x))

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
x_1 : α
h h₁ : f x_1 = f x_1
⊢ f x_1 = log (rexp (f x_1))

Tactic:
rw [log_exp]

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

Tactic:
have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
this : f = fun (x : α) ↦ log (rexp (f x))
rw : Measurable (β := ℝ) fun (x : α) ↦ log (rexp (f x))
⊢ Measurable f

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
this : f = fun (x : α) ↦ log (rexp (f x))
⊢ Measurable (β := ℝ) fun (x : α) ↦ log (rexp (f x))

Tactic:
measurable_log.comp hf

Premises used: Measurable.comp, Real.log, dite, Real.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
hf : Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)
this : f = fun (x : α) ↦ log (rexp (f x))
⊢ Measurable (β := ℝ) fun (x : α) ↦ log (rexp (f x))

Tactic:
exact measurable_log.comp hf

Premises used: Measurable.comp, Real.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : ∀ (x : α), f x = log (rexp (f x))
⊢ f = fun (x : α) ↦ log (rexp (f x))

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
x_1 : α
h h₁ : f x_1 = f x_1
⊢ f x_1 = log (rexp (f x_1))

Tactic:
rw [log_exp]

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

Tactic:
have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
this : f = fun (x : α) ↦ log (rexp (f x))
rw : AEMeasurable (β := ℝ) (fun (x : α) ↦ log (rexp (f x))) μ
⊢ AEMeasurable f μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
this : f = fun (x : α) ↦ log (rexp (f x))
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ log (rexp (f x))) μ

Tactic:
measurable_log.comp_aemeasurable hf

Premises used: Real.log, dite, Measurable.comp_aemeasurable, Real.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
this : f = fun (x : α) ↦ log (rexp (f x))
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ log (rexp (f x))) μ

Tactic:
exact measurable_log.comp_aemeasurable hf

Premises used: Measurable.comp_aemeasurable, Real.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ
μ : Measure α
t : ℝ
ht : t ≠ 0
hf : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (t * f x)) μ
⊢ AEMeasurable f μ

Tactic:
simpa only [mul_div_cancel_left₀ _ ht]
    using (aemeasurable_of_aemeasurable_exp hf).div (aemeasurable_const (b := t))

Premises used: mul_div_cancel_left₀, AEMeasurable.div, Real.aemeasurable_of_aemeasurable_exp, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable sin

Tactic:
continuous_sin.measurable

Premises used: Real.continuous_sin, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable cos

Tactic:
continuous_cos.measurable

Premises used: Real.continuous_cos, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable sinh

Tactic:
continuous_sinh.measurable

Premises used: Real.continuous_sinh, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable cosh

Tactic:
continuous_cosh.measurable

Premises used: Real.continuous_cosh, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable arcsin

Tactic:
continuous_arcsin.measurable

Premises used: Real.continuous_arcsin, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable arccos

Tactic:
continuous_arccos.measurable

Premises used: Continuous.measurable, Real.continuous_arccos
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable re

Tactic:
continuous_re.measurable

Premises used: Complex.continuous_re, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable im

Tactic:
continuous_im.measurable

Premises used: Continuous.measurable, Complex.continuous_im
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable ofReal

Tactic:
continuous_ofReal.measurable

Premises used: Complex.continuous_ofReal, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable cexp

Tactic:
continuous_exp.measurable

Premises used: Complex.continuous_exp, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable sin

Tactic:
continuous_sin.measurable

Premises used: Complex.continuous_sin, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable cos

Tactic:
continuous_cos.measurable

Premises used: Complex.continuous_cos, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable sinh

Tactic:
continuous_sinh.measurable

Premises used: Complex.continuous_sinh, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable cosh

Tactic:
continuous_cosh.measurable

Premises used: Complex.continuous_cosh, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable arg

Tactic:
have A : Measurable fun x : ℂ => Real.arcsin (x.im / ‖x‖) :=
    Real.measurable_arcsin.comp (measurable_im.div measurable_norm)
  have B : Measurable fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) :=
    Real.measurable_arcsin.comp ((measurable_im.comp measurable_neg).div measurable_norm)
  Measurable.ite (isClosed_le continuous_const continuous_re).measurableSet A <|
    Measurable.ite (isClosed_le continuous_const continuous_im).measurableSet (B.add_const _)
      (B.sub_const _)

Premises used: measurable_norm, Real.pi, Measurable.comp, Complex.continuous_re, continuous_const, Measurable.add_const, MeasurableNeg.measurable_neg, isClosed_le, Measurable.div, Measurable.ite, Complex.arg, IsClosed.measurableSet, Complex.measurable_im, Measurable.sub_const, Real.measurable_arcsin, Complex.continuous_im
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable log

Tactic:
(measurable_ofReal.comp <| Real.measurable_log.comp measurable_norm).add <|
    (measurable_ofReal.comp measurable_arg).mul_const I

Premises used: Complex.log, measurable_norm, Complex.measurable_arg, Measurable.comp, Measurable.add, Real.log, dite, Real.measurable_log, Complex.measurable_ofReal, Measurable.mul_const, Complex.I
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ rexp (f x)

Tactic:
Real.measurable_exp.comp hf

Premises used: Measurable.comp, Real.exp, Real.measurable_exp
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ log (f x)

Tactic:
measurable_log.comp hf

Premises used: Measurable.comp, Real.log, dite, Real.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ cos (f x)

Tactic:
measurable_cos.comp hf

Premises used: Measurable.comp, Real.cos, Real.measurable_cos
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ sin (f x)

Tactic:
measurable_sin.comp hf

Premises used: Measurable.comp, Real.measurable_sin, Real.sin
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ cosh (f x)

Tactic:
measurable_cosh.comp hf

Premises used: Measurable.comp, Real.measurable_cosh, Real.cosh
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ sinh (f x)

Tactic:
measurable_sinh.comp hf

Premises used: Real.measurable_sinh, Measurable.comp, Real.sinh
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ √(f x)

Tactic:
continuous_sqrt.measurable.comp hf

Premises used: Measurable.comp, Real.continuous_sqrt, Continuous.measurable, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
measurable_exp.comp_aemeasurable hf

Premises used: Real.exp, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ log (f x)) μ

Tactic:
measurable_log.comp_aemeasurable hf

Premises used: Real.log, dite, Measurable.comp_aemeasurable, Real.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ cos (f x)) μ

Tactic:
measurable_cos.comp_aemeasurable hf

Premises used: Real.cos, Real.measurable_cos, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ sin (f x)) μ

Tactic:
measurable_sin.comp_aemeasurable hf

Premises used: Real.measurable_sin, Measurable.comp_aemeasurable, Real.sin
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ cosh (f x)) μ

Tactic:
measurable_cosh.comp_aemeasurable hf

Premises used: Real.measurable_cosh, Real.cosh, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ sinh (f x)) μ

Tactic:
measurable_sinh.comp_aemeasurable hf

Premises used: Real.measurable_sinh, Real.sinh, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ √(f x)) μ

Tactic:
continuous_sqrt.measurable.comp_aemeasurable hf

Premises used: Real.continuous_sqrt, Continuous.measurable, Measurable.comp_aemeasurable, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ cexp (f x)

Tactic:
Complex.measurable_exp.comp hf

Premises used: Measurable.comp, Complex.measurable_exp
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ cos (f x)

Tactic:
Complex.measurable_cos.comp hf

Premises used: Complex.cos, Measurable.comp, Complex.measurable_cos
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ sin (f x)

Tactic:
Complex.measurable_sin.comp hf

Premises used: Measurable.comp, Complex.sin, Complex.measurable_sin
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ cosh (f x)

Tactic:
Complex.measurable_cosh.comp hf

Premises used: Measurable.comp, Complex.measurable_cosh, Complex.cosh
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ sinh (f x)

Tactic:
Complex.measurable_sinh.comp hf

Premises used: Complex.sinh, Measurable.comp, Complex.measurable_sinh
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ (f x).arg

Tactic:
measurable_arg.comp hf

Premises used: Complex.measurable_arg, Measurable.comp, Complex.arg, ite
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℂ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ log (f x)

Tactic:
measurable_log.comp hf

Premises used: Complex.log, Measurable.comp, Complex.measurable_log
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ cexp (f x)) μ

Tactic:
measurable_exp.comp_aemeasurable hf

Premises used: Complex.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ cos (f x)) μ

Tactic:
measurable_cos.comp_aemeasurable hf

Premises used: Complex.cos, Complex.measurable_cos, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ sin (f x)) μ

Tactic:
measurable_sin.comp_aemeasurable hf

Premises used: Complex.sin, Complex.measurable_sin, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ cosh (f x)) μ

Tactic:
measurable_cosh.comp_aemeasurable hf

Premises used: Complex.measurable_cosh, Measurable.comp_aemeasurable, Complex.cosh
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ sinh (f x)) μ

Tactic:
measurable_sinh.comp_aemeasurable hf

Premises used: Complex.sinh, Complex.measurable_sinh, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (f x).arg) μ

Tactic:
measurable_arg.comp_aemeasurable hf

Premises used: Complex.measurable_arg, Complex.arg, Measurable.comp_aemeasurable, ite
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℂ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ log (f x)) μ

Tactic:
measurable_log.comp_aemeasurable hf

Premises used: Complex.log, Complex.measurable_log, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℂ) fun (x : α) ↦ (↑(f x) : ℂ)

Tactic:
Complex.measurable_ofReal.comp hf

Premises used: Measurable.comp, Complex.measurable_ofReal
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℂ) (fun (x : α) ↦ (↑(f x) : ℂ)) μ

Tactic:
Complex.measurable_ofReal.comp_aemeasurable hf

Premises used: Measurable.comp_aemeasurable, Complex.measurable_ofReal
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ MeasurablePow ℂ ℂ

Tactic:
⟨Measurable.ite (measurable_fst (measurableSet_singleton 0))
      (Measurable.ite (measurable_snd (measurableSet_singleton 0)) measurable_one measurable_zero)
      (measurable_fst.clog.mul measurable_snd).cexp⟩

Premises used: Measurable.mul, MeasurableSingletonClass.measurableSet_singleton, MeasurablePow.mk, Measurable.ite, Measurable.cexp, measurable_one, measurable_zero, measurable_snd, OfNat.ofNat, Measurable.clog, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ MeasurablePow ℝ ℝ

Tactic:
⟨Complex.measurable_re.comp <|
      (Complex.measurable_ofReal.comp measurable_fst).pow
        (Complex.measurable_ofReal.comp measurable_snd)⟩

Premises used: Measurable.comp, Complex.measurable_re, MeasurablePow.mk, measurable_snd, Complex.measurable_ofReal, Measurable.pow, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ MeasurablePow ℝ≥0 ℝ

Tactic:
⟨(measurable_fst.coe_nnreal_real.pow measurable_snd).subtype_mk⟩

Premises used: Measurable.subtype_mk, MeasurablePow.mk, Measurable.coe_nnreal_real, measurable_snd, Measurable.pow, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ MeasurablePow ℝ≥0∞ ℝ

Tactic:
⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩

Premises used: MeasurablePow.mk, ENNReal.measurable_of_measurable_nnreal_prod
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
refine_1 : Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ≥0∞), p.2).1 ^ ((↑p.1 : ℝ≥0∞), p.2).2
refine_2 : Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ HPow.hPow (α := ℝ≥0∞) (∞, x).1 (∞, x).2
⊢ MeasurablePow ℝ≥0∞ ℝ

Tactic:
refine ⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ) ↦ if p.1 = 0 ∧ p.2 < 0 then ∞ else (↑(p.1 ^ p.2) : ℝ≥0∞)

Tactic:
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