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

Goal state before:
pp: case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ (∑' (i_1 : α), ‖↑(lp.single (↑p) i x) i_1‖ ^ (↑p).toReal) ^ (1 / (↑p).toReal) = ‖x‖

Tactic:
tsum_eq_single i,

Goal state after:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ (‖↑(lp.single (↑p) i x) i‖ ^ (↑p).toReal) ^ (1 / (↑p).toReal) = ‖x‖

case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ⇑((Homeomorph.smulOfNeZero r ⋯).trans (IsometryEquiv.vaddConst c).toHomeomorph) '' ball 0 1 = ball c r

Tactic:
change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (⇑(IsometryEquiv.vaddConst c) ∘ fun x ↦ r • x) '' ball 0 1 = ball c r
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
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜

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
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x 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 𝕜
⊢ UniformCauchySeqOn f l (Metric.ball x r)
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr.left
ι : 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' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
⊢ (∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < q) →
    ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x_1 - f n.2 x_1 - (f n.1 x - f n.2 x)) < ε

Tactic:
hn

Goal state after:
case inr.left
ι : 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' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
hn : ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < q
⊢ ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x_1 - f n.2 x_1 - (f n.1 x - f n.2 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 : ι
⊢ (fun n ↦ f n x ∈ t) n →
    ∀ {y : ι}, (fun n ↦ f n x ∈ t) y → ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f (n, y).1 x - f (n, y).2 x) < ε

Tactic:
hn

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
⊢ ∀ {y : ι}, (fun n ↦ f n x ∈ t) y → ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f (n, y).1 x - f (n, y).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 : 1 < R
⊢ ContDiffWithinAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (Set.Ioi 1 ×ˢ Set.univ) (R, x)

Tactic:
apply ContDiffAt.contDiffWithinAt

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
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
⊢ (fderiv ℝ (fun t ↦ ⟪f t, g t⟫) x) y = ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫

Tactic:
rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]

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⟫
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffWithinAt ℝ (↑n) (↑univUnitBall.symm) (ball 0 1) y

Tactic:
apply ContDiffAt.contDiffWithinAt

Goal state after:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ (↑n) (↑univUnitBall.symm) y
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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
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))
⊢ HasFDerivAt g (g' x) x

Tactic:
let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜

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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
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))
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ HasFDerivAt g (g' x) x
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case refine_1
ι : 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
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))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
ε : ℝ
hε : ε > 0
n : ι × E
⊢ dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε →
    dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x - (f n.1 n.2 - f n.1 x))) 0 < ε

Tactic:
hn

Goal state after:
case refine_1
ι : 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
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))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
ε : ℝ
hε : ε > 0
n : ι × E
hn : dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
⊢ dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x - (f n.1 n.2 - f n.1 x))) 0 < ε
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 : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
⊢ Integrable F' μ ∧ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ ∧ x ∈ s :=
    eventually_nhds_iff_ball.mp (hF_meas.and hs)
  choose hδ_meas hδε using hδ
  replace h_lip : ∀ᵐ a : α ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖ :=
    h_lip.mono fun a lip x hx ↦ lip.norm_sub_le (hδε x hx) (mem_of_mem_nhds hs)
  replace bound_integrable := bound_integrable.norm
  apply hasFDerivAt_integral_of_dominated_loc_of_lip' (ball_mem_nhds x₀ δ_pos) <;> assumption

Goal state after:
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 → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : H
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ ↑(Real.nnabs (bound a))

Tactic:
Real.coe_nnabs

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 → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : H
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound 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
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ ↑(Real.nnabs (bound a))

Tactic:
Real.coe_nnabs

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
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound a|
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := (Homeomorph.smul (Units.mk0 R hR)).toMeasurableEquiv
⊢ |(R ^ finrank ℝ E)⁻¹| • ∫ (y : E) in ⇑e.symm ⁻¹' s, f y ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E) in R • s, f x ∂μ

Tactic:
by
    congr 3
    ext y
    rw [mem_smul_set_iff_inv_smul_mem₀ hR]
    rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst✝¹] w
xw : x ∈ w
A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Tactic:
have B : w ∈ 𝓝 x := w_open.mem_nhds xw

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst✝¹] w
xw : x ∈ w
A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
B : w ∈ 𝓝 x
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
⊢ n ∈ 𝓝[μ.everywherePosSubset s] x → 0 < μ n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
⊢ 0 < μ n
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
⊢ n ∈ 𝓝[μ.everywherePosSubset s] x → 0 < μ n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
⊢ 0 < μ n
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
⊢ n ∈ 𝓝[s] x → 0 < ν n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < ν n
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen[inst✝²] s
x : α
xs : x ∈ s
n : Set α
⊢ n ∈ 𝓝[s] x → 0 < μ n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : μ.IsOpenPosMeasure
hs : IsOpen[inst✝²] s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < μ n
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ∃ u, ContDiff ℝ ∞ u ∧ (∀ (x : E), u x ∈ Icc 0 1) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x

Tactic:
refine ⟨fun x => (f x + f (-x)) / 2, ?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ContDiff ℝ ∞ fun x ↦ (f x + f (-x)) / 2

case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ∀ (x : E), (fun x ↦ (f x + f (-x)) / 2) x ∈ Icc 0 1

case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ (support fun x ↦ (f x + f (-x)) / 2) = ball 0 1

case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ∀ (x : E), (fun x ↦ (f x + f (-x)) / 2) (-x) = (fun x ↦ (f x + f (-x)) / 2) x