-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma tangentBundleCore.isContMDiff [h : IsManifold I (n + 1) M] :
    haveI : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
    (tangentBundleCore I M).IsContMDiff I n

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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ (tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j ⊆ (↑i).source

Tactic:
apply inter_subset_left

Result:
no goals

Proof state:
case refine_1
𝕜 : 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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
x : E
hx : x ∈ ((↑i).extend I).symm.source ∩ ↑((↑i).extend I).symm ⁻¹' (((↑i).extend I).symm.target ∩ ((↑j).extend I).source)
⊢ ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm) x =
    fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x

Tactic:
simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]

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
h : IsManifold I (n + 1) M
this : IsManifold I n M
⊢ (tangentBundleCore I M).IsContMDiff I n

Tactic:
refine ⟨fun i j => ?_⟩

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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContMDiffOn I 𝓘(𝕜, E →L[𝕜] E) n ((tangentBundleCore I M).coordChange i j)
    ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j)

Proof state:
case refine_1
𝕜 : 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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm) x =
    fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x

Tactic:
rw [PartialEquiv.trans_source'] at hx

Result:
case refine_1
𝕜 : 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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
x : E
hx : x ∈ ((↑i).extend I).symm.source ∩ ↑((↑i).extend I).symm ⁻¹' (((↑i).extend I).symm.target ∩ ((↑j).extend I).source)
⊢ ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm) x =
    fderivWithin 𝕜 (↑((↑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
h : IsManifold I (n + 1) M
⊢ (tangentBundleCore I M).IsContMDiff I n

Tactic:
have : IsManifold I n M := .of_le (n := n + 1) (le_self_add)

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
h : IsManifold I (n + 1) M
this : IsManifold I n M
⊢ (tangentBundleCore I M).IsContMDiff I n

Proof state:
case refine_2
𝕜 : 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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j) ⊆
    (((↑i).extend I).symm ≫ (↑j).extend I).source

Tactic:
exact (i.1.extend_image_source_inter j.1).subset

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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContDiffOn 𝕜 n ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm)
    (↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j))

Tactic:
refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_

Result:
case refine_1
𝕜 : 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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm) x =
    fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x

case refine_2
𝕜 : 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
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j) ⊆
    (((↑i).extend I).symm ≫ (↑j).extend I).source