awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
funProp : a ∈ s
funProp₁ : b ∈ s
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ p • f x a + q • f x b) μ

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ p • f x a + q • f x b) μ

Tactic:
case rhs => fun_prop (disch := aesop)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
h : ∀ (x : α) (hx : ConvexOn ℝ s (f x)), f x (p • a + q • b) ≤ p • f x a + q • f x b
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x (p • a + q • b)) fun (x : α) ↦ p • f x a + q • f x b

Tactic:
filter_upwards [hf_conv] with x hx
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : α
hx : ConvexOn ℝ s (f x)
⊢ f x (p • a + q • b) ≤ p • f x a + q • f x b

Tactic:
hx.2 ha hb hp hq hpq

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : α
hx : ConvexOn ℝ s (f x)
⊢ f x (p • a + q • b) ≤ p • f x a + q • f x b

Tactic:
exact hx.2 ha hb hp hq hpq

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ConvexOn ℝ s (f x)) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  LE.le.{u_2} (α := E) ((fun (x : α) ↦ f x (p • a + q • b)) x)
                    ((fun (x : α) ↦ p • f x a + q • f x b) x))
                x}
            x}
      a_1
h₁ h₂ : ∀ (x : α) (hx : ConvexOn ℝ s (f x)), f x (p • a + q • b) ≤ p • f x a + q • f x b
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x (p • a + q • b)) fun (x : α) ↦ p • f x a + q • f x b

Tactic:
case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
hf : Integrable.{u_2, u_1} (ε := E) (fun (a_1 : α) ↦ p • f a_1 a) μ
hg : Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ q • f a b) μ
⊢ ∫ (x : α), p • f x a + q • f x b ∂μ = HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ)

Tactic:
apply integral_add

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
funProp : a ∈ s
⊢ Integrable.{u_2, u_1} (ε := E) (fun (a_1 : α) ↦ p • f a_1 a) μ

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
funProp : b ∈ s
⊢ Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ q • f a b) μ

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ) =
    HSMul.hSMul (β := E) p (∫ (x : α), f x a ∂μ) + HSMul.hSMul (β := E) q (∫ (x : α), f x b ∂μ)

Tactic:
simp [integral_smul]

Premises used: MeasureTheory.integral_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
calc : LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
calc₁ : ∫ (x : α), p • f x a + q • f x b ∂μ = HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ)
calc₂ :
  HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ) =
    HSMul.hSMul (β := E) p (∫ (x : α), f x a ∂μ) + HSMul.hSMul (β := E) q (∫ (x : α), f x b ∂μ)
⊢ (fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) (p • a + q • b) ≤
    HSMul.hSMul (β := E) p ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) +
      HSMul.hSMul (β := E) q ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)

Tactic:
calc ∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ := by
                  refine integral_mono_ae ?lhs ?rhs ?ae_le
                  case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq
                  case rhs => fun_prop (disch := aesop)
                  case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
            _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)
            _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conc : ∀ᵐ (x : α) ∂μ, ConcaveOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
simp_rw :
  ∀ (hf_conc : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (-f x)),
    ConvexOn.{0, u_6, u_2} ℝ (β := E) s (-fun (b : β) ↦ ∫ (x : α), f x b ∂μ)
⊢ ConcaveOn.{0, u_6, u_2} ℝ (β := E) s fun (b : β) ↦ ∫ (x : α), f x b ∂μ

Tactic:
simp_rw [← neg_convexOn_iff] at hf_conc ⊢

Premises used: neg_convexOn_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
hf_conc : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (-f x)
⊢ ConvexOn.{0, u_6, u_2} ℝ (β := E) s (-fun (b : β) ↦ ∫ (x : α), f x b ∂μ)

Tactic:
simpa only [Pi.neg_apply, integral_neg] using
    integral_convexOn_of_integrand_ae hs hf_conc (hf_int · · |>.neg)

Premises used: MeasureTheory.integral_convexOn_of_integrand_ae, MeasureTheory.Integrable.neg, MeasureTheory.integral_neg, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
simp_rw : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ)

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun x => (f x).coe_nonneg)
      hfi.aestronglyMeasurable, ← ENNReal.coe_nnreal_eq]

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, ENNReal.coe_nnreal_eq, NNReal.coe_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
rw : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal

Tactic:
rw [ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞

Tactic:
simpa [← lt_top_iff_ne_top, hasFiniteIntegral_iff_enorm, NNReal.enorm_eq] using
    hfi.hasFiniteIntegral

Premises used: NNReal.enorm_eq, lt_top_iff_ne_top, MeasureTheory.hasFiniteIntegral_iff_enorm, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ f =ᶠ[ae μ] fun (x : α) ↦ ‖f x‖

Tactic:
have : f =ᵐ[μ] (‖f ·‖) := f_nn.mono fun _x hx ↦ (abs_of_nonneg hx).symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun (x : α) ↦ ‖f x‖
simp_rw : ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
simp_rw [integral_congr_ae this, ofReal_integral_norm_eq_lintegral_enorm hfi,
    ← ofReal_norm]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm, ofReal_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun (x : α) ↦ ‖f x‖
⊢ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)

Premises used: ENNReal.ofReal, MeasureTheory.lintegral_congr_ae, Filter.EventuallyEq.fun_comp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun (x : α) ↦ ‖f x‖
⊢ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
exact lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)

Premises used: ENNReal.ofReal, MeasureTheory.lintegral_congr_ae, Filter.EventuallyEq.fun_comp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
rw : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (f x).toReal
⊢ ∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ hfm.ennreal_toReal.aestronglyMeasurable,
    lintegral_congr_ae (ofReal_toReal_ae_eq hf)]

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.lintegral_congr_ae, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, AEMeasurable.ennreal_toReal, MeasureTheory.ofReal_toReal_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (f x).toReal

Tactic:
Eventually.of_forall fun x => ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, Filter.Eventually.of_forall, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (f x).toReal

Tactic:
exact Eventually.of_forall fun x => ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
b : ℝ≥0
rw : ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
rw₁ : (↑(Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ)) : ℝ≥0∞) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
rw₂ : Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ b ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
rw₃ rw₄ : ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)

Tactic:
rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
    Real.toNNReal_le_iff_le_coe]

Premises used: ENNReal.ofReal, ENNReal.coe_le_coe, Real.toNNReal_le_iff_le_coe, MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
pos : ∀ (hf : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ), ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
neg : ∀ (hf : ¬Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ), ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)

Tactic:
by_cases hf : Integrable (fun a => (f a : ℝ)) μ

Premises used: MeasureTheory.Integrable, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
hf : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)

Tactic:
(lintegral_coe_le_coe_iff_integral_le hf).1 h

Premises used: Iff.mp, MeasureTheory.lintegral_coe_le_coe_iff_integral_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
hf : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)

Tactic:
exact (lintegral_coe_le_coe_iff_integral_le hf).1 h

Premises used: Iff.mp, MeasureTheory.lintegral_coe_le_coe_iff_integral_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
hf : ¬Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ
neg : 0 ≤ (↑b : ℝ)
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)

Tactic:
rw [integral_undef hf]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
hf : ¬Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ
⊢ 0 ≤ (↑b : ℝ)

Tactic:
b.2

Premises used: NNReal.toReal, Subtype.property
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
hf : ¬Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ
⊢ 0 ≤ (↑b : ℝ)

Tactic:
exact b.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ f =ᶠ[ae μ] 0

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ENNReal.toReal_eq_zero_iff,
    ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, not_true_eq_false, or_false]

Premises used: not_true_eq_false, MeasureTheory.hasFiniteIntegral_iff_ofReal, And.right, And.left, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, ENNReal.not_lt_top, or_false, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
rw : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) 0 ↔ f =ᶠ[ae μ] 0
rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [lintegral_eq_zero_iff']

Premises used: MeasureTheory.lintegral_eq_zero_iff'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
rw : (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x) = 0 x) ↔ ∀ᵐ (x : α) ∂μ, f x ≤ 0 x
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [← hf.ge_iff_eq', Filter.EventuallyEq, Filter.EventuallyLE]

Premises used: Filter.EventuallyEq, Filter.EventuallyLE, Filter.EventuallyLE.ge_iff_eq'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x) = 0 x) ↔ ∀ᵐ (x : α) ∂μ, f x ≤ 0 x

Tactic:
simp only [Pi.zero_apply, ofReal_eq_zero]

Premises used: ENNReal.ofReal_eq_zero, Pi.zero_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) μ

Tactic:
(ENNReal.measurable_ofReal.comp_aemeasurable hfi.1.aemeasurable)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ENNReal.ofNNReal, ENNReal.ofReal, WithTop.some, And.left, ENNReal.measurable_ofReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) μ

Tactic:
exact (ENNReal.measurable_ofReal.comp_aemeasurable hfi.1.aemeasurable)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, ENNReal.measurable_ofReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ f
hfi : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ f =ᶠ[ae μ] 0

Tactic:
integral_eq_zero_iff_of_nonneg_ae (Eventually.of_forall hf) hfi

Premises used: Filter.Eventually.of_forall, MeasureTheory.integral_eq_zero_iff_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ↔ f =ᶠ[ae μ] g

Tactic:
⟨fun h_le ↦ EventuallyEq.symm ?_, fun h ↦ integral_congr_ae h⟩

Premises used: MeasureTheory.integral_congr_ae, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
refine : ∀ (h_le : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)), g =ᶠ[ae μ] f
⊢ Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ↔ f =ᶠ[ae μ] g

Tactic:
refine ⟨fun h_le ↦ EventuallyEq.symm ?_, fun h ↦ integral_congr_ae h⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
rw : Eq (α := ℝ) (∫ (x : α), (g - f) x ∂μ) 0
⊢ g =ᶠ[ae μ] f

Tactic:
rw [← sub_ae_eq_zero,
    ← integral_eq_zero_iff_of_nonneg_ae ((sub_nonneg_ae _ _).mpr hfg) (hg.sub hf)]

Premises used: Iff.mpr, MeasureTheory.sub_ae_eq_zero, MeasureTheory.Integrable.sub, MeasureTheory.sub_nonneg_ae, MeasureTheory.integral_eq_zero_iff_of_nonneg_ae