mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: 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 = ∅}
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst✝] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this✝ : (e.restr s).source = univ
this : e.source ∩ interior s = univ
⊢ univ ⊆ interior s

Tactic:
by

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

Goal state before:
pp: H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
by

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 M
inst✝² : TopologicalSpace M'
inst✝¹ : TopologicalSpace H
inst✝ : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
q : M'
⊢ q ∈ (hf.localInverseAt (g q) ≫ₕ chartAt H (g q)).source

Tactic:
by

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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
hs : IsOpen[inst✝²] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ e.symm.restr s ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s

Tactic:
by

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 M
inst✝² : TopologicalSpace M'
inst✝¹ : TopologicalSpace H
inst✝ : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
⊢ ∀ (x : M'), hf.localInverseAt (g x) ≫ₕ chartAt H (g x) ∈ {x | ∃ q, hf.localInverseAt (g q) ≫ₕ chartAt H (g q) = x}

Tactic:
by

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[c.toTopologicalSpace] e.source

Tactic:
by

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

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

Tactic:
by

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),
    ∃ δ,
      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:
by

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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
by

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
⊢ ContinuousOn (↑e) e.source

Tactic:
by

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
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
⊢ e' ∈ maximalAtlas M G

Tactic:
by

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

Goal state before:
pp: 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 = ∅}
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst✝] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this✝¹ : (e.restr s).source = univ
this✝ : e.source ∩ interior s = univ
this : univ ⊆ interior s
⊢ s = univ

Tactic:
by

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

Goal state before:
pp: H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ OpenPartialHomeomorph.refl H ∈ atlas H H

Tactic:
by

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

Goal state before:
pp: H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf : f ∈ G
⊢ f ∈ maximalAtlas H G

Tactic:
by

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
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝³] (↑e '' (e.source ∩ s))

Tactic:
by

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
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst✝] s
ts : t = ↑e' ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)

Tactic:
by

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
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
hs'' : IsOpen[inst✝³] (↑e '' (e.source ∩ s))
⊢ (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G

Tactic:
by

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
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
⊢ (e.restr s).symm ≫ₕ e' ∈ G

Tactic:
by

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
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝³] (↑e' '' (e'.source ∩ s))

Tactic:
by

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
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
hs'' : IsOpen[inst✝³] (↑e' '' (e'.source ∩ s))
⊢ IsOpen[inst✝³] (e'.target ∩ ↑e'.symm ⁻¹' s)

Tactic:
by

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
this✝ : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst✝] s
ts : t = ↑e' ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)
⊢ ↑e' ∘ ↑e.symm ⁻¹' s ∩ (e.target ∩ ↑e.symm ⁻¹' e'.source) = e.target ∩ (↑e' ∘ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source)

Tactic:
by

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
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
⊢ e'.symm ≫ₕ e.restr s ∈ G

Tactic:
by

Goal state after:
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
α : Type u_5
inst✝ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x✝ : α
⊢ x✝ ∈ e.source

Tactic:
by

Goal state after:
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
α : Type u_5
inst✝ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x✝ : α
⊢ e ∈ {e}

Tactic:
by

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
⊢ ContinuousOn e.invFun e.target

Tactic:
by

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

Goal state before:
pp: H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ ClosedUnderRestriction G

Tactic:
by

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[c.toTopologicalSpace] e.source

Tactic:
by

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

Goal state before:
pp: H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
⊢ ∀ {e_1 e' : OpenPartialHomeomorph α H}, e_1 ∈ atlas H α → e' ∈ atlas H α → e_1.symm ≫ₕ e' ∈ G

Tactic:
by

Goal state after:
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
G : StructureGroupoid H
inst✝ : HasGroupoid M G
s : Opens M
x : ↥s
⊢ (chartAt H ↑x).subtypeRestr ⋯ ∈ ⋃ x, {(chartAt H ↑x).subtypeRestr ⋯}

Tactic:
by

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

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
s : Opens M
hs : Nonempty ↥s
e : OpenPartialHomeomorph (↥s) H
xset : Set (OpenPartialHomeomorph (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun x ↦ {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ e ∈ {(chartAt H ↑x).subtypeRestr hs}

Tactic:
by

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
s : Opens M
hs : Nonempty ↥s
e : OpenPartialHomeomorph (↥s) H
he : e ∈ atlas H ↥s
⊢ ∃ x, e = (chartAt H ↑x).subtypeRestr hs

Tactic:
by

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 : PartialEquiv M H
x : M
⊢ c.openPartialHomeomorph (c.chartAt x) ⋯ ∈ ⋃ e, ⋃ (he : e ∈ c.atlas), {c.openPartialHomeomorph e he}

Tactic:
by

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

Goal state before:
pp: 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 = ∅}
⊢ e ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

Tactic:
by

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 < ε
δ : (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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
⊢ μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n))

Tactic:
by

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

Goal state before:
pp: H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : e ∈ {OpenPartialHomeomorph.refl H}
⊢ e = e'

Tactic:
by

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 < ε
δ : (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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
⊢ ∑' (n : ℕ), μ (f '' (s ∩ t n)) ≤ ∑' (n : ℕ), (ENNReal.ofReal |(A n).det| + ↑ε) * μ (s ∩ t n)

Tactic:
by

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 < ε
δ : (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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
⊢ ∑' (n : ℕ), (ENNReal.ofReal |(A n).det| + ↑ε) * μ (s ∩ t n) =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + ↑ε ∂μ

Tactic:
by

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

Goal state before:
pp: H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he : e ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
he'e : e' ≈ e
⊢ e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

Tactic:
by

Goal state after:
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
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
s : Opens M
inst✝ : ClosedUnderRestriction G
⊢ ∀ {e e' : OpenPartialHomeomorph (↥s) H}, e ∈ atlas H ↥s → e' ∈ atlas H ↥s → e.symm ≫ₕ e' ∈ G

Tactic:
by

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
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H ↑x
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)

Tactic:
by

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
U : Opens M
x : ↥U
⊢ ↑(chartAt H ↑x).symm =ᶠ[𝓝 (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(chartAt H x).symm

Tactic:
by

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

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
⊢ ∀ (a : StructureGroupoid H), idGroupoid H ≤ a

Tactic:
by

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
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H ↑x
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)

Tactic:
by

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
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ ↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (Set.inclusion hUV x))]
    inclusion hUV ∘ ↑(chartAt H x).symm

Tactic:
by

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 < ε
δ : (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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ |(A n).det| = |(f' x).det - ((f' x).det - (A n).det)|

Tactic:
by

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

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
he' : e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e ≫ₕ e' ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}

Tactic:
by

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.subtypeRestr hs ∈ maximalAtlas (↥s) G

Tactic:
by

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 < ε
δ : (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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
I : |(A n).det| ≤ |(f' x).det| + ↑ε
⊢ ENNReal.ofReal |(A n).det| + ↑ε ≤ ENNReal.ofReal (|(f' x).det| + ↑ε) + ↑ε

Tactic:
by

Goal state after:
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''
M : Type u_5
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : HasGroupoid M G
c c' : OpenPartialHomeomorph M H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M
⊢ c.symm ≫ₕ (Homeomorph.refl M).toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
by

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 < ε
δ : (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) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ 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))
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
I : |(A n).det| ≤ |(f' x).det| + ↑ε
⊢ ENNReal.ofReal (|(f' x).det| + ↑ε) + ↑ε = ENNReal.ofReal |(f' x).det| + 2 * ↑ε

Tactic:
by

Goal state after: