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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
⊢ ∀ i ∈ Finset.range (m + 1), ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x

Tactic:
intro i hi

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
⊢ ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal

Tactic:
intro i hi

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
i : α
hi : i ∈ s
⊢ ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
⊢ ∀ i ∉ s, F i = 0

Tactic:
intro i hi

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
i : α
hi : i ∉ s
⊢ F i = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
⊢ ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal

Tactic:
intro i hi

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
i : α
hi : i ∈ s
⊢ F i = ‖↑f i‖ ^ p.toReal
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)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
rcases le_or_gt r 0 with (hr | hr)

Goal state after:
case inl
ι : 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 𝕜
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : r ≤ 0
⊢ UniformCauchySeqOn f l (Metric.ball x r)

case inr
ι : 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 𝕜
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ UniformCauchySeqOn f l (Metric.ball x r)
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: x : ℝ
x✝ : x ≤ 0 ∨ 0 < x
⊢ 0 ≤ expNegInvGlue x

Tactic:
cases le_or_gt x 0 with

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

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

Tactic:
refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ (by fun_prop) hR.ne')
      exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)

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

Goal state before:
pp: case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ ↑n ↑(IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph

Tactic:
· exact contDiff_id.add contDiff_const

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 →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
h_ball : ball x₀ ε ∈ 𝓝 x₀
this✝ :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
a : α
ha : HasFDerivAt (fun x ↦ F x a) (F' a) x₀
this : Tendsto (fun x ↦ ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀))) (𝓝 x₀) (𝓝 0)
⊢ Tendsto (fun n ↦ ‖n - x₀‖⁻¹ • (F n a - F x₀ a - (F' a) (n - x₀))) (𝓝 x₀)
    (𝓝 (‖x₀ - x₀‖⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀))))

Tactic:
simpa

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace H
inst✝¹ : SeminormedGroup H
inst✝ : OpensMeasurableSpace H
f : G →* H
hf : Measurable ⇑f
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
this : haar (interior ↑K ∩ ⋃ i, ⇑f ⁻¹' ball 1 ↑i) = 0
⊢ False

Tactic:
← preimage_iUnion,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace H
inst✝¹ : SeminormedGroup H
inst✝ : OpensMeasurableSpace H
f : G →* H
hf : Measurable ⇑f
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
this : haar (interior ↑K ∩ ⇑f ⁻¹' ⋃ i, ball 1 ↑i) = 0
⊢ False
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
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a ↦ (L (f a)) (g x.1 (x.2 - a))) μ
I2 : Integrable (fun a ↦ (L (f a)) (g q₀.1 (q₀.2 - a))) μ
⊢ AEStronglyMeasurable (fun a ↦ L (f a) ∘SL g' (q₀.1, q₀.2 - a)) μ

Tactic:
have T : HasCompactSupport fun y => g' (q₀.1, y) :=
      HasCompactSupport.intro hk fun x hx => g'_zero q₀.1 x hq₀ 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
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a ↦ (L (f a)) (g x.1 (x.2 - a))) μ
I2 : Integrable (fun a ↦ (L (f a)) (g q₀.1 (q₀.2 - a))) μ
T : HasCompactSupport fun y ↦ g' (q₀.1, y)
⊢ AEStronglyMeasurable (fun a ↦ L (f a) ∘SL g' (q₀.1, q₀.2 - a)) μ
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 }
this : ⋃ f, support ↑f = s
⊢ ∃ T, T.Countable ∧ ⋃ f ∈ T, support ↑f = s

Tactic:
← this

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 }
this : ⋃ f, support ↑f = s
⊢ ∃ T, T.Countable ∧ ⋃ f ∈ T, support ↑f = ⋃ f, support ↑f
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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
⊢ ∀ i ≤ n, R i ≤ M

Tactic:
intro i hi

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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ R i ≤ M
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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ R i ≤ M

Tactic:
refine le_trans ?_ (le_max_left _ _)

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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ R i ≤ (Finset.image R (Finset.range (n + 1))).max' ⋯
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ univ.Nonempty

Tactic:
exact ⟨⟨_, h⟩, mem_univ _⟩

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
this : sInf (univ \ A) ≠ N
⊢ sInf (univ \ A) < N

Tactic:
by
    rcases (csInf_le (OrderBot.bddBelow (univ \ A)) N_mem).lt_or_eq with (H | H)
    · exact H
    · exact (this H).elim

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
this : ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ

Tactic:
rw [integral_smul_nnreal_measure] at this

Goal state after:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
this : ∫ (x : G), f x ∂μ' = μ'.haarScalarFactor μ • ∫ (x : G), f x ∂μ
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case ind
α : 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)
⊢ False

Tactic:
let G : ℕ → Ordinal := fun n => if n = N then i else g n

Goal state after:
case ind
α : 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
⊢ False
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case h_bound
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun x ↦ 1) x

Tactic:
by_cases hx : x ∈ tsupport f

Goal state after:
case pos
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∈ tsupport f
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun x ↦ 1) x

case neg
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
n : ℕ
x : G
hx : x ∉ tsupport f
⊢ ‖v n (f x)‖ ≤ (tsupport f).indicator (fun x ↦ 1) x
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: 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

Tactic:
apply ball_subset_ball' _ hy
        simp only [hz, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right,
          Real.norm_eq_abs, abs_div]
        field_simp
        linarith only

Goal state after: