mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: case neg.inr
α : 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₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : ¬CompleteSpace E
hH : Nontrivial H
this : ¬CompleteSpace (H →L[𝕜] E)
⊢ HasFDerivAt (fun x ↦ 0) 0 x₀

Tactic:
exact hasFDerivAt_const 0 x₀

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
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 𝕜
⊢ (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)

Tactic:
ext

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 𝕜
x✝ : ι × E
⊢ (↑‖x✝.2 - x‖)⁻¹ • (g x✝.2 - g x - (g' x) (x✝.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))
      x✝
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✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
⊢ y • f ⋆[L, μ] g = y • (f ⋆[L, μ] g)

Tactic:
ext

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✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
x✝ : G
⊢ (y • f ⋆[L, μ] g) x✝ = (y • (f ⋆[L, μ] g)) x✝
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✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
⊢ f ⋆[L, μ] y • g = y • (f ⋆[L, μ] g)

Tactic:
ext

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✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
x✝ : G
⊢ (f ⋆[L, μ] y • g) x✝ = (y • (f ⋆[L, μ] g)) x✝
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
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✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
⊢ 0 ⋆[L, μ] g = 0

Tactic:
ext

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
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✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x✝ : G
⊢ (0 ⋆[L, μ] g) x✝ = 0 x✝
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
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
⊢ f ⋆[L, μ] 0 = 0

Tactic:
ext

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
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
x✝ : G
⊢ (f ⋆[L, μ] 0) x✝ = 0 x✝
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case neg
𝕜 : 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₀
⊢ ContinuousWithinAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)

Tactic:
let k' : Set G := (-k) +ᵥ t

Goal state after:
case neg
𝕜 : 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
⊢ ContinuousWithinAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
Module: Mathlib.Analysis.Calculus.ContDiff.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✝¹¹ : 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
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt (f ⋆[L, μ] g) ((fderiv 𝕜 f ⋆[precompL G L, μ] g) x₀) x₀

Tactic:
by
  simp +singlePass only [← convolution_flip]
  exact hcf.hasFDerivAt_convolution_right L.flip hg hf x₀

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
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
by
  let : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
  rcases Metric.mem_nhds_iff.1 hs with ⟨ε, ε_pos, hε⟩
  have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
  have diff_x₀ : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (F' x₀ a) x₀ :=
    h_diff.mono fun a ha ↦ ha x₀ (hε x₀_in)
  have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (F · a) (ball x₀ ε) := by
    apply (h_diff.and h_bound).mono
    rintro a ⟨ha_deriv, ha_bound⟩
    refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasFDerivWithinAt) fun x x_in ↦ ?_
    rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
    exact (ha_bound x (hε x_in)).trans (le_abs_self _)
  apply (hasFDerivAt_integral_of_dominated_loc_of_lip (ball_mem_nhds x₀ ε_pos)
    hF_meas hF_int hF'_meas this bound_integrable diff_x₀).2

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
⊢ closedBall x r = dist x ⁻¹' closedBall 0 r

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ closedBall x r ↔ x✝ ∈ dist x ⁻¹' closedBall 0 r
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: 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 → ℝ
ε0 : ∀ (i : ↑s), 0 < ε i
c : ℝ
hεc : HasSum ε c
hc1 : c ≤ 1
UV : ↑s
⊢ ε UV ≤ 1

Tactic:
exact (le_hasSum hεc UV fun _ _ => (ε0 _).le).trans hc1

Goal state after:
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: case refine_2
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
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst✝²] U ⊆ V
⊢ ∃ i, 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V

Tactic:
set UV : ↥s := ⟨(U, V), ⟨hUB, hVB⟩, hUV⟩

Goal state after:
case refine_2
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
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst✝²] U ⊆ V
UV : ↑s := ⟨(U, V), ⋯⟩
⊢ ∃ i, 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: case refine_1
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
K_comp : IsCompact K
K_closed : IsClosed[inst✝⁷] K
r : ℝ≥0∞
hr : r < μ K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst✝⁷] L
⊢ (fun s ↦ ∃ f, Continuous[inst✝⁷, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L

Tactic:
have : μ.IsEverywherePos L :=
      isEverywherePos_everywherePosSubset_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.ne

Goal state after:
case refine_1
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
K_comp : IsCompact K
K_closed : IsClosed[inst✝⁷] K
r : ℝ≥0∞
hr : r < μ K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst✝⁷] L
this : μ.IsEverywherePos L
⊢ (fun s ↦ ∃ f, Continuous[inst✝⁷, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r (last N)

Tactic:
exact le_mul_of_one_le_left (a.rpos _).le h

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
k : ℕ
hk : k < N
⊢ ∃ j < i,
    (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
      k = p.color j

Tactic:
rw [← Inf_eq_N] at hk

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
k : ℕ
hk : k < sInf (univ \ A)
⊢ ∃ j < i,
    (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
      k = p.color j
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: 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
⊢ 0 ≤ (f x + f (-x)) / 2 ∧ (f x + f (-x)) / 2 ≤ 1

Tactic:
constructor

Goal state after:
case refine_2.left
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
⊢ 0 ≤ (f x + f (-x)) / 2

case refine_2.right
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
⊢ (f x + f (-x)) / 2 ≤ 1
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_2.right
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
⊢ (f x + f (-x)) / 2 ≤ 1

Tactic:
· linarith [(B x).2, (B (-x)).2]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ y ∈ ball 0 D ∧ ‖x - y‖ ≤ 1

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := ⋯
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ y ∈ ball 0 D

case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := ⋯
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ ‖x - y‖ ≤ 1
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
⊢ p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
    p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))

Tactic:
constructor

Goal state after:
case left
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ := ⋯
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := ⋯
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
⊢ p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b)))

case right
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ := ⋯
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := ⋯
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
⊢ p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
⊢ ball 0 ((R + 1) / 2 * (1 + (R - 1) / (R + 1))) = ball 0 R

Tactic:
refine congr (congr_arg ball (Eq.refl 0)) ?_

Goal state after:
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
⊢ (R + 1) / 2 * (1 + (R - 1) / (R + 1)) = R