mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
h : HasProdLocallyUniformlyOn f g s
hs : IsCompact s
⊢ TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
h : HasProdLocallyUniformlyOn f g s
hs : IsCompact s
⊢ TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
H : ∀ (R : ℝ), μ (f '' (s ∩ closedBall 0 R)) = 0
⊢ μ (f '' ⋃ n, s ∩ closedBall 0 ↑n) ≤ 0

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
H : ∀ (R : ℝ), μ (f '' (s ∩ closedBall 0 R)) = 0
⊢ μ (f '' ⋃ n, s ∩ closedBall 0 ↑n) ≤ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
hs : IsOpen[inst✝¹] s
inst✝ : LocallyCompactSpace β
h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
hs : IsOpen[inst✝¹] s
inst✝ : LocallyCompactSpace β
h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : 0 = r
h : (w - z) ^ 2 = 0
⊢ 0 = r

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : 0 = r
h : (w - z) ^ 2 = 0
⊢ 0 = r
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
H : ∀ (R : ℝ), μ (f '' (s ∩ closedBall 0 R)) = 0
⊢ μ (⋃ i, f '' (s ∩ closedBall 0 ↑i)) ≤ ∑' (n : ℕ), μ (f '' (s ∩ closedBall 0 ↑n))

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
H : ∀ (R : ℝ), μ (f '' (s ∩ closedBall 0 R)) = 0
⊢ μ (⋃ i, f '' (s ∩ closedBall 0 ↑i)) ≤ ∑' (n : ℕ), μ (f '' (s ∩ closedBall 0 ↑n))
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ TendstoLocallyUniformlyOn (fun N b ↦ ∏ i ∈ Finset.range N, f i b) g atTop s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ TendstoLocallyUniformlyOn (fun N b ↦ ∏ i ∈ Finset.range N, f i b) g atTop s
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: case inr
E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε

Tactic:
]

Goal state after:
case inr
E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : CommMonoid α
f : ι → β → α
g : β → α
inst✝ : UniformSpace α
f' : ι → β → α
h : TendstoUniformly (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop
hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), ∏ i ∈ n, f i b = ∏ i ∈ n, f' i b
⊢ TendstoUniformly (fun x1 x2 ↦ ∏ i ∈ x1, f' i x2) g atTop

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : CommMonoid α
f : ι → β → α
g : β → α
inst✝ : UniformSpace α
f' : ι → β → α
h : TendstoUniformly (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop
hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), ∏ i ∈ n, f i b = ∏ i ∈ n, f' i b
⊢ TendstoUniformly (fun x1 x2 ↦ ∏ i ∈ x1, f' i x2) g atTop
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)
B : Tendsto (fun ε ↦ ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)
⊢ μ (f '' (s ∩ closedBall 0 R)) ≤ 0

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)
B : Tendsto (fun ε ↦ ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)
⊢ μ (f '' (s ∩ closedBall 0 R)) ≤ 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a = b' - a'

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a = b' - a'
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn

Goal state before:
pp: ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable fun i ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : ∏' (i : ι), f i x ≠ 0
⊢ ∑' (i : ι), logDeriv (f i) x = logDeriv (fun x ↦ ∏' (i : ι), f i x) x

Tactic:
← hm.hasSum_iff

Goal state after:
ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable fun i ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : ∏' (i : ι), f i x ≠ 0
⊢ HasSum (fun i ↦ logDeriv (f i) x) (logDeriv (fun x ↦ ∏' (i : ι), f i x) x)
Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn

Goal state before:
pp: ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable fun i ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : ∏' (i : ι), f i x ≠ 0
⊢ HasSum (fun i ↦ logDeriv (f i) x) (logDeriv (fun x ↦ ∏' (i : ι), f i x) x)

Tactic:
]

Goal state after:
ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable fun i ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : ∏' (i : ι), f i x ≠ 0
⊢ HasSum (fun i ↦ logDeriv (f i) x) (logDeriv (fun x ↦ ∏' (i : ι), f i x) x)
Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn

Goal state before:
pp: ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable fun i ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : ∏' (i : ι), f i x ≠ 0
b : Finset ι
⊢ ∑ i ∈ b, logDeriv (f i) x = ∑ b ∈ b, (fun i ↦ logDeriv (f i) x) b

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasFDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1
⊢ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasFDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1
⊢ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = s ∩ ⋃ i, t i

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = s ∩ ⋃ i, t i
Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1
⊢ IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1
⊢ IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a = a' - b'

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a = a' - b'
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K

Tactic:
]

Goal state after:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K