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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
⊢ e.symm.source ∩ ↑e.symm ⁻¹' ∅ = e.symm.source ∩ ∅

Tactic:
preimage_empty

Goal state after:
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
⊢ e.symm.source ∩ ∅ = e.symm.source ∩ ∅
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
⊢ ↑I.symm ⁻¹' ∅ ∩ range ↑I = ∅ ∩ range ↑I

Tactic:
preimage_empty

Goal state after:
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty M
e e' : OpenPartialHomeomorph M H
a✝¹ : e ∈ atlas H M
a✝ : e' ∈ atlas H M
x : E
t : Set E := ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
⊢ ∅ ∩ range ↑I = ∅ ∩ range ↑I
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
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
x : M
f : M → M'
⊢ MapsTo (writtenInExtChartAt I I' x f)
    ((extChartAt I x).target ∩ f ∘ ↑(extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) (extChartAt I' (f x)).target

Tactic:
intro x' hx'
  simpa using (chartAt H' (f x)).mapsTo (by simpa using hx'.2)

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst✝³] u
xu : x ∈ u
this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u
⊢ ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u) (↑I x) ↔
    ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)

Tactic:
apply contDiffWithinAt_inter

Goal state after:
𝕜 : 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst✝³] u
xu : x ∈ u
this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u
⊢ ↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)
Module: Mathlib.Geometry.Manifold.ContMDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
n : ℕ∞ω
f : M → M
hf : ContMDiffOn I I n f s
hmaps : MapsTo f s s
k : ℕ
⊢ ContMDiffOn I I n f^[k] s

Tactic:
induction k with

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'
n : ℕ∞ω
x : M
⊢ ContinuousWithinAt f univ x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) univ x

Tactic:
continuousWithinAt_univ

Goal state after:
𝕜 : 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'
n : ℕ∞ω
x : M
⊢ ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) univ x
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
n : ℕ∞ω
⊢ ContMDiffAt I I' n f x ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_source]

Goal state after:
𝕜 : 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
n : ℕ∞ω
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I)
      (↑(extChartAt I x) x) ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)
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'
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he' : e' ∈ maximalAtlas I' n M'
hy : f x ∈ e'.source
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

Tactic:
contMDiffWithinAt_iff_target_of_mem_maximalAtlas he' (by simpa)

Goal state after:
𝕜 : 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'
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he' : e' ∈ maximalAtlas I' n M'
hy : f x ∈ e'.source
⊢ ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x) ∧
      ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n (↑(e'.extend I') ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.MFDeriv.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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst✝³] u
xu : x ∈ u
this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u
⊢ ↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)

Tactic:
have : u ∈ 𝓝 (I.symm (I x)) := by
        rw [ModelWithCorners.left_inv]
        exact u_open.mem_nhds xu

Goal state after:
𝕜 : 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst✝³] u
xu : x ∈ u
this✝ : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u
this : u ∈ 𝓝 (↑I.symm (↑I x))
⊢ ↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)
Module: Mathlib.Geometry.Manifold.MFDeriv.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
⊢ ContinuousAt f x ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x) ↔
    ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)

Tactic:
congrm _ ∧ ?_

Goal state after:
𝕜 : 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
⊢ DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x) ↔
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: case mp
𝕜 : 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'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiffOn I I' n f s →
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
intro h
    refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
    simp only [mfld_simps] at hz
    let w := (extChartAt I x).symm z
    have : w ∈ s := by simp only [w, hz, mfld_simps]
    specialize h w this
    have w1 : w ∈ (chartAt H x).source := by simp only [w, hz, mfld_simps]
    have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
    convert! ((contMDiffWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _
    · simp only [w, hz, mfld_simps]
    · mfld_set_tac

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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hs : s ⊆ e.source
x : M
hx : x ∈ s
⊢ ↑(e.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(e.extend I) x)] ↑(e.extend I) '' s

Tactic:
simp_rw [e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]

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

Goal state before:
pp: case e'_23
𝕜 : 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
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
⊢ (extChartAt I x).target = ↑I '' (chartAt H x).target

pp: case convert_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
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
⊢ IsManifold I n M

Tactic:
· rw [extChartAt_target, I.image_eq]

Goal state after:
case convert_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
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
⊢ IsManifold I n M
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

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
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x ∈ e.source
⊢ ↑c' X = (↑c' ∘ ↑f ∘ ↑c.symm) (↑c x)

Tactic:
dsimp only [Function.comp_def]

Goal state after:
𝕜 : 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
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x ∈ e.source
⊢ ↑c' X = ↑c' (↑f (↑c.symm (↑c x)))
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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
⊢ ContinuousWithinAt f univ x ∧ MDiffAt[univ] (↑(extChartAt I' (f x)) ∘ f) x ↔
    ContinuousAt f x ∧ MDiffAt[univ] (↑(extChartAt I' (f x)) ∘ f) x

Tactic:
continuousWithinAt_univ

Goal state after:
𝕜 : 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
⊢ ContinuousAt f x ∧ MDiffAt[univ] (↑(extChartAt I' (f x)) ∘ f) x ↔
    ContinuousAt f x ∧ MDiffAt[univ] (↑(extChartAt I' (f x)) ∘ f) x
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B × F₁ × F₂
h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ x) = x

Tactic:
obtain ⟨x, w₁, w₂⟩ := x

Goal state after:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝[s] x
⊢ HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f'

Tactic:
by
  rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq,
    hasFDerivWithinAt_inter', continuousWithinAt_inter' h]
  exact extChartAt_preimage_mem_nhdsWithin h

Goal state after: