awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ ≤
    (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.1.nnnorm.aemeasurable.coe_nnreal_ennreal
      hg.1.nnnorm.aemeasurable.coe_nnreal_ennreal

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.nnnorm, AEMeasurable.coe_nnreal_ennreal, ENNReal.lintegral_mul_le_Lp_mul_Lq, And.left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
refine : (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ ‖f a‖ * ‖g a‖
⊢ Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h : ∀ (x : α) (hxf : 0 x ≤ f x) (hxg : 0 x ≤ g x), f x * g x = ‖f x‖ * ‖g x‖
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ ‖f a‖ * ‖g a‖

Tactic:
filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
hxf : 0 x ≤ f x
hxg : 0 x ≤ g x
h : f x * g x = f x * ‖g x‖
h₁ h₂ : f x * g x = f x * g x
⊢ f x * g x = ‖f x‖ * ‖g x‖

Tactic:
rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)

Tactic:
have h_left : ∫ a, f a * g a ∂μ = ∫ a, ‖f a‖ * ‖g a‖ ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg
    rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
refine : (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a ^ p) fun (a : α) ↦ ‖f a‖ ^ p
⊢ Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h : ∀ (x : α) (hxf : 0 x ≤ f x), f x ^ p = ‖f x‖ ^ p
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a ^ p) fun (a : α) ↦ ‖f a‖ ^ p

Tactic:
filter_upwards [hf_nonneg] with x hxf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
x : α
hxf : 0 x ≤ f x
h h₁ : f x ^ p = f x ^ p
⊢ f x ^ p = ‖f x‖ ^ p

Tactic:
rw [Real.norm_of_nonneg hxf]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)

Tactic:
have h_right_f : ∫ a, f a ^ p ∂μ = ∫ a, ‖f a‖ ^ p ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hf_nonneg] with x hxf
    rw [Real.norm_of_nonneg hxf]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
refine : (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ g a ^ q) fun (a : α) ↦ ‖g a‖ ^ q
⊢ Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
h : ∀ (x : α) (hxg : 0 x ≤ g x), g x ^ q = ‖g x‖ ^ q
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : α) ↦ g a ^ q) fun (a : α) ↦ ‖g a‖ ^ q

Tactic:
filter_upwards [hg_nonneg] with x hxg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
x : α
hxg : 0 x ≤ g x
h h₁ : g x ^ q = g x ^ q
⊢ g x ^ q = ‖g x‖ ^ q

Tactic:
rw [Real.norm_of_nonneg hxg]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)

Tactic:
have h_right_g : ∫ a, g a ^ q ∂μ = ∫ a, ‖g a‖ ^ q ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hg_nonneg] with x hxg
    rw [Real.norm_of_nonneg hxg]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
h_right_g : Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)
rw :
  ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)
⊢ ∫ (a : α), f a * g a ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (1 / q)

Tactic:
rw [h_left, h_right_f, h_right_g]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
h_right_g : Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)

Tactic:
integral_mul_norm_le_Lp_mul_Lq hpq hf hg

Premises used: MeasureTheory.integral_mul_norm_le_Lp_mul_Lq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hg_nonneg : 0 ≤ᶠ[ae μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : Eq (α := ℝ) (∫ (a : α), f a * g a ∂μ) (∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ)
h_right_f : Eq (α := ℝ) (∫ (a : α), f a ^ p ∂μ) (∫ (a : α), ‖f a‖ ^ p ∂μ)
h_right_g : Eq (α := ℝ) (∫ (a : α), g a ^ q ∂μ) (∫ (a : α), ‖g a‖ ^ q ∂μ)
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)

Tactic:
exact integral_mul_norm_le_Lp_mul_Lq hpq hf hg

Premises used: MeasureTheory.integral_mul_norm_le_Lp_mul_Lq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
hE : CompleteSpace E
μ : Measure α
f : α → E
hf : StronglyMeasurable f
a : α
⊢ ∫ (a : α) in {a}, f a ∂μ = μ.real {a} • f a

Tactic:
simp only [Measure.restrict_singleton, integral_smul_measure, integral_dirac' f a hf,
    measureReal_def]

Premises used: MeasureTheory.Measure.restrict_singleton, MeasureTheory.integral_dirac', MeasureTheory.measureReal_def, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
hE : CompleteSpace E
inst_2 : MeasurableSingletonClass α
μ : Measure α
f : α → E
a : α
⊢ ∫ (a : α) in {a}, f a ∂μ = μ.real {a} • f a

Tactic:
simp only [Measure.restrict_singleton, integral_smul_measure, integral_dirac, measureReal_def]

Premises used: MeasureTheory.Measure.restrict_singleton, MeasureTheory.integral_dirac, MeasureTheory.measureReal_def, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
e_f : ∀ (x : α), f x = f default
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f default ∂μ)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
x : α
e_f : x = default
⊢ f x = f default

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
x : α
⊢ x = default

Tactic:
Unique.uniq _ x

Premises used: Unique.uniq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
x : α
⊢ x = default

Tactic:
exact Unique.uniq _ x

Premises used: Unique.uniq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : Unique α
f : α → E
rw rw₁ : μ.real univ • f default = μ.real univ • f default
⊢ ∫ (x : α), f default ∂μ = μ.real univ • f default

Tactic:
rw [integral_const]

Premises used: MeasureTheory.integral_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : μ.IsOpenPosMeasure
f : α → ℝ
x : α
f_cont : Continuous[inst, _] f
f_int : Integrable f μ
f_nonneg : 0 ≤ f
f_x : f x ≠ 0
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ)

Tactic:
(integral_pos_iff_support_of_nonneg f_nonneg f_int).2
    (IsOpen.measure_pos μ f_cont.isOpen_support ⟨x, f_x⟩)

Premises used: Iff.mpr, IsOpen.measure_pos, Continuous.isOpen_support, MeasureTheory.integral_pos_iff_support_of_nonneg, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
β : Type u_6
γ : Type u_7
m m0 : MeasurableSpace β
hm : m ≤ m0
f : β →ₛ γ
⊢ Eq (α := (a : β) → γ) (⇑(toLargerSpace hm f) : (a : β) → γ) (⇑f : (a : β) → γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
simp_rw :
  Eq (α := F) (∫ (x : β), (SimpleFunc.toLargerSpace hm f : (a : β) → F) x ∂μ)
    (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
⊢ Eq (α := F) (∫ (x : β), (f : (a : β) → F) x ∂μ) (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)

Tactic:
simp_rw [← f.coe_toLargerSpace_eq hm]

Premises used: MeasureTheory.SimpleFunc.coe_toLargerSpace_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
rw :
  Eq (α := F)
    (∑ x ∈ (SimpleFunc.toLargerSpace hm f).range,
      μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
    (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
⊢ Eq (α := F) (∫ (x : β), (SimpleFunc.toLargerSpace hm f : (a : β) → F) x ∂μ)
    (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)

Tactic:
rw [SimpleFunc.integral_eq_sum _ hf_int]

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
⊢ Eq (α := F)
    (∑ x ∈ (SimpleFunc.toLargerSpace hm f).range,
      μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)
    (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑(SimpleFunc.toLargerSpace hm f) : (a : β) → F) {x}) • x)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
⊢ StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)

Tactic:
have hf : StronglyMeasurable[m] f := @SimpleFunc.stronglyMeasurable β F m _ f
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
⊢ Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)

Tactic:
have hf_int_m := hf_int.trim hm hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
rw :
  Eq (α := F) (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
    (∑ x ∈ f.range, (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : β), (f : (a : β) → F) x ∂μ) (∫ (x : β), (f : (a : β) → F) x ∂μ.trim hm)

Tactic:
rw [integral_simpleFunc_larger_space (le_refl m) f hf_int_m,
    integral_simpleFunc_larger_space hm f hf_int]

Premises used: le_refl, MeasureTheory.integral_simpleFunc_larger_space
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
e_f :
  ∀ (x : F),
    μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x =
      (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x
⊢ Eq (α := F) (∑ x ∈ f.range, μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)
    (∑ x ∈ f.range, (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
x : F
e_f :
  ENNReal.toReal ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x =
    ENNReal.toReal ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x
⊢ μ.real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x =
    (μ.trim hm).real (preimage (β := F) (⇑f : (a : β) → F) {x}) • x

Tactic:
simp only [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
x : F
e_f :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)
    ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x =
    ENNReal.toReal ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x})) • x

Tactic:
congr 2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
x : F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)
    ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)

Tactic:
(trim_measurableSet_eq hm (@SimpleFunc.measurableSet_fiber β F m f x)).symm

Premises used: MeasureTheory.trim_measurableSet_eq, MeasureTheory.SimpleFunc.measurableSet_fiber, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) μ
hf : StronglyMeasurable.{u_6, u_3} (α := β) (β := F) (⇑f : (a : β) → F)
hf_int_m : Integrable.{u_3, u_6} (ε := F) (⇑f : (a : β) → F) (μ.trim hm)
x : F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)
    ((μ.trim hm : (a : Set β) → ℝ≥0∞) (preimage (β := F) (⇑f : (a : β) → F) {x}) : ℝ≥0∞)

Tactic:
exact (trim_measurableSet_eq hm (@SimpleFunc.measurableSet_fiber β F m f x)).symm

Premises used: MeasureTheory.trim_measurableSet_eq, MeasureTheory.SimpleFunc.measurableSet_fiber, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
pos : ∀ (hG : CompleteSpace G), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
neg : ∀ (hG : ¬CompleteSpace G), Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : ¬CompleteSpace G
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ.trim hm)

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.integral