mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
i j : ↑(atlas H M)
this : IsManifold I (0 + 1) M
⊢ ContinuousOn (fun x ↦ fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x))
    ((↑i).source ∩ (↑j).source)

Tactic:
refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
      (i.1.continuousOn_extend.mono ?_) ?_

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
i j : ↑(atlas H M)
this : IsManifold I (0 + 1) M
⊢ (↑i).source ∩ (↑j).source ⊆ ((↑i).extend I).source

case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
i j : ↑(atlas H M)
this : IsManifold I (0 + 1) M
⊢ MapsTo (↑((↑i).extend I)) ((↑i).source ∩ (↑j).source) (((↑i).extend I).symm ≫ (↑j).extend I).source
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (TotalSpace.toProd H E).toFun

Tactic:
by
      let p : TangentBundle I H := ⟨I.symm (0 : E), (0 : E)⟩
      have : Continuous (chartAt (ModelProd H E) p) := by
        rw [← continuousOn_univ]
        convert! (chartAt (ModelProd H E) p).continuousOn
        simp only [mfld_simps]
      simpa only [mfld_simps] using this

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case hx
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
⊢ writtenInExtChartAt I I p Sum.swap (↑(extChartAt I p) p) = id (↑(extChartAt I p) p)

Tactic:
simp only [mfld_simps]
    cases p <;> simp

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
t : Set M'
this : writtenInExtChartAt I I q' Sum.inr =ᶠ[𝓝[↑(extChartAt I q').symm ⁻¹' t ∩ range ↑I] ↑(extChartAt I q') q'] id
⊢ HasFDerivWithinAt (writtenInExtChartAt I I q' Sum.inr) (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
    (↑(extChartAt I q').symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I q') q')

Tactic:
exact (hasFDerivWithinAt_id (extChartAt I q' q') _).congr_of_eventuallyEq this
    (by simp [writtenInExtChartAt, extChartAt])

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ (mfderiv% ↑(extChartAt I x) y).IsInvertible

Tactic:
by
  have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy
  have Z := ContinuousLinearMap.IsInvertible.of_inverse
    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
    (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt h'y)
  have : (extChartAt I x).symm ((extChartAt I x) y) = y := (extChartAt I x).left_inv hy
  rwa [this] at Z

Goal state after:
Module: Mathlib.Geometry.Manifold.BumpFunction

Goal state before:
pp: E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst✝²] s
hs : s ⊆ support ↑f
⊢ ∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r

Tactic:
set e := extChartAt I c
  have : IsClosed (e '' s) := f.isClosed_image_of_isClosed hsc hs
  rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs
  rcases exists_pos_lt_subset_ball f.rOut_pos this hs.2 with ⟨r, hrR, hr⟩
  exact ⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩

Goal state after:
Module: Mathlib.Order.Filter.Ring

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
l : Filter α
f g : α → β
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
⊢ 0 ≤ᶠ[l] f * g

Tactic:
by filter_upwards [hf, hg] with x using _root_.mul_nonneg

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(fs.toFun i) x = 1
⊢ x ∈ support ↑(fs.toFun i)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ∞ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ∞
⊢ μ (s ∩ t) < ∞

Tactic:
rwa [Measure.restrict_apply hs] at h's

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I✝ : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝
L'_cont : Continuous ⇑L'
A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm
I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))
μS : Measure ↥S := addHaar
μT : Measure ↥T := addHaar
c₀ : ℝ≥0∞
c₀_pos : c₀ ≠ 0
c₀_fin : c₀ ≠ ∞
h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT
J : map (⇑P) (μS.prod μT) = μS univ • μT
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν

Tactic:
obtain ⟨c₁, c₁_pos, c₁_fin, h₁⟩ : ∃ c₁ : ℝ≥0∞, c₁ ≠ 0 ∧ c₁ ≠ ∞ ∧ μT.map L' = c₁ • ν := by
    have : IsAddHaarMeasure (μT.map L') :=
      L'.toContinuousLinearEquiv.isAddHaarMeasure_map μT
    refine ⟨addHaarScalarFactor (μT.map L') ν, ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩
    simpa only [ne_eq, ENNReal.coe_eq_zero] using
      (addHaarScalarFactor_pos_of_isAddHaarMeasure (μT.map L') ν).ne'

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I✝ : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝
L'_cont : Continuous ⇑L'
A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm
I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))
μS : Measure ↥S := addHaar
μT : Measure ↥T := addHaar
c₀ : ℝ≥0∞
c₀_pos : c₀ ≠ 0
c₀_fin : c₀ ≠ ∞
h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT
J : map (⇑P) (μS.prod μT) = μS univ • μT
c₁ : ℝ≥0∞
c₁_pos : c₁ ≠ 0
c₁_fin : c₁ ≠ ∞
h₁ : map (⇑L') μT = c₁ • ν
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
x : M
hx : x ∉ ↑U
⊢ Function.extend Subtype.val g 0 x • f x = 0

Tactic:
rw [Function.extend_apply' _ _ _ (mt _ hx)]

Goal state after:
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
x : M
hx : x ∉ ↑U
⊢ 0 x • f x = 0

E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
x : M
hx : x ∉ ↑U
⊢ (∃ a, ↑a = x) → x ∈ ↑U
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g x‖)

Goal state after:
case hF_meas
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (fun a ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ

case h_bound
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ ↑C * ‖v‖ * ‖g a‖

case bound_integrable
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ Integrable (fun x ↦ ↑C * ‖v‖ * ‖g x‖) μ

case h_lim
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ ∀ᵐ (a : E) ∂μ, Tendsto (fun n ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : t ∈ Ioc 0 1
t_pos : 0 < t
x : E
hx : x ∈ K
⊢ t⁻¹ * (↑C * ‖x + t • v - x‖) * ‖g x‖ = ↑C * ‖v‖ * ‖g x‖

Tactic:
by simp [field, norm_smul, abs_of_nonneg t_pos.le]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
B : s = ⋃ n, t n
m : ℕ
⊢ ∀ ⦃b : ℕ⦄, m ≤ b → t m ⊆ t b

Tactic:
n

Goal state after:
case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
B : s = ⋃ n, t n
m n : ℕ
⊢ m ≤ n → t m ⊆ t n
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case refine_1
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ (fun n x ↦ G (↑n)⁻¹ x) n x) atTop (𝓝 (deriv f x))

Tactic:
rw [← restrict_Ioo_eq_restrict_Icc, MeasureTheory.ae_restrict_iff' measurableSet_Ioo]
    filter_upwards [hg.ae_differentiableAt] with x hx₁ hx₂
    rw [hfg hx₂]
    exact hx₁.hasDerivAt.tendsto_slope.comp <|
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      (by convert! tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ)); simp)
      (by simp [eventually_ne_atTop 0])

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
⊢ a ∈ Icc a b

Tactic:
by simp [hab]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
⊢ b ∈ Icc a b

Tactic:
by simp [hab]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ UniformContinuousOn f (uIcc a b)

Tactic:
simp only [UniformContinuousOn, Filter.tendsto_iff_comap, uniformity_eq_comap_totalLengthFilter]

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) ≤
    comap (fun x ↦ (f x.1, f x.2)) (comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
⊢ ε > 0 →
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε

Tactic:
hε

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ E ∈ disjWithin a b,
      ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
        ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
suffices H : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x by
    filter_upwards [H] with x hx xs
    have : f = (A.symm ∘ A) ∘ f := by
      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
    rw [this]
    exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ↑k ≤ ↑(n + 1)

Tactic:
by norm_cast; omega

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

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ ↑k < ↑(n + 1)

Tactic:
by norm_cast; omega

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

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ↑(k + 1) ≤ ↑(n + 1)

Tactic:
by norm_cast; omega

Goal state after:
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun x ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
| fun x ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1

Tactic:
n

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun x ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n : ℕ
| (1 - z) * ∑ x ∈ range n, (∑ i ∈ Ico (x + 1) n, f i) * z ^ x
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u‖ • b • u = ‖b • u‖ • a • u

Tactic:
simp only [norm_smul_of_nonneg, *, mul_smul]

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u