awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
refine_3 :
  ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
rw [contMDiffWithinAt_iff_contDiffWithinAt]

Premises used: contMDiffWithinAt_iff_contDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I) : M → E) '' s) ↔
    ContMDiffOn I J n f s

Tactic:
forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr, Iff.trans, Set.forall_mem_image, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
refine :
  ∀ (x : M) (hx : x ∈ s),
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
        ((↑(φ.extend I) : M → E) '' s) ((↑(φ.extend I) : M → E) x) ↔
      ContMDiffWithinAt I J n f s x
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I) : M → E) '' s) ↔
    ContMDiffOn I J n f s

Tactic:
refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr, Iff.trans, Set.forall_mem_image
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
x : M
hx : x ∈ s
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I) : M → E) '' s) ((↑(φ.extend I) : M → E) x) ↔
    ContMDiffWithinAt I J n f s x

Tactic:
(contMDiffWithinAt_congr_set ?_).trans
    (contMDiffWithinAt_writtenInExtend_iff hφ hψ (hs hx) (hmaps hx) hmaps)

Premises used: contMDiffWithinAt_congr_set, Iff.trans, OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
x : M
hx : x ∈ s
refine :
  (↑(φ.extend I) : M → E) '' s =ᶠ[nhds ((↑(φ.extend I) : M → E) x)]
    (↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I) : M → E) '' s) ((↑(φ.extend I) : M → E) x) ↔
    ContMDiffWithinAt I J n f s x

Tactic:
refine (contMDiffWithinAt_congr_set ?_).trans
    (contMDiffWithinAt_writtenInExtend_iff hφ hψ (hs hx) (hmaps hx) hmaps)

Premises used: contMDiffWithinAt_congr_set, Iff.trans, OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
x : M
hx : x ∈ s
rw hy : x ∈ φ.source
hs₁ : s ⊆ φ.source
⊢ (↑(φ.extend I) : M → E) '' s =ᶠ[nhds ((↑(φ.extend I) : M → E) x)]
    (↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq, ← φ.map_extend_nhdsWithin_eq_image_of_subset,
    ← φ.map_extend_nhdsWithin]

Premises used: OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset, nhdsWithin_eq_iff_eventuallyEq, OpenPartialHomeomorph.map_extend_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
x : M
hx : x ∈ s
⊢ x ∈ φ.source

Tactic:
hs hx
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
x : M
hx : x ∈ s
⊢ s ⊆ φ.source

Tactic:
hs
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
inst_5 : ChartedSpace H M
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hs : s ⊆ φ.source
hmaps : MapsTo f s ψ.source
x : M
hx : x ∈ s
⊢ x ∈ φ.source

Tactic:
exacts [hs hx, hs hx, hs]
-- 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 : ContMDiffWithinAt I' I'' n g t (f x)
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
rw :
  ∀
    (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)))
    (hf :
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (st : MapsTo f s t),
    ContinuousWithinAt (g ∘ f) s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
rw [contMDiffWithinAt_iff] at hg hf ⊢

Premises used: contMDiffWithinAt_iff
-- 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))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
st : MapsTo f s t
⊢ ContinuousWithinAt (g ∘ f) s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
⟨hg.1.comp hf.1 st, ?_⟩

Premises used: And.left, And.intro, ContinuousWithinAt.comp
-- 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))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
st : MapsTo f s t
refine :
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (g ∘ f) s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
refine ⟨hg.1.comp hf.1 st, ?_⟩
-- 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))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
st : MapsTo f s t
set :
  let 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)),
    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)
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
set e := extChartAt I 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
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)
⊢ 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))

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

Premises used: extChartAt