chore: avoid unfold _; infer_instance

[JovanGerb]

Avoid the pattern unfold _; infer_instance whenever possible by using either inferInstanceAs, or deriving.

---

[github-actions]

PR summary 81059bbf91

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement
+ instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement
+ instance (n : ℕ) : TopologicalSpace (Vector α n)
+ instance (x : FGModuleRepr R) : Module.Finite R x
+ instance : Countable (FreeAbelianGroup α) := inferInstanceAs <| Countable (Quot _)
+ instance : Countable (FreeCommRing α)
+ instance : Countable (FreeGroup α) := inferInstanceAs <| Countable (Quot _)
+ instance : Countable (FreeMonoid α) := inferInstanceAs <| Countable (List α)
+ instance : Countable (FreeRing α) := inferInstanceAs <| Countable (Quot _)
+ instance : Decidable (IsPrefix f s) := inferInstanceAs <| Decidable (∀ _, _)
+ instance : DecidableRel (G.replaceVertex s t).Adj := inferInstanceAs <| DecidableRel (mk _ _ _).Adj
+ instance : Definable₂ pair := inferInstanceAs <| Definable₂ fun x y ↦ {{x}, {x, y}}
+ instance : Epi (H0π A) := inferInstanceAs <| Epi (_ ≫ _)
+ instance : Infinite (FreeCommRing α)
+ instance : Infinite (FreeRing α)
+ instance : LinearOrder (MulArchimedeanClass M)
+ instance [DecidableEq α] : DecidableEq (Lists α) := inferInstanceAs <| DecidableEq (Sigma _)
+ instance [F.EssSurj] : F.mapSkeleton.EssSurj := inferInstanceAs <| (_ ⋙ _).EssSurj
+ instance [F.Faithful] : F.mapSkeleton.Faithful := inferInstanceAs <| (_ ⋙ _).Faithful
+ instance [F.Full] : F.mapSkeleton.Full := inferInstanceAs <| (_ ⋙ _).Full
+ instance [Inhabited α] : Inhabited (Antisymmetrization α r)
+ instance [IsEmpty M] : IsEmpty (SingularManifold.empty X M I (k := k)).M
+ instance [IsEmpty α] : Unique (FreeGroup α) := inferInstanceAs <| Unique (Quot _)
+ instance [SizeOf α] : SizeOf (Lists α) := inferInstanceAs <| SizeOf (Sigma _)
+ instance [Subsingleton α] : Subsingleton (Antisymmetrization α r)
+ instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (setOf _)
+ instance π_epi : Epi D.π := inferInstanceAs <| Epi (Multicoequalizer.sigmaπ D.diagram)
++ instance : Epi (H1π A) := inferInstanceAs <| Epi (_ ≫ _)
++ instance : Epi (H2π A) := inferInstanceAs <| Epi (_ ≫ _)
- IsUniform.instDecidableRel
- Machine.inhabited
- decValidFinite
- decidable_enle
- enle.isLinearOrder
- inhabited
- instCountableInterFilter
- instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement := by
- instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement := by
- instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance
- instance (x : FGModuleRepr R) : AddCommGroup x := by
- instance (x : FGModuleRepr R) : Module R x := by
- instance (x : FGModuleRepr R) : Module.Finite R x := by
- instance : (Etale.forget X).Faithful
- instance : (Etale.forget X).Full
- instance : AddCommGroup (PreLp E) := by unfold PreLp; infer_instance
- instance : Category X.Etale
- instance : CommRing (CyclotomicRing n A K)
- instance : CommRing (FiniteElement K) := by
- instance : Countable (FreeAbelianGroup α) := Quotient.countable
- instance : Countable (FreeCommRing α) := by
- instance : Countable (FreeGroup α) := Quotient.countable
- instance : Countable (FreeMonoid α) := by unfold FreeMonoid; infer_instance
- instance : Countable (FreeRing α) := Quotient.countable
- instance : Decidable (IsPrefix f s) := by unfold IsPrefix; infer_instance
- instance : DecidableEq NONote := by unfold NONote; infer_instance
- instance : DecidablePred Decstr := by unfold Decstr; infer_instance
- instance : DecidablePred Goodm := by unfold Goodm; infer_instance
- instance : DecidableRel (G.replaceVertex s t).Adj := by unfold replaceVertex; infer_instance
- instance : Definable₂ pair := by unfold pair; infer_instance
- instance : Epi (H0π A) := by unfold H0π; infer_instance
- instance : Field (CyclotomicField n K)
- instance : HasPullbacks X.Etale := by
- instance : Infinite (FreeCommRing α) := by unfold FreeCommRing; infer_instance
- instance : Infinite (FreeRing α) := by unfold FreeRing; infer_instance
- instance : Inhabited (CyclotomicField n K)
- instance : Inhabited (CyclotomicRing n A K)
- instance : IsDomain (CyclotomicRing n A K)
- instance : IsDomain (FiniteElement K) := by
- instance : IsStrictOrderedRing (FiniteElement K) := by
- instance : LinearOrder (FiniteElement K) := by
- instance : LinearOrder (MulArchimedeanClass M) := by
- instance : Membership MiuAtom Miustr := by unfold Miustr; infer_instance
- instance : MetricSpace (OptimalGHCoupling X Y) := by
- instance : ValuationRing (FiniteElement K) := by
- instance [DecidableEq α] : DecidableEq (Lists α) := by unfold Lists; infer_instance
- instance [F.EssSurj] : F.mapSkeleton.EssSurj := by unfold mapSkeleton; infer_instance
- instance [F.Faithful] : F.mapSkeleton.Faithful := by unfold mapSkeleton; infer_instance
- instance [F.Full] : F.mapSkeleton.Full := by unfold mapSkeleton; infer_instance
- instance [HasGlobalSectionsFunctor J A] : (Γ J A).IsRightAdjoint := by
- instance [Inhabited α] : Inhabited (Antisymmetrization α r) := by
- instance [IsEmpty M] : IsEmpty (SingularManifold.empty X M I (k := k)).M := by
- instance [IsEmpty α] : Unique (FreeGroup α) := by unfold FreeGroup; infer_instance
- instance [SizeOf α] : SizeOf (Lists α) := by unfold Lists; infer_instance
- instance [Subsingleton α] : Subsingleton (Antisymmetrization α r) := by
- instance {k : ℕ} : Fintype (fiber α k) := by unfold fiber; infer_instance
- instance {s : Set Ω} : IsZeroOrProbabilityMeasure (uniformOn s) := by
- instance π_epi : Epi D.π := by
- isAlgebraic_constantsOn
- terminatedAtDecidable
-- instance : Epi (H1π A) := by unfold H1π; infer_instance
-- instance : Epi (H2π A) := by unfold H2π; infer_instance

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.03, 0.03)

Current number	Change	Type
32	-1	backward.inferInstanceAs
8469	-9	backward.isDefEq
1245	-1	backward.privateInPublic

Current commit bcc1137cac
Reference commit 81059bbf91

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Repeating what I said on zulip; should we prefer

Suggested change

	haveI : Encodable (Constructors α) := inferInstanceAs <| Encodable (α ⊕ Unit ⊕ Unit ⊕ Unit)
	haveI : Encodable (Constructors α) := inferInstanceAs <| Encodable (delta% Constructors α)

etc?

[JovanGerb]

It doesn't save that many characters, and I think there is an advantage to being able to see directly what the instance is actually synthesizing.