case refine'_1
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ I.source

case refine'_2
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ I.target ∩ ↑(LocalEquiv.symm I.toLocalEquiv) ⁻¹' s = ↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ ↑I '' s = ↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I
refine' (I.toLocalEquiv.image_eq_target_inter_inv_preimage _).trans _
case refine'_1
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ univ
case refine'_1
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ I.source
rw [I.source_eq]
no goals
case refine'_1
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ univ
exact subset_univ _
no goals
case refine'_2
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ I.target ∩ ↑(LocalEquiv.symm I.toLocalEquiv) ⁻¹' s = ↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I
rw [inter_comm, I.target_eq, I.toLocalEquiv_coe_symm]