chore: make Injective and Surjective fun_propable

[MichaelStollBayreuth]

---

[github-actions]

PR summary 8e01cc0328

Import changes exceeding 2%

%	File
+22.09%	Mathlib.Logic.Function.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Function.Basic	86	105	+19 (+22.09%)

Import changes for all files

Files	Import difference
3 files Mathlib.Order.ScottContinuity.Complete Mathlib.Order.ScottContinuity.Prod Mathlib.Order.ScottContinuity	3
368 files Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.ModEq Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Pointwise.Set.Small Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.MulOpposite Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Support Mathlib.Algebra.Group.TypeTags.Pointwise Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero Mathlib.Algebra.GroupWithZero.Submonoid.Instances Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Notation.Indicator Mathlib.Algebra.Notation.Support Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.Archimedean.Defs Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Equiv Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.Submonoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.IsBotOne Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Lex Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Defs Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.Ring.Unbundled.Basic Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Submonoid.Basic Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Ring.Torsion Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Ring.Units Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Weight Mathlib.Control.Fix Mathlib.Data.Bool.Set Mathlib.Data.Bundle Mathlib.Data.Countable.Small Mathlib.Data.FP.Basic Mathlib.Data.FunLike.Graded Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.Range Mathlib.Data.List.Iterate Mathlib.Data.List.SplitLengths Mathlib.Data.List.TakeWhile Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.Cast.Synonym Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Log Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.Pairing Mathlib.Data.Nat.Set Mathlib.Data.Nat.Upto Mathlib.Data.Nat.WithBot Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PEquiv Mathlib.Data.PFun Mathlib.Data.PNat.Defs Mathlib.Data.PNat.Equiv Mathlib.Data.PSigma.Order Mathlib.Data.Part Mathlib.Data.Prod.Lex Mathlib.Data.Rel.Cover Mathlib.Data.Rel.Separated Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Basic Mathlib.Data.Set.BoolIndicator Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Insert Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Order Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Chain Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Restrict Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.Subsingleton Mathlib.Data.Set.SymmDiff Mathlib.Data.Set.UnionLift Mathlib.Data.SetLike.Basic Mathlib.Data.Setoid.Basic Mathlib.Data.Sigma.Order Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.InformationTheory.Coding.UniquelyDecodable Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.Nat Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Function.DependsOn Mathlib.Logic.Function.FiberPartition Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.Order.Antichain Mathlib.Order.Antisymmetrization Mathlib.Order.Basic Mathlib.Order.BooleanAlgebra.Basic Mathlib.Order.BooleanAlgebra.Defs Mathlib.Order.BooleanAlgebra.Set Mathlib.Order.Booleanisation Mathlib.Order.BoundedOrder.Basic Mathlib.Order.BoundedOrder.Lattice Mathlib.Order.BoundedOrder.Monotone Mathlib.Order.Bounded Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Circular Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Group Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.ConditionallyCompletePartialOrder.Basic Mathlib.Order.ConditionallyCompletePartialOrder.Defs Mathlib.Order.ConditionallyCompletePartialOrder.Indexed Mathlib.Order.Copy Mathlib.Order.Directed Mathlib.Order.Disjoint Mathlib.Order.Extension.Linear Mathlib.Order.Filter.AtTopBot.Basic Mathlib.Order.Filter.AtTopBot.CompleteLattice Mathlib.Order.Filter.AtTopBot.Defs Mathlib.Order.Filter.AtTopBot.Disjoint Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Map Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Ring Mathlib.Order.Filter.AtTopBot.Tendsto Mathlib.Order.Filter.Bases.Basic Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Curry Mathlib.Order.Filter.Defs Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Lift Mathlib.Order.Filter.Map Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Prod Mathlib.Order.Filter.SmallSets Mathlib.Order.Filter.Tendsto Mathlib.Order.GaloisConnection.Basic Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Hom Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.Basic Mathlib.Order.Hom.BoundedLattice Mathlib.Order.Hom.Bounded Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Lattice Mathlib.Order.Hom.Lex Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Hom.WithTopBot Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Lex Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.LinearOrder Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.Iterate Mathlib.Order.Lattice.Congruence Mathlib.Order.LatticeIntervals Mathlib.Order.Lattice Mathlib.Order.Lex Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Minimal Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Monovary Mathlib.Order.Monotone.Odd Mathlib.Order.Monotone.Union Mathlib.Order.Nat Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.OrderDual Mathlib.Order.Preorder.Chain Mathlib.Order.Prod.Lex.Hom Mathlib.Order.PropInstances Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.RelIso.Set Mathlib.Order.SemiconjSup Mathlib.Order.SetIsMax Mathlib.Order.Set Mathlib.Order.SymmDiff Mathlib.Order.Synonym Mathlib.Order.Types.Defs Mathlib.Order.ULift Mathlib.Order.UpperLower.Relative Mathlib.Order.WellFounded Mathlib.Order.WithBotTop Mathlib.Order.WithBot Mathlib.Order.Zorn Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.OreLocalization.OreSet Mathlib.RingTheory.RingInvo Mathlib.SetTheory.Lists Mathlib.SetTheory.ZFC.PSet Mathlib.Tactic.ApplyFun Mathlib.Tactic.CancelDenoms.Core Mathlib.Tactic.DeriveCountable Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Tactic.NormNum.Core Mathlib.Tactic.NormNum.Parity Mathlib.Tactic.Peel Mathlib.Tactic.Zify	17
28 files Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.GrindInstances Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.Idempotent Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Int.Defs Mathlib.Combinatorics.Quiver.ConnectedComponent Mathlib.Combinatorics.Quiver.Subquiver Mathlib.Data.Int.Basic Mathlib.Data.Int.Cast.Basic Mathlib.Data.Int.Cast.Field Mathlib.Data.Int.Cast.Prod Mathlib.Data.Int.NatAbs Mathlib.Data.Nat.PSub Mathlib.Data.Set.Notation Mathlib.Data.Set.Operations Mathlib.Data.Set.Opposite Mathlib.Dynamics.FixedPoints.Defs Mathlib.GroupTheory.GroupAction.Hom Mathlib.Order.SetNotation Mathlib.Tactic.NormNum.Result	18
151 files Mathlib.Algebra.AddTorsor.Defs Mathlib.Algebra.Field.MinimalAxioms Mathlib.Algebra.Free Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Defs Mathlib.Algebra.Group.Action.Faithful Mathlib.Algebra.Group.Action.Hom Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Option Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Action.Sigma Mathlib.Algebra.Group.Action.Sum Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.Basic Mathlib.Algebra.Group.Commute.Basic Mathlib.Algebra.Group.Commute.Hom Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Defs Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Group.Ext Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Algebra.Group.Hom.Defs Mathlib.Algebra.Group.Hom.End Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.Group.Idempotent Mathlib.Algebra.Group.InjSurj Mathlib.Algebra.Group.Int.TypeTags Mathlib.Algebra.Group.Int.Units Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.ModEq Mathlib.Algebra.Group.Nat.Hom Mathlib.Algebra.Group.Nat.TypeTags Mathlib.Algebra.Group.Nat.Units Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.Pi.Basic Mathlib.Algebra.Group.Pi.Units Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Torsion Mathlib.Algebra.Group.TypeTags.Basic Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.ULift Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Faithful Mathlib.Algebra.GroupWithZero.Action.Hom Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Idempotent Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pi Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.ULift Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.Homology.ComplexShape Mathlib.Algebra.Homology.HasNoLoop Mathlib.Algebra.Homology.SpectralSequence.ComplexShape Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Prod Mathlib.Algebra.Notation.Pi.Basic Mathlib.Algebra.Notation.Prod Mathlib.Algebra.Opposites Mathlib.Algebra.Regular.Basic Mathlib.Algebra.Regular.Opposite Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.Ext Mathlib.Algebra.Ring.Hom.InjSurj Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Algebra.Ring.Regular Mathlib.Combinatorics.Quiver.Basic Mathlib.Combinatorics.Quiver.Cast Mathlib.Combinatorics.Quiver.Path Mathlib.Combinatorics.Quiver.Prefunctor Mathlib.Combinatorics.Quiver.Push Mathlib.Combinatorics.Quiver.SingleObj Mathlib.Combinatorics.Quiver.Symmetric Mathlib.Control.EquivFunctor Mathlib.Control.Monad.Basic Mathlib.Control.Monad.Cont Mathlib.Control.Monad.Writer Mathlib.Control.Traversable.Equiv Mathlib.Data.Countable.Defs Mathlib.Data.Erased Mathlib.Data.Finite.Defs Mathlib.Data.FunLike.Basic Mathlib.Data.FunLike.Embedding Mathlib.Data.FunLike.Equiv Mathlib.Data.List.Pairwise Mathlib.Data.Matrix.DMatrix Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Opposite Mathlib.Data.Option.Basic Mathlib.Data.Prod.Basic Mathlib.Data.Quot Mathlib.Data.Sigma.Basic Mathlib.Data.Subtype Mathlib.Data.Sum.Basic Mathlib.Data.ULift Mathlib.GroupTheory.GroupAction.IterateAct Mathlib.GroupTheory.GroupAction.Ring Mathlib.LinearAlgebra.AffineSpace.Defs Mathlib.Logic.Embedding.Basic Mathlib.Logic.Equiv.Basic Mathlib.Logic.Equiv.Bool Mathlib.Logic.Equiv.Defs Mathlib.Logic.Equiv.Option Mathlib.Logic.Equiv.Pairwise Mathlib.Logic.Equiv.Prod Mathlib.Logic.Equiv.Sum Mathlib.Logic.Function.Basic Mathlib.Logic.Function.Conjugate Mathlib.Logic.Function.Iterate Mathlib.Logic.IsEmpty.Basic Mathlib.Logic.IsEmpty Mathlib.Logic.Nontrivial.Basic Mathlib.Logic.Pairwise Mathlib.Logic.Small.Defs Mathlib.Logic.Unique Mathlib.Logic.UnivLE Mathlib.SetTheory.Cardinal.Defs Mathlib.Tactic.Choose Mathlib.Tactic.DeriveFintype Mathlib.Tactic.MoveAdd Mathlib.Tactic.ProdAssoc Mathlib.Tactic.ProxyType	19

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

---

No changes to strong technical debt.

No changes to weak technical debt.