slow decl

Stream: general

[Johan Commelin]

I'm touching topology/connected for unrelated reasons, and noticed that docs#sum.is_connected_iff is ridiculously slow compared to the rest of the file. Squeezing the two simps doesn't help. The rest of the proof basically only uses refine so I don't understand why it's so slow.

[Ruben Van de Velde]

It's instantaneous with

@@ -535,13 +537,13 @@ begin
     let v : set (α ⊕ β) := range sum.inr,
     have hu : is_open u, exact is_open_range_inl,
     obtain ⟨x | x, hx⟩ := hs.nonempty,
-    { have h := is_preconnected.subset_left_of_subset_union
+    { have h : s ⊆ range sum.inl := is_preconnected.subset_left_of_subset_union
         is_open_range_inl is_open_range_inr is_compl_range_inl_range_inr.disjoint
         (show s ⊆ range sum.inl ∪ range sum.inr, by simp) ⟨sum.inl x, hx, x, rfl⟩ hs.2,
       refine or.inl ⟨sum.inl ⁻¹' s, _, _⟩,
       { exact hs.preimage_of_open_map sum.inl_injective open_embedding_inl.is_open_map h },
       { exact (set.image_preimage_eq_of_subset h).symm } },
-    { have h := is_preconnected.subset_right_of_subset_union
+    { have h : s ⊆ range sum.inr := is_preconnected.subset_right_of_subset_union
         is_open_range_inl is_open_range_inr is_compl_range_inl_range_inr.disjoint
         (show s ⊆ range sum.inl ∪ range sum.inr, by simp) ⟨sum.inr x, hx, x, rfl⟩ hs.2,
       refine or.inr ⟨sum.inr ⁻¹' s, _, _⟩,

[Johan Commelin]

Wow! So it was just spending ages on type inference?

[Johan Commelin]

Could you please PR?

[Ruben Van de Velde]

Yeah

[Ruben Van de Velde]

#16353