awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑(extChartAt I' (f x)).symm : E' → M'))
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑(extChartAt I' (f x)) : M' → E') (f x))
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑e.symm : E → M))
      ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)
hg₁ :
  let e' := extChartAt I' (f x);
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑e' : M' → E') (f x))
⊢ let e' := extChartAt I' (f x);
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)

Tactic:
set e' := extChartAt I' (f x)

Premises used: extChartAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑e' : M' → E') (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
⊢ (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)

Tactic:
simp only [e, e', mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑e' : M' → E') (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
⊢ (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)

Tactic:
have : e' (f x) = (writtenInExtChartAt I I' x f) (e x) := by simp only [e, e', mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑e' : M' → E') (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
⊢ ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))

Tactic:
rw [this] at hg
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑e' : M' → E') (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
hg₁ :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
⊢ ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)

Tactic:
rw [this] at hg
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ((↑e' : M' → E') (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
hg₁ :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf₁ :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
⊢ (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)

Tactic:
rw [this] at hg
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
simp :
  ∀ᶠ (a : M) in 𝓝[s] x,
    f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ t ∧
      f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ e'.source
⊢ ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source

Tactic:
simp only [e, ← map_extChartAt_nhdsWithin, eventually_map]

Premises used: Filter.eventually_map, map_extChartAt_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
h :
  ∀ a ∈ f ⁻¹' (extChartAt I' (f x)).source,
    a ∈ s ∩ (extChartAt I x).source →
      f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ t ∧
        f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ e'.source
⊢ ∀ᶠ (a : M) in 𝓝[s] x,
    f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ t ∧
      f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ e'.source

Tactic:
filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds (I := I') (f x)),
      inter_mem_nhdsWithin s (extChartAt_source_mem_nhds (I := I) x)]

Premises used: inter_mem_nhdsWithin, extChartAt_source_mem_nhds, And.left, ContinuousWithinAt.tendsto
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
x' : M
hfx' : f x' ∈ e'.source
hx's : x' ∈ s
hx' : x' ∈ (extChartAt I x).source
⊢ f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x')) ∈ t ∧
    f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x')) ∈ e'.source

Tactic:
simp only [e, true_and, e.left_inv hx', st hx's, *]

Premises used: PartialEquiv.left_inv, true_and
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
⊢ ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source

Tactic:
have A : ∀ᶠ y in 𝓝[e.symm ⁻¹' s ∩ range I] e x, f (e.symm y) ∈ t ∧ f (e.symm y) ∈ e'.source := by
    simp only [e, ← map_extChartAt_nhdsWithin, eventually_map]
    filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds (I := I') (f x)),
      inter_mem_nhdsWithin s (extChartAt_source_mem_nhds (I := I) x)]
    rintro x' (hfx' : f x' ∈ e'.source) ⟨hx's, hx'⟩
    simp only [e, true_and, e.left_inv hx', st hx's, *]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M))
    ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)

Tactic:
((hg.2.comp _ (hf.2.mono inter_subset_right)
      ((mapsTo_preimage _ _).mono_left inter_subset_left)).mono_of_mem_nhdsWithin
      (inter_mem ?_ self_mem_nhdsWithin)).congr_of_eventuallyEq ?_ ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Filter.inter_mem, ContDiffWithinAt.comp, Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left, And.right, self_mem_nhdsWithin, ContDiffWithinAt.congr_of_eventuallyEq, Set.inter_subset_right, ContDiffWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : 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))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
refine_1 :
  writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ∈
    𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x
refine_2 :
  (↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘
      (g ∘ f) ∘ (↑e.symm : E → M) =ᶠ[𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x]
    ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f
refine_3 :
  ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M)) ((↑e : M → E) x) =
    (((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f)
      ((↑e : M → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M))
    ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)

Tactic:
refine ((hg.2.comp _ (hf.2.mono inter_subset_right)
      ((mapsTo_preimage _ _).mono_left inter_subset_left)).mono_of_mem_nhdsWithin
      (inter_mem ?_ self_mem_nhdsWithin)).congr_of_eventuallyEq ?_ ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Filter.inter_mem, ContDiffWithinAt.comp, Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left, And.right, self_mem_nhdsWithin, ContDiffWithinAt.congr_of_eventuallyEq, Set.inter_subset_right, ContDiffWithinAt.mono