Fix second mistake

leanprover-community · Jun 20, 2021 · c86e1bb · c86e1bb
1 parent 1b404df
commit c86e1bb
Showing 1 changed file with 2 additions and 2 deletions.
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),