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
f : α → E
hf : f ≤ᶠ[ae μ] 0
rw : LE.le.{u_2} (α := E) 0 (∫ (a : α), -f a ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x ∂μ) 0

Tactic:
rw [← neg_nonneg, ← integral_neg]

Premises used: MeasureTheory.integral_neg, neg_nonneg
-- 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
f : α → E
hf : f ≤ᶠ[ae μ] 0
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : α), -f a ∂μ)

Tactic:
integral_nonneg_of_ae ?_

Premises used: MeasureTheory.integral_nonneg_of_ae
-- 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
f : α → E
hf : f ≤ᶠ[ae μ] 0
refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ -f a
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : α), -f a ∂μ)

Tactic:
refine integral_nonneg_of_ae ?_

Premises used: MeasureTheory.integral_nonneg_of_ae
-- 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
f : α → E
hf : f ≤ᶠ[ae μ] 0
h : ∀ (x : α) (hx : f x ≤ 0 x), 0 x ≤ -f x
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ -f a

Tactic:
filter_upwards [hf] 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
f : α → E
hf : f ≤ᶠ[ae μ] 0
x : α
hx : f x ≤ 0 x
⊢ 0 x ≤ -f x

Tactic:
simpa
-- 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
f : α → E
hf : f ≤ 0
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x ∂μ) 0

Tactic:
integral_nonpos_of_ae (ae_of_all _ hf)

Premises used: MeasureTheory.integral_nonpos_of_ae, MeasureTheory.ae_of_all
-- 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
rw : LE.le.{u_2} (α := E) 0 (∫ (a : α), g a - f a ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), g x ∂μ)

Tactic:
rw [← sub_nonneg, ← integral_sub hg hf]

Premises used: MeasureTheory.integral_sub, sub_nonneg
-- 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : α), g a - f a ∂μ)

Tactic:
integral_nonneg_of_ae ?_

Premises used: MeasureTheory.integral_nonneg_of_ae
-- 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ g a - f a
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : α), g a - f a ∂μ)

Tactic:
refine integral_nonneg_of_ae ?_

Premises used: MeasureTheory.integral_nonneg_of_ae
-- 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
h₁ : ∀ (x : α) (hx : f x ≤ g x), 0 x ≤ g x - f x
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ g a - f a

Tactic:
filter_upwards [h] 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
x : α
hx : f x ≤ g x
⊢ 0 x ≤ g x - f x

Tactic:
simpa
-- 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
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ g
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), g x ∂μ)

Tactic:
integral_mono_ae hf hg (ae_of_all _ h)

Premises used: MeasureTheory.integral_mono_ae, MeasureTheory.ae_of_all
-- 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
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
pos : ∀ (hfi : Integrable f μ), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
neg : ∀ (hfi : ¬Integrable f μ), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- 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
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfi : Integrable f μ
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
integral_mono_ae hfi hgi h

Premises used: MeasureTheory.integral_mono_ae
-- 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
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfi : Integrable f μ
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
exact integral_mono_ae hfi hgi h

Premises used: MeasureTheory.integral_mono_ae
-- 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
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfi : ¬Integrable f μ
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
integral_undef hfi ▸ integral_nonneg_of_ae (hf.trans h)

Premises used: MeasureTheory.integral_undef, Eq.rec, MeasureTheory.integral_nonneg_of_ae, Eq.symm, Filter.EventuallyLE.trans
-- 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
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfi : ¬Integrable f μ
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
exact integral_undef hfi ▸ integral_nonneg_of_ae (hf.trans h)
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ LE.le.{u_2} (α := E) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)

Tactic:
integral_mono_ae (hf_int a ha) (hf_int b hb) ?_

Premises used: MeasureTheory.integral_mono_ae
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x a) fun (x : α) ↦ f x b
⊢ LE.le.{u_2} (α := E) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)

Tactic:
refine integral_mono_ae (hf_int a ha) (hf_int b hb) ?_

Premises used: MeasureTheory.integral_mono_ae
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
h : ∀ (x : α) (hx : MonotoneOn (f x) s), f x a ≤ f x b
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x a) fun (x : α) ↦ f x b

Tactic:
filter_upwards [hf_mono] 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 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
x : α
hx : MonotoneOn (f x) s
⊢ f x a ≤ f x b

Tactic:
hx ha hb hab
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
x : α
hx : MonotoneOn (f x) s
⊢ f x a ≤ f x b

Tactic:
exact hx ha hb hab
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ LE.le.{u_2} (α := E) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a)

Tactic:
integral_mono_ae (hf_int b hb) (hf_int a ha) ?_

Premises used: MeasureTheory.integral_mono_ae
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x b) fun (x : α) ↦ f x a
⊢ LE.le.{u_2} (α := E) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a)

Tactic:
refine integral_mono_ae (hf_int b hb) (hf_int a ha) ?_

Premises used: MeasureTheory.integral_mono_ae
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
h : ∀ (x : α) (hx : AntitoneOn (f x) s), f x b ≤ f x a
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x b) fun (x : α) ↦ f x a

Tactic:
filter_upwards [hf_anti] 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 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
x : α
hx : AntitoneOn (f x) s
⊢ f x b ≤ f x a

Tactic:
hx ha hb hab
-- 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 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
x : α
hx : AntitoneOn (f x) s
⊢ f x b ≤ f x a

Tactic:
exact hx ha hb hab
-- 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) μ
⊢ ConvexOn.{0, u_6, u_2} ℝ (β := E) s fun (b : β) ↦ ∫ (x : α), f x b ∂μ

Tactic:
⟨hs, ?_⟩

Premises used: And.intro, ConvexOn
-- 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) μ
refine :
  ∀ ⦃x : β⦄,
    x ∈ s →
      ∀ ⦃y : β⦄,
        y ∈ s →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) (a • x + b • y) ≤
                    HSMul.hSMul (β := E) a ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) x) +
                      HSMul.hSMul (β := E) b ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) y)
⊢ ConvexOn.{0, u_6, u_2} ℝ (β := E) s fun (b : β) ↦ ∫ (x : α), f x b ∂μ

Tactic:
refine ⟨hs, ?_⟩
-- 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
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)

Tactic:
integral_mono_ae ?lhs ?rhs ?ae_le

Premises used: MeasureTheory.integral_mono_ae
-- 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
refine : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ
refine₁ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ p • f x a + q • f x b) μ
refine₂ :
  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
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)

Tactic:
refine integral_mono_ae ?lhs ?rhs ?ae_le

Premises used: MeasureTheory.integral_mono_ae
-- 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 : α) ↦ f x (p • a + q • b)) μ

Tactic:
hf_int _ ?_
-- 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
refine : p • a + q • b ∈ s
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ

Tactic:
refine hf_int _ ?_
-- 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
rw :
  ∀ (hs : ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ 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), p • a + q • b ∈ s
⊢ p • a + q • b ∈ s

Tactic:
rw [convex_iff_add_mem] at hs

Premises used: convex_iff_add_mem
-- 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 : ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ 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
⊢ p • a + q • b ∈ s

Tactic:
hs 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 : ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ 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
⊢ p • a + q • b ∈ s

Tactic:
exact hs 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
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ

Tactic:
case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq

Premises used: convex_iff_add_mem