-- Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
theorem UniqueMDiffWithinAt.image_denseRange (hs : UniqueMDiffWithinAt I s x)
    {f : M → M'} {f' : E →L[𝕜] E'} (hf : HasMFDerivWithinAt I I' f s x f')
    (hd : DenseRange f') : UniqueMDiffWithinAt I' (f '' s) (f x)

Proof state:
case sub1
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange ⇑f'
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I ⊆
    ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I

case sub2
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange ⇑f'
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ writtenInExtChartAt I I' x f '' (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) ⊆
    ↑(extChartAt I' (f x)).symm ⁻¹' (f '' s) ∩ range ↑I'

case pt
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange ⇑f'
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)

Tactic:
case pt => simp only [mfld_simps]

Result:
case sub1
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange ⇑f'
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I ⊆
    ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I

case sub2
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange ⇑f'
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ writtenInExtChartAt I I' x f '' (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) ⊆
    ↑(extChartAt I' (f x)).symm ⁻¹' (f '' s) ∩ range ↑I'