case refine'_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ContinuousWithinAt f s x

case refine'_2
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
⊢ ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x) ↔
    ContinuousWithinAt f s x
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
this :
  ContinuousWithinAt ((f ∘ ↑(ModelWithCorners.symm I)) ∘ ↑I) (↑I ⁻¹' (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I)) x
⊢ ContinuousWithinAt f s x
case refine'_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ContinuousWithinAt f s x
have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
case refine'_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑(ModelWithCorners.symm I)) ∘ ↑I) s x
⊢ ContinuousWithinAt f s x
case refine'_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
this :
  ContinuousWithinAt ((f ∘ ↑(ModelWithCorners.symm I)) ∘ ↑I) (↑I ⁻¹' (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I)) x
⊢ ContinuousWithinAt f s x
simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
  inter_univ] at this
no goals
case refine'_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑(ModelWithCorners.symm I)) ∘ ↑I) s x
⊢ ContinuousWithinAt f s x
rwa [Function.comp.assoc, I.symm_comp_self] at this
case refine'_2
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s (↑(ModelWithCorners.symm I) (↑I x))
⊢ ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
case refine'_2
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
rw [← I.left_inv x] at h
no goals
case refine'_2
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_2
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
X : Type u_1
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s (↑(ModelWithCorners.symm I) (↑I x))
⊢ ContinuousWithinAt (f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I) (↑I x)
exact h.comp I.continuousWithinAt_symm (inter_subset_left _ _)