-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem contMDiff_inclusion {n : WithTop ℕ∞} {U V : Opens M} (h : U ≤ V) :
    ContMDiff I I n (Opens.inclusion h : U → V)

Proof state:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
y : H
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (range ↑I) (↑I y)

Tactic:
exact contDiffWithinAt_id.congr I.rightInvOn (congr_arg I (I.left_inv y))

Result:
no goals

Proof state:
case mk
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
⊢ ContMDiffAt I I n (Opens.inclusion h) ⟨x, hx⟩

Tactic:
apply (contDiffWithinAt_localInvariantProp n).liftProp_inclusion

Result:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
⊢ ∀ (y : H), ContDiffWithinAtProp I I n id univ y

Proof state:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
y : H
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (univ ∩ range ↑I) (↑I y)

Tactic:
rw [Set.univ_inter]

Result:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
y : H
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (range ↑I) (↑I y)

Proof state:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
⊢ ∀ (y : H), ContDiffWithinAtProp I I n id univ y

Tactic:
intro y

Result:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
y : H
⊢ ContDiffWithinAtProp I I n id univ y

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
⊢ ContMDiff I I n (Opens.inclusion h)

Tactic:
rintro ⟨x, hx : x ∈ U⟩

Result:
case mk
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
⊢ ContMDiffAt I I n (Opens.inclusion h) ⟨x, hx⟩

Proof state:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
y : H
⊢ ContDiffWithinAtProp I I n id univ y

Tactic:
dsimp only [ContDiffWithinAtProp, id_comp, preimage_univ]

Result:
case mk.hQ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : WithTop ℕ∞
U V : Opens M
h : U ≤ V
x : M
hx : x ∈ U
y : H
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (univ ∩ range ↑I) (↑I y)