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

Goal state before:
pp: case inr.refine_2.inl
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
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : μ t = ∞
⊢ ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t

pp: case inr.refine_2.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 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : μ t ≠ ∞
⊢ ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t

Tactic:
·

Goal state after:
case inr.refine_2.inl
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
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : μ t = ∞
⊢ ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t
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)
⊢ ContinuousWithinAt f s x

pp: case refine_2
𝕜 : 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 s x
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)

Tactic:
·

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)
⊢ ContinuousWithinAt f s x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case refine_2
𝕜 : 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 s x
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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 s x
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I 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
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn 𝕜 (extendCoordChange e e').source

Tactic:
by
  rw [extendCoordChange_source, I.image_eq]
  exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I ×ˢ range ↑I' = univ

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I ×ˢ range ↑I' = univ

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I ×ˢ range ↑I' = univ
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_1
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ fderivWithin 𝕜 (↑φ) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm) φ.target (↑φ x) = ContinuousLinearMap.id 𝕜 E

pp: case refine_2
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ fderivWithin 𝕜 (↑φ.symm) φ.target (↑φ x) ∘SL fderivWithin 𝕜 (↑φ) φ.source x = ContinuousLinearMap.id 𝕜 E

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ fderivWithin 𝕜 (↑φ) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm) φ.target (↑φ x) = ContinuousLinearMap.id 𝕜 E
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case pos
𝕜 : 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)
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv)

pp: case neg
𝕜 : 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)
h : ¬IsRCLikeNormedField 𝕜
⊢ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv) = univ

Tactic:
·

Goal state after:
case pos
𝕜 : 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)
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case neg
𝕜 : 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)
h : ¬IsRCLikeNormedField 𝕜
⊢ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv) = univ

Tactic:
·

Goal state after:
case neg
𝕜 : 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)
h : ¬IsRCLikeNormedField 𝕜
⊢ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv) = univ
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_1.hg
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ) φ.source (↑φ.symm (↑φ x))

pp: case refine_1.hf
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm) φ.target (↑φ x)

pp: case refine_1.h
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ MapsTo (↑φ.symm) φ.target φ.source

pp: case refine_1.hxs
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.target (↑φ x)

Tactic:
·

Goal state after:
case refine_1.hg
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ) φ.source (↑φ.symm (↑φ x))
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_1.hf
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm) φ.target (↑φ x)

pp: case refine_1.h
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ MapsTo (↑φ.symm) φ.target φ.source

pp: case refine_1.hxs
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.target (↑φ x)

Tactic:
·

Goal state after:
case refine_1.hf
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm) φ.target (↑φ x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_1
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 ↔ ContinuousWithinAt (f ∘ Subtype.val) univ x

pp: case refine_2
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
⊢ P (↑(chartAt H' (f ↑x)) ∘ f ∘ ↑(chartAt H ↑x).symm) (↑(chartAt H ↑x).symm ⁻¹' univ) (↑(chartAt H ↑x) ↑x) ↔
    P (↑(chartAt H' ((f ∘ Subtype.val) x)) ∘ (f ∘ Subtype.val) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ)
      (↑(chartAt H x) x)

Tactic:
·

Goal state after:
case refine_1
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 ↔ ContinuousWithinAt (f ∘ Subtype.val) univ x
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_1.h
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ MapsTo (↑φ.symm) φ.target φ.source

pp: case refine_1.hxs
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.target (↑φ x)

Tactic:
·

Goal state after:
case refine_1.h
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ MapsTo (↑φ.symm) φ.target φ.source
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: case refine_1.hxs
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.target (↑φ x)

Tactic:
·

Goal state after:
case refine_1.hxs
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.target (↑φ x)