Fix second mistake

leanprover-community · Jun 20, 2021 · 6eaf958 · 6eaf958
1 parent 1b404df
commit 6eaf958
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/geometry/manifold/basic_smooth_bundle.lean b/src/geometry/manifold/basic_smooth_bundle.lean
@@ -500,7 +500,7 @@ them, noting in particular that the tangent bundle is a smooth manifold. -/
 variable (M)
 
 instance : topological_space (tangent_bundle I M) :=
-(tangent_bundle_core I M).to_topological_fiber_bundle_core.to_topological_space
+(tangent_bundle_core I M).to_topological_fiber_bundle_core.to_topological_space (atlas H M)
 
 instance : charted_space (model_prod H E) (tangent_bundle I M) :=
 (tangent_bundle_core I M).to_charted_space

diff --git a/src/topology/topological_fiber_bundle.lean b/src/topology/topological_fiber_bundle.lean
@@ -1002,8 +1002,8 @@ begin
   apply le_induced_generate,
   simp only [mem_Union, mem_singleton_iff, local_triv'_source, local_triv'_coe, mem_image],
   rintros s ⟨i, t, ht, rfl⟩,
-  rw [←(source_inter_preimage_target_inter_eq (Z.local_triv i) t), preimage_inter, ←preimage_comp,
-    local_triv_source, bundle_trivialization.source_eq],
+  rw [←(local_homeomorph.source_inter_preimage_target_inter (Z.local_triv i) t),
+    preimage_inter, ←preimage_comp, local_triv_source, bundle_trivialization.source_eq],
   apply is_open.inter,
   { simp only [bundle.proj, proj, ←preimage_comp],
     by_cases (b ∈ (Z.local_triv_ext i).base_set),