chore(*): linting (#9342)

src/set_theory/surreal/basic.lean

@@ -104,6 +104,9 @@ theorem numeric_neg : Π {x : pgame} (o : numeric x), numeric (-x)
 ⟨λ j i, lt_iff_neg_gt.1 (o.1 i j),
   ⟨λ j, numeric_neg (o.2.2 j), λ i, numeric_neg (o.2.1 i)⟩⟩
 
+-- We provide this as an analogue for `numeric.move_left_le`,
+-- even though it does not need the `numeric` hypothesis.
+@[nolint unused_arguments]
 theorem numeric.move_left_lt {x : pgame.{u}} (o : numeric x) (i : x.left_moves) :
   x.move_left i < x :=
 begin
@@ -116,6 +119,9 @@ theorem numeric.move_left_le {x : pgame} (o : numeric x) (i : x.left_moves) :
   x.move_left i ≤ x :=
 le_of_lt (o.move_left i) o (o.move_left_lt i)
 
+-- We provide this as an analogue for `numeric.le_move_right`,
+-- even though it does not need the `numeric` hypothesis.
+@[nolint unused_arguments]
 theorem numeric.lt_move_right {x : pgame} (o : numeric x) (j : x.right_moves) :
   x < x.move_right j :=
 begin
@@ -129,7 +135,7 @@ theorem numeric.le_move_right {x : pgame} (o : numeric x) (j : x.right_moves) :
 le_of_lt o (o.move_right j) (o.lt_move_right j)
 
 theorem add_lt_add
-  {w x y z : pgame.{u}} (ow : numeric w) (ox : numeric x) (oy : numeric y) (oz : numeric z)
+  {w x y z : pgame.{u}} (oy : numeric y) (oz : numeric z)
   (hwx : w < x) (hyz : y < z) : w + y < x + z :=
 begin
   rw lt_def_le at *,
@@ -168,13 +174,9 @@ theorem numeric_add : Π {x y : pgame} (ox : numeric x) (oy : numeric y), numeri
    { show xL ix + ⟨yl, yr, yL, yR⟩ < xR jx + ⟨yl, yr, yL, yR⟩,
      exact add_lt_add_right (ox.1 ix jx), },
    { show xL ix + ⟨yl, yr, yL, yR⟩ < ⟨xl, xr, xL, xR⟩ + yR jy,
-     apply add_lt_add (ox.move_left ix) ox oy (oy.move_right jy),
-     apply ox.move_left_lt,
-     apply oy.lt_move_right },
+     exact add_lt_add oy (oy.move_right jy) (ox.move_left_lt _) (oy.lt_move_right _), },
    { --  show ⟨xl, xr, xL, xR⟩ + yL iy < xR jx + ⟨yl, yr, yL, yR⟩, -- fails?
-     apply add_lt_add ox (ox.move_right jx) (oy.move_left iy) oy,
-     apply ox.lt_move_right,
-     apply oy.move_left_lt, },
+     exact add_lt_add (oy.move_left iy) oy (ox.lt_move_right _) (oy.move_left_lt _), },
    { --  show ⟨xl, xr, xL, xR⟩ + yL iy < ⟨xl, xr, xL, xR⟩ + yR jy, -- fails?
      exact @add_lt_add_left ⟨xl, xr, xL, xR⟩ _ _ (oy.1 iy jy), }
  end,

src/topology/category/Top/open_nhds.lean

@@ -16,6 +16,7 @@ variables {X Y : Top.{u}} (f : X ⟶ Y)
 
 namespace topological_space
 
+/-- The type of open neighbourhoods of a point `x` in a (bundled) topological space. -/
 def open_nhds (x : X) := { U : opens X // x ∈ U }
 
 namespace open_nhds
@@ -61,6 +62,8 @@ The inclusion `U ⊓ V ⟶ V` as a morphism in the category of open sets.
 def inf_le_right {x : X} (U V : open_nhds x) : U ⊓ V ⟶ V :=
 hom_of_le inf_le_right
 
+/-- The inclusion functor from open neighbourhoods of `x`
+to open sets in the ambient topological space. -/
 def inclusion (x : X) : open_nhds x ⥤ opens X :=
 full_subcategory_inclusion _
 
@@ -85,6 +88,8 @@ by simp
 @[simp] lemma op_map_id_obj (x : X) (U : (open_nhds x)ᵒᵖ) : (map (𝟙 X) x).op.obj U = U :=
 by simp
 
+/-- `opens.map f` and `open_nhds.map f` form a commuting square (up to natural isomorphism)
+with the inclusion functors into `opens X`. -/
 def inclusion_map_iso (x : X) : inclusion (f x) ⋙ opens.map f ≅ map f x ⋙ inclusion x :=
 nat_iso.of_components
   (λ U, begin split, exact 𝟙 _, exact 𝟙 _ end)

src/topology/category/UniformSpace.lean

@@ -74,6 +74,7 @@ instance : has_coe_to_sort CpltSepUniformSpace :=
 
 attribute [instance] is_uniform_space is_complete_space is_separated
 
+/-- The function forgetting that a complete separated uniform spaces is complete and separated. -/
 def to_UniformSpace (X : CpltSepUniformSpace) : UniformSpace :=
 UniformSpace.of X
 

src/topology/compact_open.lean

@@ -44,6 +44,7 @@ section compact_open
 variables {α : Type*} {β : Type*} {γ : Type*}
 variables [topological_space α] [topological_space β] [topological_space γ]
 
+/-- A generating set for the compact-open topology (when `s` is compact and `u` is open). -/
 def compact_open.gen (s : set α) (u : set β) : set C(α,β) := {f | f '' s ⊆ u}
 
 -- The compact-open topology on the space of continuous maps α → β.
@@ -79,10 +80,13 @@ end functorial
 section ev
 
 variables (α β)
+
+/-- The evaluation map `map C(α, β) × α → β` -/
 def ev (p : C(α, β) × α) : β := p.1 p.2
 
 variables {α β}
--- The evaluation map C(α, β) × α → β is continuous if α is locally compact.
+
+/-- The evaluation map `C(α, β) × α → β` is continuous if `α` is locally compact. -/
 lemma continuous_ev [locally_compact_space α] : continuous (ev α β) :=
 continuous_iff_continuous_at.mpr $ assume ⟨f, x⟩ n hn,
   let ⟨v, vn, vo, fxv⟩ := mem_nhds_iff.mp hn in
@@ -209,6 +213,9 @@ end Inf_induced
 section coev
 
 variables (α β)
+
+/-- The coevaluation map `β → C(α, β × α)` sending a point `x : β` to the continuous function
+on `α` sending `y` to `(x, y)`. -/
 def coev (b : β) : C(α, β × α) := ⟨λ a, (b, a), continuous.prod_mk continuous_const continuous_id⟩
 
 variables {α β}

src/topology/sheaves/presheaf.lean

@@ -30,6 +30,7 @@ variables (C : Type u) [category.{v} C]
 
 namespace Top
 
+/-- The category of `C`-valued presheaves on a (bundled) topological space `X`. -/
 @[derive category]
 def presheaf (X : Top.{v}) := (opens X)ᵒᵖ ⥤ C
 
@@ -51,6 +52,10 @@ infix ` _* `: 80 := pushforward_obj
   {U V : (opens Y)ᵒᵖ} (i : U ⟶ V) :
   (f _* ℱ).map i = ℱ.map ((opens.map f).op.map i) := rfl
 
+/--
+An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf
+along those maps.
+-/
 def pushforward_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf C) :
   f _* ℱ ≅ g _* ℱ :=
 iso_whisker_right (nat_iso.op (opens.map_iso f g h).symm) ℱ
@@ -76,6 +81,8 @@ rfl
 namespace pushforward
 variables {X : Top.{v}} (ℱ : X.presheaf C)
 
+/-- The natural isomorphism between the pushforward of a presheaf along the identity continuous map
+and the original presheaf. -/
 def id : (𝟙 X) _* ℱ ≅ ℱ :=
 (iso_whisker_right (nat_iso.op (opens.map_id X).symm) ℱ) ≪≫ functor.left_unitor _
 
@@ -91,6 +98,9 @@ local attribute [tidy] tactic.op_induction'
 @[simp] lemma id_inv_app' (U) (p) : (id ℱ).inv.app (op ⟨U, p⟩) = ℱ.map (𝟙 (op ⟨U, p⟩)) :=
 by { dsimp [id], simp, }
 
+/-- The natural isomorphism between
+the pushforward of a presheaf along the composition of two continuous maps and
+the corresponding pushforward of a pushforward. -/
 def comp {Y Z : Top.{v}} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ) :=
 iso_whisker_right (nat_iso.op (opens.map_comp f g).symm) ℱ
 

src/topology/sheaves/stalks.lean

@@ -291,6 +291,8 @@ end
 
 variables (C)
 
+/-- A continuous map `X ⟶ Y` induces a morphism
+from the `f _* ℱ` stalk at `f x` to the `ℱ` stalk at `x`. -/
 def stalk_pushforward (f : X ⟶ Y) (ℱ : X.presheaf C) (x : X) : (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
 begin
   -- This is a hack; Lean doesn't like to elaborate the term written directly.