awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
⊢ dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..(p, s).2, f (p, s).1 t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ) < ε
have h : ∀ (hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ),
  ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ < ε
Tactic: simp only [dist_eq_norm] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
⊢ ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ < ε
have J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
Tactic: have J r u v : IntervalIntegrable (f r) μ u v := (hf.uncurry_left _).intervalIntegrable _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ =
    ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) +
        HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖
have e_a : HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ) =
  HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) +
    HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ)‖ +
      ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ =
    norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) + norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ)
have e_a : HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) = ∫ (t : ℝ) in b₀..s, f p t ∂μ
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
e_a : HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) = ∫ (t : ℝ) in b₀..s, f p t ∂μ
⊢ ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ)‖ +
      ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ =
    norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) + norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ)
have e_a₁ : HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ) =
  ∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) = ∫ (t : ℝ) in b₀..s, f p t ∂μ
have e_a : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in b₀..s, f p x ∂μ) (∫ (t : ℝ) in b₀..s, f p t ∂μ)
Tactic: rw [integral_interval_sub_left (J _ _ _) (J _ _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ) =
    ∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ
have e_a : HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ) =
  HSub.hSub (α := E) (∫ (x : ℝ) in a₀..b₀, f p x ∂μ) (∫ (x : ℝ) in a₀..b₀, f q x ∂μ)
Tactic: rw [integral_sub (J _ _ _) (J _ _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) + norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ)
have h₁ : norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) ≤ ∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
h₁ : norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) ≤ ∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ
⊢ norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) + norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ)
have h₂ : norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ) ≤ ∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
have h₁ : (ae (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
h₁ : (ae (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a‖
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
have h₂ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a‖) (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
h₁ : (ae (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a‖
h₂ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a‖) (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
have h₃ : Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
h₁ : (ae (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a‖
h₂ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a‖) (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))
h₃ : Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ)
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
have h₄ : (ae (μ.restrict (Icc a b))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a - f q a‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
h₁ : (ae (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a‖
h₂ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a‖) (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))
h₃ : Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ)
h₄ : (ae (μ.restrict (Icc a b))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a - f q a‖
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
have h₅ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a - f q a‖) (μ.restrict (Icc a b))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
h₁ : (ae (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a‖
h₂ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a‖) (μ.restrict (Icc (b₀ - δ) (b₀ + δ)))
h₃ : Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ)
h₄ : (ae (μ.restrict (Icc a b))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f p a - f q a‖
h₅ : Integrable (ε := ℝ) (fun (a : ℝ) ↦ ‖f p a - f q a‖) (μ.restrict (Icc a b))
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
have h₆ : Ι a₀ b₀ ⊆ Icc a b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ)
have apply : b₀ ∈ Icc (b₀ - δ) (b₀ + δ)
Tactic: apply uIoc_subset_uIcc.trans (uIcc_subset_Icc ?_ ⟨hs.1.le, hs.2.le⟩ )