mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.RemovableSingularity

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

Tactic:
have h1 : ContinuousOn (fun z : ℂ => ((z - w₀) ^ 2)⁻¹) (sphere c R) := by
      refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_
      exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))
    have h2 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f z) c R := by
      refine ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_
      exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))
    have h3 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f w₀) c R :=
      ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le (h1.smul continuousOn_const)
    have h4 : (∮ z : ℂ in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0 := by
      simpa using! circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R
    simp only [smul_sub, circleIntegral.integral_sub h2 h3, h4, circleIntegral.integral_smul_const,
      zero_smul, sub_zero]

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
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
refine aemeasurable_of_unif_approx fun ε εpos => ?_

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
⊢ ∃ f, AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
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
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U

Tactic:
by
  rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
  rcases φ.eq_or_neBot with rfl | hne
  · simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
  rintro K hKU hK
  obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
  refine h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ ?_
  exact (closedBall_subset_cthickening hz δ).trans hK4

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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
⊢ ∃ δ', 0 < δ' ∧ ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε

Tactic:
by
      refine continuousAt_iff.1 ?_ ε εpos
      exact ContinuousLinearMap.continuous_det.continuousAt

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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
⊢ ∃ δ,
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t

Tactic:
refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩

Goal state after:
case refine_1
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
⊢ ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(min δ δ'') → |B.det - A.det| ≤ ↑ε

case refine_2
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
⊢ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (min δ δ'') → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t
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
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
this :
  Tendsto (fun ε ↦ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0)
    (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))
ε : ℝ≥0
εpos : ε ∈ Ioi 0
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s

Tactic:
rw [mem_Ioi] at εpos

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
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
this :
  Tendsto (fun ε ↦ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0)
    (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))
ε : ℝ≥0
εpos : 0 < ε
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
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 < ε
A : E →L[ℝ] E
⊢ ∃ δ', 0 < δ' ∧ ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε

Tactic:
by
      refine continuousAt_iff.1 ?_ ε εpos
      exact ContinuousLinearMap.continuous_det.continuousAt

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

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst✝] s
⊢ ofSet s hs ≫ₕ e ∈ G

Tactic:
refine G.trans ?_ he

Goal state after:
case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst✝] s
⊢ ofSet s 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 : OpenPartialHomeomorph M H
he : e ∈ atlas H M
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
⊢ let s := { carrier := e.source, is_open' := ⋯ };
  let t := { carrier := e.target, is_open' := ⋯ };
  Structomorph G ↥s ↥t

Tactic:
intro s t

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 : OpenPartialHomeomorph M H
he : e ∈ atlas H M
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
⊢ Structomorph G ↥s ↥t
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f (s ∩ o) x ↔ P f t x

Tactic:
host,

Goal state after:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f (t ∩ o) x ↔ P f t x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x | f x = g x}) x ↔ P g (s ∩ {x | f x = g x}) x

Tactic:
exact ⟨hG.congr_of_forall (fun y hy ↦ hy.2) h2, hG.congr_of_forall (fun y hy ↦ hy.2.symm) h2.symm⟩

Goal state after:
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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
⊢ ∃ δ,
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t

Tactic:
refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩

Goal state after:
case inr.refine_1
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 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
⊢ ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(min δ δ'') → |B.det - A.det| ≤ ↑ε

case inr.refine_2
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 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
⊢ ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g A t (min δ δ'') → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t
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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
⊢ ∀ᶠ (z : E) in 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y, (g ∘ ↑(f.extend I).symm) z ∈ f'.source

Tactic:
rw [← f.map_extend_nhdsWithin (I := I) hy, eventually_map]

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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
⊢ ∀ᶠ (a : M) in 𝓝[s] y, (g ∘ ↑(f.extend I).symm) (↑(f.extend I) a) ∈ f'.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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] z = 𝓝[range ↑I] z

Tactic:
rw [← PartialEquiv.right_inv (extChartAt I x) hz]
  exact nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

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
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this : Tendsto (fun ε ↦ μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))
ε : ℝ≥0
εpos : ε ∈ Ioi 0
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s

Tactic:
rw [mem_Ioi] at εpos

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
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this : Tendsto (fun ε ↦ μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))
ε : ℝ≥0
εpos : 0 < ε
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
Module: Mathlib.Geometry.Manifold.ContMDiff.Basic

Goal state before:
pp: case hi
𝕜 : 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'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst✝⁷] s
y : M
hy : y ∈ s
⊢ y ∉ (closure[inst✝⁷] s)ᶜ

Tactic:
simpa using subset_closure hy

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

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
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H 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'
inst✝¹ : ChartedSpace H' M'
f : M → M'
x : M
y : M'
n : ℕ∞ω
inst✝ : IsManifold I' n M'
hy : f x ∈ (chartAt H' y).source
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) x

Tactic:
rw [ContMDiffAt, contMDiffWithinAt_iff_target_of_mem_source hy, continuousWithinAt_univ,
    ContMDiffAt]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
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
g : E → F
⊢ IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x ↦ |(f' x).det| • g (f x)) s μ

Tactic:
rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
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
g : E → F
⊢ Integrable (g ∘ s.domRestrict f) (Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) ↔
    IntegrableOn (fun x ↦ |(f' x).det| • g (f x)) s μ
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H 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'
inst✝ : ChartedSpace H' M'
f : M → M'
⊢ ContMDiff I I' 0 f ↔ Continuous[inst✝⁶, inst✝¹] f

Tactic:
by
  rw [← contMDiffOn_univ, ← continuousOn_univ, contMDiffOn_zero_iff]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u_1
F : Type u_2
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : Zero F
b : B
f : F
⊢ (trivialization B F).symm b f = f

Tactic:
by
  simp [trivialization, homeomorphProd, TotalSpace.toProd, Trivialization.symm,
    Pretrivialization.symm, Trivialization.toPretrivialization]

Goal state after:
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : TopologicalSpace B
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜₁
inst✝⁴ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst✝³ : TopologicalSpace B'
inst✝² : NormedSpace 𝕜₁ F
F' : Type u_8
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜₂ F'
ι : Type u_10
ι' : Type u_11
Z : VectorBundleCore 𝕜₁ B F ι
Z' : VectorBundleCore 𝕜₂ B' F' ι'
x₀ x : B
y₀ y : B'
ϕ : F →SL[σ] F'
hx : x ∈ Z.baseSet (Z.indexAt x₀)
hy : y ∈ Z'.baseSet (Z'.indexAt y₀)
⊢ inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
    Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x

Tactic:
by
  simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy,
    Z.trivializationAt_symmL hx]

Goal state after: