mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: case refine_2.hf'_nonneg
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ ∀ x ∈ interior (Ici b), 0 ≤ deriv f x

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : h ∈ Ioi 0
⊢ ‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤
    ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖

Tactic:
replace hpos : 0 < h := hpos

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
⊢ ‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤
    ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hω : ContDiffWithinAt 𝕜 r ω s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 ω s) s x

Tactic:
refine (hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt one_ne_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hω : ContDiffWithinAt 𝕜 r ω s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
⊢ 1 + 1 ≤ r
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖

Tactic:
have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun t ↦ x₀ + t • v
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖

Tactic:
have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun t ↦ x₀ + t • v
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y✝ : ℕ → E
hy✝ : ∀ (n : ℕ), y✝ n ∈ interior s
y_lim : Tendsto y✝ atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y✝ k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y✝ k)
this : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u)
y : E
hy : y ∈ s ∩ u
z : E
hz : z ∈ u
⊢ (z ∈ s) = (z ∈ s ∩ u)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * deriv (fun t ↦ 1 + t) 0 * ‖x‖ = ‖x‖

pp: case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

pp: case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0

Tactic:
deriv_const_add_id

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * 1 * ‖x‖ = ‖x‖

case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0
Module: Mathlib.Analysis.Calculus.Implicit

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ (fderiv 𝕜 φ.prodFun φ.pt).IsInvertible

Tactic:
φ.hasStrictFDerivAt.hasFDerivAt.fderiv

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)).IsInvertible
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i, Λ i • f' i + Λ₀ • φ' = 0

Tactic:
let := Classical.decEq ι
  replace hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀ := by
    simpa only [funext_iff] using hextr
  rcases hextr.exists_linear_map_of_hasStrictFDerivAt (hasStrictFDerivAt_pi.2 fun i => hf' i)
      hφ' with
    ⟨Λ, Λ₀, h0, hsum⟩
  rcases (LinearEquiv.piRing ℝ ℝ ι ℝ).symm.surjective Λ with ⟨Λ, rfl⟩
  refine ⟨Λ, Λ₀, ?_, ?_⟩
  · simpa only [Ne, Prod.ext_iff, LinearEquiv.map_eq_zero_iff, Prod.fst_zero] using! h0
  · ext x; simpa [mul_comm] using hsum x

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

Goal state before:
pp: case refine_3
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint b c

Tactic:
simpa [c] using disjoint_sdiff_right

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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
⊢ f y = f x

Tactic:
apply le_antisymm (hf hy.1 hx.1.1 hy.2.2.le)

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := ⋯
a_count : a.Countable
s₁ : Set ℝ := ⋯
hs₁ : MeasurableSet s₁
u : Set ℝ := ⋯
hu : u.Countable
b : Set ℝ := ⋯
hb : MeasurableSet b
c : Set ℝ := ⋯
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
⊢ f x ≤ f y
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
⊢ (𝓝[s \ {x}] x).NeBot

Tactic:
have : (𝓝[s ∩ Iio x] x).NeBot := neBot_iff.2 hx.1.2

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
this : (𝓝[s ∩ Iio x] x).NeBot
⊢ (𝓝[s \ {x}] x).NeBot
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: l : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : s₁ ∈ atBot
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atBot
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atBot
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
have hs : s ∈ atBot := inter_mem (inter_mem hs₁ hs₂) hs₃

Goal state after:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : s₁ ∈ atBot
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atBot
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atBot
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : s ∈ atBot
⊢ Tendsto (fun x ↦ f x / g x) atBot l
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))
⊢ AEStronglyMeasurable f μ

Tactic:
by
  obtain ⟨u, hu⟩ := l.exists_seq_tendsto
  have := aestronglyMeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
  rwa [Measure.restrict_eq_self_of_ae_mem] at this
  filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
h : ∃ b, IntegrableOn f (Iic b) μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)

Tactic:
obtain ⟨b, hb⟩ := h

Goal state after:
case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
this : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in a i..b, f x ∂μ = ∫ (x : ℝ) in Iic (a i), f x ∂μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)

Tactic:
rw [← sub_self (∫ x in Iic b, f x ∂μ)]

Goal state after:
case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
this : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in a i..b, f x ∂μ = ∫ (x : ℝ) in Iic (a i), f x ∂μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic b, f x ∂μ))
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
h : ∃ b, IntegrableOn f (Iio b) μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)

Tactic:
obtain ⟨b, hb⟩ := h

Goal state after:
case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iio b) μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0

Tactic:
let B := A.toContinuousLinearEquivOfDetNeZero hA

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
h : ∃ b, IntegrableOn f (Ici b) μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
obtain ⟨b, hb⟩ := h

Goal state after:
case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ (b_1 : ℝ), b ≤ b_1 → b_1 ∈ s
⊢ volume (Ici b) ≤ volume s

Tactic:
exact measure_mono hb

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn f' (Ioc a (id x)) volume

Tactic:
exact f'int.mono (fun y hy => hy.1) le_rfl

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

Goal state before:
pp: f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
hf_int : IntegrableOn g (f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ (Measure.comap f (volume.withDensity fun x ↦ ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
rw [hf.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul volume hs
    hg hf_int hf']
  simp only [det_toSpanSingleton]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (atBot.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atBot volume
s : Set ℝ
hs : s ∈ atBot
b : ℝ
hb : ∀ b_1 ≤ b, b_1 ∈ s
⊢ volume (Iic b) ≤ volume s

Tactic:
exact measure_mono hb

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case e'_3
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := ⇑I ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
⊢ ‖f x‖ₑ = ‖f' x‖ₑ

Tactic:
simp [f', I, Completion.enorm_coe]

Goal state after:
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))

Tactic:
eventually_nhdsWithin_iff

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)
this : Tendsto (fun ε ↦ ↑ε * μ (closedBall 0 R)) (𝓝 0) (𝓝 0)
⊢ Tendsto (fun ε ↦ ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)

Tactic:
exact Tendsto.mono_left this nhdsWithin_le_nhds

Goal state after: