mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case e_a.hg
𝕜 : 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' → M''
p : M × M'
hf : MDiffAt f p
this : (fun z ↦ f (z.1, p.2)) = (fun z ↦ f (z, p.2)) ∘ Prod.fst
⊢ (MDiffAt fun z ↦ f (z, p.2)) p.1

Tactic:
exact hf.comp _ (mdifferentiableAt_id.prodMk mdifferentiableAt_const)

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

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
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
EM : Type u_9
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
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
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst✝ : Z.IsContMDiff IB n
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
rintro - - ⟨i, rfl⟩ ⟨i', rfl⟩
    refine (Z.contMDiffOn_coordChange IB i i').congr fun b hb ↦ ?_
    ext v
    exact Z.localTriv_coordChange_eq i i' hb v

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

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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
e : OpenPartialHomeomorph M M'
he : OpenPartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffAt[↑e '' (s ∩ e.source)] (↑e x)

Tactic:
exact (hs.inter (e.open_source.mem_nhds hx)).image_denseRange
    (he.mdifferentiableAt hx).hasMFDerivAt.hasMFDerivWithinAt
    (he.mfderiv_surjective hx).denseRange

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ ⟨x, V x⟩) s x

Tactic:
· apply Bundle.contMDiffWithinAt_totalSpace.2
    refine ⟨contMDiffWithinAt_id, ?_⟩
    convert! h.contMDiffWithinAt with y
    simp

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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
⊢ (ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n fun x ↦ ⟨x, V x⟩) ↔ ContDiff 𝕜 n V

Tactic:
by
  simp only [← contMDiffOn_univ, ← contDiffOn_univ, contMDiffOn_vectorSpace_iff_contDiffOn]

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

Goal state before:
pp: case left
𝕜 : 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
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        ((fun p ↦ (↑(chartAt H x).symm p.1, ↑(OpenPartialHomeomorph.refl F) p.2))
          ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)))).proj ∈
    s

Tactic:
OpenPartialHomeomorph.refl_apply

Goal state after:
case left
𝕜 : 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
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        ((fun p ↦ (↑(chartAt H x).symm p.1, id p.2)) ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)))).proj ∈
    s
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case neg
𝕜 : 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'
s : Set M
x : M
f : M → E'
hs : UniqueMDiffAt[s] x
hf : ¬MDiffAt[s] (-f) x
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case neg
𝕜 : 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'
s : Set M
x : M
f : M → E'
hs : UniqueMDiffAt[s] x
hf : ¬MDiffAt[s] (-f) x
⊢ 0 = 0
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_4
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∀ (a : ι), (fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a) a ⊆ u a

Tactic:
simp only [subset_def, mem_iUnion]

Goal state after:
case refine_4
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∀ (a : ι) (x : X), (∃ i, ∃ (_ : ind i = a), x ∈ t i) → x ∈ u a
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
v : PartialRefinement u s p
i : ι
⊢ v.toFun i ⊆ u i

Tactic:
exact if h : i ∈ v.carrier then subset_closure.trans (v.closure_subset h) else (v.apply_eq h).le

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

Goal state before:
pp: case refine_3
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)
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ ↑(T n)
x : X
this : (⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)).Finite
⊢ {i |
      ((fun a ↦ B ((fun a ↦ ↑↑a.snd) a) ((fun a ↦ r a.fst ↑a.snd) a)) i ∩ interior (K (K'.find x + 3))).Nonempty}.Finite

Tactic:
apply this.subset

Goal state after:
case refine_3
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 := ⋯
K : CompactExhaustion X := ⋯
Kdiff : ℕ → Set X := ⋯
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := ⋯
x : X
this : (⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)).Finite
⊢ {i | ((fun a ↦ B ((fun a ↦ ↑↑a.snd) a) ((fun a ↦ r a.fst ↑a.snd) a)) i ∩ interior (K (K'.find x + 3))).Nonempty} ⊆
    ⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case pos
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : j = i
⊢ IsCompact (closure (update v.toFun j vi j))

Tactic:
simp only [update_self]

Goal state after:
case pos
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : j = i
⊢ IsCompact (closure vi)
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_8
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ IsCompact
    (closure
      ({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
            closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
        i))

Tactic:
simp only [update_self]

Goal state after:
case refine_8
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ IsCompact (closure vi)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ∞
H : μ {x | f x ≤ b} ≠ 0
⊢ μ (toMeasurable μ s) < ∞

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ∞
H : μ {x | f x ≤ b} ≠ 0
⊢ μ s < ∞
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) ∂μ, x ∈ U → f x = 0

Tactic:
rw [← ae_restrict_iff' meas_U, 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 ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ 0 ≤ -∫ (a : α) in s, f a ∂μ

Tactic:
neg_nonneg

Goal state after:
α : 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 ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (a : α) in s, f a ∂μ ≤ 0
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: case refine_2.hs
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) in ↑U, Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ MeasurableSet ↑U

Tactic:
exact meas_U

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 < ∞
⊢ IntegrableOn f s ((μ.restrict t).trim hm)

Tactic:
unfold IntegrableOn

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 t).trim hm).restrict s)
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
x✝ : True
n : ℕ
hn : N ≤ n
⊢ (1 / (2 * ‖c‖)) ^ n ≤ 1 / 2 ^ n / ‖c‖ ^ n

pp: case ha
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
x✝ : True
n : ℕ
hn : N ≤ n
⊢ 1 ≤ 2

Tactic:
· simp [mul_pow, div_eq_inv_mul]

Goal state after:
case ha
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
x✝ : True
n : ℕ
hn : N ≤ n
⊢ 1 ≤ 2
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case e_f
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))
n : ℕ
y : ℝ
⊢ ‖G (↑n)⁻¹ y‖ = G (↑n)⁻¹ y

Tactic:
exact abs_eq_self.mpr (hg.monotoneOn univ |>.slope_nonneg trivial trivial)

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

Goal state before:
pp: case zero
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n : ℕ
inst✝ : CompleteSpace F
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
⊢ f (x + y) =
    (∑ k ∈ Finset.range (0 + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑0!)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ 0 • (iteratedFDeriv ℝ (0 + 1) f (x + t • y)) fun x ↦ y

Tactic:
have h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun (s : ℝ) ↦ f (x + s • y))
        (Set.uIcc 0 1) := by
      intro t ht
      rw [DifferentiableAt.deriv_comp_add_smul]
      exact (hf t ht).differentiableAt (by simp)
    simp only [zero_add, Finset.range_one, Finset.sum_singleton, factorial_zero, cast_one, inv_one,
      iteratedFDeriv_zero_apply, one_smul, pow_zero, reduceAdd, iteratedFDeriv_one_apply]
    rw [← sub_eq_iff_eq_add', Eq.comm, intervalIntegral.integral_congr h_eq]
    have hf' : ∀ (t : ℝ) (ht : t ∈ Set.uIcc 0 1), DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t :=
      fun t ht ↦ ((hf t ht).differentiableAt (by simp)).comp t (by fun_prop)
    have hint : IntervalIntegrable (deriv (fun s ↦ f (x + s • y))) MeasureTheory.volume 0 1 := by
      have h₁ : ContinuousOn (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc (0 : ℝ) 1) := by
        intro z ⟨t, ht, hz⟩
        rw [← hz]
        exact (((hf t ht).fderiv_right (le_refl _)).continuousAt (n := 0)).continuousWithinAt
      have h₂ : ContinuousOn (fun x_1 ↦ fderiv ℝ f (x + x_1 • y)) (Set.uIcc (0 : ℝ) 1) := by
        apply h₁.comp (t := (fun t ↦ x + t • y) '' (Set.uIcc (0 : ℝ) 1)) (by fun_prop)
        intro t ht
        use t
      apply (ContinuousOn.congr _ h_eq.symm).intervalIntegrable
      fun_prop
    simpa using intervalIntegral.integral_deriv_eq_sub hf' hint

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
hu : ∀ (t : ℝ), HasDerivAt (u (n + 1)) (-u n t) t
hu' : Continuous (u n)
v : ℕ → ℝ → F := fun k t ↦ (iteratedFDeriv ℝ k f (x + t • y)) fun x ↦ y
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t

Tactic:
unfold v

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
hu : ∀ (t : ℝ), HasDerivAt (u (n + 1)) (-u n t) t
hu' : Continuous (u n)
v : ℕ → ℝ → F := fun k t ↦ (iteratedFDeriv ℝ k f (x + t • y)) fun x ↦ y
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ HasDerivAt (fun t ↦ (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y)
    ((iteratedFDeriv ℝ (n + 1 + 1) f (x + t • y)) fun x ↦ y) t