chore(Logic/Relation): use ≤ to spell subrelation

[SnirBroshi]

Replace every ∀ x y, r x y → r' x y with r ≤ r'

---

NOTE: this PR began as an effort to use Subrelation since ≤ wasn't available in this file, but it was agreed on Zulip to instead make ≤ available there.

• depends on: [Merged by Bors] - refactor(Order/Basic): move Pi & Prop orders to a new file #40658

[github-actions]

PR summary 79563b8dc5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Relation	81	82	+1 (+1.23%)

Import changes for all files

Files

Import difference

202 files Mathlib.Algebra.AddTorsor.Defs Mathlib.Algebra.CharZero.AddMonoidHom Mathlib.Algebra.Divisibility.Prod Mathlib.Algebra.Field.Equiv Mathlib.Algebra.Field.Opposite Mathlib.Algebra.Field.Power Mathlib.Algebra.FreeMonoid.Basic Mathlib.Algebra.FreeMonoid.Count 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.Embedding Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Defs Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Int.Even Mathlib.Algebra.Group.Int.TypeTags Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Nat.Hom Mathlib.Algebra.Group.Nat.TypeTags Mathlib.Algebra.Group.NatPowAssoc Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.Pi.Units Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.TypeTags.Basic Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.ULift Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.Group.WithOne.Basic 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.Equiv Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.ProdHom Mathlib.Algebra.GroupWithZero.Prod Mathlib.Algebra.GroupWithZero.ULift Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.GroupWithZero.WithZero Mathlib.Algebra.Homology.ComplexShape Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Homology.HasNoLoop Mathlib.Algebra.Homology.SpectralSequence.ComplexShape Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.End Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.NatInt Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Module.Torsion.Field Mathlib.Algebra.Module.Torsion.Free Mathlib.Algebra.Module.Torsion.Prod Mathlib.Algebra.NoZeroSMulDivisors.Basic Mathlib.Algebra.NoZeroSMulDivisors.Defs Mathlib.Algebra.NonAssoc.PreLie.Basic Mathlib.Algebra.Opposites Mathlib.Algebra.Regular.Opposite Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.Associator Mathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.Divisibility.Basic Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Int.Parity Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Parity Mathlib.Algebra.Ring.Torsion Mathlib.Algebra.Ring.Units Mathlib.Algebra.Ring.WithZero Mathlib.Algebra.Torsor.Defs Mathlib.CategoryTheory.Bicategory.Adjunction.Basic Mathlib.CategoryTheory.Bicategory.Adjunction.Mate Mathlib.CategoryTheory.Bicategory.Basic Mathlib.CategoryTheory.Category.Basic Mathlib.CategoryTheory.Category.KleisliCat Mathlib.CategoryTheory.Functor.Basic Mathlib.CategoryTheory.Functor.Category Mathlib.CategoryTheory.Functor.FullyFaithful Mathlib.CategoryTheory.Functor.Functorial Mathlib.CategoryTheory.Functor.ReflectsIso.Basic Mathlib.CategoryTheory.Functor.Trifunctor Mathlib.CategoryTheory.HomCongr Mathlib.CategoryTheory.InducedCategory Mathlib.CategoryTheory.Iso Mathlib.CategoryTheory.NatIso Mathlib.CategoryTheory.NatTrans Mathlib.CategoryTheory.Sigma.Basic Mathlib.CategoryTheory.Thin Mathlib.CategoryTheory.Whiskering Mathlib.Combinatorics.Quiver.Basic Mathlib.Combinatorics.Quiver.Cast Mathlib.Combinatorics.Quiver.ConnectedComponent Mathlib.Combinatorics.Quiver.Covering Mathlib.Combinatorics.Quiver.Path Mathlib.Combinatorics.Quiver.Prefunctor Mathlib.Combinatorics.Quiver.Push Mathlib.Combinatorics.Quiver.Schreier Mathlib.Combinatorics.Quiver.SingleObj Mathlib.Combinatorics.Quiver.Subquiver Mathlib.Combinatorics.Quiver.Symmetric Mathlib.Control.EquivFunctor Mathlib.Control.Monad.Basic Mathlib.Control.Monad.Cont Mathlib.Control.Monad.Writer Mathlib.Control.Traversable.Equiv Mathlib.Control.ULiftable Mathlib.Data.Countable.Defs Mathlib.Data.Erased Mathlib.Data.Finite.Defs Mathlib.Data.Int.Cast.Lemmas Mathlib.Data.Int.Cast.Prod Mathlib.Data.List.AList Mathlib.Data.List.OffDiag Mathlib.Data.List.Pairwise Mathlib.Data.List.Perm.Basic Mathlib.Data.List.Perm.Subperm Mathlib.Data.List.Sigma Mathlib.Data.Nat.Cast.Basic Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.Cast.Field Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Nat.EvenOddRec Mathlib.Data.Nat.Factorial.Cast Mathlib.Data.Opposite Mathlib.Data.Quot Mathlib.Data.Set.Opposite Mathlib.Data.SubtypeNeLift Mathlib.Data.ULift Mathlib.GroupTheory.GroupAction.Hom 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.Functor Mathlib.Logic.Equiv.Option Mathlib.Logic.Equiv.Prod Mathlib.Logic.Equiv.Sum Mathlib.Logic.Relation Mathlib.Logic.Small.Defs Mathlib.Logic.UnivLE Mathlib.SetTheory.Cardinal.Defs Mathlib.Tactic.Abel Mathlib.Tactic.CategoryTheory.BicategoricalComp Mathlib.Tactic.CategoryTheory.Bicategory.Basic Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes Mathlib.Tactic.CategoryTheory.Bicategory.Normalize Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence Mathlib.Tactic.CategoryTheory.CancelIso Mathlib.Tactic.CategoryTheory.CheckCompositions Mathlib.Tactic.CategoryTheory.Coherence.Basic Mathlib.Tactic.CategoryTheory.IsoReassoc Mathlib.Tactic.CategoryTheory.Reassoc Mathlib.Tactic.DeriveFintype Mathlib.Tactic.NoncommRing Mathlib.Tactic.NormNum.Basic Mathlib.Tactic.NormNum.BigOperators Mathlib.Tactic.NormNum.Core Mathlib.Tactic.NormNum.Parity Mathlib.Tactic.NormNum.PowMod Mathlib.Tactic.NormNum.Pow Mathlib.Tactic.NormNum.Result Mathlib.Tactic.Positivity.Finset Mathlib.Tactic.ProdAssoc Mathlib.Tactic.ProxyType Mathlib.Tactic.ReduceModChar Mathlib.Tactic.Widget.CommDiag

1

---

Declarations diff (regex)

+ irrefl_iff_le_ne
+ refl_iff_eq_le
+++ le_reflTransGen
++-- to_reflTransGen
+-+- mono

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 79563b8).

• +5 new declarations
• −0 removed declarations

+Relation.ReflGen.le_reflTransGen
+Relation.ReflTransGen.le_reflTransGen
+Relation.TransGen.le_reflTransGen
+irrefl_iff_le_ne
+refl_iff_eq_le

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 79563b8dc5
Reference commit 8b068a6bd8

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.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).

[thorimur]

Thanks for this PR! :) I'd like to give this a quick review, but just a quick question first: has this refactor to Subrelation been discussed on Zulip?

This refactor makes sense to me personally (and I'm glad it makes sense to Violeta as well!) but if it hasn't been discussed yet, it would be nice to reach some consensus and give people an opportunity to comment, especially if this will have ripple effects across Mathlib. It does change the argument plicity, after all (requiring some new @s), and suggests that maybe some other theorems in Mathlib should (in the future) be stated (and named) in terms of Subrelation too.

If it has already been discussed, linking the Zulip thread in the commit message will help keep changes like this in context. :)

[SnirBroshi]

has this refactor to Subrelation been discussed on Zulip?

Not yet, I've opened a topic with my thoughts: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2330526.20use.20Subrelation.20in.20Mathlib.2ELogic.2ERelation/with/546572676

[thorimur]

Awesome, thanks! :) (I'll mark this awaiting-zulip for the time being.)

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[vihdzp]

To recap what's been said on Zulip, I think we should rather move the ≤ instance on pi types to a more basic file, and remove all use of Subrelation.

[SnirBroshi]

I found ~10 lines that got caught in the turmoil and indeed no longer need changing (the <| places previously needed other fixes), but it seems minor, most of the changes do need to happen.

(is that move the only relevant change, or did I overlook something?)

Wdym, what about the PR title and description? The major change is the spelling, that's what this PR is about.
Modules other than Logic/Relation mostly got hit by the binder change that's caused by it.

[joneugster]

Wdym, what about the PR title and description?

Thank you for updating the PR! Title and description is fine. Last time I couldn't quite tell if it was title/description or content which was outdated but you've cleaned it up nicely. Sorry if that caused confusion.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - refactor(Order/Basic): move Pi & Prop orders to a new file #40658
  By Dependent Issues (🤖). Happy coding!

[plp127]

Relation.ReflGen.le_reflTransGen is sort of a weird name, since this is not a statement which is more "about" ReflGen than it is about ReflTransGen, can this be Relation.reflGen_le_reflTransGen instead? (same below for transGen_le_reflTransGen)

[SnirBroshi]

No, then we'll lose the dot-notation

[plp127]

When I have h : Foo and I see h.le_bar I'm expecting that to be a proof of _ ≤ bar taking Foo as an assumption, for example Fin.le_last or LT.lt.le or GaloisConnection.le_iff_le. But in this case we have h : ReflGen r a b and h.le_reflTransGen has type ReflTransGen r a b, which breaks that expectation, so I claim we shouldn't have this dot notation anyways.

[SnirBroshi]

That's why I said I think the previous state was the best, can I revert the rename?

[plp127]

in the previous state, there is no indication from the name that the lemma statement contains ≤, which also breaks my expectation

[SnirBroshi]

So what do you suggest?

[plp127]

I would suggest just duplicating it