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

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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
j : Fin (2 + 1)
⊢ Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j = 1

Tactic:
fin_cases j

Goal state after:
case «0»
𝕜 : 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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ Fin.cons 1 (Fin.cons 1 fun x ↦ 1) ((fun i ↦ i) ⟨0, ⋯⟩) = 1

case «1»
𝕜 : 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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ Fin.cons 1 (Fin.cons 1 fun x ↦ 1) ((fun i ↦ i) ⟨1, ⋯⟩) = 1

case «2»
𝕜 : 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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ Fin.cons 1 (Fin.cons 1 fun x ↦ 1) ((fun i ↦ i) ⟨2, ⋯⟩) = 1
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
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
⊢ MeasurableSet b

Tactic:
this

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
this : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}
⊢ MeasurableSet (⋃ z ∈ u, s₁ ∩ f ⁻¹' {z})
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x

Tactic:
[

Goal state after:
a b : ℝ
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x • v x + u x • v' x = u b • v b - u a • v a

Tactic:
[

Goal state after:
a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x • v x + u x • v' x = u b • v b - u a • v a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x = ∫ (x : ℝ) in a..b, u' x • v x + u x • v' x - u' x • v x

Tactic:
[

Goal state after:
a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x = ∫ (x : ℝ) in a..b, u' x • v x + u x • v' x - u' x • v x
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
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
[

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
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case inl.inr
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : (s ∩ Ioi a).Nonempty
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
[

Goal state after:
case inl.inr
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : (s ∩ Ioi a).Nonempty
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case inr.inl
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : s ∩ Ioi a = ∅
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
[

Goal state after:
case inr.inl
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : s ∩ Ioi a = ∅
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case inr.inr
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : (s ∩ Ioi a).Nonempty
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
[

Goal state after:
case inr.inr
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : (s ∩ Ioi a).Nonempty
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l
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∞
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)

Tactic:
rcases exists_decomposition_of_monotoneOn_hasDerivWithinAt hs hf hf' with
    ⟨a, b, c, h_union, ha, hb, hc, h_disj, h_disj', a_count, fb_count, deriv_b, deriv_c, inj_c⟩

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
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)
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
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hf' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
this : ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
this

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
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hf' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
this : ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
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
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hf' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
this : ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)

Tactic:
exact lintegral_image_eq_lintegral_abs_det_fderiv_mul _ hc hf' inj_c _

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
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) s volume

Tactic:
rcases exists_decomposition_of_monotoneOn_hasDerivWithinAt hs hf hf' with
    ⟨a, b, c, h_union, ha, hb, hc, h_disj, h_disj', a_count, fb_count, deriv_b, deriv_c, 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
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)

Tactic:
rcases exists_decomposition_of_monotoneOn_hasDerivWithinAt hs hf hf' with
    ⟨a, b, c, h_union, ha, hb, hc, h_disj, h_disj', a_count, fb_count, deriv_b, deriv_c, inj_c⟩

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
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : Countable ι
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Preorder ι
φ : ι → Set α
hφ : AECover μ atTop φ
x : α
h : ∀ᶠ (i : ι) in atTop, x ∈ φ i
⊢ ∀ᶠ (i : ι) in atTop, x ∈ ⋂ k ∈ Ici i, φ k

Tactic:
simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]

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
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:
this

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.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
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
this : ∫ (x : ℝ) in c, f' x • g (f x) = ∫ (x : ℝ) in c, |(F' x).det| • g (f x)
⊢ ∫ (x : ℝ) in f '' c, g x = ∫ (x : ℝ) in c, f' x • g (f x)

Tactic:
this

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
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
this : ∫ (x : ℝ) in c, f' x • g (f x) = ∫ (x : ℝ) in c, |(F' x).det| • g (f x)
⊢ ∫ (x : ℝ) in f '' c, g x = ∫ (x : ℝ) in c, |(F' x).det| • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : 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
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
by_cases! h : ∀ b, ¬ IntegrableOn f (Ici b) μ
  · exact tendsto_const_nhds.congr (fun i => (integral_undef (h (a i))).symm)
  obtain ⟨b, hb⟩ := h
  have : ∀ᶠ i in l, ∫ x in Ici b, f x ∂μ - ∫ x in Ico b (a i), f x ∂μ =
      ∫ x in Ici (a i), f x ∂μ := by
    filter_upwards [ha.eventually_mem (Ici_mem_atTop b)] with i hi
    rw [sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici hb hi]
  rw [← sub_self (∫ x in Ici b, f x ∂μ)]
  exact Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Ici b hb ha)

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
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
B : ⋂ n, Ici ↑n = ∅
L : Tendsto (fun n ↦ ∫ (x : ℝ) in Ici ↑n, ‖f' x‖) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε

Tactic:
exact (tendsto_order.1 L).2 _ εpos

Goal state after:
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 : ℝ) in a..id x, g' y = ∫ (y : ℝ) in a..id x, ‖g' y‖

Tactic:
[

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 = ∫ (y : ℝ) in a..id x, ‖g' y‖