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
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst_5 : CompleteSpace F
refine :
  ∀ (ε : ℝ),
    0 < ε →
      ∀ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        ((∀ (c : ℝ≥0), l.RCond (r c)) ∧
            ∀
              x ∈
                SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
                  {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π ∧ π.IsPartition}
                  {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π ∧ π.IsPartition},
              Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε}
                (integralSum f vol x.1, integralSum f vol x.2)) ↔
          (∀ (c : ℝ≥0), l.RCond (r c)) ∧
            ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
              l.MemBaseSet I c₁ (r c₁) π₁ →
                π₁.IsPartition →
                  l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε
⊢ (∀ (ib : ℝ),
      0 < ib →
        ∃ (ia : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
          (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
            ∀
              x ∈
                SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
                  {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition}
                  {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (ia c) π ∧ π.IsPartition},
              Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ib}
                (integralSum f vol x.1, integralSum f vol x.2)) ↔
    ∀ ε > 0,
      ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
refine forall₂_congr fun ε _ => exists_congr fun r => ?_

Premises used: exists_congr, forall₂_congr
-- 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
inst_5 : CompleteSpace F
ε : ℝ
h : 0 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
simp :
  ((∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (a b : TaggedPrepartition I) (x : ℝ≥0),
        l.MemBaseSet I x (r x) a →
          a.IsPartition →
            ∀ (x : ℝ≥0),
              l.MemBaseSet I x (r x) b → b.IsPartition → dist (integralSum f vol a) (integralSum f vol b) ≤ ε) ↔
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε
⊢ ((∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀
        x ∈
          SProd.sprod (α := Set (TaggedPrepartition I)) (β := Set (TaggedPrepartition I))
            {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π ∧ π.IsPartition}
            {π : TaggedPrepartition I | ∃ (c : ℝ≥0), l.MemBaseSet I c (r c) π ∧ π.IsPartition},
        Membership.mem (γ := Set (F × F)) {p : F × F | dist p.1 p.2 ≤ ε}
          (integralSum f vol x.1, integralSum f vol x.2)) ↔
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
simp only [Prod.forall, exists_imp, prodMk_mem_set_prod_eq, and_imp, mem_setOf_eq]

Premises used: and_imp, Set.prodMk_mem_set_prod_eq, Set.mem_setOf_eq, Prod.forall, exists_imp
-- 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
inst_5 : CompleteSpace F
ε : ℝ
h : 0 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ ((∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (a b : TaggedPrepartition I) (x : ℝ≥0),
        l.MemBaseSet I x (r x) a →
          a.IsPartition →
            ∀ (x : ℝ≥0),
              l.MemBaseSet I x (r x) b → b.IsPartition → dist (integralSum f vol a) (integralSum f vol b) ≤ ε) ↔
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
and_congr Iff.rfl
      ⟨fun H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂ => H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂,
        fun H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂ => H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂⟩

Premises used: Iff.rfl, Iff.intro, and_congr
-- 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
inst_5 : CompleteSpace F
ε : ℝ
h : 0 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
⊢ ((∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (a b : TaggedPrepartition I) (x : ℝ≥0),
        l.MemBaseSet I x (r x) a →
          a.IsPartition →
            ∀ (x : ℝ≥0),
              l.MemBaseSet I x (r x) b → b.IsPartition → dist (integralSum f vol a) (integralSum f vol b) ≤ ε) ↔
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε

Tactic:
exact
    and_congr Iff.rfl
      ⟨fun H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂ => H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂,
        fun H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂ => H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂⟩

Premises used: Iff.rfl, Iff.intro, and_congr
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
l₁ l₂ : IntegrationParams
h : HasIntegral I l₁ f vol y
hl : l₂ ≤ l₁
⊢ HasIntegral I l₂ f vol y

Tactic:
h.mono_left <| IntegrationParams.toFilteriUnion_mono _ hl _

Premises used: Filter.Tendsto.mono_left, BoxIntegral.IntegrationParams.toFilteriUnion_mono, 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
h : Integrable I l f vol
rw : HasIntegral I l f vol (Exists.choose (p := HasIntegral I l f vol) h)
⊢ HasIntegral I l f vol (integral I l f vol)

Tactic:
rw [integral, dif_pos h]

Premises used: dif_pos, BoxIntegral.integral
-- 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
h : Integrable I l f vol
⊢ HasIntegral I l f vol (Exists.choose (p := HasIntegral I l f vol) h)

Tactic:
Classical.choose_spec h

Premises used: Classical.choose_spec
-- 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
h : Integrable I l f vol
⊢ HasIntegral I l f vol (Exists.choose (p := HasIntegral I l f vol) h)

Tactic:
exact Classical.choose_spec h

Premises used: Classical.choose_spec
-- 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
l' : IntegrationParams
h : Integrable I l f vol
hle : l' ≤ l
⊢ Integrable I l' f vol

Tactic:
⟨_, h.hasIntegral.mono hle⟩

Premises used: BoxIntegral.Integrable, BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.mono, Exists.intro
-- 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 y' : F
h : HasIntegral I l f vol y
h' : HasIntegral I l f vol y'
⊢ y = y'

Tactic:
tendsto_nhds_unique h h'

Premises used: tendsto_nhds_unique
-- 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
h : HasIntegral I l f vol y
⊢ Integrable I l f vol

Tactic:
⟨_, h⟩

Premises used: BoxIntegral.Integrable, Exists.intro
-- 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
h : HasIntegral I l f vol y
⊢ integral I l f vol = y

Tactic:
h.integrable.hasIntegral.unique h

Premises used: BoxIntegral.HasIntegral.integrable, BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.unique
-- 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 g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
h : HasIntegral I l f vol y
h' : HasIntegral I l g vol y'
⊢ HasIntegral I l (f + g) vol (y + y')

Tactic:
simpa only [HasIntegral, ← integralSum_add] using h.add h'

Premises used: BoxIntegral.integralSum_add, BoxIntegral.HasIntegral.add, 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 g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : Integrable I l f vol
hg : Integrable I l g vol
⊢ Integrable I l (f + g) vol

Tactic:
(hf.hasIntegral.add hg.hasIntegral).integrable

Premises used: BoxIntegral.HasIntegral.integrable, BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.add
-- 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 g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : Integrable I l f vol
hg : Integrable I l g vol
⊢ integral I l (f + g) vol = integral I l f vol + integral I l g vol

Tactic:
(hf.hasIntegral.add hg.hasIntegral).integral_eq

Premises used: BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.add, 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
y : F
hf : HasIntegral I l f vol y
⊢ HasIntegral I l (-f) vol (-y)

Tactic:
simpa only [HasIntegral, ← integralSum_neg] using hf.neg

Premises used: BoxIntegral.integralSum_neg, BoxIntegral.HasIntegral.neg, 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
⊢ Integrable I l (-f) vol

Tactic:
hf.hasIntegral.neg.integrable

Premises used: BoxIntegral.HasIntegral.integrable, BoxIntegral.Integrable.hasIntegral, BoxIntegral.HasIntegral.neg
-- 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
⊢ Integrable I l f vol

Tactic:
neg_neg f ▸ hf.neg

Premises used: BoxIntegral.Integrable.neg, Eq.rec, neg_neg
-- 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
⊢ Integrable I l (-f) vol ↔ Integrable I l f vol

Tactic:
⟨fun h => h.of_neg, fun h => h.neg⟩

Premises used: BoxIntegral.Integrable.of_neg, BoxIntegral.Integrable.neg, Iff.intro
-- 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
h : ¬Integrable I l f vol
rw : (if h : Integrable I l (-f) vol then Exists.choose (p := HasIntegral I l (-f) vol) h else 0) = -integral I l f vol
rw₁ :
  Eq.{w + 1} (α := F) (if h : Integrable I l (-f) vol then Exists.choose (p := HasIntegral I l (-f) vol) h else 0)
    (-if h : Integrable I l f vol then Exists.choose (p := HasIntegral I l f vol) h else 0)
rw₂ :
  Eq.{w + 1} (α := F) (if h : Integrable I l (-f) vol then Exists.choose (p := HasIntegral I l (-f) vol) h else 0) (-0)
rw₃ : Eq.{w + 1} (α := F) 0 (-0)
rw₄ rw₅ : Eq.{w + 1} (α := F) 0 0
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

Premises used: BoxIntegral.Integrable.of_neg, mt, dif_neg, neg_zero, BoxIntegral.integral
-- 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 (-f) vol = -integral I l f vol

Tactic:
exact if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
  else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

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
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
classical
  exact if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
  else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

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 g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
h : HasIntegral I l f vol y
h' : HasIntegral I l g vol y'
⊢ HasIntegral I l (f - g) vol (y - y')

Tactic:
simpa only [sub_eq_add_neg] using h.add h'.neg

Premises used: sub_eq_add_neg, BoxIntegral.HasIntegral.neg, BoxIntegral.HasIntegral.add
-- 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 g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : Integrable I l f vol
hg : Integrable I l g vol
⊢ Integrable I l (f - g) vol

Tactic:
(hf.hasIntegral.sub hg.hasIntegral).integrable

Premises used: BoxIntegral.HasIntegral.sub, 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 g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : Integrable I l f vol
hg : Integrable I l g vol
⊢ integral I l (f - g) vol = integral I l f vol - integral I l g vol

Tactic:
(hf.hasIntegral.sub hg.hasIntegral).integral_eq

Premises used: BoxIntegral.HasIntegral.sub, 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : E
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ c) vol ((((vol : (a : Box ι) → E →L[ℝ] F) I : E →L[ℝ] F) : (a : E) → F) c)

Tactic:
tendsto_const_nhds.congr' <| (l.eventually_isPartition I).mono fun _π hπ => Eq.symm <|
    (vol.map ⟨⟨fun g : E →L[ℝ] F ↦ g c, rfl⟩, fun _ _ ↦ rfl⟩).sum_partition_boxes le_top hπ

Premises used: BoxIntegral.BoxAdditiveMap.map, tendsto_const_nhds, BoxIntegral.IntegrationParams.eventually_isPartition, AddMonoidHom.mk, ZeroHom.mk, Filter.Eventually.mono, BoxIntegral.BoxAdditiveMap.sum_partition_boxes, le_top, Filter.Tendsto.congr', Eq.symm, DFunLike.coe, rfl, 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : E
⊢ integral I l (fun (x : ι → ℝ) ↦ c) vol = (((vol : (a : Box ι) → E →L[ℝ] F) I : E →L[ℝ] F) : (a : E) → F) c

Tactic:
(hasIntegral_const c).integral_eq

Premises used: BoxIntegral.hasIntegral_const, 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : E
⊢ Integrable I l (fun (x : ι → ℝ) ↦ c) vol

Tactic:
⟨_, hasIntegral_const c⟩

Premises used: BoxIntegral.Integrable, BoxIntegral.hasIntegral_const, Exists.intro
-- 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
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ 0) vol 0

Tactic:
simpa only [← (vol I).map_zero] using hasIntegral_const (0 : E)

Premises used: ContinuousLinearMap.map_zero, BoxIntegral.hasIntegral_const, OfNat.ofNat, DFunLike.coe
-- 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
⊢ Integrable I l (fun (x : ι → ℝ) ↦ 0) vol

Tactic:
⟨0, hasIntegral_zero⟩

Premises used: BoxIntegral.Integrable, BoxIntegral.hasIntegral_zero, Exists.intro, OfNat.ofNat
-- 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
⊢ integral I l (fun (x : ι → ℝ) ↦ 0) vol = 0

Tactic:
hasIntegral_zero.integral_eq

Premises used: BoxIntegral.hasIntegral_zero, 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
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)

Tactic:
simp [hasIntegral_zero]

Premises used: BoxIntegral.hasIntegral_zero
-- 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
f : α → (ι → ℝ) → E
g : α → F
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)
insert : HasIntegral I l (fun (x : ι → ℝ) ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ Insert.insert a s, f i x) vol (∑ i ∈ Insert.insert a s, g i)

Tactic:
simp only [Finset.sum_insert ha]

Premises used: Finset.sum_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
f : α → (ι → ℝ) → E
g : α → F
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 a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)

Tactic:
rw [Finset.forall_mem_insert] at h

Premises used: Finset.forall_mem_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
f : α → (ι → ℝ) → E
g : α → F
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 : HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)

Tactic:
h.1.add (ihs h.2)

Premises used: And.right, And.left, BoxIntegral.HasIntegral.add
-- 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
f : α → (ι → ℝ) → E
g : α → F
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 : HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)

Tactic:
exact h.1.add (ihs h.2)

Premises used: And.right, And.left, BoxIntegral.HasIntegral.add