refactor: change pset to a structure

[Shreyas4991]

I was fiddling with ZFSets when I found that replacing PSets inductive definition with a structure simplified the file. Some proofs were using the wrong API lemmas. The new definition is as follows:

structure PSet : Type (u + 1) where
  «Type» : Type u
  Func : «Type» → PSet

Zulip thread : https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/PSets.20as.20structures.3F/near/625458978

---

[github-actions]

PR summary 08bc8e498a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

- Func
- eta
- mk_func
- mk_type
- «Type»

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 08bc8e4).

• +0 new declarations
• −3 removed declarations

-PSet.eta
-PSet.mk_func
-PSet.mk_type

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 08bc8e498a
Reference commit 0acbe13e16

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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]

!radar

[leanprover-radar]

Benchmark results for d2cfb58 against 0acbe13 are in. No significant results found. @Shreyas4991 @eric-wieser

• 🟥 build//instructions: +8.6G (+0.01%)

No significant changes detected.

[eric-wieser]

I'm not convinced ext is useful here; I'd suggest adding it in a later PR, and only if you have a proof that uses it.

[Shreyas4991]

Done

[eric-wieser]

I think these should be kept but deprecated (and de-simped)

[Shreyas4991]

`[deprecated]` attribute should specify either a new name or a deprecation message

there is no new name to specify