awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
egauge : ‖c‖ₑ * ‖f x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ _root_.egauge 𝕜 (ball 0 ((↑r : ℝ) / ((↑C : ℝ) * (↑‖c‖₊ : ℝ)))) (g x)
have egauge₁ : ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞) = ‖g x‖ₑ / (↑(r / (C * ‖c‖₊)) : ℝ≥0∞)
Tactic: calc
      egauge 𝕜 (ball 0 r) (f x) ≤ ‖c‖ₑ * ‖f x‖ₑ / r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ ≤ ‖c‖ₑ * (C * ‖g x‖ₑ) / r := by
        gcongr
        simp only [enorm_eq_nnnorm, ← coe_nnnorm] at hx ⊢
        exact mod_cast hx
      _ = ‖g x‖ₑ / (r / (C * ‖c‖₊) : ℝ≥0) := by
        simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]
        ac_rfl
      _ ≤ _ := div_le_egauge_ball _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n
have ofNat : ∀ (a : ℕ),
  IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.ofNat a) fun (x : α) ↦ g x ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
ofNat :
  ∀ (a : ℕ),
    IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.ofNat a) fun (x : α) ↦ g x ^ Int.ofNat a
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n
have negSucc : ∀ (a : ℕ),
  IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.negSucc a) fun (x : α) ↦ g x ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ f =Θ[l] g
have refine : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 c⁻¹)
Tactic: refine ⟨isBigO_of_div_tendsto_nhds_of_ne_zero h hc,
    isBigO_of_div_tendsto_nhds_of_ne_zero ?_ (inv_ne_zero hc)⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 c⁻¹)
have h₁ : Eq (α := α → 𝕜) (fun (x : α) ↦ f x / g x) fun (x : α) ↦ (g x / f x)⁻¹
Tactic: convert! h.inv₀ hc using 1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ Eq (α := α → 𝕜) (fun (x : α) ↦ f x / g x) fun (x : α) ↦ (g x / f x)⁻¹
have h₁ : ∀ (x : α), f x / g x = (g x / f x)⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g →
    ∀ᶠ (x : α) in l,
      IsTheta.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x_1 : β) ↦ f (x, x_1)) fun (x_1 : β) ↦ g (x, x_1)
have simp : f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
  (∀ᶠ (x : α) in l,
      IsBigO.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x_1 : β) ↦ f (x, x_1)) fun (x_1 : β) ↦ g (x, x_1)) ∧
    ∀ᶠ (x : α) in l, IsBigO.{u_2, u_4, u_3} (E := F) (F := E) l' (fun (x_1 : β) ↦ g (x, x_1)) fun (x_1 : β) ↦ f (x, x_1)
Tactic: simp only [IsTheta, eventually_and]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Theta (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g →
    ∀ᶠ (y : β) in l', IsTheta.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x : α) ↦ f (x, y)) fun (x : α) ↦ g (x, y)
have simp : f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
  (∀ᶠ (x : β) in l',
      IsBigO.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x_1 : α) ↦ f (x_1, x)) fun (x_1 : α) ↦ g (x_1, x)) ∧
    ∀ᶠ (x : β) in l', IsBigO.{u_1, u_4, u_3} (E := F) (F := E) l (fun (x_1 : α) ↦ g (x_1, x)) fun (x_1 : α) ↦ f (x_1, x)
Tactic: simp only [IsTheta, eventually_and]
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
have obtain : ∀ (p q : ℝ → ℝ) (hp : MonotoneOn p s) (hq : MonotoneOn q s) (h : LocallyBoundedVariationOn (p - q) s),
  ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x
Tactic: obtain ⟨p, q, hp, hq, rfl⟩ : ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q :=
    h.exists_monotoneOn_sub_monotoneOn
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x
have h₁ : ∀ (x : ℝ) (hxp : x ∈ s → DifferentiableWithinAt ℝ p s x) (hxq : x ∈ s → DifferentiableWithinAt ℝ q s x) (xs : x ∈ s),
  DifferentiableWithinAt ℝ (p - q) s x
Tactic: filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem] with
    x hxp hxq xs
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
have A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
Tactic: have A : ∀ i : ι, LipschitzWith 1 fun x : ι → ℝ => x i := fun i => LipschitzWith.eval i
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x
have h₁ : LocallyBoundedVariationOn (E := ℝ) (fun (x : ℝ) ↦ f x i) s
Tactic: apply ae_differentiableWithinAt_of_mem_real
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
have this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x
Tactic: have : ∀ i : ι, ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (fun x : ℝ => f x i) s x := fun i ↦ by
    apply ae_differentiableWithinAt_of_mem_real
    exact LipschitzWith.comp_locallyBoundedVariationOn (A i) h
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
have h₁ : ∀ (x : ℝ) (hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x) (xs : x ∈ s),
  DifferentiableWithinAt ℝ f s x
Tactic: filter_upwards [ae_all_iff.2 this] with x hx xs
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
H :
  ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
have h₁ : ∀ (x : ℝ)
  (hx :
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x)
  (xs : x ∈ s), DifferentiableWithinAt ℝ f s x
Tactic: filter_upwards [H] with x hx xs
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
have suffices : ∀ᵐ (x : ℝ),
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
      ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
Tactic: suffices H : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x by
    filter_upwards [H] with x hx xs
    exact (ContinuousLinearEquiv.comp_differentiableWithinAt_iff _).mp (hx xs)
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
⊢ ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
have h₁ : LocallyBoundedVariationOn (E := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
  ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s
Tactic: apply ae_differentiableWithinAt_of_mem_pi
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → DifferentiableAt ℝ f x
have h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
Tactic: have h₁ : ∀ᵐ x, x ≠ min a b := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → DifferentiableAt ℝ f x
have h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
Tactic: have h₂ : ∀ᵐ x, x ≠ max a b := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → DifferentiableAt ℝ f x
have h₃ : ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x) (hx₂ : x ≠ min a b) (hx₃ : x ≠ max a b)
  (hx₄ : x ∈ uIcc a b), DifferentiableAt ℝ f x
Tactic: filter_upwards [h.locallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, h₁, h₂]
    with x hx₁ hx₂ hx₃ hx₄
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x
hx₂ : x ≠ min a b
hx₃ : x ≠ max a b
hx₄ : x ∈ uIcc a b
⊢ DifferentiableAt ℝ f x
have hx₅ : min a b ≤ x ∧ x ≤ max a b
Tactic: rw [uIcc, mem_Icc] at hx₄
Cleared hypotheses: hx₄
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume s, DifferentiableWithinAt ℝ f s x
have rw : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
Tactic: rw [ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
have h₁ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) univ x → DifferentiableWithinAt ℝ f univ x), DifferentiableAt ℝ f x
Tactic: filter_upwards [h.ae_differentiableWithinAt_of_mem] with x hx
-- Lean 4 proof step from Mathlib.Analysis.BoundedVariation (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x → DifferentiableWithinAt ℝ f univ x
⊢ DifferentiableAt ℝ f x
have hx₁ : Membership.mem (γ := Set ℝ) univ x → DifferentiableAt ℝ f x
Tactic: rw [differentiableWithinAt_univ] at hx
Cleared hypotheses: hx
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J)
have refine : ∀ (J : Box ι) (hJ : J ∈ π.boxes) (J' : Box ι) (hJ' : J' ∈ (πi J).boxes),
  Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionTagged πi).tag J')) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
Tactic: refine (π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionTagged πi).tag J')) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
have rw : Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
  ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
Tactic: rw [π.tag_biUnionTagged hJ hJ']
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
⊢ integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π
have refine : ∀ (J : Box ι) (hJ : J ∈ π.boxes),
  Eq.{w + 1} (α := F)
    (∑ J' ∈ (πi J).boxes,
        (((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionPrepartition πi).tag J')) :
      F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
Tactic: refine (π.sum_biUnion_boxes _ _).trans (sum_congr rfl fun J hJ => ?_)
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag (π.biUnionIndex πi J'))) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
have rw : Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
  ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
Tactic: rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ integralSum f vol π₁ - integralSum f vol π₂ =
    ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      HSub.hSub (α := F) (β := F)
        ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) :
          F)
        ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
            (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) :
          F)
have rw : HSub.hSub (α := F)
    (∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes,
      (((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
        (f ((π₁.infPrepartition π₂.toPrepartition).tag J)))
    (∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes,
      (((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F)
        (f ((π₂.infPrepartition π₁.toPrepartition).tag J))) =
  HSub.hSub (α := F)
    (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F)
        (f ((π₁.infPrepartition π₂.toPrepartition).tag x)))
    (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      (((vol : (a : Box ι) → E →L[ℝ] F) x : E →L[ℝ] F) : (a : E) → F)
        (f ((π₂.infPrepartition π₁.toPrepartition).tag x)))
Tactic: rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁,
    integralSum, integralSum, Finset.sum_sub_distrib]
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂
have refine_1 : ∀ (J : Box ι) (hJ : J ∈ π₁.boxes),
  Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
Tactic: refine (Prepartition.sum_disj_union_boxes h _).trans
      (congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
refine_1 :
  ∀ (J : Box ι) (hJ : J ∈ π₁.boxes),
    Eq.{w + 1} (α := F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
⊢ integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂
have refine_2 : ∀ (J : Box ι) (hJ : J ∈ π₂.boxes),
  Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
Tactic: refine (Prepartition.sum_disj_union_boxes h _).trans
      (congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
have refine_1 : Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
  ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₁.tag J)) : F)
Tactic: rw [disjUnion_tag_of_mem_left _ hJ]
-- 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f ((π₁.disjUnion π₂ h).tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
have refine_2 : Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
  ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π₂.tag J)) : F)
Tactic: rw [disjUnion_tag_of_mem_right _ hJ]
-- 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 * ε
⊢ HasIntegral I l f vol y
have refine : ∀ (ε : ℝ) (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 ≤ ε
Tactic: refine hasIntegral_iff.2 fun ε hε => ?_