mathlib-initiative/mathlib-tactics huggingface dataset:
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 : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x).symm y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source (I := I)]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case snd
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (contMDiffCoordChange n IB a he he' b) v).2 = (↑e' { proj := b, snd := e.symm b v }).2

Tactic:
exact a.contMDiffCoordChange_apply he he' hb v

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
x : M
inst✝ : FiniteDimensional ℝ E
⊢ ↑f x ∈ Icc 0 1

Tactic:
have : f x = 0 ∨ f x = _ := indicator_eq_zero_or_self _ _ _

Goal state after:
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
x : M
inst✝ : FiniteDimensional ℝ E
this : ↑f x = 0 ∨ ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ ↑f x ∈ Icc 0 1
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (-s) x⟩) u x₀

Tactic:
rw [contMDiffWithinAt_section] at hs ⊢

Goal state after:
𝕜 : 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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, (-s) x⟩).2) u x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (f • s) x⟩) u x₀

Tactic:
rw [contMDiffWithinAt_section] at hs ⊢

Goal state after:
𝕜 : 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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, (f • s) x⟩).2) u x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀

Tactic:
induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using! contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)

Goal state after:
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 μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0
meas_U : MeasurableSet U
⊢ ∀ᵐ (x : M) ∂μ.restrict U, f x = 0

Tactic:
ae_restrict_iff_subtype meas_U

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 μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0
meas_U : MeasurableSet U
⊢ ∀ᵐ (x : ↑U) ∂Measure.comap Subtype.val μ, f ↑x = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
h_neg : 0 ≤ᵐ[μ.restrict t] -f
x : α
hx : 0 x ≤ -f x
⊢ f x ≤ 0 x

Tactic:
simpa using hx

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, c (f x) ∂μ = 0

Tactic:
rw [ContinuousLinearMap.integral_comp_comm c (hf_int_finite s hs hμs), hf_zero s hs hμs]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : StrongDual ℝ E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ c 0 = 0
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 f' : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x

Tactic:
have : ∀ᵐ x ∂μ, (f - f') x = 0 := by
    apply ae_eq_zero_of_integral_contMDiff_smul_eq_zero I (hf.sub hf')
    intro g g_diff g_supp
    simp only [Pi.sub_apply, smul_sub]
    rw [integral_sub, sub_eq_zero]
    · exact h g g_diff g_supp
    · exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
    · exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp

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 f' : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact hf_int_finite _ (hs.inter hf.measurableSet) hμs

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

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ Integrable f (((μ.restrict t).trim hm).restrict s)

Tactic:
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 0

Tactic:
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 0
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: case mp
R : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul R E
inst✝¹ : TopologicalSpace E
inst✝ : FirstCountableTopology E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
cd : ℕ → R × E
hcd : Tendsto cd atTop (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ ∃ c d, Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) atTop (𝓝 y)

Tactic:
simp only [tendsto_inf, tendsto_comap_iff, tendsto_prod_iff', tendsto_nhdsWithin_iff] at hcd

Goal state after:
case mp
R : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul R E
inst✝¹ : TopologicalSpace E
inst✝ : FirstCountableTopology E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
cd : ℕ → R × E
hcd :
  Tendsto ((fun p ↦ p.1 • p.2) ∘ cd) atTop (𝓝 y) ∧
    Tendsto (fun n ↦ (cd n).1) atTop ⊤ ∧
      Tendsto (fun n ↦ (cd n).2) atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, (cd n).2 ∈ (fun x_1 ↦ x + x_1) ⁻¹' s
⊢ ∃ c d, Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) atTop (𝓝 y)
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀ : Tendsto (fun x ↦ ‖d x‖) atTop (𝓝 ‖0‖)
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hcd : Tendsto (fun x ↦ ‖c x • d x‖) atTop (𝓝 ‖y‖)
⊢ Tendsto (fun x ↦ ‖c x‖) atTop atTop

Tactic:
simp only [norm_smul, norm_zero, ← div_inv_eq_mul] at hd₀ hcd

Goal state after:
case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (fun x ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun x ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (fun x ↦ ‖c x‖) atTop atTop
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: 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))
⊢ liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖(fun n x ↦ G (↑n)⁻¹ x) n x‖ₑ) atTop =
    liminf (fun n ↦ ENNReal.ofReal (∫ (x : ℝ) in Icc a b, G (↑n)⁻¹ x)) atTop

Tactic:
apply Filter.liminf_congr

Goal state after:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := ⋯
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := ⋯
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
⊢ ∀ᶠ (a_1 : ℕ) in atTop,
    ∫⁻ (x : ℝ) in Icc a b, ‖(fun n x ↦ G (↑n)⁻¹ x) a_1 x‖ₑ = ENNReal.ofReal (∫ (x : ℝ) in Icc a b, G (↑a_1)⁻¹ x)
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case e'_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v) i • B i) = ∑ i, (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx : ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v) i • B i) = ∑ i, (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : StrongDual ℝ E := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i ↦ lineDeriv ℝ f x (B i))
v : E
hv : v ∈ s
⊢ L v = ∑ i, (B.repr v) i • lineDeriv ℝ f x (B i)

Tactic:
simp [L, B.sum_repr v]

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

Goal state before:
pp: case e'_3
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v) i • B i) = ∑ i, (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx : ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v) i • B i) = ∑ i, (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : StrongDual ℝ E := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i ↦ lineDeriv ℝ f x (B i))
v : E
hv : v ∈ s
⊢ v = ∑ i, (B.repr v) i • B i

Tactic:
simp [L, B.sum_repr v]

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

Goal state before:
pp: case μB
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
A : ℝ × ℝ
hA : A ∈ t
⊢ ENNReal.ofReal (2 * (3 * (A.2 - A.1))) ≤ ENNReal.ofReal (6 * (A.2 - A.1))

Tactic:
ENNReal.ofReal_le_ofReal_iff (by grind)

Goal state after:
case μB
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
A : ℝ × ℝ
hA : A ∈ t
⊢ 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
obtain ⟨x', h1, h2⟩ := taylor_mean_remainder_lagrange hx hf.of_succ (hd.mono Ioo_subset_Icc_self)

Goal state after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e'_3.a.e'_4
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝¹ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 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) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (n + 1)
⊢ ↑x✝ + 1 = ↑(x✝ + 1)

Tactic:
· norm_cast

Goal state after: