mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

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

Tactic:
rcases hx.2 with ⟨p, q, ps₁, qs₁, pq, hp, hq⟩

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

Goal state before:
pp: a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] b) l

Tactic:
exact HasDerivAt.lhopital_zero_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfb hgb hdiv

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

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

Tactic:
apply UniqueDiffWithinAt.eq_deriv _ _ K' K

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

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

Tactic:
apply UniqueDiffWithinAt.eq_deriv _ _ K' K

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := ⋯
a_count : a.Countable
s₁ : Set ℝ := ⋯
hs₁ : MeasurableSet s₁
u : Set ℝ := ⋯
hu : u.Countable
b : Set ℝ := ⋯
hb : MeasurableSet b
c : Set ℝ := ⋯
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
⊢ UniqueDiffWithinAt ℝ (s ∩ Ioo x p) x
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:
simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[<] a) l ∧ Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x ↦ f x / g x) (𝓝[>] 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∞
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:
rw [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: 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:
rw [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: case hfi
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ Integrable (fun x ↦ ‖f x‖) (volume.restrict (Ioc (a i) (b i)))

Tactic:
exact (hfi i).norm

Goal state after:
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
⊢ ∫ (x : ℝ) in Icc a b, f' x • g (f x) = ∫ (u : ℝ) in Icc (f a) (f b), g u

Tactic:
by
  have M : MonotoneOn f (Icc a b) := by
    apply monotoneOn_of_deriv_nonneg (convex_Icc a b) hf
    · rw [interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt
    · rw [interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz
  have A : ∫ u in Icc (f a) (f b), g u = ∫ u in f '' (Ioo a b), g u := by
    apply setIntegral_congr_set
    rw [← hf.image_Icc_of_monotoneOn hab M]
    refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩
    have : f '' (Icc a b) \ f '' Ioo a b ⊆ {f a, f b} := by grind
    apply measure_mono_null this
    apply Finite.measure_zero (by simp)
  rw [A, integral_Icc_eq_integral_Ioo,
    integral_image_eq_integral_deriv_smul_of_monotoneOn measurableSet_Ioo]
  · exact fun z hz ↦ (hff' z hz).hasDerivWithinAt
  · exact M.mono Ioo_subset_Icc_self

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
a : (fun x ↦ x ^ p) '' Ioi 0 = Ioi 0
this : ∫ (x : ℝ) in Ioi 0, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y

Tactic:
rw [this]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
a : (fun x ↦ x ^ p) '' Ioi 0 = Ioi 0
this : ∫ (x : ℝ) in Ioi 0, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr
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
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
⊢ μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)

Tactic:
obtain ⟨t, A, t_disj, t_meas, t_cover, ht, Af'⟩ :
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
      Pairwise (Disjoint on t) ∧
        (∀ n : ℕ, MeasurableSet (t n)) ∧
          (s ⊆ ⋃ n : ℕ, t n) ∧
            (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧
              (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
    exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'

Goal state after:
case inr
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
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x ↦ x ^ p) S
a3 : (fun t ↦ t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Tactic:
rw [this]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x ↦ x ^ p) S
a3 : (fun t ↦ t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔
    IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
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 : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ n, s ∩ t n
| μ.restrict s

Tactic:
rw [this]

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 : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ n, s ∩ t n
| μ.restrict (⋃ n, s ∩ t n)
Module: Mathlib.Geometry.Manifold.StructureGroupoid

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

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

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

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[inst✝] e.target

Tactic:
convert! c.open_target he

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
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
s : Opens M
hs : Nonempty ↥s
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
e' : OpenPartialHomeomorph (↥s) H
he' : e' ∈ atlas H ↥s
x : ↥s
this : e' = (chartAt H ↑x).subtypeRestr hs
⊢ (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
rw [this]

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
s : Opens M
hs : Nonempty ↥s
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
e' : OpenPartialHomeomorph (↥s) H
he' : e' ∈ atlas H ↥s
x : ↥s
this : e' = (chartAt H ↑x).subtypeRestr hs
⊢ (e.subtypeRestr hs).symm ≫ₕ (chartAt H ↑x).subtypeRestr hs ∈ G ∧
    ((chartAt H ↑x).subtypeRestr hs).symm ≫ₕ e.subtypeRestr hs ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
have open_s : IsOpen s := by
        apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage <;> apply open_source

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
open_s : IsOpen[inst✝⁶] s
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr 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'
P : (H → H') → Set H → H → Prop
f : M → M'
x : M
⊢ LiftPropAt P f x ↔ ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
by
  rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen[inst✝] s
⊢ UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)

Tactic:
exact I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun)

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv))
  else range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv) = univ

Tactic:
rw [PartialEquiv.pi_apply, Set.range_piMap]
    split_ifs with h
    · let := h.rclike
      let := fun i ↦ NormedSpace.restrictScalars ℝ 𝕜 (E i)
      exact convex_pi fun i _hi ↦ (I i).convex_range
    · simp [range_eq_univ_of_not_isRCLikeNormedField, h]

Goal state after:
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'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ LiftPropAt P f ↑x ↔ LiftPropAt P (f ∘ Subtype.val) x

Tactic:
simp only [LiftPropAt, liftPropWithinAt_iff']

Goal state after:
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'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ ContinuousWithinAt f univ ↑x ∧
      P (↑(chartAt H' (f ↑x)) ∘ f ∘ ↑(chartAt H ↑x).symm) (↑(chartAt H ↑x).symm ⁻¹' univ) (↑(chartAt H ↑x) ↑x) ↔
    ContinuousWithinAt (f ∘ Subtype.val) univ x ∧
      P (↑(chartAt H' ((f ∘ Subtype.val) x)) ∘ (f ∘ Subtype.val) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ)
        (↑(chartAt H x) x)