awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
⊢ 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) ↔
    ContMDiffWithinAt I J n f s y
have rw : 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) ↔
  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)
Tactic: rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hφ hψ hy hgy]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
⊢ 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) ↔
    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)
have refine_1 : ∀
  (h :
    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)),
  ContinuousWithinAt f s y
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
refine_1 :
  ∀
    (h :
      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)),
    ContinuousWithinAt f s 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) ↔
    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)
have refine_2 : ∀
  (h :
    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)),
  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: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
refine_1 :
  ∀
    (h :
      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)),
    ContinuousWithinAt f s y
refine_2 :
  ∀
    (h :
      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)),
    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) ↔
    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)
have refine_3 : ∀
  (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)),
  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: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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 :
  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)
⊢ ContinuousWithinAt f s y
have refine_1 : ContinuousWithinAt ((↑(ψ.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 [← φ.continuousWithinAt_writtenInExtend_iff (I := I) (I' := J) hy hgy hmaps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [contMDiffWithinAt_iff_contDiffWithinAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
have 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
Tactic: refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
have refine : (↑(φ.extend I) : M → E) '' s =ᶠ[nhds ((↑(φ.extend I) : M → E) x)]
  (↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: refine (contMDiffWithinAt_congr_set ?_).trans
    (contMDiffWithinAt_writtenInExtend_iff hφ hψ (hs hx) (hmaps hx) hmaps)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Atlas (goal)
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
⊢ (↑(φ.extend I) : M → E) '' s =ᶠ[nhds ((↑(φ.extend I) : M → E) x)]
    (↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
have rw : x ∈ φ.source
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq, ← φ.map_extend_nhdsWithin_eq_image_of_subset,
    ← φ.map_extend_nhdsWithin]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x
have 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)
Tactic: rw [contMDiffWithinAt_iff] at hg hf ⊢
Cleared hypotheses: hg, hf, st
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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)
have 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)
Tactic: refine ⟨hg.1.comp hf.1 st, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (goal)
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
⊢ 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)
have 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)
Tactic: set e := extChartAt I x
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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)
⊢ 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)
have this : (↑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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (hypothesis)
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)
⊢ 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)
have 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))
Tactic: rw [this] at hg
Cleared hypotheses: hg, hf, this