mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case pos
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
s_eq : s = ⋃ n, s ∩ f n • (k * k⁻¹)
I : μ' s = ∑' (n : ℕ), μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
J : ν s = ∑' (n : ℕ), ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
⊢ μ' s = ν s

Tactic:
I,

Goal state after:
case pos
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
s_eq : s = ⋃ n, s ∩ f n • (k * k⁻¹)
I : μ' s = ∑' (n : ℕ), μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
J : ν s = ∑' (n : ℕ), ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
⊢ ∑' (n : ℕ), μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n) = ν s
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: x : ℝ
⊢ deriv (fun x ↦ |x|) x = ↑(SignType.sign x)

Tactic:
obtain rfl | hx := eq_or_ne x 0
  · simpa using deriv_abs_zero
  · simpa [hx] using (hasDerivAt_abs hx).deriv

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

Goal state before:
pp: f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ioo a c) b

Tactic:
refine isMaxOn_Ioo_of_mono_anti ?_ ?_
  · apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc h hd₀) <;> simp_all
  · apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico h hd₁) <;> simp_all

Goal state after:
Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField

Goal state before:
pp: case succ
𝕜 : 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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun i j ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) s x) (V i x) -
      ∑ i,
        ∑ j ≥ i,
          (-1) ^ (↑i + ↑j) •
            (ω x)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                (j.removeNth (i.castSucc.removeNth fun x_1 ↦ V x_1 x))) =
    ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) s x) (V i x)

Tactic:
sub_eq_self

Goal state after:
case succ
𝕜 : 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
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun i j ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (ω x)
            (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
              (j.removeNth (i.castSucc.removeNth fun x_1 ↦ V x_1 x))) =
    0
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
rcases le_total r (δ / 2) with (H | H)

Goal state after:
case inl
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : r ≤ δ / 2
⊢ (g x ∩ Ioo 0 δ).Nonempty

case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ (↑f'u).range = ⊤

Tactic:
by
    have : (f'u ∘L .inr 𝕜 E₁ E₂).range ≤ f'u.range := LinearMap.range_comp_le_range ..
    rwa [LinearMap.range_eq_top.mpr if₂u.surjective, top_le_iff] at this

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : ↑i ≤ n
⊢ iteratedDeriv i (g ∘ f) x = ∑ c, (∏ j, iteratedDeriv (c.partSize j) f x) • iteratedDeriv c.length g (f x)

Tactic:
rw [iteratedDeriv_vcomp_eq_sum_orderedFinpartition hg hf hi]
  simp only [iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod]

Goal state after:
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
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f').range = ⊤
hker : (↑f').ker.ClosedComplemented
⊢ ↑(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) a = (f a, 0)

Tactic:
simp [hf.implicitToOpenPartialHomeomorphOfComplemented_apply]

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l

Tactic:
by
  rw [eventually_iff_exists_mem] at *
  rcases hff' with ⟨s₁, hs₁, hff'⟩
  rcases hgg' with ⟨s₂, hs₂, hgg'⟩
  rcases hg' with ⟨s₃, hs₃, hg'⟩
  let s := s₁ ∩ s₂ ∩ s₃
  have hs : s ∈ 𝓝[>] a := inter_mem (inter_mem hs₁ hs₂) hs₃
  rw [mem_nhdsGT_iff_exists_Ioo_subset] at hs
  rcases hs with ⟨u, hau, hu⟩
  refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv <;> grind

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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)

Tactic:
I,

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume

Tactic:
apply integrableOn_congr_set_ae

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
⊢ f '' s =ᵐ[volume] f '' c
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case refine_1
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
x✝ : ℝ
a✝¹ : s \ {a} ∈ 𝓝 x✝
a✝ : deriv g x✝ ≠ 0
⊢ derivWithin g (s \ {a}) x✝ ≠ 0

Tactic:
rwa [derivWithin_of_mem_nhds ‹_›]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) s volume

Tactic:
I,

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
exact HasDerivAt.lhopital_zero_atBot hdf' hdg' hg' hfbot hgbot hdiv

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

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
J : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in f '' c, g x
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)

Tactic:
I,

Goal state after:
case pos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
J : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in f '' c, g x
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in c, f' x • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i ↦ Ioc (a i) (b i)
⊢ Integrable f μ

Tactic:
refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i ↦ Ioc (a i) (b i)
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun i ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
⊢ IntegrableOn f (Iic b) μ

Tactic:
refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun i ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
⊢ IntegrableOn f (Ioi a) μ

Tactic:
refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
⊢ IntegrableOn g (Icc (f a) (f b)) volume ↔ IntegrableOn g (f '' Ioo a b) volume

Tactic:
apply integrableOn_congr_set_ae

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
⊢ Icc (f a) (f b) =ᵐ[volume] f '' Ioo a b
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ IntegrableOn g (Icc (f b) (f a)) volume ↔ IntegrableOn g (f '' Ioo a b) volume

Tactic:
apply integrableOn_congr_set_ae

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ Icc (f b) (f a) =ᵐ[volume] f '' Ioo a b
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: g g' : ℝ → ℝ
a l : ℝ
hcont✝ : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ 0 ≤ g' y

Tactic:
exact g'pos _ hy.1

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ

Tactic:
have Hf'g : Integrable (fun x ↦ B (f' x) (g x)) (ν.prod volume) := by
    rw [A]; exact hf'g.smul_measure_nnreal

Goal state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
F : ℂ → E := fun z ↦ (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x ↦ (x - c) • f x) c)) s
hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c ((𝓝[≠] c).limUnder f)) s

Tactic:
rwa [hc.limUnder_eq]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : CommMonoid α
f : ι → β → α
g : β → α
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
h : HasProdUniformly f g
⊢ HasProdLocallyUniformly f g

Tactic:
simp only [hasProdUniformly_iff_tendstoUniformly, HasProdLocallyUniformly] at *
  exact TendstoUniformly.tendstoLocallyUniformly h

Goal state after: