mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ ∀ (x : α), Tendsto (fun i ↦ id (fun i ↦ ↑((fun f ↦ F n - f) (F i))) i x) atTop (𝓝 (↑(F n - f) x))

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ ∀ (x : α), Tendsto (fun i ↦ id (fun i ↦ ↑((fun f ↦ F n - f) (F i))) i x) atTop (𝓝 (↑(F n - f) x))
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr.right
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n ↦ f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
n : ι
hn : f n x ∈ t
n' : ι
hn' : f n' x ∈ t
z : E
a✝ : z ∈ Metric.ball x r
⊢ dist (f (n, n').1 x) (f (n, n').2 x) < ε

Tactic:
]

Goal state after:
case inr.right
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n ↦ f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
n : ι
hn : f n x ∈ t
n' : ι
hn' : f n' x ∈ t
z : E
a✝ : z ∈ Metric.ball x r
⊢ dist (f (n, n').1 x) (f (n, n').2 x) < ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ ∀ x ∈ t, ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ ∀ x ∈ t, ∃ ε > 0, Metric.ball x ε ⊆ t
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case mpr
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖f x - f y‖ ≤ ↑K * dist x y

Tactic:
]

Goal state after:
case mpr
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖f x - f y‖ ≤ ↑K * dist x y
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x

Tactic:
]

Goal state after:
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist x y ≤ ε

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist x y ≤ ε
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case inr.inl
p : ℝ[X]
⊢ Tendsto (slope (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)

Tactic:
]

Goal state after:
case inr.inl
p : ℝ[X]
⊢ Tendsto (slope (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m + 1) fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
]

Goal state after:
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m + 1) fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: x : ℝ
h : 1 ≤ x
⊢ expNegInvGlue x = expNegInvGlue x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case refine_1
x✝ x : ℝ
hx : x < 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case refine_2
x✝ x : ℝ
hx : 1 < x
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter (fun n z ↦ -((↑‖z - x‖)⁻¹ • (f n.1 z - f n.1 x)) + (↑‖z - x‖)⁻¹ • (f n.2 z - f n.2 x)) 0
    (l ×ˢ l) (𝓝 x)

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter (fun n z ↦ -((↑‖z - x‖)⁻¹ • (f n.1 z - f n.1 x)) + (↑‖z - x‖)⁻¹ • (f n.2 z - f n.2 x)) 0
    (l ×ˢ l) (𝓝 x)
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x * (expNegInvGlue y + expNegInvGlue (1 - y)) ≤
    expNegInvGlue y * (expNegInvGlue x + expNegInvGlue (1 - x))

Tactic:
]

Goal state after:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x * (expNegInvGlue y + expNegInvGlue (1 - y)) ≤
    expNegInvGlue y * (expNegInvGlue x + expNegInvGlue (1 - x))
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
x : E
⊢ 0 < (R - ‖x‖) / (R - 1) ↔ ‖x‖ < R

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
x : E
⊢ 0 < (R - ‖x‖) / (R - 1) ↔ ‖x‖ < R
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
x : H
x_in : x ∈ ball x₀ ε
a : α
ha : ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ b a * ‖x - x₀‖ ≤ b a * ε

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
x : H
x_in : x ∈ ball x₀ ε
a : α
ha : ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ b a * ‖x - x₀‖ ≤ b a * ε
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
x : H
x_in : ‖x - x₀‖ < ε
a : α
ha : ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ b a * ‖x - x₀‖ ≤ b a * ε

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
x : H
x_in : ‖x - x₀‖ < ε
a : α
ha : ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ b a * ‖x - x₀‖ ≤ b a * ε
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ -t + x₀) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
⊢ Integrable (fun t ↦ (L (f t)) (g (x₀ - t))) μ

Tactic:
]

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ -t + x₀) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
⊢ Integrable (fun t ↦ (L (f t)) (g (x₀ - t))) μ
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ -t + x₀) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
⊢ IntegrableOn (fun t ↦ (L (f t)) (g (x₀ - t))) s μ

Tactic:
]

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ -t + x₀) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
⊢ IntegrableOn (fun t ↦ (L (f t)) (g (x₀ - t))) s μ
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ (fderivInnerCLM 𝕜 (f x, g x) ∘SL (fderiv ℝ f x).prod (fderiv ℝ g x)) y =
    ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ (fderivInnerCLM 𝕜 (f x, g x) ∘SL (fderiv ℝ f x).prod (fderiv ℝ g x)) y =
    ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫