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
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 Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₃ : NullMeasurableSet (Icc (b₀ - δ) (b₀ + δ)) μ
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
h₃ : NullMeasurableSet (Icc (b₀ - δ) (b₀ + δ)) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₄ : ∀ (x : ℝ) (hx : x ∈ Icc (b₀ - δ) (b₀ + δ)), ‖f p x‖ ≤ M + 1
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
h₃ : NullMeasurableSet (Icc (b₀ - δ) (b₀ + δ)) μ
h₄ : ∀ (x : ℝ) (hx : x ∈ Icc (b₀ - δ) (b₀ + δ)), ‖f p x‖ ≤ M + 1
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₅ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x - f q x‖) (Icc a b) μ
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
h₃ : NullMeasurableSet (Icc (b₀ - δ) (b₀ + δ)) μ
h₄ : ∀ (x : ℝ) (hx : x ∈ Icc (b₀ - δ) (b₀ + δ)), ‖f p x‖ ≤ M + 1
h₅ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x - f q x‖) (Icc a b) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₆ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ δ) (Icc a b) μ
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
h₃ : NullMeasurableSet (Icc (b₀ - δ) (b₀ + δ)) μ
h₄ : ∀ (x : ℝ) (hx : x ∈ Icc (b₀ - δ) (b₀ + δ)), ‖f p x‖ ≤ M + 1
h₅ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x - f q x‖) (Icc a b) μ
h₆ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ δ) (Icc a b) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₇ : NullMeasurableSet (Icc a b) μ
Tactic: gcongr with x hx x hx
-- 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₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x‖) (Icc (b₀ - δ) (b₀ + δ)) μ
h₂ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ M + 1) (Icc (b₀ - δ) (b₀ + δ)) μ
h₃ : NullMeasurableSet (Icc (b₀ - δ) (b₀ + δ)) μ
h₄ : ∀ (x : ℝ) (hx : x ∈ Icc (b₀ - δ) (b₀ + δ)), ‖f p x‖ ≤ M + 1
h₅ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖f p x - f q x‖) (Icc a b) μ
h₆ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ δ) (Icc a b) μ
h₇ : NullMeasurableSet (Icc a b) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
have h₈ : ∀ (x : ℝ) (hx : x ∈ Icc a b), ‖f p x - f q x‖ ≤ δ
Tactic: gcongr with x hx x hx
-- 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ ‖f p x‖ = ‖f q x + (f p x - f q x)‖
have e_a : f p x = f q x + (f p x - f q x)
Tactic: congr
-- 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ ‖f q x‖ + ‖f p x - f q x‖ ≤ M + δ
have h₁ : ‖f q x‖ ≤ M
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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
h₁ : ‖f q x‖ ≤ M
⊢ ‖f q x‖ + ‖f p x - f q x‖ ≤ M + δ
have h₂ : ‖f p x - f q x‖ ≤ δ
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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ ‖f q x‖ ≤ M
have h₁ : Membership.mem (γ := Set ℝ) ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))
  ‖f q x‖
Tactic: apply hM
-- 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ Membership.mem (γ := Set ℝ) ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))
    ‖f q x‖
have h₁ : Membership.mem (γ := Set ℝ) ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))
  ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) (q, x))
Tactic: change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
-- 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ Membership.mem (γ := Set ℝ) ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))
    ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) (q, x))
have h₁ : (q, x) ∈ SProd.sprod (α := Set X) {q} (Icc a b)
Tactic: apply mem_image_of_mem
-- 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ (q, x) ∈ SProd.sprod (α := Set X) {q} (Icc a b)
have h₁ : x ∈ Icc a b
Tactic: simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
-- 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ M + δ ≤ M + 1
have linarith : M + 1 < M + δ → δ - 1 + (M + 1 - (M + δ)) = 0
Tactic: linarith