mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case pos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntervalIntegrable (fun x ↦ f' x • (g ∘ f) x) volume a b
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ (∫ (t : ℝ) in f a..f b, g t) - ∫ (t : ℝ) in f a..f a, g t = ∫ (t : ℝ) in f a..f b, g t

Tactic:
integral_same,

Goal state after:
case pos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntervalIntegrable (fun x ↦ f' x • (g ∘ f) x) volume a b
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ (∫ (t : ℝ) in f a..f b, g t) - 0 = ∫ (t : ℝ) in f a..f b, g t
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case refine_6
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 ∈ c, 0 ≤ f' x

Tactic:
intro x hx

Goal state after:
case refine_6
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 ∈ c
⊢ 0 ≤ f' x
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
this : (𝓝[s ∩ Iio x] x).NeBot
y : ℝ
yt : y ∈ s
yx : y < x
⊢ y ∉ {x}

Tactic:
simpa using yx.ne

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
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
⊢ IntegrableOn g (f '' c) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume

Tactic:
integrableOn_image_iff_integrableOn_abs_det_fderiv_smul _ hc hF' inj_c

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
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
⊢ IntegrableOn (fun x ↦ |(F' x).det| • g (f x)) c volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case neg
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
⊢ 0 = ∫ (x : ℝ) in s, f' x • g (f x)

Tactic:
integral_undef

Goal state after:
case neg
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
⊢ 0 = 0

case neg
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
⊢ ¬Integrable (fun x ↦ f' x • g (f x)) (volume.restrict s)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: 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 : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (d * μ (closedBall 0 1)))

Tactic:
convert! L1

Goal state after:
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 : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ d * μ (closedBall 0 1) = μ (⇑A '' closedBall 0 1)
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)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I

Tactic:
← intervalIntegral.integral_of_le (hai.trans hbi)

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)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: 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 : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this✝ : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
this : ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = {f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)
⊢ μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)

Tactic:
rw [this] at K

Goal state after:
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 : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this✝ : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ {f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)
this : ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = {f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)
⊢ μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)
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
⊢ Tendsto f atTop (𝓝 0)

Tactic:
let F : E →L[ℝ] Completion E := Completion.toComplL
  have Fderiv : ∀ x ∈ Ioi a, HasDerivAt (F ∘ f) (F (f' x)) x :=
    fun x hx ↦ F.hasFDerivAt.comp_hasDerivAt _ (hderiv x hx)
  have Fint : IntegrableOn (F ∘ f) (Ioi a) := by apply F.integrable_comp fint
  have F'int : IntegrableOn (F ∘ f') (Ioi a) := by apply F.integrable_comp f'int
  have A : Tendsto (F ∘ f) atTop (𝓝 (limUnder atTop (F ∘ f))) := by
    apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi Fderiv F'int
  have B : limUnder atTop (F ∘ f) = F 0 := by
    have : IntegrableAtFilter (F ∘ f) atTop := by exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩
    apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
    intro s hs
    rcases mem_atTop_sets.1 hs with ⟨b, hb⟩
    rw [← top_le_iff, ← volume_Ici (a := b)]
    exact measure_mono hb
  rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A
  exact (Completion.isUniformEmbedding_coe E).isEmbedding

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)
⊢ ContinuousOn f (Ici a)

Tactic:
intro x hx

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)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) x
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)
⊢ ContinuousOn g (Ici a)

Tactic:
intro x hx

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)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x ↦ -x
⊢ ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x

Tactic:
intro x hx

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x ↦ -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ HasDerivAt g (-f' (-x)) x
Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
v : E
hf : Continuous f
⊢ MeasurableSet {x | LineDifferentiableAt 𝕜 f x v}

Tactic:
borelize 𝕜
  let g : E → 𝕜 → F := fun x t ↦ f (x + t • v)
  have hg : Continuous g.uncurry := by fun_prop
  exact measurable_prodMk_right (measurableSet_of_differentiableAt_with_param 𝕜 hg)

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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ContinuousOn f (Iic a)

Tactic:
intro x hx

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)
x : ℝ
hx : x ∈ Iic a
⊢ ContinuousWithinAt f (Iic a) x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
x : ℝ
⊢ x ∈ Ioi 0 → ∃ x_1 ∈ Ioi 0, x_1 ^ p = x

Tactic:
exact fun hx ↦ ⟨x ^ (1 / p), rpow_pos_of_pos hx _, by simp [← rpow_mul (le_of_lt hx), hp]⟩

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

Goal state before:
pp: case pos.inr.hf
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
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := ⋯
E' : Type := ⋯
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := ⋯
L_emb : MeasurableEmbedding ⇑L
⊢ ∀ x ∈ tsupport fun x ↦ g (L.symm x), HasLineDerivAt ℝ (fun x ↦ f (L.symm x)) (f' (L.symm x)) x (0, 1)

Tactic:
intro x hx

Goal state after:
case pos.inr.hf
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
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
hx : x ∈ tsupport fun x ↦ g (L.symm x)
⊢ HasLineDerivAt ℝ (fun x ↦ f (L.symm x)) (f' (L.symm x)) x (0, 1)
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: case hg
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
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := ⋯
E' : Type := ⋯
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := ⋯
L_emb : MeasurableEmbedding ⇑L
⊢ ∀ x ∈ tsupport fun x ↦ f (L.symm x), HasLineDerivAt ℝ (fun x ↦ g (L.symm x)) (g' (L.symm x)) x (0, 1)

Tactic:
intro x hx

Goal state after:
case hg
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
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
hx : x ∈ tsupport fun x ↦ f (L.symm x)
⊢ HasLineDerivAt ℝ (fun x ↦ g (L.symm x)) (g' (L.symm x)) x (0, 1)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
⊢ ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x

Tactic:
intro x hx

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
x : ℝ
hx : x ∈ Iio a
⊢ HasDerivAt f (u' x * v x + u x * v' x) x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := ⋯
x : ℝ
hx : x ∈ Iio a
⊢ f =ᶠ[𝓝 x] u * v

Tactic:
filter_upwards [Iio_mem_nhds hx] with x (hx : x < a)

Goal state after:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : ℝ → A := Function.update (u * v) a a'
x✝ : ℝ
hx✝ : x✝ ∈ Iio a
x : ℝ
hx : x < a
⊢ f x = (u * v) x
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
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
A : f '' s =ᵐ[μ] f '' t
⊢ ∀ x ∈ t, HasFDerivWithinAt f (f' x) t x

Tactic:
intro x hx

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
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
A : f '' s =ᵐ[μ] f '' t
x : E
hx : x ∈ t
⊢ HasFDerivWithinAt f (f' x) t x
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e ∈ G.members ∧ e ∈ G'.members

Tactic:
refine And.intro (G.locality' e ?_) (G'.locality' e ?_)

Goal state after:
case refine_1
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members

case refine_2
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case inl
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
hM : IsEmpty M
⊢ IsEmpty M

pp: case inr
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
x : M
⊢ IsEmpty M

Tactic:
· exact hM

Goal state after:
case inr
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
x : M
⊢ IsEmpty M
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ ∀ e ∈ ⋂ s ∈ S, s.members, e.symm ∈ ⋂ s ∈ S, s.members

Tactic:
simp only [mem_iInter]
      intro e he i hi
      exact i.symm' e (he i hi)

Goal state after: