-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiffWithinAt_snd {s : Set (M × N)} {p : M × N} :
    ContMDiffWithinAt (I.prod J) J n Prod.snd s p

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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContinuousWithinAt Prod.snd s p ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm)
      ((extChartAt (I.prod J) p).target ∩
        ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source))
      (↑(extChartAt (I.prod J) p) p)

Tactic:
refine ⟨continuousWithinAt_snd, contDiffWithinAt_snd.congr (fun y hy => ?_) ?_⟩

Result:
case refine_1
𝕜 : 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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
y : E × F
hy :
  y ∈
    (extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) y = y.2

case refine_2
𝕜 : 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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) =
    (↑(extChartAt (I.prod J) p) p).2

Proof state:
case refine_2
𝕜 : 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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) =
    (↑(extChartAt (I.prod J) p) p).2

Tactic:
exact (extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _)

Result:
no goals

Proof state:
case refine_1
𝕜 : 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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
y : E × F
hy :
  y ∈
    (extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) y = y.2

Tactic:
exact (extChartAt J p.2).right_inv ⟨hy.1.1.2, hy.1.2.2⟩

Result:
no goals

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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContMDiffWithinAt (I.prod J) J n Prod.snd s p

Tactic:
rw [contMDiffWithinAt_iff']

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
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContinuousWithinAt Prod.snd s p ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm)
      ((extChartAt (I.prod J) p).target ∩
        ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source))
      (↑(extChartAt (I.prod J) p) p)