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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ∞)
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ∞)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ∀ (i : α), ‖↑f i‖ ≤ C

Tactic:
exact norm_apply_le_of_tendsto hCF hf

Goal state after:
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 : E
⊢ x ∈ t → ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
hx

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 : E
hx : x ∈ t
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t
Module: Mathlib.Analysis.Normed.Lp.lpSpace

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

Tactic:
hx

Goal state after:
case mp
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
i : ι
x : α
hx : x ∈ s
⊢ ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
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 : α
⊢ x ∈ s → ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y

Tactic:
hx

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 ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
apply integral_mono hfg hfg'
  simp only [lsmul_apply, smul_eq_mul]
  intro t
  dsimp
  gcongr
  exacts [hf _, hg _]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case inr.h_bound
𝕜 : 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✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
t x : G
⊢ x ∈ ball x₀ 1 → ‖(L' (f t)) (fderiv 𝕜 g (x - t))‖ ≤ ?m.596 t

Tactic:
hx

Goal state after:
case inr.h_bound
𝕜 : 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✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
t x : G
hx : x ∈ ball x₀ 1
⊢ ‖(L' (f t)) (fderiv 𝕜 g (x - t))‖ ≤ ?m.596 t
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : 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✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∃ p ∈ s, ∃ x, g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun p x ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (s' ×ˢ univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : (p, x).2 - y ∈ k
⊢ y ∈ k'

Tactic:
exact ⟨y - x, by simpa using hy, x, hx, by simp⟩

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : 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✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
x : P
⊢ x ∈ s → (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ

Tactic:
hx

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : 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✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
p : P
x : G
hp : p ∈ s
⊢ x ∉ k → g' (p, x) = 0

Tactic:
hx

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
p : P
x : G
hp : p ∈ s
hx : x ∉ k
⊢ g' (p, x) = 0
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
⊢ HasDerivAt g (g' x) x

Tactic:
by
  -- The first part of the proof rewrites `hf` and the goal to be functions so that Lean
  -- can recognize them when we apply `hasFDerivAt_of_tendstoUniformlyOnFilter`
  let F' n z := (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)
  let G' z := (1 : 𝕜 →L[𝕜] 𝕜).smulRight (g' z)
  simp_rw [hasDerivAt_iff_hasFDerivAt] at hf ⊢
  have hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x) :=
    (ContinuousLinearMap.smulRightL 𝕜 𝕜 G 1).uniformContinuous.comp_tendstoUniformlyOnFilter hf'
  exact hasFDerivAt_of_tendstoUniformlyOnFilter hf' hf hfg

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist

Goal state before:
pp: case hf
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun y ↦ toEuclidean (f y)

pp: case hg
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ ↑n fun y ↦ toEuclidean (g y)

pp: case hne
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n) f
hg : ContDiff ℝ (↑n) g
h : ∀ (x : F), f x ≠ g x
⊢ ∀ (x : F), toEuclidean (f x) ≠ toEuclidean (g x)

Tactic:
exacts [(toEuclidean (E := G)).contDiff.comp hf,
    (toEuclidean (E := G)).contDiff.comp hg, fun x => toEuclidean.injective.ne (h x)]

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

Goal state before:
pp: case hnhds
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
⊢ x ∈ k → ∃ t ∈ 𝓝[k] x, μ t = 0

Tactic:
hx

Goal state after:
case hnhds
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, μ t = 0
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 : α
⊢ x ∈ μ.everywherePosSubset s → ∀ n ∈ 𝓝[μ.everywherePosSubset s] x, 0 < μ n

Tactic:
hx

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 ∈ 𝓝[μ.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 : α
⊢ x ∈ μ.everywherePosSubset s → ∀ n ∈ 𝓝[μ.everywherePosSubset s] x, 0 < μ n

Tactic:
hx

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 ∈ 𝓝[μ.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 : α
⊢ x ∈ s → ∀ n ∈ 𝓝[s] x, 0 < ν n

Tactic:
hx

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 ∈ 𝓝[s] x, 0 < ν n
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure[inst✝²] UV.1 ⊆ UV.2}
this✝² : Encodable ↑s
this✝¹ : TopologicalSpace ↑s := ⊥
this✝ : DiscreteTopology ↑s
hd : ∀ (UV : ↑s), Disjoint (closure[inst✝²] (↑UV).1) (↑UV).2ᶜ
ε : ↑s → ℝ
ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1
hε : Tendsto ε cofinite (𝓝 0)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : {UV | δ ≤ ε UV}.Finite
this : ∀ᶠ (y : X) in 𝓝 x, ∀ (UV : ↑s), δ ≤ ε UV → dist ((F y) UV) ((F x) UV) ≤ δ
⊢ F ⁻¹' closedBall (F x) δ ∈ 𝓝 x

Tactic:
refine this.mono fun y hy => (BoundedContinuousFunction.dist_le δ0.le).2 fun UV => ?_

Goal state after:
case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure[inst✝²] UV.1 ⊆ UV.2}
this✝² : Encodable ↑s
this✝¹ : TopologicalSpace ↑s := ⊥
this✝ : DiscreteTopology ↑s
hd : ∀ (UV : ↑s), Disjoint (closure[inst✝²] (↑UV).1) (↑UV).2ᶜ
ε : ↑s → ℝ
ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1
hε : Tendsto ε cofinite (𝓝 0)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : {UV | δ ≤ ε UV}.Finite
this : ∀ᶠ (y : X) in 𝓝 x, ∀ (UV : ↑s), δ ≤ ε UV → dist ((F y) UV) ((F x) UV) ≤ δ
y : X
hy : ∀ (UV : ↑s), δ ≤ ε UV → dist ((F y) UV) ((F x) UV) ≤ δ
UV : ↑s
⊢ dist ((F y) UV) ((F x) UV) ≤ δ
Module: Mathlib.MeasureTheory.Measure.EverywherePos

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

Tactic:
hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝 x
h't : ∀ u ⊆ t, ν u = μ u
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Tactic:
exact ⟨t, ht, fun u hu ↦ (h't u hu).symm⟩

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

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
⊢ x ∈ ⋂ n, V n * k → x ∈ k

Tactic:
hx

Goal state after:
G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : x ∈ ⋂ n, V n * k
⊢ x ∈ k
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case hfs
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : LocallyCompactSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : G → E
hg : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
⊢ x ∉ k' → g (x⁻¹ * p) = 0

Tactic:
hx

Goal state after:
case hfs
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : LocallyCompactSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : G → E
hg : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : x ∉ k'
⊢ g (x⁻¹ * p) = 0
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
x : E
⊢ x ∈ s → x ∈ ⋃ f, support ↑f

Tactic:
hx

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
x : E
hx : x ∈ s
⊢ x ∈ ⋃ f, support ↑f
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos.e_f.inr.inr
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : x ≤ t
⊢ 0 = (L ((Ioi 0).indicator f t)) 0

Tactic:
map_zero

Goal state after:
case pos.e_f.inr.inr
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : x ≤ t
⊢ 0 = 0