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

Goal state before:
pp: case hgg'
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hgg'
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
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case hg'
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hg'
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
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case hfa
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 f (𝓝[≠] a) (𝓝 0)

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hfa
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 f (𝓝 a) (𝓝 0)
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case hga
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 g (𝓝[≠] a) (𝓝 0)

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hga
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 g (𝓝 a) (𝓝 0)
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case hdiv
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:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hdiv
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
Module: Mathlib.Analysis.Calculus.LHopital

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

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hdf
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
Module: Mathlib.Analysis.Calculus.LHopital

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

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hg'
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
Module: Mathlib.Analysis.Calculus.LHopital

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

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hfa
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto f (𝓝 a) (𝓝 0)
Module: Mathlib.Analysis.Calculus.LHopital

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

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hga
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto g (𝓝 a) (𝓝 0)
Module: Mathlib.Analysis.Calculus.LHopital

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

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hdiv
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝 a) l
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I

Tactic:
refine hbounded.mono fun i hi => ?_

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
hi : (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I
⊢ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
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
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x

Tactic:
symm

Goal state after:
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
⊢ ∫ (x : ℝ) in a..id x, f' x = f x - f a
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ ?m.74 - f b = -f b

pp: case f'int
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (deriv f) (Ioi b) volume

pp: case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 ?m.74)

pp: E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ E

Tactic:
zero_sub

Goal state after:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ -f b = -f b

case f'int
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (deriv f) (Ioi b) volume

case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)
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
⊢ g x - g a = ∫ (y : ℝ) in a..id x, g' y

Tactic:
symm

Goal state after:
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 : ℝ) in a..id x, g' y = g x - g a
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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ f a - f x = ∫ (x : ℝ) in id x..a, f' x

Tactic:
symm

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ ∫ (x : ℝ) in id x..a, f' x = f a - f x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ ∫ (x : ℝ) in Ioi a, rexp x • g (rexp x) = ∫ (y : ℝ) in Ioi (rexp a), g y

Tactic:
symm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ ∫ (y : ℝ) in Ioi (rexp a), g y = ∫ (x : ℝ) in Ioi a, rexp x • g (rexp x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ IntegrableOn (fun x ↦ rexp x • g (rexp x)) (Ioi a) volume ↔ IntegrableOn g (Ioi (rexp a)) volume

Tactic:
symm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ IntegrableOn g (Ioi (rexp a)) volume ↔ IntegrableOn (fun x ↦ rexp x • g (rexp x)) (Ioi a) volume
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x ↦ x⁻¹ • g (log x)) (Ioi a) volume ↔ IntegrableOn g (Ioi (log a)) volume

Tactic:
symm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
ha : 0 < a
⊢ IntegrableOn g (Ioi (log a)) volume ↔ IntegrableOn (fun x ↦ x⁻¹ • g (log x)) (Ioi a) volume
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z = dslope f w₀ w₀
h1 : ContinuousOn (fun z ↦ ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z ↦ ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z ↦ ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ -2 ≠ -1

Tactic:
decide

Goal state after:
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)
⊢ μ (f '' (s ∩ closedBall 0 R)) = 0

Tactic:
have B : Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0) := by
    have :
      Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝 0)
        (𝓝 (((0 : ℝ≥0) : ℝ≥0∞) * μ (closedBall 0 R))) :=
      ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 tendsto_id)
        (Or.inr measure_closedBall_lt_top.ne)
    simp only [zero_mul, ENNReal.coe_zero] at this
    exact Tendsto.mono_left this nhdsWithin_le_nhds

Goal state after:
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)
B : Tendsto (fun ε ↦ ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)
⊢ μ (f '' (s ∩ closedBall 0 R)) = 0
Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasDerivAt (fun x ↦ (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀

Tactic:
have := hasDerivAt_integral_of_dominated_loc_of_lip hs hF_meas hF_int hF'_meas h_lipsch
    bound_integrable h_diff

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable F' (μ.restrict (Ι a b)) ∧
    HasDerivAt (fun x ↦ ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) μ ∧
    HasDerivAt (fun x ↦ (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e '' t) (↑e x) ⊆ e.target

Tactic:
unfold t

Goal state after:
case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e '' (s ∩ e.source)) (↑e x) ⊆ e.target
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' : e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
he : e ∈ {e | e.source = ∅}
⊢ e ≫ₕ e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

Tactic:
have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _
      rw [he] at this
      have : e ≫ₕ e' ∈ { e : OpenPartialHomeomorph H H | e.source = ∅ } := eq_bot_iff.2 this
      exact (mem_union _ _ _).2 (Or.inr this)

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ (OpenPartialHomeomorph.refl H).subtypeRestr this ∈
    maximalAtlas (↥s) G

Tactic:
rw [OpenPartialHomeomorph.subtypeRestr_def, OpenPartialHomeomorph.trans_refl]

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

Tactic:
by
  rw [← liftPropWithinAt_indep_chart_aux' hG he' xe' hf' xf' hgs,
    liftPropWithinAt_indep_chart_aux' hG he xe hf xf hgs]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
hx : x ∈ (extendCoordChange e e').source
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange e e')) (range ↑I) x

Tactic:
apply (I.contDiffOn_extendCoordChange he he' x hx).mono_of_mem_nhdsWithin

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
hx : x ∈ (extendCoordChange e e').source
⊢ (extendCoordChange e e').source ∈ 𝓝[range ↑I] x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type w
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝⁴ : I.Boundaryless
E' : Type v'
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H' : Type w'
inst✝¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst✝ : I'.Boundaryless
⊢ (I.prod I').Boundaryless

Tactic:
by
  constructor
  dsimp
  rw [Set.range_prodMap, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]

Goal state after: