mathlib-initiative/mathlib-tactics huggingface dataset:
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 f' : G → E
g 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✝³ : MeasurableAdd₂ G
inst✝² : MeasurableNeg G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddRightInvariant
h1 : f =ᵐ[μ] f'
h2 : g =ᵐ[μ] g'
⊢ f ⋆[L, μ] g = f' ⋆[L, μ] g'

Tactic:
ext x
  apply integral_congr_ae
  exact (h1.prodMk <| h2.comp_tendsto
    (quasiMeasurePreserving_sub_left_of_right_invariant μ x).tendsto_ae).fun_comp ↿fun x y ↦ L x y

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
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f f' : G → E
g 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✝³ : MeasurableAdd₂ G
inst✝² : MeasurableNeg G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddRightInvariant
h1 : f =ᵐ[μ] f'
h2 : g =ᵐ[μ] g'
⊢ f ⋆[L, μ] g = f' ⋆[L, μ] g'

Tactic:
by
  ext x
  apply integral_congr_ae
  exact (h1.prodMk <| h2.comp_tendsto
    (quasiMeasurePreserving_sub_left_of_right_invariant μ x).tendsto_ae).fun_comp ↿fun x y ↦ L x y

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₀)) ∂μ‖
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a)‖ + ‖‖x - x₀‖⁻¹ • (F' a) (x - x₀)‖ =
    ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a‖ + ‖x - x₀‖⁻¹ * ‖(F' a) (x - x₀)‖

Tactic:
rw [norm_smul_of_nonneg, norm_smul_of_nonneg] <;> exact nneg _

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

Tactic:
have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x : 𝕜 ↦ F x a) (ball x₀ ε) := by
    apply (h_diff.and h_bound).mono
    rintro a ⟨ha_deriv, ha_bound⟩
    refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasDerivWithinAt) 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 _)

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₀
this : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) (ball x₀ ε)
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
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
hx : x ∉ k'
⊢ g (x⁻¹ * p) = 0

Tactic:
contrapose! 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 : g (x⁻¹ * p) ≠ 0
⊢ x ∈ k'
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Tactic:
let f : E → ℝ := c ∘ toEuclidean

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
⊢ ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
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
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
x : E
hx : x ∉ s
n : ℕ
⊢ g n x = 0

Tactic:
contrapose! 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 }
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
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
x : E
n : ℕ
hx : g n x ≠ 0
⊢ x ∈ s
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case inr
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
Hf : LocallyCompactSpace G
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ

Tactic:
simp only [haarScalarFactor, Hf, not_true_eq_false, ite_false]

Goal state after:
case inr
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
Hf : LocallyCompactSpace G
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⋯.choose • μ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case F_measurable
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 : ℕ → ℝ → ℝ := ⋯
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
⊢ ∀ (n : ℕ), AEStronglyMeasurable (fun a ↦ v n (f a)) ν

Tactic:
exact fun n ↦ (vf_cont n).aestronglyMeasurable

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 ∈ ball 0 (1 + D)
⊢ 0 < y D x

Tactic:
simp only [mem_ball_zero_iff] at hx
  refine (integral_pos_iff_support_of_nonneg (w_mul_φ_nonneg D x) ?_).2 ?_
  · have F_comp : HasCompactSupport (w D) := w_compact_support E Dpos
    have B : LocallyIntegrable (φ : E → ℝ) μ :=
      (locallyIntegrable_const _).indicator measurableSet_closedBall
    have C : Continuous (w D : E → ℝ) :=
      continuous_const.mul ((u_continuous E).comp (by fun_prop))
    exact (F_comp.convolutionExists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) C B x).integrable
  · set z := (D / (1 + D)) • x with hz
    have B : 0 < 1 + D := by linarith
    have C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support fun y : E => w D y * φ (x - y) := by
      intro y hy
      simp only [support_mul, w_support E Dpos]
      simp only [φ, mem_inter_iff, mem_support, Ne, indicator_apply_eq_zero,
        mem_closedBall_zero_iff, one_ne_zero, not_forall, not_false_iff, exists_prop, and_true]
      constructor
      · 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
      · have ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D) := by
          rw [Real.norm_of_nonpos]
          · field
          · field_simp
            linarith only
        rw [← mem_closedBall_iff_norm']
        apply closedBall_subset_closedBall' _ (ball_subset_closedBall hy)
        rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID]
        field_simp
        nlinarith only [hx, D_lt_one]
    apply lt_of_lt_of_le _ (measure_mono C)
    apply measure_ball_pos
    exact div_pos (mul_pos Dpos (by linarith only [hx])) B

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

Goal state before:
pp: case refine_2
𝕜 : 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex ↦ isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := ↑(isoE'.arrowCongr isoF).symm ∘SL L
R : eP × eG → eF := fun q ↦ (ef ⋆[eL, eμ] eg q.1) q.2
hek : IsCompact (⇑isoG ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] (⇑isoP ⁻¹' s)
⊢ LocallyIntegrable ef eμ

Tactic:
exact (locallyIntegrable_map_homeomorph isoG.symm.toHomeomorph).2 hf

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
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)
⊢ μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})

Tactic:
have I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ x, v n (f x) ∂ν) atTop
      (𝓝 (∫ x, Set.indicator ({1} : Set ℝ) (fun _ ↦ 1) (f x) ∂ν)) := by
    intro ν hν
    apply tendsto_integral_of_dominated_convergence
        (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
    · exact fun n ↦ (vf_cont n).aestronglyMeasurable
    · apply IntegrableOn.integrable_indicator _ (isClosed_tsupport f).measurableSet
      simpa using IsCompact.measure_lt_top h'f
    · refine fun n ↦ Eventually.of_forall (fun x ↦ ?_)
      by_cases hx : x ∈ tsupport f
      · simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, indicator_of_mem]
        norm_cast
        exact thickenedIndicator_le_one _ _ _
      · simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, not_false_eq_true, indicator_of_notMem]
        rw [thickenedIndicator_zero]
        · simp
        · simpa [image_eq_zero_of_notMem_tsupport hx] using (u_mem n).2.le
    · filter_upwards with x
      have T := tendsto_pi_nhds.1 (thickenedIndicator_tendsto_indicator_closure
        (fun n ↦ (u_mem n).1) u_lim ({1} : Set ℝ)) (f x)
      simp only [thickenedIndicator_apply, closure_singleton] at T
      convert! NNReal.tendsto_coe.2 T
      simp

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
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)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
⊢ μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : x ∉ closedBall 0 1
⊢ u (p⁻¹ • x) = 0

Tactic:
contrapose! hx

Goal state after:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : u (p⁻¹ • x) ≠ 0
⊢ x ∈ closedBall 0 1
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
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ 2 / (R + 1) = 1 - (R - 1) / (R + 1)

Tactic:
by field

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
d : E := (s / ‖a.c j‖) • a.c j
hd : d = (s / ‖a.c j‖) • a.c j
I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖
J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ
invs_nonneg : 0 ≤ 2 / s
⊢ 1 - δ = 2 / s * (s / 2 - s / 2 * δ)

Tactic:
by field

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

Goal state before:
pp: case succ
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n✝ : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn :
  ContDiffWithinAt 𝕜' (↑n) f s x →
    restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s
h : ContDiffWithinAt 𝕜' (↑(n + 1)) f s x
⊢ restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' (n + 1) f s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f s

Tactic:
| succ n hn =>

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
this : ∀ (i j : Fin N.succ), i ≠ j → ‖a.c i‖ ≤ ‖a.c j‖ → (fun i j ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
hij : ¬‖a.c i‖ ≤ ‖a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
· rw [norm_sub_rev]; exact this j i inej.symm (le_of_not_ge hij)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
y : Y
x₁ x₂ : X
⊢ edist (Function.const X y x₁) (Function.const X y x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Tactic:
by
  simp only [Function.const_apply, edist_self, zero_le]

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

Goal state before:
pp: f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m
⊢ ∃ x ∈ s, f' x = m

Tactic:
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩

Goal state after:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x ∈ s, f' x = m