Merge master into nightly-testing

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -1030,7 +1030,7 @@ theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : PartialHomeomor
   have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc
     (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
     _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
-      EqOnSource.trans' (refl _) (EqOnSource.trans' (trans_self_symm _) (refl _))
+      EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _))
     _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
     _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
     _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
@@ -1098,7 +1098,7 @@ theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H
       intro e' e'' he' he''
       rw [e.singletonChartedSpace_mem_atlas_eq h e' he',
         e.singletonChartedSpace_mem_atlas_eq h e'' he'']
-      refine' G.eq_on_source _ e.trans_symm_self
+      refine' G.eq_on_source _ e.symm_trans_self
       have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)
       exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _) }
 #align local_homeomorph.singleton_has_groupoid PartialHomeomorph.singleton_hasGroupoid
@@ -1262,7 +1262,7 @@ def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') :
         F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by simp only [trans_assoc, _root_.refl]
         _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
           EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
-            (EqOnSource.trans' (trans_self_symm g) (_root_.refl _)))
+            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
         _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' :=
           by simp only [trans_assoc, _root_.refl]
         _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']

Mathlib/Geometry/Manifold/Diffeomorph.lean

@@ -195,6 +195,7 @@ theorem coe_refl : ⇑(Diffeomorph.refl I M n) = id :=
 end
 
 /-- Composition of two diffeomorphisms. -/
+@[trans]
 protected def trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J⟯ N) : M ≃ₘ^n⟮I, J⟯ N where
   contMDiff_toFun := h₂.contMDiff.comp h₁.contMDiff
   contMDiff_invFun := h₁.contMDiff_invFun.comp h₂.contMDiff_invFun
@@ -217,7 +218,7 @@ theorem coe_trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J
 #align diffeomorph.coe_trans Diffeomorph.coe_trans
 
 /-- Inverse of a diffeomorphism. -/
-@[pp_dot]
+@[symm]
 protected def symm (h : M ≃ₘ^n⟮I, J⟯ N) : N ≃ₘ^n⟮J, I⟯ M where
   contMDiff_toFun := h.contMDiff_invFun
   contMDiff_invFun := h.contMDiff_toFun

Mathlib/Geometry/Manifold/InteriorBoundary.lean

@@ -103,25 +103,42 @@ lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) :
   rw [mem_nhds_iff]
   exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩
 
-section boundaryless
+/-- Type class for manifold without boundary. This differs from `ModelWithCorners.Boundaryless`,
+  which states that the `ModelWithCorners` maps to the whole model vector space. -/
+class _root_.BoundarylessManifold {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
+    (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : Prop where
+  isInteriorPoint' : ∀ x : M, IsInteriorPoint I x
+
+section Boundaryless
 variable [I.Boundaryless]
 
-/-- If `I` is boundaryless, every point of `M` is an interior point. -/
-lemma isInteriorPoint {x : M} : I.IsInteriorPoint x := by
-  let r := ((chartAt H x).isOpen_extend_target I).interior_eq
-  have : extChartAt I x = (chartAt H x).extend I := rfl
-  rw [← this] at r
-  rw [ModelWithCorners.isInteriorPoint_iff, r]
-  exact PartialEquiv.map_source _ (mem_extChartAt_source _ _)
+/-- Boundaryless `ModelWithCorners` implies boundaryless manifold. -/
+instance : BoundarylessManifold I M where
+  isInteriorPoint' x := by
+    let r := ((chartAt H x).isOpen_extend_target I).interior_eq
+    have : extChartAt I x = (chartAt H x).extend I := rfl
+    rw [← this] at r
+    rw [ModelWithCorners.isInteriorPoint_iff, r]
+    exact PartialEquiv.map_source _ (mem_extChartAt_source _ _)
 
-/-- If `I` is boundaryless, `M` has full interior. -/
+end Boundaryless
+
+section BoundarylessManifold
+variable [BoundarylessManifold I M]
+
+lemma _root_.BoundarylessManifold.isInteriorPoint {x : M} :
+    IsInteriorPoint I x := BoundarylessManifold.isInteriorPoint' x
+
+/-- Boundaryless manifolds have full interior. -/
 lemma interior_eq_univ : I.interior M = univ := by
   ext
-  refine ⟨fun _ ↦ trivial, fun _ ↦ I.isInteriorPoint⟩
+  refine ⟨fun _ ↦ trivial, fun _ ↦ BoundarylessManifold.isInteriorPoint I⟩
 
-/-- If `I` is boundaryless, `M` has empty boundary. -/
+/-- Boundaryless manifolds have empty boundary. -/
 lemma Boundaryless.boundary_eq_empty : I.boundary M = ∅ := by
   rw [I.boundary_eq_complement_interior, I.interior_eq_univ, compl_empty_iff]
 
-end boundaryless
+end BoundarylessManifold
 end ModelWithCorners

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -478,7 +478,9 @@ end ModelWithCornersProd
 
 section Boundaryless
 
-/-- Property ensuring that the model with corners `I` defines manifolds without boundary. -/
+/-- Property ensuring that the model with corners `I` defines manifolds without boundary. This
+  differs from the more general `BoundarylessManifold`, which requires every point on the manifold
+  to be an interior point.  -/
 class ModelWithCorners.Boundaryless {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
     (I : ModelWithCorners 𝕜 E H) : Prop where
@@ -617,7 +619,7 @@ the `C^n` groupoid. -/
 theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) :
     e.symm.trans e ∈ contDiffGroupoid n I :=
   haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
-    PartialHomeomorph.trans_symm_self _
+    PartialHomeomorph.symm_trans_self _
   StructureGroupoid.eq_on_source _ (ofSet_mem_contDiffGroupoid n I e.open_target) this
 #align symm_trans_mem_cont_diff_groupoid symm_trans_mem_contDiffGroupoid
 
@@ -776,7 +778,7 @@ the analytic groupoid. -/
 theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) :
     e.symm.trans e ∈ analyticGroupoid I :=
   haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
-    PartialHomeomorph.trans_symm_self _
+    PartialHomeomorph.symm_trans_self _
   StructureGroupoid.eq_on_source _ (ofSet_mem_analyticGroupoid I e.open_target) this
 
 /-- The analytic groupoid is closed under restriction. -/

Mathlib/Logic/Equiv/PartialEquiv.lean

@@ -148,6 +148,7 @@ instance [Inhabited α] [Inhabited β] : Inhabited (PartialEquiv α β) :=
       eqOn_empty _ _⟩⟩
 
 /-- The inverse of a partial equivalence -/
+@[symm]
 protected def symm : PartialEquiv β α where
   toFun := e.invFun
   invFun := e.toFun
@@ -689,6 +690,7 @@ protected def trans' (e' : PartialEquiv β γ) (h : e.target = e'.source) : Part
 
 /-- Composing two partial equivs, by restricting to the maximal domain where their composition
 is well defined. -/
+@[trans]
 protected def trans : PartialEquiv α γ :=
   PartialEquiv.trans' (e.symm.restr e'.source).symm (e'.restr e.target) (inter_comm _ _)
 #align local_equiv.trans PartialEquiv.trans
@@ -896,18 +898,18 @@ theorem EqOnSource.source_inter_preimage_eq {e e' : PartialEquiv α β} (he : e
 
 /-- Composition of a partial equivlance and its inverse is equivalent to
 the restriction of the identity to the source. -/
-theorem trans_self_symm : e.trans e.symm ≈ ofSet e.source := by
+theorem self_trans_symm : e.trans e.symm ≈ ofSet e.source := by
   have A : (e.trans e.symm).source = e.source := by mfld_set_tac
   refine' ⟨by rw [A, ofSet_source], fun x hx => _⟩
   rw [A] at hx
   simp only [hx, mfld_simps]
-#align local_equiv.trans_self_symm PartialEquiv.trans_self_symm
+#align local_equiv.self_trans_symm PartialEquiv.self_trans_symm
 
 /-- Composition of the inverse of a partial equivalence and this partial equivalence is equivalent
 to the restriction of the identity to the target. -/
-theorem trans_symm_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target :=
-  trans_self_symm e.symm
-#align local_equiv.trans_symm_self PartialEquiv.trans_symm_self
+theorem symm_trans_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target :=
+  self_trans_symm e.symm
+#align local_equiv.symm_trans_self PartialEquiv.symm_trans_self
 
 /-- Two equivalent partial equivs are equal when the source and target are `univ`. -/
 theorem eq_of_eqOnSource_univ (e e' : PartialEquiv α β) (h : e ≈ e') (s : e.source = univ)

Mathlib/Probability/Independence/Basic.lean

@@ -650,11 +650,12 @@ theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' :
     rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
 
 @[symm]
-nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g μ) :
-    IndepFun g f μ := hfg.symm
+nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'}
+    (hfg : IndepFun f g μ) : IndepFun g f μ := hfg.symm
 #align probability_theory.indep_fun.symm ProbabilityTheory.IndepFun.symm
 
-theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g μ)
+theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g μ)
     (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : IndepFun f' g' μ := by
   refine kernel.IndepFun.ae_eq hfg ?_ ?_ <;>
     simp only [ae_dirac_eq, Filter.eventually_pure, kernel.const_apply]

Mathlib/Probability/Independence/Kernel.lean

@@ -788,10 +788,11 @@ theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : Measur
   · rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]
 
 @[symm]
-nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g κ μ) :
-    IndepFun g f κ μ := hfg.symm
+nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'}
+    (hfg : IndepFun f g κ μ) : IndepFun g f κ μ := hfg.symm
 
-theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g κ μ)
+theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g κ μ)
     (hf : ∀ᵐ a ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ a ∂μ, g =ᵐ[κ a] g') :
     IndepFun f' g' κ μ := by
   rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩

Mathlib/Topology/Homeomorph.lean

@@ -74,6 +74,7 @@ protected def empty [IsEmpty X] [IsEmpty Y] : X ≃ₜ Y where
   __ := Equiv.equivOfIsEmpty X Y
 
 /-- Inverse of a homeomorphism. -/
+@[symm]
 protected def symm (h : X ≃ₜ Y) : Y ≃ₜ X where
   continuous_toFun := h.continuous_invFun
   continuous_invFun := h.continuous_toFun
@@ -117,6 +118,7 @@ protected def refl (X : Type*) [TopologicalSpace X] : X ≃ₜ X where
 #align homeomorph.refl Homeomorph.refl
 
 /-- Composition of two homeomorphisms. -/
+@[trans]
 protected def trans (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z where
   continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun
   continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun

Mathlib/Topology/PartialHomeomorph.lean

@@ -76,6 +76,7 @@ instance : CoeFun (PartialHomeomorph α β) fun _ => α → β :=
   ⟨fun e => e.toFun'⟩
 
 /-- The inverse of a partial homeomorphism -/
+@[symm]
 protected def symm : PartialHomeomorph β α where
   toPartialEquiv := e.toPartialEquiv.symm
   open_source := e.open_target
@@ -816,6 +817,7 @@ protected def trans' (h : e.target = e'.source) : PartialHomeomorph α γ where
 
 /-- Composing two partial homeomorphisms, by restricting to the maximal domain where their
 composition is well defined. -/
+@[trans]
 protected def trans : PartialHomeomorph α γ :=
   PartialHomeomorph.trans' (e.symm.restrOpen e'.source e'.open_source).symm
     (e'.restrOpen e.target e.open_target) (by simp [inter_comm])
@@ -1024,13 +1026,13 @@ theorem Set.EqOn.restr_eqOn_source {e e' : PartialHomeomorph α β}
 
 /-- Composition of a partial homeomorphism and its inverse is equivalent to the restriction of the
 identity to the source -/
-theorem trans_self_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source :=
-  PartialEquiv.trans_self_symm _
-#align local_homeomorph.trans_self_symm PartialHomeomorph.trans_self_symm
+theorem self_trans_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source :=
+  PartialEquiv.self_trans_symm _
+#align local_homeomorph.self_trans_symm PartialHomeomorph.self_trans_symm
 
-theorem trans_symm_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
-  e.symm.trans_self_symm
-#align local_homeomorph.trans_symm_self PartialHomeomorph.trans_symm_self
+theorem symm_trans_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
+  e.symm.self_trans_symm
+#align local_homeomorph.symm_trans_self PartialHomeomorph.symm_trans_self
 
 theorem eq_of_eqOnSource_univ {e e' : PartialHomeomorph α β} (h : e ≈ e') (s : e.source = univ)
     (t : e.target = univ) : e = e' :=
@@ -1445,7 +1447,7 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph α β) :
   rw [ofSet_trans', sets_identity, ← trans_of_set' _ openness₂, trans_assoc]
   refine' EqOnSource.trans' (eqOnSource_refl _) _
   -- f has been eliminated !!!
-  refine' Setoid.trans (trans_symm_self s.localHomeomorphSubtypeCoe) _
+  refine' Setoid.trans (symm_trans_self s.localHomeomorphSubtypeCoe) _
   simp only [mfld_simps, Setoid.refl]
 #align local_homeomorph.subtype_restr_symm_trans_subtype_restr PartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr