Merge master into nightly-testing

Mathlib.lean

@@ -3362,6 +3362,7 @@ import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.FreeProduct.Basic
 import Mathlib.LinearAlgebra.GeneralLinearGroup
+import Mathlib.LinearAlgebra.Goursat
 import Mathlib.LinearAlgebra.InvariantBasisNumber
 import Mathlib.LinearAlgebra.Isomorphisms
 import Mathlib.LinearAlgebra.JordanChevalley
@@ -4314,7 +4315,6 @@ import Mathlib.RingTheory.Finiteness.Projective
 import Mathlib.RingTheory.Finiteness.Subalgebra
 import Mathlib.RingTheory.Finiteness.TensorProduct
 import Mathlib.RingTheory.Fintype
-import Mathlib.RingTheory.Flat.Algebra
 import Mathlib.RingTheory.Flat.Basic
 import Mathlib.RingTheory.Flat.CategoryTheory
 import Mathlib.RingTheory.Flat.Equalizer
@@ -4538,6 +4538,7 @@ import Mathlib.RingTheory.Regular.RegularSequence
 import Mathlib.RingTheory.RingHom.Finite
 import Mathlib.RingTheory.RingHom.FinitePresentation
 import Mathlib.RingTheory.RingHom.FiniteType
+import Mathlib.RingTheory.RingHom.Flat
 import Mathlib.RingTheory.RingHom.Injective
 import Mathlib.RingTheory.RingHom.Integral
 import Mathlib.RingTheory.RingHom.Locally
@@ -4960,6 +4961,7 @@ import Mathlib.Topology.Algebra.Group.SubmonoidClosure
 import Mathlib.Topology.Algebra.Group.TopologicalAbelianization
 import Mathlib.Topology.Algebra.GroupCompletion
 import Mathlib.Topology.Algebra.GroupWithZero
+import Mathlib.Topology.Algebra.Indicator
 import Mathlib.Topology.Algebra.InfiniteSum.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Constructions
 import Mathlib.Topology.Algebra.InfiniteSum.Defs

Mathlib/Algebra/Category/Ring/Under/Limits.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Category.Ring.Under.Basic
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 import Mathlib.CategoryTheory.Limits.Over
 import Mathlib.RingTheory.TensorProduct.Pi
-import Mathlib.RingTheory.Flat.Algebra
+import Mathlib.RingTheory.RingHom.Flat
 import Mathlib.RingTheory.Flat.Equalizer
 
 /-!
@@ -208,6 +208,7 @@ lemma preservesFiniteLimits_of_flat (hf : RingHom.Flat f) :
     PreservesFiniteLimits (Under.pushout f) where
   preservesFiniteLimits _ :=
     letI : Algebra R S := RingHom.toAlgebra f
+    haveI : Module.Flat R S := hf
     preservesLimitsOfShape_of_natIso (tensorProdIsoPushout R S)
 
 end CommRingCat.Under

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -90,8 +90,8 @@ structure.
 When possible, instead of parametrizing results over `(f : α ≃+o β)`,
 you should parametrize over
 `(F : Type*) [FunLike F M N] [AddEquivClass F M N] [OrderIsoClass F M N] (f : F)`. -/
-structure OrderAddMonoidIso (α β : Type*) [Preorder α] [Preorder β] [AddZeroClass α]
-  [AddZeroClass β] extends α ≃+ β where
+structure OrderAddMonoidIso (α β : Type*) [Preorder α] [Preorder β] [Add α] [Add β]
+  extends α ≃+ β where
   /-- An `OrderAddMonoidIso` respects `≤`. -/
   map_le_map_iff' {a b : α} : toFun a ≤ toFun b ↔ a ≤ b
 
@@ -146,8 +146,8 @@ When possible, instead of parametrizing results over `(f : α ≃*o β)`,
 you should parametrize over
 `(F : Type*) [FunLike F M N] [MulEquivClass F M N] [OrderIsoClass F M N] (f : F)`. -/
 @[to_additive]
-structure OrderMonoidIso (α β : Type*) [Preorder α] [Preorder β] [MulOneClass α]
-  [MulOneClass β] extends α ≃* β where
+structure OrderMonoidIso (α β : Type*) [Preorder α] [Preorder β] [Mul α] [Mul β]
+  extends α ≃* β where
   /-- An `OrderMonoidIso` respects `≤`. -/
   map_le_map_iff' {a b : α} : toFun a ≤ toFun b ↔ a ≤ b
 
@@ -513,8 +513,8 @@ namespace OrderMonoidIso
 
 section Preorder
 
-variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [MulOneClass α] [MulOneClass β]
-  [MulOneClass γ] [MulOneClass δ] {f g : α ≃*o β}
+variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [Mul α] [Mul β]
+  [Mul γ] [Mul δ] {f g : α ≃*o β}
 
 @[to_additive]
 instance : EquivLike (α ≃*o β) α β where

Mathlib/Algebra/Order/Quantale.lean

@@ -176,4 +176,21 @@ theorem rightMulResiduation_le_iff_mul_le : x ≤ y ⇨ᵣ z ↔ y * x ≤ z whe
       iSup_le_iff, implies_true]
   mpr h1 := le_sSup h1
 
+section Zero
+
+variable {α : Type*} [Semigroup α] [CompleteLattice α] [IsQuantale α]
+variable {x : α}
+
+@[to_additive (attr := simp)]
+theorem bot_mul : ⊥ * x = ⊥ := by
+  rw [← sSup_empty, sSup_mul_distrib]
+  simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]
+
+@[to_additive (attr := simp)]
+theorem mul_bot : x * ⊥ = ⊥ := by
+  rw [← sSup_empty, mul_sSup_distrib]
+  simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]
+
+end Zero
+
 end IsQuantale

Mathlib/Algebra/Polynomial/Degree/Domain.lean

@@ -40,6 +40,15 @@ lemma natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p*q).natDegree = p.natDegre
   rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
     Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]
 
+variable (p) in
+lemma natDegree_smul (ha : a ≠ 0) : (a • p).natDegree = p.natDegree := by
+  by_cases hp : p = 0
+  · simp only [hp, smul_zero]
+  · apply natDegree_eq_of_le_of_coeff_ne_zero
+    · exact (natDegree_smul_le _ _).trans (le_refl _)
+    · simpa only [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq, mul_eq_zero,
+        leadingCoeff_eq_zero, not_or] using ⟨ha, hp⟩
+
 @[simp]
 lemma natDegree_pow (p : R[X]) (n : ℕ) : natDegree (p ^ n) = n * natDegree p := by
   classical

Mathlib/Analysis/Calculus/ContDiff/Defs.lean

@@ -107,12 +107,7 @@ attribute [local instance 1001]
 
 open Set Fin Filter Function
 
-/-- Smoothness exponent for analytic functions. -/
-scoped [ContDiff] notation3 "ω" => (⊤ : WithTop ℕ∞)
-/-- Smoothness exponent for infinitely differentiable functions. -/
-scoped [ContDiff] notation3 "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞)
-
-open ContDiff
+open scoped ContDiff
 
 universe u uE uF uG uX
 

Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

@@ -98,18 +98,20 @@ In this file, we denote `⊤ : ℕ∞` with `∞`.
 
 noncomputable section
 
-open scoped Classical
-open ENat NNReal Topology Filter
-
-local notation "∞" => (⊤ : ℕ∞)
+open ENat NNReal Topology Filter Set Fin Filter Function
 
 /-
 Porting note: These lines are not required in Mathlib4.
 attribute [local instance 1001]
   NormedAddCommGroup.toAddCommGroup NormedSpace.toModule' AddCommGroup.toAddCommMonoid
 -/
 
-open Set Fin Filter Function
+/-- Smoothness exponent for analytic functions. -/
+scoped [ContDiff] notation3 "ω" => (⊤ : WithTop ℕ∞)
+/-- Smoothness exponent for infinitely differentiable functions. -/
+scoped [ContDiff] notation3 "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞)
+
+open scoped ContDiff
 
 universe u uE uF
 
@@ -129,7 +131,7 @@ Notice that `p` does not sum up to `f` on the diagonal (`FormalMultilinearSeries
 structure HasFTaylorSeriesUpToOn
   (n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F) (s : Set E) : Prop where
   zero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
-  protected fderivWithin : ∀ m : ℕ, (m : ℕ∞) < n → ∀ x ∈ s,
+  protected fderivWithin : ∀ m : ℕ, m < n → ∀ x ∈ s,
     HasFDerivWithinAt (p · m) (p x m.succ).curryLeft s x
   cont : ∀ m : ℕ, m ≤ n → ContinuousOn (p · m) s
 
@@ -609,7 +611,7 @@ theorem HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn
     (hx : x ∈ s) : p x m = iteratedFDerivWithin 𝕜 m f s x := by
   induction' m with m IH generalizing x
   · rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp]; rfl
-  · have A : (m : ℕ∞) < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
+  · have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
     have :
       HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
         (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
@@ -807,7 +809,7 @@ theorem iteratedFDerivWithin_univ {n : ℕ} :
     rw [iteratedFDeriv_succ_apply_left, iteratedFDerivWithin_succ_apply_left, IH, fderivWithin_univ]
 
 theorem HasFTaylorSeriesUpTo.eq_iteratedFDeriv
-    (h : HasFTaylorSeriesUpTo n f p) {m : ℕ} (hmn : (m : ℕ∞) ≤ n) (x : E) :
+    (h : HasFTaylorSeriesUpTo n f p) {m : ℕ} (hmn : m ≤ n) (x : E) :
     p x m = iteratedFDeriv 𝕜 m f x := by
   rw [← iteratedFDerivWithin_univ]
   rw [← hasFTaylorSeriesUpToOn_univ_iff] at h

Mathlib/Combinatorics/Enumerative/Catalan.lean

@@ -30,7 +30,7 @@ triangulations of convex polygons.
 * `catalan_eq_centralBinom_div`: The explicit formula for the Catalan number using the central
   binomial coefficient, `catalan n = Nat.centralBinom n / (n + 1)`.
 
-* `treesOfNodesEq_card_eq_catalan`: The number of binary trees with `n` internal nodes
+* `treesOfNumNodesEq_card_eq_catalan`: The number of binary trees with `n` internal nodes
   is `catalan n`
 
 ## Implementation details

Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

@@ -211,7 +211,7 @@ instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] : SmoothInv₀ 𝓘(𝕜)
     exact contDiffAt_inv 𝕜 hx
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [TopologicalSpace H] {E : Type*}
-  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type*}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*}
   [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type*}
   [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
   {I' : ModelWithCorners 𝕜 E' H'} {M : Type*} [TopologicalSpace M] [ChartedSpace H' M]
@@ -227,23 +227,23 @@ include I in
 This is not an instance for technical reasons, see
 note [Design choices about smooth algebraic structures]. -/
 theorem hasContinuousInv₀_of_hasSmoothInv₀ : HasContinuousInv₀ G :=
-  { continuousAt_inv₀ := fun _ hx ↦ (contMDiffAt_inv₀ I hx).continuousAt }
+  { continuousAt_inv₀ := fun _ hx ↦ (contMDiffAt_inv₀ (I := I) hx).continuousAt }
 
 theorem contMDiffOn_inv₀ : ContMDiffOn I I ⊤ (Inv.inv : G → G) {0}ᶜ := fun _x hx =>
-  (contMDiffAt_inv₀ I hx).contMDiffWithinAt
+  (contMDiffAt_inv₀ hx).contMDiffWithinAt
 
 @[deprecated (since := "2024-11-21")] alias smoothOn_inv₀ := contMDiffOn_inv₀
 @[deprecated (since := "2024-11-21")] alias SmoothOn_inv₀ := contMDiffOn_inv₀
 
-variable {I} {s : Set M} {a : M}
+variable {s : Set M} {a : M}
 
 theorem ContMDiffWithinAt.inv₀ (hf : ContMDiffWithinAt I' I n f s a) (ha : f a ≠ 0) :
     ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s a :=
-  ((contMDiffAt_inv₀ I ha).of_le le_top).comp_contMDiffWithinAt a hf
+  ((contMDiffAt_inv₀ ha).of_le le_top).comp_contMDiffWithinAt a hf
 
 theorem ContMDiffAt.inv₀ (hf : ContMDiffAt I' I n f a) (ha : f a ≠ 0) :
     ContMDiffAt I' I n (fun x ↦ (f x)⁻¹) a :=
-  ((contMDiffAt_inv₀ I ha).of_le le_top).comp a hf
+  ((contMDiffAt_inv₀ ha).of_le le_top).comp a hf
 
 theorem ContMDiff.inv₀ (hf : ContMDiff I' I n f) (h0 : ∀ x, f x ≠ 0) :
     ContMDiff I' I n (fun x ↦ (f x)⁻¹) :=

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -1051,6 +1051,10 @@ theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid {f : PartialHomeomorp
   rintro e (rfl : e = PartialHomeomorph.refl H)
   exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩
 
+theorem StructureGroupoid.maximalAtlas_mono {G G' : StructureGroupoid H} (h : G ≤ G') :
+    G.maximalAtlas M ⊆ G'.maximalAtlas M :=
+  fun _ he e' he' ↦ ⟨h (he e' he').1, h (he e' he').2⟩
+
 end MaximalAtlas
 
 section Singleton

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -479,6 +479,21 @@ theorem contMDiffOn_iff :
     convert hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1
     mfld_set_tac
 
+/-- zero-smoothness on a set is equivalent to continuity on this set. -/
+theorem contMDiffOn_zero_iff :
+    ContMDiffOn I I' 0 f s ↔ ContinuousOn f s := by
+  rw [contMDiffOn_iff]
+  refine ⟨fun h ↦ h.1, fun h ↦ ⟨h, ?_⟩⟩
+  intro x y
+  rw [show ((0 : ℕ∞) : WithTop ℕ∞) = 0 by rfl, contDiffOn_zero]
+  apply (continuousOn_extChartAt _).comp
+  · apply h.comp ((continuousOn_extChartAt_symm _).mono inter_subset_left) (fun z hz ↦ ?_)
+    simp only [preimage_inter, mem_inter_iff, mem_preimage] at hz
+    exact hz.2.1
+  · intro z hz
+    simp only [preimage_inter, mem_inter_iff, mem_preimage] at hz
+    exact hz.2.2
+
 /-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
 extended chart in the target. -/
 theorem contMDiffOn_iff_target :
@@ -525,6 +540,11 @@ theorem contMDiff_iff_target :
 
 @[deprecated (since := "2024-11-20")] alias smooth_iff_target := contMDiff_iff_target
 
+/-- zero-smoothness is equivalent to continuity. -/
+theorem contMDiff_zero_iff :
+    ContMDiff I I' 0 f ↔ Continuous f := by
+  rw [← contMDiffOn_univ, continuous_iff_continuousOn_univ, contMDiffOn_zero_iff]
+
 end SmoothManifoldWithCorners
 
 /-! ### Deducing smoothness from smoothness one step beyond -/

Mathlib/Geometry/Manifold/Diffeomorph.lean

@@ -79,9 +79,7 @@ scoped[Manifold] notation M " ≃ₘ^" n:1000 "⟮" I ", " J "⟯ " N => Diffeom
 scoped[Manifold] notation M " ≃ₘ⟮" I ", " J "⟯ " N => Diffeomorph I J M N ⊤
 
 /-- `n`-times continuously differentiable diffeomorphism between `E` and `E'`. -/
-scoped[Manifold]
-  notation E " ≃ₘ^" n:1000 "[" 𝕜 "] " E' =>
-    Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n
+scoped[Manifold] notation E " ≃ₘ^" n:1000 "[" 𝕜 "] " E' => Diffeomorph 𝓘(𝕜, E) 𝓘(𝕜, E') E E' n
 
 /-- Infinitely differentiable diffeomorphism between `E` and `E'`. -/
 scoped[Manifold]

Mathlib/Geometry/Manifold/Instances/Real.lean

@@ -14,16 +14,18 @@ or with boundary or with corners. As a concrete example, we construct explicitly
 boundary structure on the real interval `[x, y]`.
 
 More specifically, we introduce
-* `ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)` for the model space
+* `modelWithCornersEuclideanHalfSpace n :
+  ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)` for the model space
   used to define `n`-dimensional real manifolds with boundary
-* `ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)` for the model space used
+* `modelWithCornersEuclideanQuadrant n :
+  ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)` for the model space used
   to define `n`-dimensional real manifolds with corners
 
 ## Notations
 
 In the locale `Manifold`, we introduce the notations
 * `𝓡 n` for the identity model with corners on `EuclideanSpace ℝ (Fin n)`
-* `𝓡∂ n` for `ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)`.
+* `𝓡∂ n` for `modelWithCornersEuclideanHalfSpace n`.
 
 For instance, if a manifold `M` is boundaryless, smooth and modelled on `EuclideanSpace ℝ (Fin m)`,
 and `N` is smooth with boundary modelled on `EuclideanHalfSpace n`, and `f : M → N` is a smooth

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

@@ -79,7 +79,7 @@ theorem Differentiable.comp_mdifferentiable {g : F → F'} {f : M → F} (hg : D
 
 end Module
 
-/-! ### Linear maps between normed spaces are smooth -/
+/-! ### Linear maps between normed spaces are differentiable -/
 
 #adaptation_note
 /--
@@ -189,8 +189,8 @@ theorem MDifferentiable.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F
     (hg : MDifferentiable I 𝓘(𝕜, F₁ →L[𝕜] F₃) g) (hf : MDifferentiable I 𝓘(𝕜, F₂ →L[𝕜] F₁) f) :
     MDifferentiable I 𝓘(𝕜, F₂ →L[𝕜] F₃) fun x => (g x).comp (f x) := fun x => (hg x).clm_comp (hf x)
 
-/-- Applying a linear map to a vector is smooth within a set. Version in vector spaces. For a
-version in nontrivial vector bundles, see `MDifferentiableWithinAt.clm_apply_of_inCoordinates`. -/
+/-- Applying a linear map to a vector is differentiable within a set. Version in vector spaces. For
+a version in nontrivial vector bundles, see `MDifferentiableWithinAt.clm_apply_of_inCoordinates`. -/
 theorem MDifferentiableWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
     (hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x)
     (hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x) :
@@ -201,7 +201,7 @@ theorem MDifferentiableWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f :
         exact differentiable_fst.clm_apply differentiable_snd) (hg.prod_mk_space hf)
     (by simp_rw [mapsTo_univ])
 
-/-- Applying a linear map to a vector is smooth. Version in vector spaces. For a
+/-- Applying a linear map to a vector is differentiable. Version in vector spaces. For a
 version in nontrivial vector bundles, see `MDifferentiableAt.clm_apply_of_inCoordinates`. -/
 theorem MDifferentiableAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M}
     (hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x) (hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x) :
@@ -282,7 +282,7 @@ theorem MDifferentiable.clm_prodMap {g : M → F₁ →L[𝕜] F₃} {f : M →
     MDifferentiable I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) fun x => (g x).prodMap (f x) := fun x =>
   (hg x).clm_prodMap (hf x)
 
-/-! ### Smoothness of scalar multiplication -/
+/-! ### Differentiability of scalar multiplication -/
 
 variable {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V]
 

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -48,12 +48,14 @@ but add these assumptions later as needed. (Quite a few results still do not req
   `extChartAt I x` is the canonical such partial equiv around `x`.
 
 As specific examples of models with corners, we define (in `Geometry.Manifold.Instances.Real`)
-* `modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))` for the model space used to define
+* `modelWithCornersEuclideanHalfSpace n :
+  ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)` for the model space
   `n`-dimensional real manifolds without boundary (with notation `𝓡 n` in the locale `Manifold`)
 * `ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)` for the model space
   used to define `n`-dimensional real manifolds with boundary (with notation `𝓡∂ n` in the locale
   `Manifold`)
-* `ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)` for the model space used
+* `modelWithCornersEuclideanQuadrant n :
+  ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)` for the model space used
   to define `n`-dimensional real manifolds with corners
 
 With these definitions at hand, to invoke an `n`-dimensional real manifold without boundary,
@@ -369,7 +371,7 @@ protected theorem secondCountableTopology [SecondCountableTopology E] (I : Model
   I.isClosedEmbedding.isEmbedding.secondCountableTopology
 
 include I in
-/-- Every smooth manifold is a Fréchet space (T1 space) -- regardless of whether it is
+/-- Every manifold is a Fréchet space (T1 space) -- regardless of whether it is
 Hausdorff. -/
 protected theorem t1Space (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : T1Space M := by
   have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space