-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffWithinAt_iff_target :
    ContMDiffWithinAt I I' n f s x ↔
      ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (extChartAt I' (f x) ∘ f) s x

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
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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm)
        (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

Tactic:
have cont :
  ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔
      ContinuousWithinAt f s x :=
    and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt

Result:
𝕜 : 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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm)
        (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

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
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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) s x

Tactic:
simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff', ← and_assoc]

Result:
𝕜 : 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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm)
        (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

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
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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm)
        (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

Tactic:
simp_rw [cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
  ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
  chartAt_self_eq, PartialHomeomorph.refl_apply, id_comp]

Result:
𝕜 : 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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
        (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x)) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((((↑I' ∘ ↑(chartAt H' (f x))) ∘ f) ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
        (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))

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
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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
        (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x)) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((((↑I' ∘ ↑(chartAt H' (f x))) ∘ f) ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
        (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))

Tactic:
rfl

Result:
no goals