mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i : ι
x : B
x✝² : x ∈ (Z.localTriv i).baseSet
x✝¹ x✝ : Z.Fiber x
⊢ (↑(Z.localTriv i) { proj := x, snd := x✝¹ + x✝ }).2 =
    (↑(Z.localTriv i) { proj := x, snd := x✝¹ }).2 + (↑(Z.localTriv i) { proj := x, snd := x✝ }).2

Tactic:
by simp only [map_add, localTriv_apply, mfld_simps]

Goal state after:
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
by
      have : ContinuousOn (fun x : B × F ↦ a.coordChange he' he x.1 x.2)
          ((e'.baseSet ∩ e.baseSet) ×ˢ univ) :=
        isBoundedBilinearMap_apply.continuous.comp_continuousOn
          ((a.continuousOn_coordChange he' he).prodMap continuousOn_id)
      rw [e.target_inter_preimage_symm_source_eq e', inter_comm]
      refine (continuousOn_fst.prodMk this).congr ?_
      rintro ⟨b, f⟩ ⟨hb, -⟩
      dsimp only [Function.comp_def, Prod.map]
      rw [a.mk_coordChange _ _ hb, e'.mk_symm hb.1]

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x

Tactic:
simp_rw [← mdifferentiableWithinAt_univ]

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDiffAt[univ] f x ↔ MDiffAt[univ] (Prod.fst ∘ f) x ∧ MDiffAt[univ] (Prod.snd ∘ f) x
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDiffAt[u] g (f x)
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffAt[s] x
⊢ HasMFDerivAt[s] (g ∘ f) x (mfderiv[u] g (f x) ∘SL mfderiv[s] f x)

Tactic:
exact HasMFDerivWithinAt.comp x hg.hasMFDerivWithinAt hf.hasMFDerivWithinAt h

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

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDiffAt[u] g (f x)
hf : MDiffAt[s] f x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffAt[s] x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
⊢ MDiffAt[s ∩ f ⁻¹' u] (g ∘ f) x

Tactic:
exact hg.comp _ (hf.mono inter_subset_left) inter_subset_right

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

Goal state before:
pp: 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✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝¹¹] a
ha' : a ⊆ e.baseSet
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) a

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩ <;>
  have := (h x hx).contMDiffAt <| ha.mem_nhds hx
  · exact ((e.contMDiffAt_section_iff (ha' hx)).mp this).contMDiffWithinAt
  · exact ((e.contMDiffAt_section_iff (ha' hx)).mpr this).contMDiffWithinAt

Goal state after:
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
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ContMDiff I.tangent (I.prod 𝓘(𝕜, E)) n ⇑(tangentBundleModelSpaceHomeomorph I)

Tactic:
apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : TangentBundle I H
y : ModelProd H E
⊢ ContDiffOn 𝕜 n
    (↑(extChartAt (I.prod 𝓘(𝕜, E)) y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I) ∘ ↑(extChartAt I.tangent x).symm)
    ((extChartAt I.tangent x).target ∩
      ↑(extChartAt I.tangent x).symm ⁻¹'
        ⇑(tangentBundleModelSpaceHomeomorph I) ⁻¹' (extChartAt (I.prod 𝓘(𝕜, E)) y).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
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ContMDiff I.tangent I.tangent n ⇑(tangentBundleModelSpaceHomeomorph I).symm

Tactic:
apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : ModelProd H E
y : TangentBundle I H
⊢ ContDiffOn 𝕜 n
    (↑(extChartAt I.tangent y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I).symm ∘ ↑(extChartAt I.tangent x).symm)
    ((extChartAt I.tangent x).target ∩
      ↑(extChartAt I.tangent x).symm ⁻¹'
        ⇑(tangentBundleModelSpaceHomeomorph I).symm ⁻¹' (extChartAt I.tangent y).source)
Module: Mathlib.Geometry.Manifold.BumpFunction

Goal state before:
pp: case h₂
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
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s ⊆ ↑(extChartAt I c) '' s

Tactic:
· refine Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_
    rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]

Goal state after:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: X : Type v
inst✝³ : TopologicalSpace X
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed[inst✝³] s
hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := K'.shiftr.shiftr
Kdiff : ℕ → Set X := fun n ↦ K (n + 1) \ interior (K n)
x : X
⊢ x ∈ Kdiff (K'.find x + 1)

Tactic:
by
    simpa only [K'.find_shiftr] using
      sdiff_subset_sdiff_right interior_subset (K'.shiftr.mem_sdiff_shiftr_find x)

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ find c ne i ∈ c

Tactic:
rw [find]
  split_ifs with h
  exacts [h.choose_spec.1, ne.some_mem]

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

Goal state before:
pp: case refine_1
𝕜 : 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
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, s x⟩).2) u x₀
⊢ (fun x ↦ (↑e ⟨x, (-s) x⟩).2) =ᶠ[nhdsWithin x₀ u] fun x ↦ -(↑e ⟨x, s x⟩).2

Tactic:
apply eventually_of_mem (U := e.baseSet)
    · exact mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)
    · intro x hx
      apply (e.linear 𝕜 hx).map_neg

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
⊢ ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1

Tactic:
← ρ.sum_eq_one hx₀,

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
⊢ ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = ∑ᶠ (i : ι), (ρ i) 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
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑' (i : ι), t i x⟩) u x₀

Tactic:
obtain ⟨u', hu', hfin⟩ := ht x₀
  -- All sections `t i` but a finite set `s` vanish near `x₀`: choose a neighbourhood `u` of `x₀`
  -- and a finite set `s` of sections which don't vanish.
  let s := {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
  have := hfin.fintype
  have : CMDiffAt[u ∩ u'] n (T% (fun x ↦ (∑ i ∈ s, (t i x)))) x₀ :=
    .sum_section fun i hi ↦ ((ht' i).mono Set.inter_subset_left)
  apply (contMDiffWithinAt_inter hu').mp
  apply this.congr fun y hy ↦ ?_
  · rw [TotalSpace.mk_inj, tsum_eq_sum']
    refine support_subset_iff'.mpr fun i hi ↦ ?_
    by_contra! h
    have : i ∈ s.toFinset := by
      refine Set.mem_toFinset.mpr ?_
      simp only [s, ne_eq, Set.mem_ofPred_eq]
      use x₀
      simpa using ⟨h, mem_of_mem_nhds hu'⟩
    exact hi this
  rw [TotalSpace.mk_inj, tsum_eq_sum']
  refine support_subset_iff'.mpr fun i hi ↦ ?_
  by_contra! h
  have : i ∈ s.toFinset := by
    refine Set.mem_toFinset.mpr ?_
    simp only [s, ne_eq, Set.mem_ofPred_eq]
    use y
    simpa using ⟨h, Set.mem_of_mem_inter_right hy⟩
  exact hi this

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : E
h'x : x ∈ d
hx : dist a x < ‖a‖ / 2
⊢ ∃ x, dist a ↑x < ‖a‖ / 2

Tactic:
exact ⟨⟨x, h'x⟩, hx⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
t_meas : MeasurableSet t
t_lt_top : μ t < ∞
⊢ ∀ᵐ (x : α) ∂μ.restrict t, 0 x ≤ f x

Tactic:
apply ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter (hf_int_finite t t_meas t_lt_top)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
t_meas : MeasurableSet t
t_lt_top : μ t < ∞
⊢ ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ∞ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

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

Tactic:
have : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ 0 ≤ᵐ[μ.restrict t] f
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : 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
⊢ f =ᵐ[μ.restrict t] 0

Tactic:
have : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict

Goal state after:
α : 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)
⊢ f =ᵐ[μ.restrict t] 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
by
  have hg (x y : ℝ) : IntervalIntegrable f volume x y :=
    intervalIntegrable_iff.mpr <|
      (hf.integrableOn_isCompact isCompact_uIcc).mono_set uIoc_subset_uIcc
  have LDT := (vitaliFamily volume 1).ae_tendsto_average hf
  have h {a b : ℝ} : ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t :=
    integral_Icc_eq_integral_Ioc (x := a) (y := b) (X := ℝ) |>.symm
  filter_upwards [LDT] with x hx
  intro c
  rw [hasDerivAt_iff_tendsto_slope_left_right]
  constructor
  · refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left)
    filter_upwards [self_mem_nhdsWithin] with y hy
    replace hy : y ≤ x := hy.le
    suffices -((y - x)⁻¹ • ∫ (t : ℝ) in Icc y x, f t) = (x - y)⁻¹ • ∫ (t : ℝ) in Icc y x, f t by
      simpa [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_ge, hy, h]
    rw [← neg_smul, neg_inv, neg_sub]
  · refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_right)
    filter_upwards [self_mem_nhdsWithin] with y hy
    replace hy : x ≤ y := hy.le
    simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_le, hy, h]

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

Goal state before:
pp: a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ uIoc a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x

Tactic:
rw [uIoc, mem_Ioc] at hx₄

Goal state after:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: 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}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
α : ℝ
hα : 0 < α
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → x < α

Tactic:
eventually_nhds_iff

Goal state after:
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}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
α : ℝ
hα : 0 < α
⊢ ∃ t, (∀ y ∈ t, y ∈ Ioi 0 → y < α) ∧ IsOpen t ∧ 0 ∈ t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: 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}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ}, 0 < α → ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
⊢ ε < δ → ε < (b - x) / 2 → ∃ a ∈ t, (Prod.snd - Prod.fst) a = ε ∧ a.1 = x

Tactic:
hε₃

Goal state after:
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}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ}, 0 < α → ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
⊢ ε < (b - x) / 2 → ∃ a ∈ t, (Prod.snd - Prod.fst) a = ε ∧ a.1 = x
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + v) - f x - L v‖ = ‖f (x + ρ • w) - f x - ρ • L w‖

Tactic:
by simp [hvw]

Goal state after: