mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set M
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t✝ : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
hf : HasMFDerivAt[s] (f i) z (f' i) ∧ ∀ x ∈ t, HasMFDerivAt[s] (f x) z (f' x)
e_1✝ : (TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, F') ((f i * ∏ x ∈ t, f x) z)) = (TangentSpace I z →L[𝕜] F')
j : ι
hj : j ∈ t
⊢ i ≠ j

Tactic:
by grind

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
s : Set M
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t✝ : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
hf : HasMFDerivAt[s] (f i) z (f' i) ∧ ∀ x ∈ t, HasMFDerivAt[s] (f x) z (f' x)
e_1✝ : (TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, F') ((f i * ∏ x ∈ t, f x) z)) = (TangentSpace I z →L[𝕜] F')
j : ι
hj : j ∈ t
⊢ i ∉ t.erase j

Tactic:
by grind

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

Goal state before:
pp: case e'_6
𝕜 : 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
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t✝ : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
hf : HasMFDerivAt[s] (f i) z (f' i) ∧ ∀ x ∈ t, HasMFDerivAt[s] (f x) z (f' x)
e_2✝ : (TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, F') ((f i * ∏ x ∈ t, f x) z)) = (TangentSpace I z →L[𝕜] F')
⊢ (∏ j ∈ t, f j z) • f' i = (∏ i ∈ t, f i) z • f' i

Tactic:
· simp

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
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑e '' s)
⊢ ∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r

Tactic:
support_eq_inter_preimage,

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
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst✝²] s
hs : s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑e '' s)
⊢ ∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i ↦ (ρ i) x) ⊆ ↑I
x : X
hx : (support fun i ↦ (ρ i) x) ⊆ ↑I
x_in : x ∈ s
this : ∑ i ∈ I, (ρ i) x = ∑ᶠ (i : ι), (ρ i) x
⊢ ∑ i ∈ I, (ρ i) x = 1

Tactic:
ρ.sum_eq_one x_in

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i ↦ (ρ i) x) ⊆ ↑I
x : X
hx : (support fun i ↦ (ρ i) x) ⊆ ↑I
x_in : x ∈ s
this : ∑ i ∈ I, (ρ i) x = 1
⊢ ∑ i ∈ I, (ρ i) x = 1
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed[inst✝²] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝²] (U i)
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen[inst✝²] (V i)
hsV : s ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, f.IsSubordinate U

Tactic:
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩

Goal state after:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed[inst✝²] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝²] (U i)
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen[inst✝²] (V i)
hsV : s ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : f.IsSubordinate V
⊢ ∃ f, f.IsSubordinate U
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₀
⊢ u ⊆ Set.univ

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3.inl
ι : 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
vi : Set X
j : ι
hi : j ∉ v.carrier
si : Set X := s ∩ (⋃ j_1, ⋃ (_ : j_1 ≠ j), v.toFun j_1)ᶜ
hsi : si = s ∩ ⋂ i, ⋂ (_ : ¬i = j), (v.toFun i)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun j
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun j ∧ IsCompact (closure vi)
⊢ closure vi ⊆ u j

Tactic:
exact subset_trans hvi.2.2.1 <| PartialRefinement.subset v j

Goal state after:
Module: Mathlib.Topology.MetricSpace.PartitionOfUnity

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Tactic:
by
  rcases Metric.exists_continuous_nnreal_forall_closedEBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
  refine ⟨δ, hδ0, fun i x hx => ?_⟩
  rw [← Metric.closedEBall_coe]
  exact hδ i x hx

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

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
n : ℕ∞
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
hd : Disjoint s t
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
by
  have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd hx)
  rcases SmoothBumpCovering.exists_isSubordinate I ht this with ⟨ι, f, hf⟩
  set g := f.toSmoothPartitionOfUnity
  refine
    ⟨⟨_, g.contMDiff_sum.of_le (by simp)⟩, fun x hx => ?_, fun x => g.sum_eq_one, fun x =>
      ⟨g.sum_nonneg x, g.sum_le_one x⟩⟩
  suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
  refine fun i => f.toSmoothPartitionOfUnity_zero_of_zero ?_
  exact notMem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)

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

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
have h'g : ∀ c x, 0 ≤ g c x := fun c x ↦ (hg c (mem_range_self (f := g c) x)).1

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ ∀ (x : M), 0 ≤ f x
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 : (μ.trim hm) (s ∩ t) < ∞
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)

Tactic:
trim_measurableSet_eq hm (hs.inter ht_meas)

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 : μ (s ∩ t) < ∞
⊢ 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 : (μ.trim hm) (s ∩ t) < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 0

Tactic:
trim_measurableSet_eq hm (hs.inter ht_meas)

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 : μ (s ∩ t) < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 0
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: case mpr
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
⊢ (∃ c d, Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) atTop (𝓝 y)) →
    y ∈ tangentConeAt R s x

Tactic:
· rintro ⟨c, d, hd₀, hds, hcd⟩
    exact mem_tangentConeAt_of_seq atTop c d hd₀ hds hcd

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

Goal state before:
pp: 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
⊢ s = ⋃ n, t n

Tactic:
rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]

Goal state after:
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ⋃ i ∈ Ico m m, Ioc (f i) (f (succ i)) = Ioc (f m) (f m)

pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ∀ (n : α),
    m ≤ n →
      ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n) →
        ⋃ i ∈ Ico m (succ n), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ n))

Tactic:
· simp

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ∀ (n : α),
    m ≤ n →
      ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n) →
        ⋃ i ∈ Ico m (succ n), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ n))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
this : 0 ≤ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2
⊢ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2

Tactic:
by grind

Goal state after:
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))
⊢ ENNReal.ofReal (g b - g a) = ENNReal.ofReal (f b - f a)

Tactic:
by grind

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 : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (Icc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
have hG'₀ : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤ :=
    lt_of_le_of_lt hG' ENNReal.ofReal_lt_top |>.ne_top

Goal state after:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (Icc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc 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 ≠ ⊤
⊢ IntervalIntegrable (deriv f) volume a b
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 : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (Icc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
have hG'₀ : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤ :=
    lt_of_le_of_lt hG' ENNReal.ofReal_lt_top |>.ne_top

Goal state after:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (Icc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc 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 ≠ ⊤
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
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
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((-f) (t.2 i).1) ((-f) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
· simp

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

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : ℝ → E := fun x ↦ if x ∈ Ioc a b then f x else 0
⊢ ∀ x ∉ Ioc a b, g x = 0

Tactic:
by grind

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

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : ℝ → E := fun x ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
a✝² : x ≠ a
a✝¹ : x ≠ b
a✝ : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ a < x

Tactic:
by grind

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

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : ℝ → E := fun x ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
a✝² : x ≠ a
a✝¹ : x ≠ b
a✝ : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ x < b

Tactic:
by grind

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

Goal state before:
pp: case inl
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‖
hv : 0 ∈ ball 0 r
⊢ 0 ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}

pp: case inr
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
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}

Tactic:
· simp

Goal state after:
case inr
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
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
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}
A : ℝ × ℝ
hA : A ∈ t
⊢ 0 ≤ 6 * (A.2 - A.1)

Tactic:
by grind

Goal state after: