mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝²² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝²¹ : TopologicalSpace H
E : Type u_3
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹⁸ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝¹⁵ : TopologicalSpace H''
E'' : Type u_7
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝¹² : TopologicalSpace G
inst✝¹¹ : ChartedSpace H G
M : Type u_9
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H' M
G' : Type u_11
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : ChartedSpace H'' G'
inst✝⁶ : Monoid G'
inst✝⁵ : SMul G G'
inst✝⁴ : MulAction G' M
inst✝³ : SMul G M
inst✝² : IsScalarTower G G' M
n : ℕ∞ω
inst✝¹ : ContMDiffSMul I I'' n G G'
inst✝ : ContMDiffSMul I'' I' n G' M
this : ContMDiff (I.prod I') I' n fun p ↦ (p.1 • 1) • p.2
⊢ ContMDiff (I.prod I') I' n fun p ↦ p.1 • p.2

Tactic:
simpa

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'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hq : HasMFDerivAt[s] q z q'
⊢ HasMFDerivAt[s] (p * q) z (p z • q' + q z • p')

Tactic:
convert! hp.mul' hq; ext _; apply mul_comm

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

Goal state before:
pp: case insert
𝕜 : 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 : ∀ i_1 ∈ insert i t, HasMFDerivAt[s] (f i_1) z (f' i_1)
⊢ HasMFDerivAt[s] (f i * ∏ x ∈ t, f x) z ((∏ j ∈ t, f j z) • f' i + ∑ x ∈ t, (∏ j ∈ (insert i t).erase x, f j z) • f' x)

Tactic:
add_comm

Goal state after:
case insert
𝕜 : 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 : ∀ i_1 ∈ insert i t, HasMFDerivAt[s] (f i_1) z (f' i_1)
⊢ HasMFDerivAt[s] (f i * ∏ x ∈ t, f x) z (∑ x ∈ t, (∏ j ∈ (insert i t).erase x, f j z) • f' x + (∏ j ∈ t, f j z) • f' i)
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
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)

Tactic:
exact hind _ hxa

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

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : R1Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed[inst✝³] s →
      (∀ x ∈ s, ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
        ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
s t : Set X
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hst : Disjoint s t
x : X
hx : x ∈ s
v u : Set X
hv : IsOpen[inst✝³] v
hu : IsOpen[inst✝³] u
htv : t ⊆ v
hxu : {x} ⊆ u
huv : Disjoint v u
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst✝¹] s →
      IsClosed[inst✝¹] t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝¹] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst✝¹] (V i)
hVU : ∀ (i : ι), closure[inst✝¹] (V i) ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U

Tactic:
have hVU' : ∀ i, V i ⊆ U i := fun i => Subset.trans subset_closure (hVU i)

Goal state after:
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst✝¹] s →
      IsClosed[inst✝¹] t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝¹] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst✝¹] (V i)
hVU : ∀ (i : ι), closure[inst✝¹] (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
⊢ f.toPOUFun i x = (f i) x * ∏ j ∈ t with WellOrderingRel j i, (1 - (f j) x)

Tactic:
refine congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)
  rw [Ne, sub_eq_self] at hj
  rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]
  exact flip (ht j) hj

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i

Tactic:
intro i hi

Goal state after:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), (f i) x = 1
⊢ False

Tactic:
simp_rw [H] at this

Goal state after:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), 0 = 1
⊢ False
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), 0 = 1
⊢ False

Tactic:
simpa

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
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate fun x ↦ sᶜ
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
set g := f.toSmoothPartitionOfUnity

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
n : ℕ∞
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate fun x ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: case neg
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
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
ε : ℝ
εpos : 0 < ε
hε : x ∉ thickening ε s
⊢ ∀ᶠ (n : ℕ) in atTop, g n x = 0

Tactic:
filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn

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
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
ε : ℝ
εpos : 0 < ε
hε : x ∉ thickening ε s
n : ℕ
hn : u n < ε
⊢ g n x = 0
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : OrderBot α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ∀ i ∈ Ici ⊥, f ⊥ ≤ f i

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : OrderBot α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ¬BddAbove (f '' Ici ⊥)

Tactic:
simpa

Goal state after:
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 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‖)
⊢ 0 < ‖y‖

Tactic:
simpa

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))
⊢ MapsTo (fun x ↦ max a (min x b)) univ (Icc a b)

Tactic:
simpa

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
⊢ ∀ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ ↑K * dist (I i).1 (I i).2

Tactic:
intro i hi

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ ↑K * dist (I i).1 (I i).2
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
this : (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤ (↑K * edist ((n, I).2 i).1 ((n, I).2 i).2).toReal
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ ↑K * dist (I i).1 (I i).2

Tactic:
ENNReal.toReal_mul,

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
i : ℕ
hi : i ∈ Finset.range (n, I).1
this : (edist (f ((n, I).2 i).1) (f ((n, I).2 i).2)).toReal ≤ (↑K).toReal * (edist ((n, I).2 i).1 ((n, I).2 i).2).toReal
⊢ dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ ↑K * dist (I i).1 (I i).2
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
simp only [sub_self, zero_pow, Ne, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case h₁
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ |(↑n !)⁻¹ * (x - y) ^ n| ≤ (↑n !)⁻¹ * |x - a| ^ n

pp: case h₂
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C

Tactic:
· rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
      gcongr

Goal state after:
case h₂
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case a.left
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 * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
this : Icc x y ⊆ uIcc a b
⊢ ∀ i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1,
    ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ∈ uIcc a b ∧ ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 ∈ uIcc a b

Tactic:
intro i hi

Goal state after:
case a.left
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 * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
this : Icc x y ⊆ uIcc a b
i : ℕ
hi : i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1
⊢ ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ∈ uIcc a b ∧ ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 ∈ uIcc a b
Module: Mathlib.Analysis.Normed.Module.Ray

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

Tactic:
← add_smul,

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

Goal state before:
pp: case inr
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 * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
⊢ ∀ x < n + 1, ¬eVariationOn f (Icc (a + ↑x * δ') (a + (↑x + 1) * δ')) = ⊤

Tactic:
intro i hi

Goal state after:
case inr
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 * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
v_each : ∀ (x y : ℝ), a ≤ x → x ≤ y → y < x + δ → y ≤ b → eVariationOn f (Icc x y) ≤ 1
i : ℕ
hi : i < n + 1
⊢ ¬eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ')) = ⊤