-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem contDiffOn_fderiv_coord_change [IsManifold I (n + 1) M]
    (i j : atlas H M) :
    ContDiffOn 𝕜 n (fderivWithin 𝕜 (j.1.extend I ∘ (i.1.extend I).symm) (range I))
      ((i.1.extend I).symm ≫ j.1.extend I).source

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ContDiffWithinAt 𝕜 (n + 1) (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x

Tactic:
refine (PartialHomeomorph.contDiffOn_extend_coord_change (subset_maximalAtlas j.2)
  (subset_maximalAtlas i.2) x hx).mono_of_mem_nhdsWithin ?_

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ (((↑i).extend I).symm ≫ (↑j).extend I).source ∈ 𝓝[range ↑I] x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
⊢ (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I

Tactic:
rw [i.1.extend_coord_change_source]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
⊢ ↑I '' ((↑i).symm ≫ₕ ↑j).source ⊆ range ↑I

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ContDiffWithinAt 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I))
    (((↑i).extend I).symm ≫ (↑j).extend I).source x

Tactic:
refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
  <| h hx).mono h

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ContDiffWithinAt 𝕜 (n + 1) (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
⊢ ↑I '' ((↑i).symm ≫ₕ ↑j).source ⊆ range ↑I

Tactic:
apply image_subset_range

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
⊢ ContDiffOn 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I))
    (((↑i).extend I).symm ≫ (↑j).extend I).source

Tactic:
have h : ((i.1.extend I).symm ≫ j.1.extend I).source ⊆ range I := by
  rw [i.1.extend_coord_change_source]; apply image_subset_range

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
⊢ ContDiffOn 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I))
    (((↑i).extend I).symm ≫ (↑j).extend I).source

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
⊢ ContDiffOn 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I))
    (((↑i).extend I).symm ≫ (↑j).extend I).source

Tactic:
intro x hx

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ContDiffWithinAt 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I))
    (((↑i).extend I).symm ≫ (↑j).extend I).source x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ (((↑i).extend I).symm ≫ (↑j).extend I).source ∈ 𝓝[range ↑I] x

Tactic:
exact i.1.extend_coord_change_source_mem_nhdsWithin j.1 hx

Result:
no goals