src/HOL/Analysis/Homotopy.thy
changeset 69768 7e4966eaf781
parent 69712 dc85b5b3a532
child 69918 eddcc7c726f3
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Thu Jan 31 09:30:15 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Thu Jan 31 13:08:59 2019 +0000
     1.3 @@ -3168,11 +3168,11 @@
     1.4    have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)"
     1.5      using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
     1.6    have "S homeomorphic ((+) (- a) ` S)"
     1.7 -    by (simp add: homeomorphic_translation)
     1.8 +    by (fact homeomorphic_translation)
     1.9    also have "\<dots> homeomorphic ((+) (- b) ` T)"
    1.10      by (rule homeomorphic_subspaces [OF ss dd])
    1.11    also have "\<dots> homeomorphic T"
    1.12 -    using homeomorphic_sym homeomorphic_translation by auto
    1.13 +    using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T])
    1.14    finally show ?thesis .
    1.15  qed
    1.16