chore: remove useless include and omit porting notes (#10503)

Mathlib/Algebra/AddTorsor.lean

@@ -248,9 +248,6 @@ section comm
 
 variable {G : Type*} {P : Type*} [AddCommGroup G] [AddTorsor G P]
 
--- Porting note: Removed:
--- include G
-
 /-- Cancellation subtracting the results of two subtractions. -/
 @[simp]
 theorem vsub_sub_vsub_cancel_left (p₁ p₂ p₃ : P) : p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂ := by
@@ -356,9 +353,6 @@ namespace Equiv
 
 variable {G : Type*} {P : Type*} [AddGroup G] [AddTorsor G P]
 
--- Porting note: Removed:
--- include G
-
 /-- `v ↦ v +ᵥ p` as an equivalence. -/
 def vaddConst (p : P) : G ≃ P where
   toFun v := v +ᵥ p
@@ -481,9 +475,6 @@ theorem pointReflection_fixed_iff_of_injective_bit0 {x y : P} (h : Injective (bi
     neg_eq_iff_add_eq_zero, ← bit0, ← bit0_zero, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]
 #align equiv.point_reflection_fixed_iff_of_injective_bit0 Equiv.pointReflection_fixed_iff_of_injective_bit0
 
--- Porting note: Removed:
--- omit G
-
 -- Porting note: need this to calm down CI
 theorem injective_pointReflection_left_of_injective_bit0 {G P : Type*} [AddCommGroup G]
     [AddTorsor G P] (h : Injective (bit0 : G → G)) (y : P) :

Mathlib/Algebra/DirectSum/Basic.lean

@@ -104,9 +104,6 @@ theorem add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i
 
 variable (β)
 
--- Porting note: commented out
--- include dec_ι
-
 /-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
 and has coefficient `x i` for `i` in `s`. -/
 def mk (s : Finset ι) : (∀ i : (↑s : Set ι), β i.1) →+ ⨁ i, β i
@@ -256,9 +253,6 @@ def setToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, β i) →+ ⨁ i : T, β
 
 variable {β}
 
--- Porting note: commented out
--- omit dec_ι
-
 instance unique [∀ i, Subsingleton (β i)] : Unique (⨁ i, β i) :=
   DFinsupp.unique
 #align direct_sum.unique DirectSum.unique
@@ -305,9 +299,6 @@ section Option
 
 variable {α : Option ι → Type w} [∀ i, AddCommMonoid (α i)]
 
--- Porting note: commented out
--- include dec_ι
-
 /-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`.-/
 @[simps!]
 noncomputable def addEquivProdDirectSum : (⨁ i, α i) ≃+ α none × ⨁ i, α (some i) :=

Mathlib/Algebra/Order/Floor.lean

@@ -1628,9 +1628,6 @@ namespace Nat
 variable [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β]
 variable [FunLike F α β] [RingHomClass F α β] {a : α} {b : β}
 
--- Porting note: no longer needed
--- include β
-
 theorem floor_congr (h : ∀ n : ℕ, (n : α) ≤ a ↔ (n : β) ≤ b) : ⌊a⌋₊ = ⌊b⌋₊ := by
   have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
   obtain ha | ha := lt_or_le a 0
@@ -1657,9 +1654,6 @@ namespace Int
 variable [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β]
 variable [FunLike F α β] [RingHomClass F α β] {a : α} {b : β}
 
--- Porting note: no longer needed
--- include β
-
 theorem floor_congr (h : ∀ n : ℤ, (n : α) ≤ a ↔ (n : β) ≤ b) : ⌊a⌋ = ⌊b⌋ :=
   (le_floor.2 <| (h _).1 <| floor_le _).antisymm <| le_floor.2 <| (h _).2 <| floor_le _
 #align int.floor_congr Int.floor_congr
@@ -1687,9 +1681,6 @@ namespace Int
 variable [LinearOrderedField α] [LinearOrderedField β] [FloorRing α] [FloorRing β]
 variable [FunLike F α β] [RingHomClass F α β] {a : α} {b : β}
 
--- Porting note: no longer needed
--- include β
-
 theorem map_round (f : F) (hf : StrictMono f) (a : α) : round (f a) = round a := by
   have H : f 2 = 2 := map_natCast f 2
   simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, H]

Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

@@ -54,9 +54,6 @@ namespace BundledHom
 
 variable [𝒞 : BundledHom hom]
 
--- porting note: include not needed
--- include 𝒞
-
 set_option synthInstance.checkSynthOrder false in
 /-- Every `@BundledHom c _` defines a category with objects in `Bundled c`.
 
@@ -105,9 +102,6 @@ variable (hom)
 
 section
 
--- porting note: commented out
--- omit 𝒞
-
 /-- The `hom` corresponding to first forgetting along `F`, then taking the `hom` associated to `c`.
 
 For typical usage, see the construction of `CommMonCat` from `MonCat`.
@@ -132,9 +126,6 @@ def map (F : ∀ {α}, d α → c α) : BundledHom (MapHom hom @F)
 
 section
 
--- porting note: commented out
---omit 𝒞
-
 /-- We use the empty `ParentProjection` class to label functions like `CommMonoid.toMonoid`,
 which we would like to use to automatically construct `BundledHom` instances from.
 

Mathlib/CategoryTheory/GlueData.lean

@@ -249,9 +249,6 @@ theorem types_ι_jointly_surjective (D : GlueData (Type v)) (x : D.glued) :
 
 variable (F : C ⥤ C') [H : ∀ i j k, PreservesLimit (cospan (D.f i j) (D.f i k)) F]
 
--- porting note: commented out include
--- include H
-
 instance (i j k : D.J) : HasPullback (F.map (D.f i j)) (F.map (D.f i k)) :=
   ⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit F (D.f i j) (D.f i k)⟩⟩⟩
 
@@ -335,16 +332,10 @@ theorem diagramIso_inv_app_right (i : D.J) :
 
 variable [HasMulticoequalizer D.diagram] [PreservesColimit D.diagram.multispan F]
 
--- porting note: commented out omit
--- omit H
-
 theorem hasColimit_multispan_comp : HasColimit (D.diagram.multispan ⋙ F) :=
   ⟨⟨⟨_, PreservesColimit.preserves (colimit.isColimit _)⟩⟩⟩
 #align category_theory.glue_data.has_colimit_multispan_comp CategoryTheory.GlueData.hasColimit_multispan_comp
 
--- porting note: commented out include
--- include H
-
 attribute [local instance] hasColimit_multispan_comp
 
 theorem hasColimit_mapGlueData_diagram : HasMulticoequalizer (D.mapGlueData F).diagram :=
@@ -397,9 +388,6 @@ def vPullbackConeIsLimitOfMap (i j : D.J) [ReflectsLimit (cospan (D.ι i) (D.ι
 set_option linter.uppercaseLean3 false in
 #align category_theory.glue_data.V_pullback_cone_is_limit_of_map CategoryTheory.GlueData.vPullbackConeIsLimitOfMap
 
--- porting note: commenting out omit
--- omit H
-
 /-- If there is a forgetful functor into `Type` that preserves enough (co)limits, then `D.ι` will
 be jointly surjective. -/
 theorem ι_jointly_surjective (F : C ⥤ Type v) [PreservesColimit D.diagram.multispan F]

Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

@@ -2319,8 +2319,6 @@ variable {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶
 
 variable (f₄ : X₃ ⟶ Y₂) [HasPullback f₁ f₂] [HasPullback f₃ f₄]
 
--- include f₁ f₂ f₃ f₄ Porting note: removed
-
 local notation "Z₁" => pullback f₁ f₂
 
 local notation "Z₂" => pullback f₃ f₄
@@ -2520,8 +2518,6 @@ variable {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶
 
 variable (g₄ : Z₂ ⟶ X₃) [HasPushout g₁ g₂] [HasPushout g₃ g₄]
 
--- include g₁ g₂ g₃ g₄ Porting note: removed
-
 local notation "Y₁" => pushout g₁ g₂
 
 local notation "Y₂" => pushout g₃ g₄

Mathlib/CategoryTheory/Sites/CoverLifting.lean

@@ -154,9 +154,6 @@ set_option linter.uppercaseLean3 false in
 
 variable {x} {S}
 
--- porting note: no longer needed
--- include hu hS hx
-
 /-- Given a `G(Y) ⊆ U`, we can find a unique section `X ⟶ ℱ(Y)` that agrees with `x`. -/
 def getSection (Y : StructuredArrow (op U) G.op) : X ⟶ ℱ.val.obj Y.right := by
   letI hom_sh := whiskerRight ((Ran.adjunction A G.op).counit.app ℱ.val) (coyoneda.obj (op X))

Mathlib/GroupTheory/Submonoid/Inverses.lean

@@ -152,9 +152,6 @@ noncomputable def fromCommLeftInv : S.leftInv →* S where
 
 variable (hS : S ≤ IsUnit.submonoid M)
 
--- Porting note: commented out next line
- -- include hS
-
 /-- The submonoid of pointwise inverse of `S` is `MulEquiv` to `S`. -/
 @[to_additive (attr := simps apply) "The additive submonoid of pointwise additive inverse of `S` is
 `AddEquiv` to `S`."]