mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
B : atTop.limUnder (⇑F ∘ f) = F 0
⊢ Tendsto f atTop (𝓝 0)

Tactic:
B,

Goal state after:
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
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (F 0))
B : atTop.limUnder (⇑F ∘ f) = F 0
⊢ Tendsto f atTop (𝓝 0)
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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (atBot.limUnder (⇑F ∘ f)))
B : atBot.limUnder (⇑F ∘ f) = F 0
⊢ Tendsto f atBot (𝓝 0)

Tactic:
B,

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (F 0))
B : atBot.limUnder (⇑F ∘ f) = F 0
⊢ Tendsto f atBot (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := ⇑I ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
⊢ ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ

Tactic:
← HasCompactSupport.integral_Iic_deriv_eq hf' h'f' x

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := ⇑I ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
⊢ ‖∫ (x : ℝ) in Iic x, deriv f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
by
    have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
    have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
    refine
      intervalIntegral.integral_deriv_smul_comp''' (hf.mono i2)
        (fun x hx => hff' x <| mem_of_mem_of_subset hx i1) (hg_cont.mono <| image_mono ?_)
        (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2) <;> assumption

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 : 0 < p
c : ℝ
hc : 0 ≤ c
this✝ : 0 ≤ c ^ p⁻¹
this : Ioi c = (fun x ↦ x ^ p) '' Ioi (c ^ p⁻¹)
x : ℝ
x✝ : x ∈ Ioi (c ^ p⁻¹)
⊢ (p * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)

Tactic:
have : 0 ≤ x := by grind

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
c : ℝ
hc : 0 ≤ c
this✝¹ : 0 ≤ c ^ p⁻¹
this✝ : Ioi c = (fun x ↦ x ^ p) '' Ioi (c ^ p⁻¹)
x : ℝ
x✝ : x ∈ Ioi (c ^ p⁻¹)
this : 0 ≤ x
⊢ (p * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x

Tactic:
have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi
  rw [← integral_indicator (this _), ← integral_indicator (this _),
    ← abs_of_pos (inv_pos.mpr hb), ← Measure.integral_comp_mul_left]
  congr
  ext1 x
  rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ hb, mul_div_cancel_left₀ _ hb.ne',
    Function.comp_def]

Goal state after:
Module: Mathlib.Analysis.Complex.RemovableSingularity

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

Tactic:
set F : ℂ → E := fun z => (z - c) • f z

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
F : ℂ → E := fun z ↦ (z - c) • f z
⊢ DifferentiableOn ℂ (update f c ((𝓝[≠] c).limUnder f)) s
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 ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'

Tactic:
by
  rw [← Ici_sdiff_left] at h_zero
  let f := Function.update (u * v) a a'
  have hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x := by
    intro x (hx : a < x)
    apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
    filter_upwards [eventually_ne_nhds hx.ne.symm] with y hy
    exact Function.update_of_ne hy a' (u * v)
  have htendsto : Tendsto f atTop (𝓝 b') := by
    apply h_infty.congr'
    filter_upwards [eventually_ne_atTop a] with x hx
    exact (Function.update_of_ne hx a' (u * v)).symm
  simpa using integral_Ioi_of_hasDerivAt_of_tendsto
    (continuousWithinAt_update_same.mpr h_zero) hderiv huv htendsto

Goal state after:
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ
e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε

Tactic:
have hf : ContinuousOn f (sphere z δ) :=
    e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))

Goal state after:
E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ
e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
hf : ContinuousOn f (sphere z δ)
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝¹ : CompleteSpace E
inst✝ : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
⊢ DifferentiableWithinAt ℂ f U x

Tactic:
have h2 : interior K ⊆ U := interior_subset.trans hKU

Goal state after:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝¹ : CompleteSpace E
inst✝ : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
⊢ DifferentiableWithinAt ℂ f U 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),
    (∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members) → e ∈ G.members ∩ G'.members

Tactic:
intro e hx
      apply (mem_inter_iff e G.members G'.members).mpr
      refine And.intro (G.locality' e ?_) (G'.locality' e ?_)
      all_goals
        intro x hex
        rcases hx x hex with ⟨s, hs⟩
        use s
        refine And.intro hs.left (And.intro hs.right.left ?_)
      · exact hs.right.right.left
      · exact hs.right.right.right

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

Goal state before:
pp: case inl
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
h : e.source = ∅
⊢ e ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

pp: case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
h : e.source.Nonempty
⊢ e ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

Tactic:
· right
      exact h

Goal state after:
case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
h : e.source.Nonempty
⊢ e ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
⊢ s = ⋃ n, s ∩ u n

Tactic:
rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.extend I)) (f.extend I).source

Tactic:
refine I.continuous.comp_continuousOn ?_

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) (f.extend I).source
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ map (↑I ∘ ↑f) (𝓝 x) = map (↑I) (𝓝 (↑f x))

Tactic:
← f.map_nhds_eq,

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ map (↑I ∘ ↑f) (𝓝 x) = map (↑I) (map (↑f) (𝓝 x))

𝕜 : 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ x ∈ f.source
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 : OpenPartialHomeomorph M H
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
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hgs : ContinuousWithinAt g s x
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
rw [← Function.comp_assoc,
    hG.liftPropWithinAt_indep_chart_source_aux ((chartAt H' (g x)) ∘ g) he xe,
    Function.comp_assoc, hG.liftPropWithinAt_indep_chart_target_aux 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ ContinuousWithinAt (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) (↑(f.extend I) x) ↔
    ContinuousWithinAt g s x

Tactic:
refine (continuousWithinAt_congr_set ?_).trans
    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ ↑(f.extend I) '' s =ᶠ[𝓝 (↑(f.extend I) x)] ↑(f.extend I).symm ⁻¹' s ∩ range ↑I
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑I.symm) ∘ ↑I) (↑I ⁻¹' ↑I.symm ⁻¹' s ∩ ↑I ⁻¹' range ↑I) x
⊢ ContinuousWithinAt f s x

Tactic:
preimage_preimage,

Goal state after:
case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑I.symm) ∘ ↑I) ((fun x ↦ ↑I.symm (↑I x)) ⁻¹' s ∩ ↑I ⁻¹' range ↑I) x
⊢ ContinuousWithinAt f s x
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
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ ↑((chartAt H x).extend I) '' s ∈ 𝓝 (↑((chartAt H x).extend I) x)

Tactic:
exact extend_image_nhds_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx

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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ 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))
s_eq : s = ⋃ n, s ∩ t n
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ ENNReal.ofReal |(f' x).det| ≤ ENNReal.ofReal |(A n).det| + ↑ε

Tactic:
have I : |(f' x).det| ≤ |(A n).det| + ε :=
        calc
          |(f' x).det| = |(A n).det + ((f' x).det - (A n).det)| := by congr 1; abel
          _ ≤ |(A n).det| + |(f' x).det - (A n).det| := abs_add_le _ _
          _ ≤ |(A n).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ 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 : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ 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))
s_eq : s = ⋃ n, s ∩ t n
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
I : |(f' x).det| ≤ |(A n).det| + ↑ε
⊢ ENNReal.ofReal |(f' x).det| ≤ ENNReal.ofReal |(A n).det| + ↑ε
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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ 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))
s_eq : s = ⋃ n, s ∩ t n
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
I : |(f' x).det| ≤ |(A n).det| + ↑ε
⊢ ENNReal.ofReal (|(A n).det| + ↑ε) = ENNReal.ofReal |(A n).det| + ↑ε

Tactic:
by
          simp only [ENNReal.ofReal_add, abs_nonneg, NNReal.zero_le_coe, ENNReal.ofReal_coe_nnreal]

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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ (interior (extChartAt I x).target).Nonempty

Tactic:
by_contra! H
  have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)
  simp only [H, closure_empty, mem_empty_iff_false] at this

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

Goal state before:
pp: case refine_3
𝕜 : 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
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑e x))
hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)
A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source
⊢ (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e x) =
    ((↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) ∘ writtenInExtChartAt I I' x f) (↑e x)

Tactic:
simp only [e, e', writtenInExtChartAt, (· ∘ ·), mem_extChartAt_source,
      e.left_inv, e'.left_inv]

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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
⊢ s = ⋃ n, s ∩ u n

Tactic:
rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]

Goal state after: