Update

Mathlib/Analysis/Convolution.lean

@@ -583,8 +583,7 @@ theorem continuousOn_convolution_right_with_param {g : P → G → E'} {s : Set
   have A : ContinuousOn g'.uncurry (s' ×ˢ univ) := by
     have : g'.uncurry = g.uncurry ∘ (fun w ↦ (w.1.1, w.1.2 - w.2)) := by ext y; rfl
     rw [this]
-    refine hg.comp (continuous_fst.fst.prod_mk (continuous_fst.snd.sub
-      continuous_snd)).continuousOn ?_
+    refine hg.comp (by fun_prop) ?_
     simp +contextual [s', MapsTo]
   have B : ContinuousOn (fun a ↦ ∫ x, L (f x) (g' a x) ∂μ) s' := by
     apply continuousOn_integral_bilinear_of_locally_integrable_of_compact_support L k'_comp A _

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -223,7 +223,7 @@ theorem hasFDerivAt_fourierIntegral
   have h3 : AEStronglyMeasurable (F' w) μ := by
     refine .smul ?_ hf.1.fourierSMulRight
     refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
-    exact (L.continuous₂.comp (Continuous.Prod.mk_left w)).neg
+    fun_prop
   have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by
     filter_upwards with v w' _
     rw [Circle.norm_smul _ (fourierSMulRight L f v)]

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -234,22 +234,26 @@ section
 
 variable [TopologicalSpace α]
 
+@[fun_prop]
 theorem Continuous.vsub {f g : α → P} (hf : Continuous f) (hg : Continuous g) :
-    Continuous (f -ᵥ g) :=
+    Continuous (fun x ↦ f x -ᵥ g x) :=
   continuous_vsub.comp (hf.prod_mk hg :)
 
+@[fun_prop]
 nonrec theorem ContinuousAt.vsub {f g : α → P} {x : α} (hf : ContinuousAt f x)
     (hg : ContinuousAt g x) :
-    ContinuousAt (f -ᵥ g) x :=
+    ContinuousAt (fun x ↦ f x -ᵥ g x) x :=
   hf.vsub hg
 
+@[fun_prop]
 nonrec theorem ContinuousWithinAt.vsub {f g : α → P} {x : α} {s : Set α}
     (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
-    ContinuousWithinAt (f -ᵥ g) s x :=
+    ContinuousWithinAt (fun x ↦ f x -ᵥ g x) s x :=
   hf.vsub hg
 
+@[fun_prop]
 theorem ContinuousOn.vsub {f g : α → P} {s : Set α} (hf : ContinuousOn f s)
-    (hg : ContinuousOn g s) : ContinuousOn (f -ᵥ g) s := fun x hx ↦
+    (hg : ContinuousOn g s) : ContinuousOn (fun x ↦ f x -ᵥ g x) s := fun x hx ↦
   (hf x hx).vsub (hg x hx)
 
 end

Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

@@ -76,11 +76,9 @@ def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ) where
   open_source :=
     (isOpen_lt continuous_const continuous_fst).union
       (isOpen_ne_fun continuous_snd continuous_const)
-  continuousOn_invFun :=
-    ((continuous_fst.mul (continuous_cos.comp continuous_snd)).prod_mk
-        (continuous_fst.mul (continuous_sin.comp continuous_snd))).continuousOn
+  continuousOn_invFun := by fun_prop
   continuousOn_toFun := by
-    apply ((continuous_fst.pow 2).add (continuous_snd.pow 2)).sqrt.continuousOn.prod
+    refine .prod_mk (by fun_prop) ?_
     have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
         Complex.slitPlane := by
       rintro ⟨x, y⟩ hxy; simpa only using hxy

Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

@@ -353,12 +353,9 @@ theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0)
       rwa [neg_re, ofReal_re, neg_pos]
     · exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt
 
-#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
-  need `by exact` to deal with tricky unification -/
 theorem continuousAt_ofReal_cpow_const (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
-    ContinuousAt (fun a => (a : ℂ) ^ y : ℝ → ℂ) x := by
-  exact ContinuousAt.comp (x := x) (continuousAt_ofReal_cpow x y h)
-          ((continuous_id (X := ℝ)).prod_mk (continuous_const (y := y))).continuousAt
+    ContinuousAt (fun a => (a : ℂ) ^ y : ℝ → ℂ) x :=
+  (continuousAt_ofReal_cpow x y h).comp₂_of_eq (by fun_prop) (by fun_prop) rfl
 
 theorem continuous_ofReal_cpow_const {y : ℂ} (hs : 0 < y.re) :
     Continuous (fun x => (x : ℂ) ^ y : ℝ → ℂ) :=
@@ -385,7 +382,7 @@ theorem continuousAt_rpow {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) :
   refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)
   · apply Real.continuousAt_rpow
     simpa using h
-  · exact ((continuous_subtype_val.comp continuous_fst).prod_mk continuous_snd).continuousAt
+  · fun_prop
 
 theorem eventually_pow_one_div_le (x : ℝ≥0) {y : ℝ≥0} (hy : 1 < y) :
     ∀ᶠ n : ℕ in atTop, x ^ (1 / n : ℝ) ≤ y := by

Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

@@ -75,10 +75,11 @@ theorem arcsin_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1
     arcsin x = arcsin y ↔ x = y :=
   injOn_arcsin.eq_iff ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_arcsin : Continuous arcsin :=
   continuous_subtype_val.comp sinOrderIso.symm.continuous.Icc_extend'
 
+@[fun_prop]
 theorem continuousAt_arcsin {x : ℝ} : ContinuousAt arcsin x :=
   continuous_arcsin.continuousAt
 
@@ -365,7 +366,7 @@ theorem arccos_le_pi_div_four {x} : arccos x ≤ π / 4 ↔ √2 / 2 ≤ x := by
     · intro
       linarith
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_arccos : Continuous arccos :=
   continuous_const.sub continuous_arcsin
 

Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean

@@ -45,11 +45,8 @@ def oangle (p₁ p₂ p₃ : P) : Real.Angle :=
 /-- Oriented angles are continuous when neither end point equals the middle point. -/
 theorem continuousAt_oangle {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) :
     ContinuousAt (fun y : P × P × P => ∡ y.1 y.2.1 y.2.2) x := by
-  let f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
-  have hf1 : (f x).1 ≠ 0 := by simp [f, hx12]
-  have hf2 : (f x).2 ≠ 0 := by simp [f, hx32]
-  exact (o.continuousAt_oangle hf1 hf2).comp ((continuous_fst.vsub continuous_snd.fst).prod_mk
-    (continuous_snd.snd.vsub continuous_snd.fst)).continuousAt
+  unfold oangle
+  fun_prop (disch := simp [*])
 
 /-- The angle ∡AAB at a point. -/
 @[simp]
@@ -616,9 +613,7 @@ theorem _root_.Collinear.oangle_sign_of_sameRay_vsub {p₁ p₂ p₃ p₄ : P} (
     have hco : IsConnected s :=
       haveI : ConnectedSpace line[ℝ, p₁, p₂] := AddTorsor.connectedSpace _ _
       (isConnected_univ.prod (isConnected_setOf_sameRay_and_ne_zero
-        (vsub_ne_zero.2 hp₁p₂.symm))).image _
-        (continuous_fst.subtype_val.prod_mk (continuous_const.prod_mk
-          (continuous_snd.vadd continuous_fst.subtype_val))).continuousOn
+        (vsub_ne_zero.2 hp₁p₂.symm))).image _ (by fun_prop)
     have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) s := by
       refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
       all_goals
@@ -713,8 +708,8 @@ theorem _root_.AffineSubspace.SSameSide.oangle_sign_eq {s : AffineSubspace ℝ P
     (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign := by
   by_cases h : p₁ = p₂; · simp [h]
   let sp : Set (P × P × P) := (fun p : P => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
-  have hc : IsConnected sp := (isConnected_setOf_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _
-    (continuous_const.prod_mk (Continuous.Prod.mk_left _)).continuousOn
+  have hc : IsConnected sp :=
+    (isConnected_setOf_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _ (by fun_prop)
   have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) sp := by
     refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
     all_goals

Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean

@@ -52,6 +52,7 @@ def oangle (x y : V) : Real.Angle :=
   Complex.arg (o.kahler x y)
 
 /-- Oriented angles are continuous when the vectors involved are nonzero. -/
+@[fun_prop]
 theorem continuousAt_oangle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
     ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x := by
   refine (Complex.continuousAt_arg_coe_angle ?_).comp ?_
@@ -786,8 +787,7 @@ theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) :
     intro r'
     rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h
   let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ
-  have hc : IsConnected s := isConnected_univ.image _ (continuous_const.prod_mk
-    ((continuous_id.smul continuous_const).add continuous_const)).continuousOn
+  have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)
   have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := by
     refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
     all_goals

Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

@@ -49,9 +49,7 @@ theorem continuousAt_angle {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.
   let f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
   have hf1 : (f x).1 ≠ 0 := by simp [f, hx12]
   have hf2 : (f x).2 ≠ 0 := by simp [f, hx32]
-  exact (InnerProductGeometry.continuousAt_angle hf1 hf2).comp
-    ((continuous_fst.vsub continuous_snd.fst).prod_mk
-      (continuous_snd.snd.vsub continuous_snd.fst)).continuousAt
+  exact (InnerProductGeometry.continuousAt_angle hf1 hf2).comp (by fun_prop)
 
 @[simp]
 theorem _root_.AffineIsometry.angle_map {V₂ P₂ : Type*} [NormedAddCommGroup V₂]

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

@@ -42,11 +42,9 @@ def angle (x y : V) : ℝ :=
   Real.arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
 
 theorem continuousAt_angle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
-    ContinuousAt (fun y : V × V => angle y.1 y.2) x :=
-  Real.continuous_arccos.continuousAt.comp <|
-    continuous_inner.continuousAt.div
-      ((continuous_norm.comp continuous_fst).mul (continuous_norm.comp continuous_snd)).continuousAt
-      (by simp [hx1, hx2])
+    ContinuousAt (fun y : V × V => angle y.1 y.2) x := by
+  unfold angle
+  fun_prop (disch := simp [*])
 
 theorem angle_smul_smul {c : ℝ} (hc : c ≠ 0) (x y : V) : angle (c • x) (c • y) = angle x y := by
   have : c * c ≠ 0 := mul_ne_zero hc hc

Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean

@@ -28,6 +28,7 @@ def PrimeSpectrum.tensorProductTo (x : PrimeSpectrum (S ⊗[R] T)) :
     PrimeSpectrum S × PrimeSpectrum T :=
   ⟨comap (algebraMap _ _) x, comap Algebra.TensorProduct.includeRight.toRingHom x⟩
 
+@[fun_prop]
 lemma PrimeSpectrum.continuous_tensorProductTo : Continuous (tensorProductTo R S T) :=
   (comap _).2.prod_mk (comap _).2
 

Mathlib/Topology/Algebra/GroupWithZero.lean

@@ -222,8 +222,8 @@ theorem ContinuousAt.comp_div_cases {f g : α → G₀} (h : α → G₀ → β)
   by_cases hga : g a = 0
   · rw [ContinuousAt]
     simp_rw [comp_apply, hga, div_zero]
-    exact (h2h hga).comp (continuousAt_id.prod_mk tendsto_top)
-  · exact ContinuousAt.comp (hh hga) (continuousAt_id.prod (hf.div hg hga))
+    exact (h2h hga).comp (continuousAt_id.tendsto.prod_mk tendsto_top)
+  · fun_prop (disch := assumption)
 
 /-- `h x (f x / g x)` is continuous under certain conditions, even if the denominator is sometimes
   `0`. See docstring of `ContinuousAt.comp_div_cases`. -/

Mathlib/Topology/Algebra/Monoid.lean

@@ -221,8 +221,7 @@ theorem ContinuousWithinAt.mul {f g : X → M} {s : Set X} {x : X} (hf : Continu
 @[to_additive]
 instance Prod.continuousMul [TopologicalSpace N] [Mul N] [ContinuousMul N] :
     ContinuousMul (M × N) :=
-  ⟨(continuous_fst.fst'.mul continuous_fst.snd').prod_mk
-      (continuous_snd.fst'.mul continuous_snd.snd')⟩
+  ⟨by apply Continuous.prod_mk <;> fun_prop⟩
 
 @[to_additive]
 instance Pi.continuousMul {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Mul (C i)]
@@ -853,7 +852,7 @@ instance : ContinuousMul αˣ := isInducing_embedProduct.continuousMul (embedPro
 
 end Units
 
-@[to_additive]
+@[to_additive (attr := fun_prop)]
 theorem Continuous.units_map [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N]
     (f : M →* N) (hf : Continuous f) : Continuous (Units.map f) :=
   Units.continuous_iff.2 ⟨hf.comp Units.continuous_val, hf.comp Units.continuous_coe_inv⟩

Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean

@@ -47,8 +47,7 @@ theorem properlyDiscontinuousSMul_iff_properSMul [T2Space X] [DiscreteTopology G
     -- Because `X × X` is compactly generated, to show that f is proper
     -- it is enough to show that the preimage of a compact set `K` is compact.
     refine isProperMap_iff_isCompact_preimage.2
-      ⟨(continuous_prod_mk.2
-      ⟨continuous_prod_of_discrete_left.2 continuous_const_smul, by fun_prop⟩),
+      ⟨(continuous_prod_of_discrete_left.2 continuous_const_smul).prod_mk (by fun_prop),
       fun K hK ↦ ?_⟩
     -- We set `K' := pr₁(K) ∪ pr₂(K)`, which is compact because `K` is compact and `pr₁` and
     -- `pr₂` are continuous. We halso have that `K ⊆ K' × K'`, and `K` is closed because `X` is T2.
@@ -81,8 +80,7 @@ theorem properlyDiscontinuousSMul_iff_properSMul [T2Space X] [DiscreteTopology G
         isCompact_singleton.prod <| (hK'.image <| continuous_const_smul _).inter hK'
     -- We conclude as explained above.
     exact this.of_isClosed_subset (hK.isClosed.preimage <|
-      continuous_prod_mk.2
-      ⟨continuous_prod_of_discrete_left.2 continuous_const_smul, by fun_prop⟩) <|
+      (continuous_prod_of_discrete_left.2 continuous_const_smul).prod_mk (by fun_prop)) <|
       preimage_mono fun x hx ↦ ⟨Or.inl ⟨x, hx, rfl⟩, Or.inr ⟨x, hx, rfl⟩⟩
   · intro h; constructor
     intro K L hK hL

Mathlib/Topology/Algebra/UniformField.lean

@@ -63,6 +63,7 @@ variable {K}
 def hatInv : hat K → hat K :=
   isDenseInducing_coe.extend fun x : K => (↑x⁻¹ : hat K)
 
+@[fun_prop]
 theorem continuous_hatInv [CompletableTopField K] {x : hat K} (h : x ≠ 0) :
     ContinuousAt hatInv x := by
   refine isDenseInducing_coe.continuousAt_extend ?_
@@ -121,10 +122,7 @@ theorem mul_hatInv_cancel {x : hat K} (x_ne : x ≠ 0) : x * hatInv x = 1 := by
   let c := (fun (x : K) => (x : hat K))
   change f x = 1
   have cont : ContinuousAt f x := by
-    letI : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
-    have : ContinuousAt (fun y : hat K => ((y, hatInv y) : hat K × hat K)) x :=
-      continuous_id.continuousAt.prod (continuous_hatInv x_ne)
-    exact (_root_.continuous_mul.continuousAt.comp this :)
+    fun_prop (disch := assumption)
   have clo : x ∈ closure (c '' {0}ᶜ) := by
     have := isDenseInducing_coe.dense x
     rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,

Mathlib/Topology/Category/CompHausLike/Limits.lean

@@ -240,10 +240,7 @@ def pullback.lift {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : a ≫ f
     Z ⟶ pullback f g :=
   TopCat.ofHom
   { toFun := fun z ↦ ⟨⟨a z, b z⟩, by apply_fun (fun q ↦ q z) at w; exact w⟩
-    continuous_toFun := by
-      apply Continuous.subtype_mk
-      rw [continuous_prod_mk]
-      exact ⟨a.hom.continuous, b.hom.continuous⟩ }
+    continuous_toFun := by fun_prop }
 
 @[reassoc (attr := simp)]
 lemma pullback.lift_fst {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : a ≫ f = b ≫ g) :

Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

@@ -56,11 +56,7 @@ def pullbackConeIsLimit (f : X ⟶ Z) (g : Y ⟶ Z) : IsLimit (pullbackCone f g)
       · exact ofHom
           { toFun := fun x =>
               ⟨⟨S.fst x, S.snd x⟩, by simpa using ConcreteCategory.congr_hom S.condition x⟩
-            continuous_toFun := by
-              apply Continuous.subtype_mk <| Continuous.prod_mk ?_ ?_
-              · exact (PullbackCone.fst S).hom.continuous_toFun
-              · exact (PullbackCone.snd S).hom.continuous_toFun
-          }
+            continuous_toFun := by fun_prop }
       refine ⟨?_, ?_, ?_⟩
       · delta pullbackCone
         ext a
@@ -159,9 +155,7 @@ def pullbackHomeoPreimage
     convert x.prop
     exact Exists.choose_spec (p := fun y ↦ g y = f (↑x : X × Y).1) _
   right_inv := fun _ ↦ rfl
-  continuous_toFun := by
-    apply Continuous.subtype_mk
-    exact continuous_fst.comp continuous_subtype_val
+  continuous_toFun := by fun_prop
   continuous_invFun := by
     apply Continuous.subtype_mk
     refine continuous_prod_mk.mpr ⟨continuous_subtype_val, hg.isInducing.continuous_iff.mpr ?_⟩

Mathlib/Topology/Connected/Basic.lean

@@ -416,7 +416,7 @@ theorem IsPreconnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs
   refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩
   · rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
     exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]
-  · exact (ht.image _ (Continuous.Prod.mk _).continuousOn).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
+  · exact (ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
       ⟨a₁, ha₁, rfl⟩ (hs.image _ (continuous_id.prod_mk continuous_const).continuousOn)
 
 theorem IsConnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsConnected s)

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -622,7 +622,7 @@ theorem continuous_coordChange (e₁ e₂ : Trivialization F proj) {b : B} (h₁
     (h₂ : b ∈ e₂.baseSet) : Continuous (e₁.coordChange e₂ b) := by
   refine continuous_snd.comp (e₂.toPartialHomeomorph.continuousOn.comp_continuous
     (e₁.toPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)
-  · exact continuous_const.prod_mk continuous_id
+  · fun_prop
   · exact fun x => e₁.mem_target.2 h₁
   · intro x
     rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]
@@ -762,7 +762,7 @@ def liftCM (T : Trivialization F proj) : C(T.source × T.baseSet, T.source) wher
   continuous_toFun := by
     apply Continuous.subtype_mk
     refine T.continuousOn_invFun.comp_continuous ?_ (by simp [mem_target])
-    apply continuous_prod_mk.mpr ⟨by fun_prop, continuous_snd.comp ?_⟩
+    refine .prod_mk (by fun_prop) (.snd ?_)
     exact T.continuousOn_toFun.comp_continuous (by fun_prop) (by simp)
 
 variable {ι : Type*} [TopologicalSpace ι] [LocallyCompactPair ι T.baseSet]

Mathlib/Topology/Homotopy/HSpaces.lean

@@ -75,23 +75,14 @@ open HSpaces
 
 instance HSpace.prod (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] [HSpace X]
     [HSpace Y] : HSpace (X × Y) where
-  hmul := ⟨fun p => (p.1.1 ⋀ p.2.1, p.1.2 ⋀ p.2.2), by
-    -- Porting note: was `continuity`
-    exact ((map_continuous HSpace.hmul).comp ((continuous_fst.comp continuous_fst).prod_mk
-        (continuous_fst.comp continuous_snd))).prod_mk ((map_continuous HSpace.hmul).comp
-        ((continuous_snd.comp continuous_fst).prod_mk (continuous_snd.comp continuous_snd)))
-  ⟩
+  hmul := ⟨fun p => (p.1.1 ⋀ p.2.1, p.1.2 ⋀ p.2.2), by fun_prop⟩
   e := (HSpace.e, HSpace.e)
   hmul_e_e := by
     simp only [ContinuousMap.coe_mk, Prod.mk.inj_iff]
     exact ⟨HSpace.hmul_e_e, HSpace.hmul_e_e⟩
   eHmul := by
     let G : I × X × Y → X × Y := fun p => (HSpace.eHmul (p.1, p.2.1), HSpace.eHmul (p.1, p.2.2))
-    have hG : Continuous G :=
-      (Continuous.comp HSpace.eHmul.1.1.2
-          (continuous_fst.prod_mk (continuous_fst.comp continuous_snd))).prod_mk
-        (Continuous.comp HSpace.eHmul.1.1.2
-          (continuous_fst.prod_mk (continuous_snd.comp continuous_snd)))
+    have hG : Continuous G := by fun_prop
     use! ⟨G, hG⟩
     · rintro ⟨x, y⟩
       exact Prod.ext (HSpace.eHmul.1.2 x) (HSpace.eHmul.1.2 y)
@@ -102,11 +93,7 @@ instance HSpace.prod (X : Type u) (Y : Type v) [TopologicalSpace X] [Topological
       exact Prod.ext (HSpace.eHmul.2 t x h.1) (HSpace.eHmul.2 t y h.2)
   hmulE := by
     let G : I × X × Y → X × Y := fun p => (HSpace.hmulE (p.1, p.2.1), HSpace.hmulE (p.1, p.2.2))
-    have hG : Continuous G :=
-      (Continuous.comp HSpace.hmulE.1.1.2
-            (continuous_fst.prod_mk (continuous_fst.comp continuous_snd))).prod_mk
-        (Continuous.comp HSpace.hmulE.1.1.2
-          (continuous_fst.prod_mk (continuous_snd.comp continuous_snd)))
+    have hG : Continuous G := by fun_prop
     use! ⟨G, hG⟩
     · rintro ⟨x, y⟩
       exact Prod.ext (HSpace.hmulE.1.2 x) (HSpace.hmulE.1.2 y)
@@ -161,6 +148,7 @@ continuity of `delayReflRight`. -/
 def qRight (p : I × I) : I :=
   Set.projIcc 0 1 zero_le_one (2 * p.1 / (1 + p.2))
 
+@[fun_prop]
 theorem continuous_qRight : Continuous qRight :=
   continuous_projIcc.comp <|
     Continuous.div (by fun_prop) (by fun_prop) fun _ ↦ (add_pos zero_lt_one).ne'
@@ -202,7 +190,7 @@ variable {X : Type u} [TopologicalSpace X] {x y : X}
 the product path `γ ∧ e` to `γ`. -/
 def delayReflRight (θ : I) (γ : Path x y) : Path x y where
   toFun t := γ (qRight (t, θ))
-  continuous_toFun := γ.continuous.comp (continuous_qRight.comp <| Continuous.Prod.mk_left θ)
+  continuous_toFun := by fun_prop
   source' := by
     dsimp only
     rw [qRight_zero_left, γ.source]