awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
s : Finset α
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)
empty :
  ∀ (h : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → HasIntegral I l (f i) vol (g i)),
    HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ ∅, f i x) vol (∑ i ∈ ∅, g i)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ihs :
      ∀ (h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)),
        HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i))
    (h : ∀ i ∈ Insert.insert a s, HasIntegral I l (f i) vol (g i)),
    HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ Insert.insert a s, f i x) vol (∑ i ∈ Insert.insert a s, g i)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)

Tactic:
induction s using Finset.induction_on with
  | empty => simp [hasIntegral_zero]
  | insert a s ha ihs =>
    simp only [Finset.sum_insert ha]; rw [Finset.forall_mem_insert] at h
    exact h.1.add (ihs h.2)

Premises used: BoxIntegral.hasIntegral_zero, Finset.forall_mem_insert, Insert.insert
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
s : Finset α
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)
empty :
  ∀ (h : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → HasIntegral I l (f i) vol (g i)),
    HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ ∅, f i x) vol (∑ i ∈ ∅, g i)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ihs :
      ∀ (h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)),
        HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i))
    (h : ∀ i ∈ Insert.insert a s, HasIntegral I l (f i) vol (g i)),
    HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ Insert.insert a s, f i x) vol (∑ i ∈ Insert.insert a s, g i)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp [hasIntegral_zero]
  | insert a s ha ihs =>
    simp only [Finset.sum_insert ha]; rw [Finset.forall_mem_insert] at h
    exact h.1.add (ihs h.2)

Premises used: BoxIntegral.hasIntegral_zero, Finset.forall_mem_insert, Insert.insert
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
hf : HasIntegral I l f vol y
c : ℝ
⊢ HasIntegral I l (c • f) vol (c • y)

Tactic:
simpa only [HasIntegral, ← integralSum_smul] using
    (tendsto_const_nhds : Tendsto _ _ (𝓝 c)).smul hf

Premises used: tendsto_const_nhds, BoxIntegral.integralSum_smul, Filter.Tendsto.smul, BoxIntegral.HasIntegral
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : Integrable I l f vol
c : ℝ
⊢ Integrable I l (c • f) vol

Tactic:
(hf.hasIntegral.smul c).integrable

Premises used: BoxIntegral.HasIntegral.smul, BoxIntegral.HasIntegral.integrable, BoxIntegral.Integrable.hasIntegral
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hf : Integrable I l (c • f) vol
hc : c ≠ 0
⊢ Integrable I l f vol

Tactic:
simpa [inv_smul_smul₀ hc] using hf.smul c⁻¹

Premises used: inv_smul_smul₀, Inv.inv, BoxIntegral.Integrable.smul
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
inl : integral I l (fun (x : ι → ℝ) ↦ HSMul.hSMul (α := ℝ) 0 (f x)) vol = HSMul.hSMul (α := ℝ) 0 (integral I l f vol)
inr : ∀ (hc : c ≠ 0), integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
⊢ integral I l (fun (x : ι → ℝ) ↦ HSMul.hSMul (α := ℝ) 0 (f x)) vol = HSMul.hSMul (α := ℝ) 0 (integral I l f vol)

Tactic:
simp only [zero_smul, integral_zero]

Premises used: BoxIntegral.integral_zero, zero_smul
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
pos : ∀ (hf : Integrable I l f vol), integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
neg : ∀ (hf : ¬Integrable I l f vol), integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol

Tactic:
by_cases hf : Integrable I l f vol

Premises used: BoxIntegral.Integrable
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : Integrable I l f vol
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol

Tactic:
(hf.hasIntegral.smul c).integral_eq

Premises used: BoxIntegral.HasIntegral.smul, BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.integral_eq
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : Integrable I l f vol
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol

Tactic:
exact (hf.hasIntegral.smul c).integral_eq

Premises used: BoxIntegral.HasIntegral.smul, BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.integral_eq
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
⊢ ¬Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol

Tactic:
have : ¬Integrable I l (fun x => c • f x) vol := mt (fun h => h.of_smul hc) hf
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
inst_4 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
this : ¬Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol
neg :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    c • integral I l f vol
neg₁ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c (if h : Integrable I l f vol then Exists.choose (p := HasIntegral I l f vol) h else 0)
neg₂ :
  (if h : Integrable I l (fun (x : ι → ℝ) ↦ c • f x) vol then
      Exists.choose (p := HasIntegral I l (fun (x : ι → ℝ) ↦ c • f x) vol) h
    else 0) =
    HSMul.hSMul (β := F) c 0
neg₃ : 0 = HSMul.hSMul (β := F) c 0
neg₄ neg₅ : Eq.{w + 1} (α := F) 0 0
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol

Tactic:
rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]

Premises used: smul_zero, dif_neg, BoxIntegral.integral
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
pos : ∀ (hgi : Integrable I l g μ.toBoxAdditive.toSMul), 0 ≤ integral I l g μ.toBoxAdditive.toSMul
neg : ∀ (hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul), 0 ≤ integral I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul

Premises used: BoxIntegral.Integrable, BoxIntegral.BoxAdditiveMap.toSMul, MeasureTheory.Measure.toBoxAdditive
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_

Premises used: BoxIntegral.Integrable.hasIntegral, Finset.sum_nonneg, ge_of_tendsto'
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
pos :
  ∀ (π : TaggedPrepartition I),
    ∀ J ∈ π.boxes,
      LE.le (α := ℝ) (0 : ℝ)
        (((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
            (g (π.tag J)) :
          ℝ)
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_

Premises used: BoxIntegral.Integrable.hasIntegral, Finset.sum_nonneg, ge_of_tendsto'
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
        (g (π.tag J)) :
      ℝ)

Tactic:
mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)

Premises used: mul_nonneg, BoxIntegral.TaggedPrepartition.tag_mem_Icc, ENNReal.toReal_nonneg
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
        (g (π.tag J)) :
      ℝ)

Tactic:
exact mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)

Premises used: mul_nonneg, BoxIntegral.TaggedPrepartition.tag_mem_Icc, ENNReal.toReal_nonneg
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
I : Box ι
inst : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → 0 ≤ g x
μ : Measure (ι → ℝ)
inst_1 : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul
neg :
  LE.le (α := ℝ) 0
    (if h : Integrable I l g μ.toBoxAdditive.toSMul then Exists.choose (p := HasIntegral I l g μ.toBoxAdditive.toSMul) h
    else 0)
neg₁ neg₂ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
rw [integral, dif_neg hgi]

Premises used: dif_neg, BoxIntegral.integral
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
pos :
  ∀ (hfi : Integrable I l f μ.toBoxAdditive.toSMul),
    ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
neg :
  ∀ (hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul),
    ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
by_cases hfi : Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
le_of_tendsto_of_tendsto' hfi.hasIntegral.norm hg.hasIntegral fun π => ?_

Premises used: Filter.Tendsto.norm, BoxIntegral.Integrable.hasIntegral, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
pos : ∀ (π : TaggedPrepartition I), ‖integralSum f μ.toBoxAdditive.toSMul π‖ ≤ integralSum g μ.toBoxAdditive.toSMul π
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
refine le_of_tendsto_of_tendsto' hfi.hasIntegral.norm hg.hasIntegral fun π => ?_

Premises used: Filter.Tendsto.norm, BoxIntegral.Integrable.hasIntegral, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
⊢ ‖integralSum f μ.toBoxAdditive.toSMul π‖ ≤ integralSum g μ.toBoxAdditive.toSMul π

Tactic:
norm_sum_le_of_le _ fun J _ => ?_

Premises used: BoxIntegral.integralSum, norm_sum_le_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
pos :
  ∀ J ∈ π.boxes,
    norm (E := E)
        ((((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (f (π.tag J)) : E) ≤
      ((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
        (g (π.tag J))
⊢ ‖integralSum f μ.toBoxAdditive.toSMul π‖ ≤ integralSum g μ.toBoxAdditive.toSMul π

Tactic:
refine norm_sum_le_of_le _ fun J _ => ?_

Premises used: norm_sum_le_of_le
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
pos : μ.real (↑J : Set (ι → ℝ)) * ‖f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * g (π.tag J)
⊢ norm (E := E) ((((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (f (π.tag J)) : E) ≤
    ((((μ.toBoxAdditive.toSMul : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
      (g (π.tag J))

Tactic:
simp only [BoxAdditiveMap.toSMul_apply, norm_smul, smul_eq_mul, Real.norm_eq_abs,
      μ.toBoxAdditive_apply, abs_of_nonneg measureReal_nonneg]

Premises used: norm_smul, MeasureTheory.measureReal_nonneg, BoxIntegral.BoxAdditiveMap.toSMul_apply, MeasureTheory.Measure.toBoxAdditive_apply, abs_of_nonneg, smul_eq_mul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
pos : ‖f (π.tag J)‖ ≤ g (π.tag J)
⊢ μ.real (↑J : Set (ι → ℝ)) * ‖f (π.tag J)‖ ≤ μ.real (↑J : Set (ι → ℝ)) * g (π.tag J)

Tactic:
gcongr
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
⊢ ‖f (π.tag J)‖ ≤ g (π.tag J)

Tactic:
hle _ <| π.tag_mem_Icc _

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : Integrable I l f μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
h : J ∈ π.boxes
⊢ ‖f (π.tag J)‖ ≤ g (π.tag J)

Tactic:
exact hle _ <| π.tag_mem_Icc _

Premises used: BoxIntegral.TaggedPrepartition.tag_mem_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul
neg : 0 ≤ integral I l g μ.toBoxAdditive.toSMul
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
rw [integral, dif_neg hfi, norm_zero]

Premises used: norm_zero, dif_neg, BoxIntegral.integral
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
integral_nonneg (fun x hx => (norm_nonneg _).trans (hle x hx)) μ

Premises used: BoxIntegral.integral_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
g : (ι → ℝ) → ℝ
hle :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ g x
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
hg : Integrable I l g μ.toBoxAdditive.toSMul
hfi : ¬Integrable I l f μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
exact integral_nonneg (fun x hx => (norm_nonneg _).trans (hle x hx)) μ

Premises used: BoxIntegral.integral_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
I : Box ι
inst_2 : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
c : ℝ
hc :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ c
μ : Measure (ι → ℝ)
inst_3 : IsLocallyFiniteMeasure μ
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ μ.real (↑I : Set (ι → ℝ)) * c

Tactic:
simpa only [integral_const] using norm_integral_le_of_norm_le hc μ (integrable_const c)

Premises used: BoxIntegral.integrable_const, BoxIntegral.integral_const, BoxIntegral.norm_integral_le_of_norm_le