Porting note: added to ease automation

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to added to ease automation.

Examples

mathlib4/Mathlib/AlgebraicGeometry/Scheme.lean

Lines 62 to 64 in 9a04ccc

	-- porting note: added to ease automation
	@[continuity]
	lemma Hom.continuous {X Y : Scheme} (f : X ⟶ Y) : Continuous f.1.base := f.1.base.2

mathlib4/Mathlib/AlgebraicTopology/SimplicialObject.lean

Lines 449 to 453 in 9a04ccc

	-- porting note: added to ease automation
	@[ext]
	lemma hom_ext {X Y : CosimplicialObject C} (f g : X ⟶ Y)
	(h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g :=
	NatTrans.ext _ _ (by ext; apply h)

mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Lines 206 to 212 in 9a04ccc

	-- porting note: added the next two lemmas to ease automation; without these lemmas,
	-- `limit.hom_ext` would be applied, but the goal would involve terms
	-- in `Discrete β` rather than `β` itself
	@[ext 1050]
	lemma Pi.hom_ext {f : β → C} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ f)
	(h : ∀ (b : β), g₁ ≫ Pi.π f b = g₂ ≫ Pi.π f b) : g₁ = g₂ :=
	limit.hom_ext (fun ⟨j⟩ => h j)