style: reduce spacing variation in "porting note" comments (#10886)

In this pull request, I have systematically eliminated the leading whitespace preceding the colon (`:`) within all unlabelled or unclassified porting notes. This adjustment facilitates a more efficient review process for the remaining notes by ensuring no entries are overlooked due to formatting inconsistencies.

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -129,7 +129,7 @@ theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType.{w} F) :=
 
 @[simp]
 theorem quot_neg (x) :
-    -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
+    -- Porting note: force Lean to treat `ColimitType F` no as `Quot _`
     (by exact Quot.mk Setoid.r (neg x) : ColimitType.{w} F) =
       -(by exact Quot.mk Setoid.r x) :=
   rfl
@@ -138,7 +138,7 @@ theorem quot_neg (x) :
 @[simp]
 theorem quot_add (x y) :
     (by exact Quot.mk Setoid.r (add x y) : ColimitType.{w} F) =
-      -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
+      -- Porting note: force Lean to treat `ColimitType F` no as `Quot _`
       (by exact Quot.mk Setoid.r x) + (by exact Quot.mk Setoid.r y) :=
   rfl
 #align AddCommGroup.colimits.quot_add AddCommGroupCat.Colimits.quot_add
@@ -220,7 +220,7 @@ def descFun (s : Cocone F) : ColimitType.{w} F → s.pt := by
 def descMorphism (s : Cocone F) : colimit.{w} F ⟶ s.pt where
   toFun := descFun F s
   map_zero' := rfl
-  -- Porting note : in `mathlib3`, nothing needs to be done after `induction`
+  -- Porting note: in `mathlib3`, nothing needs to be done after `induction`
   map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp; rw [← quot_add F]; rfl
 #align AddCommGroup.colimits.desc_morphism AddCommGroupCat.Colimits.descMorphism
 

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -375,7 +375,7 @@ noncomputable instance forgetPreservesLimitsOfSize :
     PreservesLimitsOfSize.{v, v} (forget CommGroupCatMax.{v, u}) where
   preservesLimitsOfShape {J _} :=
   { preservesLimit := fun {F} =>
-    -- Porting note : add these instance to help Lean unify universe levels
+    -- Porting note: add these instance to help Lean unify universe levels
     letI : HasLimit (F ⋙ forget₂ CommGroupCatMax.{v, u} GroupCat.{max v u}) :=
       (GroupCat.hasLimitsOfSize.{v, u}.1 J).1 _
     letI h1 := CommGroupCat.forget₂CommMonPreservesLimitsOfSize.{v, u}
@@ -413,7 +413,7 @@ def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
         dsimp
         simp }
   inv := kernel.lift f (AddSubgroup.subtype f.ker) <| by
-    -- porting note : used to be `tidy`, but `aesop` can't do it
+    -- Porting note: used to be `tidy`, but `aesop` can't do it
     refine DFunLike.ext _ _ ?_
     rintro ⟨x, (hx : f _ = 0)⟩
     exact hx
@@ -452,7 +452,7 @@ theorem kernelIsoKer_inv_comp_ι {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker_inv_comp_ι AddCommGroupCat.kernelIsoKer_inv_comp_ι
 
--- Porting note : explicitly add what to be synthesized under `simps!`, because other lemmas
+-- Porting note: explicitly add what to be synthesized under `simps!`, because other lemmas
 -- automatically generated is not in normal form
 /-- The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
 agrees with the `subtype` map.

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -64,7 +64,7 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
     -- Porting note: broken dot notation
     apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1
     convert h
-    -- Porting note : no longer necessary
+    -- Porting note: no longer necessary
     -- exact Submodule.liftQ_mkQ _ _ _
 #align Module.cokernel_is_colimit ModuleCat.cokernelIsColimit
 

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -128,7 +128,7 @@ theorem colimitMulAux_eq_of_rel_left {x x' y : Σ j, F.obj j}
   use s, α, γ
   dsimp
   simp_rw [MonoidHom.map_mul]
-  -- Porting note : Lean cannot seem to use lemmas from concrete categories directly
+  -- Porting note: Lean cannot seem to use lemmas from concrete categories directly
   change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ =
     (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
   simp_rw [← F.map_comp, h₁, h₂, h₃, F.map_comp]
@@ -153,7 +153,7 @@ theorem colimitMulAux_eq_of_rel_right {x y y' : Σ j, F.obj j}
   use s, α, γ
   dsimp
   simp_rw [MonoidHom.map_mul]
-  -- Porting note : Lean cannot seem to use lemmas from concrete categories directly
+  -- Porting note: Lean cannot seem to use lemmas from concrete categories directly
   change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ =
     (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
   simp_rw [← F.map_comp, h₁, h₂, h₃, F.map_comp]
@@ -196,7 +196,7 @@ theorem colimit_mul_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1
   use s, α, β
   dsimp
   simp_rw [MonoidHom.map_mul]
-  -- Porting note : Lean cannot seem to use lemmas from concrete categories directly
+  -- Porting note: Lean cannot seem to use lemmas from concrete categories directly
   change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ =
     (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
   simp_rw [← F.map_comp, h₁, h₂]
@@ -213,15 +213,15 @@ noncomputable instance colimitMulOneClass : MulOneClass (M.{v, u} F) :=
       cases' x with j x
       rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, 1⟩ ⟨j, x⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one,
         one_mul, F.map_id]
-      -- Porting note : `id_apply` does not work here, but the two sides are def-eq
+      -- Porting note: `id_apply` does not work here, but the two sides are def-eq
       rfl
     mul_one := fun x => by
       refine Quot.inductionOn x ?_
       intro x
       cases' x with j x
       rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, 1⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one,
         mul_one, F.map_id]
-      -- Porting note : `id_apply` does not work here, but the two sides are def-eq
+      -- Porting note: `id_apply` does not work here, but the two sides are def-eq
       rfl }
 
 @[to_additive]
@@ -314,7 +314,7 @@ def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt where
     dsimp [Types.colimitCoconeIsColimit]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
     erw [MonoidHom.map_mul]
-    -- Porting note : `rw` can't see through coercion is actually forgetful functor,
+    -- Porting note: `rw` can't see through coercion is actually forgetful functor,
     -- so can't rewrite `t.w_apply`
     congr 1 <;>
     exact t.w_apply _ _

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -67,7 +67,7 @@ instance : ConcreteCategory SemiRingCat := by
 instance : CoeSort SemiRingCat (Type*) where
   coe X := X.α
 
--- Porting note : Hinting to Lean that `forget R` and `R` are the same
+-- Porting note: Hinting to Lean that `forget R` and `R` are the same
 unif_hint forget_obj_eq_coe (R : SemiRingCat) where ⊢
   (forget SemiRingCat).obj R ≟ R
 
@@ -193,7 +193,7 @@ instance : CoeSort RingCat (Type*) where
 
 instance (X : RingCat) : Ring X := X.str
 
--- Porting note : Hinting to Lean that `forget R` and `R` are the same
+-- Porting note: Hinting to Lean that `forget R` and `R` are the same
 unif_hint forget_obj_eq_coe (R : RingCat) where ⊢
   (forget RingCat).obj R ≟ R
 
@@ -298,7 +298,7 @@ instance : CoeSort CommSemiRingCat (Type*) where
 
 instance (X : CommSemiRingCat) : CommSemiring X := X.str
 
--- Porting note : Hinting to Lean that `forget R` and `R` are the same
+-- Porting note: Hinting to Lean that `forget R` and `R` are the same
 unif_hint forget_obj_eq_coe (R : CommSemiRingCat) where ⊢
   (forget CommSemiRingCat).obj R ≟ R
 
@@ -419,7 +419,7 @@ instance : ConcreteCategory CommRingCat := by
 instance : CoeSort CommRingCat (Type*) where
   coe X := X.α
 
--- Porting note : Hinting to Lean that `forget R` and `R` are the same
+-- Porting note: Hinting to Lean that `forget R` and `R` are the same
 unif_hint forget_obj_eq_coe (R : CommRingCat) where ⊢
   (forget CommRingCat).obj R ≟ R
 
@@ -557,7 +557,7 @@ def commRingCatIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y :=
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.CommRing_iso_to_ring_equiv CategoryTheory.Iso.commRingCatIsoToRingEquiv
 
--- Porting note : make this high priority to short circuit simplifier
+-- Porting note: make this high priority to short circuit simplifier
 @[simp (high)]
 theorem commRingIsoToRingEquiv_toRingHom {X Y : CommRingCat} (i : X ≅ Y) :
     i.commRingCatIsoToRingEquiv.toRingHom = i.hom := by
@@ -566,7 +566,7 @@ theorem commRingIsoToRingEquiv_toRingHom {X Y : CommRingCat} (i : X ≅ Y) :
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.CommRing_iso_to_ring_equiv_to_ring_hom CategoryTheory.Iso.commRingIsoToRingEquiv_toRingHom
 
--- Porting note : make this high priority to short circuit simplifier
+-- Porting note: make this high priority to short circuit simplifier
 @[simp (high)]
 theorem commRingIsoToRingEquiv_symm_toRingHom {X Y : CommRingCat} (i : X ≅ Y) :
     i.commRingCatIsoToRingEquiv.symm.toRingHom = i.inv := by

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -151,7 +151,7 @@ instance ColimitType.AddGroup : AddGroup (ColimitType F) where
   add_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ =>
     Quotient.sound <| Relation.add_assoc _ _ _
 
--- Porting note : failed to derive `Inhabited` instance
+-- Porting note: failed to derive `Inhabited` instance
 instance InhabitedColimitType : Inhabited <| ColimitType F where
   default := 0
 
@@ -189,13 +189,13 @@ theorem quot_one : Quot.mk Setoid.r one = (1 : ColimitType F) :=
 
 @[simp]
 theorem quot_neg (x : Prequotient F) :
-    -- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type
+    -- Porting note: Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type
     -- annotation unless we use `by exact` to change the elaboration order.
     (by exact Quot.mk Setoid.r (neg x) : ColimitType F) = -(by exact Quot.mk Setoid.r x) :=
   rfl
 #align CommRing.colimits.quot_neg CommRingCat.Colimits.quot_neg
 
--- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
+-- Porting note: Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
 -- unless we use `by exact` to change the elaboration order.
 @[simp]
 theorem quot_add (x y) :
@@ -204,7 +204,7 @@ theorem quot_add (x y) :
   rfl
 #align CommRing.colimits.quot_add CommRingCat.Colimits.quot_add
 
--- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
+-- Porting note: Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
 -- unless we use `by exact` to change the elaboration order.
 @[simp]
 theorem quot_mul (x y) :

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -99,7 +99,7 @@ def pushoutCoconeIsColimit : Limits.IsColimit (pushoutCocone f g) :=
           exact
             (s.ι.naturality Limits.WalkingSpan.Hom.snd).trans
               (s.ι.naturality Limits.WalkingSpan.Hom.fst).symm }
-    -- Porting note : Lean has forget why `A ⊗[R] B` makes sense
+    -- Porting note: Lean has forget why `A ⊗[R] B` makes sense
     letI : Algebra R A := f.toAlgebra
     letI : Algebra R B := g.toAlgebra
     letI : Algebra R (pushoutCocone f g).pt := show Algebra R (A ⊗[R] B) by infer_instance
@@ -108,13 +108,13 @@ def pushoutCoconeIsColimit : Limits.IsColimit (pushoutCocone f g) :=
     simp only [pushoutCocone_inl, pushoutCocone_inr]
     constructor
     · ext x
-      -- Porting note : Lean can't see through `forget` functor
+      -- Porting note: Lean can't see through `forget` functor
       letI : Semiring ((forget CommRingCat).obj A) := A.str.toSemiring
       letI : Algebra R ((forget CommRingCat).obj A) := show Algebra R A by infer_instance
       exact Algebra.TensorProduct.productMap_left_apply _ _ x
     constructor
     · ext x
-      -- Porting note : Lean can't see through `forget` functor
+      -- Porting note: Lean can't see through `forget` functor
       letI : Semiring ((forget CommRingCat).obj B) := B.str.toSemiring
       letI : Algebra R ((forget CommRingCat).obj B) := show Algebra R B by infer_instance
       exact Algebra.TensorProduct.productMap_right_apply _ _ x
@@ -266,7 +266,7 @@ set_option linter.uppercaseLean3 false in
 def equalizerForkIsLimit : IsLimit (equalizerFork f g) := by
   fapply Fork.IsLimit.mk'
   intro s
-  -- Porting note : Lean can't see through `(parallelPair f g).obj zero`
+  -- Porting note: Lean can't see through `(parallelPair f g).obj zero`
   haveI : SubsemiringClass (Subring A) ((parallelPair f g).obj WalkingParallelPair.zero) :=
     show SubsemiringClass (Subring A) A by infer_instance
   use s.ι.codRestrict _ fun x => (ConcreteCategory.congr_hom s.condition x : _)

Mathlib/Algebra/Category/Ring/Limits.lean

@@ -49,7 +49,7 @@ set_option linter.uppercaseLean3 false in
 /-- The flat sections of a functor into `SemiRingCat` form a subsemiring of all sections.
 -/
 def sectionsSubsemiring (F : J ⥤ SemiRingCatMax.{v, u}) : Subsemiring.{max v u} (∀ j, F.obj j) :=
-  -- Porting note : if `f` and `g` were inlined, it does not compile
+  -- Porting note: if `f` and `g` were inlined, it does not compile
   letI f : J ⥤ AddMonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} AddCommMonCat.{max v u} ⋙
     forget₂ AddCommMonCat AddMonCat
   letI g : J ⥤ MonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} MonCat.{max v u}
@@ -68,7 +68,7 @@ set_option linter.uppercaseLean3 false in
 /-- `limit.π (F ⋙ forget SemiRingCat) j` as a `RingHom`. -/
 def limitπRingHom (F : J ⥤ SemiRingCatMax.{v, u}) (j) :
     (Types.limitCone.{v, u} (F ⋙ forget SemiRingCat)).pt →+* (F ⋙ forget SemiRingCat).obj j :=
-  -- Porting note : if `f` and `g` were inlined, it does not compile
+  -- Porting note: if `f` and `g` were inlined, it does not compile
   letI f : J ⥤ AddMonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} AddCommMonCat.{max v u} ⋙
     forget₂ AddCommMonCat AddMonCat
   { AddMonCat.limitπAddMonoidHom f j,
@@ -224,7 +224,7 @@ and then reuse the existing limit.
 -/
 instance (F : J ⥤ CommSemiRingCatMax.{v, u}) :
     CreatesLimit F (forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u}) :=
-  -- Porting note : `CommSemiRingCat ⥤ Type` reflecting isomorphism is needed to make Lean see that
+  -- Porting note: `CommSemiRingCat ⥤ Type` reflecting isomorphism is needed to make Lean see that
   -- `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism. `CommSemiRingCat ⥤ Type` reflecting
   -- isomorphism is added manually since Lean can't see it, but even with this addition Lean can not
   -- see `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism, so this instance is also added.
@@ -427,7 +427,7 @@ set_option linter.uppercaseLean3 false in
 -/
 def forget₂AddCommGroupPreservesLimitsAux (F : J ⥤ RingCatMax.{v, u}) :
     IsLimit ((forget₂ RingCatMax.{v, u} AddCommGroupCat).mapCone (limitCone.{v, u} F)) := by
-  -- Porting note : inline `f` would not compile
+  -- Porting note: inline `f` would not compile
   letI f := (F ⋙ forget₂ RingCatMax.{v, u} AddCommGroupCat.{max v u})
   apply AddCommGroupCat.limitConeIsLimit.{v, u} f
 set_option linter.uppercaseLean3 false in
@@ -505,7 +505,7 @@ instance (F : J ⥤ CommRingCatMax.{v, u}) :
     ```
     but it seems this would introduce additional identity morphisms in `limit.π`.
     -/
-    -- Porting note : need to add these instances manually
+    -- Porting note: need to add these instances manually
     letI : ReflectsIsomorphisms (forget₂ CommRingCatMax.{v, u} RingCatMax.{v, u}) :=
       CategoryTheory.reflectsIsomorphisms_forget₂ _ _
     letI c : Cone F :=
@@ -536,7 +536,7 @@ instance (F : J ⥤ CommRingCatMax.{v, u}) :
 (Generally, you'll just want to use `limit F`.)
 -/
 def limitCone (F : J ⥤ CommRingCatMax.{v, u}) : Cone F :=
-  -- Porting note : add this manually to get `liftLimit`
+  -- Porting note: add this manually to get `liftLimit`
   letI : HasLimitsOfSize RingCatMax.{v, u} := RingCat.hasLimitsOfSize.{v, u}
   liftLimit (limit.isLimit (F ⋙ forget₂ CommRingCatMax.{v, u} RingCatMax.{v, u}))
 set_option linter.uppercaseLean3 false in
@@ -553,7 +553,7 @@ set_option linter.uppercaseLean3 false in
 /- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of commutative rings has all limits. -/
 instance hasLimitsOfSize : HasLimitsOfSize.{v, v} CommRingCatMax.{v, u} :=
-  -- Porting note : add this manually to get `liftLimit`
+  -- Porting note: add this manually to get `liftLimit`
   letI : HasLimitsOfSize RingCatMax.{v, u} := RingCat.hasLimitsOfSize.{v, u}
   { has_limits_of_shape := fun {_ _} =>
       { has_limit := fun F => hasLimit_of_created F

Mathlib/Algebra/Category/SemigroupCat/Basic.lean

@@ -49,7 +49,7 @@ namespace MagmaCat
 @[to_additive]
 instance bundledHom : BundledHom @MulHom :=
   ⟨@MulHom.toFun, @MulHom.id, @MulHom.comp,
-    --Porting note : was `@MulHom.coe_inj` which is deprecated
+    --Porting note: was `@MulHom.coe_inj` which is deprecated
     by intros; apply @DFunLike.coe_injective, by aesop_cat, by aesop_cat⟩
 #align Magma.bundled_hom MagmaCat.bundledHom
 #align AddMagma.bundled_hom AddMagmaCat.bundledHom
@@ -66,7 +66,7 @@ attribute [to_additive] instMagmaCatLargeCategory instConcreteCategory
 instance : CoeSort MagmaCat (Type*) where
   coe X := X.α
 
--- Porting note : Hinting to Lean that `forget R` and `R` are the same
+-- Porting note: Hinting to Lean that `forget R` and `R` are the same
 unif_hint forget_obj_eq_coe (R : MagmaCat) where ⊢
   (forget MagmaCat).obj R ≟ R
 unif_hint _root_.AddMagmaCat.forget_obj_eq_coe (R : AddMagmaCat) where ⊢
@@ -155,7 +155,7 @@ attribute [to_additive] instSemigroupCatLargeCategory SemigroupCat.instConcreteC
 instance : CoeSort SemigroupCat (Type*) where
   coe X := X.α
 
--- Porting note : Hinting to Lean that `forget R` and `R` are the same
+-- Porting note: Hinting to Lean that `forget R` and `R` are the same
 unif_hint forget_obj_eq_coe (R : SemigroupCat) where ⊢
   (forget SemigroupCat).obj R ≟ R
 unif_hint _root_.AddSemigroupCat.forget_obj_eq_coe (R : AddSemigroupCat) where ⊢

Mathlib/Algebra/Group/Aut.lean

@@ -291,7 +291,7 @@ theorem conj_symm_apply [AddGroup G] (g h : G) : (conj g).symm h = -g + h + g :=
   rfl
 #align add_aut.conj_symm_apply AddAut.conj_symm_apply
 
--- Porting note : the exact translation of this mathlib3 lemma would be`(-conj g) h = -g + h + g`,
+-- Porting note: the exact translation of this mathlib3 lemma would be`(-conj g) h = -g + h + g`,
 -- but this no longer pass the simp_nf linter, as the LHS simplifies by `toMul_neg` to
 -- `(Additive.toMul (conj g))⁻¹`.
 @[simp]

Mathlib/Algebra/Group/Pi/Basic.lean

@@ -465,13 +465,13 @@ protected def prod (f' : ∀ i, f i) (g' : ∀ i, g i) (i : I) : f i × g i :=
   (f' i, g' i)
 #align pi.prod Pi.prod
 
--- Porting note : simp now unfolds the lhs, so we are not marking these as simp.
+-- Porting note: simp now unfolds the lhs, so we are not marking these as simp.
 -- @[simp]
 theorem prod_fst_snd : Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id :=
   rfl
 #align pi.prod_fst_snd Pi.prod_fst_snd
 
--- Porting note : simp now unfolds the lhs, so we are not marking these as simp.
+-- Porting note: simp now unfolds the lhs, so we are not marking these as simp.
 -- @[simp]
 theorem prod_snd_fst : Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = Prod.swap :=
   rfl

Mathlib/Algebra/Order/Pointwise.lean

@@ -27,7 +27,7 @@ open Pointwise
 
 variable {α : Type*}
 
--- Porting note : Swapped the place of `CompleteLattice` and `ConditionallyCompleteLattice`
+-- Porting note: Swapped the place of `CompleteLattice` and `ConditionallyCompleteLattice`
 -- due to simpNF problem between `sSup_xx` `csSup_xx`.
 
 section CompleteLattice