awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
have rcases : ∀ (ε' : ℝ) (hε' : 0 < ε') (ha : a * ε' < ε),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
Tactic: rcases exists_pos_mul_lt hε a with ⟨ε', hε', ha⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
ε' : ℝ
hε' : 0 < ε'
ha : a * ε' < ε
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
have rcases : ∀ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) (hr : ∀ (c : ℝ≥0), l.RCond (r c))
  (H :
    ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
      l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε'),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
Tactic: rcases h ε' hε' with ⟨r, hr, H⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ Integrable I l f vol ↔
    ∀ ε > 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 π₂) ≤ ε
have rw : (∀ (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: rw [integrable_iff_cauchy, cauchy_map_iff',
    (l.hasBasis_toFilteriUnion_top _).prod_self.tendsto_iff uniformity_basis_dist_le]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ (∀ (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 π₂) ≤ ε
have 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 π₂) ≤ ε
Tactic: refine forall₂_congr fun ε _ => exists_congr fun r => ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)) ∧
      ∀
        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 π₂) ≤ ε
have 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 π₂) ≤ ε
Tactic: simp only [Prod.forall, exists_imp, prodMk_mem_set_prod_eq, and_imp, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 (integral I l f vol)
have rw : HasIntegral I l f vol (Exists.choose (p := HasIntegral I l f vol) h)
Tactic: rw [integral, dif_pos h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ integral I l (-f) vol = -integral I l f vol
have 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
Tactic: rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ integral I l (-f) vol = -integral I l f vol
have 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)
Tactic: rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ integral I l (-f) vol = -integral I l f vol
have 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)
Tactic: rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ integral I l (-f) vol = -integral I l f vol
have rw₃ : Eq.{w + 1} (α := F) 0 (-0)
Tactic: rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ integral I l (-f) vol = -integral I l f vol
have rw₄ : Eq.{w + 1} (α := F) 0 0
Tactic: rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 (fun (x : ι → ℝ) ↦ ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a s, g i)
have insert : HasIntegral I l (fun (x : ι → ℝ) ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)
Tactic: simp only [Finset.sum_insert ha]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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 (fun (x : ι → ℝ) ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
have 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)
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)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
have 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 a s, HasIntegral I l (f i) vol (g i)),
  HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a 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)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
have 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)
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)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
have 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 a s, HasIntegral I l (f i) vol (g i)),
  HasIntegral I l (fun (x : ι → ℝ) ↦ ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a 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)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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 : ℝ
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have inl : integral I l (fun (x : ι → ℝ) ↦ HSMul.hSMul (α := ℝ) 0 (f x)) vol = HSMul.hSMul (α := ℝ) 0 (integral I l f vol)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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)
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have inr : ∀ (hc : c ≠ 0), 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)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have pos : ∀ (hf : Integrable 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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have neg : ∀ (hf : ¬Integrable 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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
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
have this : ¬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
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have 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
Tactic: rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
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
⊢ integral I l (fun (x : ι → ℝ) ↦ c • f x) vol = c • integral I l f vol
have 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)
Tactic: rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]