mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance satisfies the triangle inequality.  -/
Metric.hausdorffDist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t u : Set α},
  Metric.hausdorffEDist s t ≠ ⊤ → Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function is non-negative.
 -/
Function.locallyFinsuppWithin.logCounting_nonneg : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {f : Function.locallyFinsupp E ℤ} {r : ℝ},
  0 ≤ f → 1 ≤ r → 0 ≤ Function.locallyFinsuppWithin.logCounting f r
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_y : ∀ (u : PNat.XgcdType), u.flip.y = u.x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.brecOn.eq : ∀ {motive : Turing.PartrecToTM2.Λ' → Sort u} (t : Turing.PartrecToTM2.Λ')
  (F_1 : (t : Turing.PartrecToTM2.Λ') → Turing.PartrecToTM2.Λ'.below t → motive t),
  Turing.PartrecToTM2.Λ'.brecOn t F_1 = F_1 t (Turing.PartrecToTM2.Λ'.brecOn.go t F_1).2
-- Mathlib.Algebra.Free
FreeSemigroup.instSemigroup.eq_1 : ∀ {α : Type u},
  FreeSemigroup.instSemigroup =
    { mul := fun L1 L2 => { head := L1.head, tail := L1.tail ++ L2.head :: L2.tail }, mul_assoc := ⋯ }
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.closed`. -/
Topology.CWComplex.Subcomplex.closed : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), IsClosed ↑E
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α}, ∅.getD a fallback = fallback
-- Mathlib.LinearAlgebra.Span.Basic
/-- If the range of `v : ι → M` generates the whole module and linear maps `f`, `g` are equal at
each `v i`, then they are equal.  -/
LinearMap.ext_on_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {ι : Sort u_8} {v : ι → M} {f g : M →ₛₗ[σ₁₂] M₂},
  Submodule.span R (Set.range v) = ⊤ → (∀ (i : ι), f (v i) = g (v i)) → f = g
-- Mathlib.Algebra.Group.Defs
add_nsmul_add : ∀ {M : Type u_2} [inst : AddMonoid M] (a b : M) (n : ℕ), n • (a + b) + a = a + n • (b + a)
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.traceDual.eq_1 : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] (I : Submodule B L),
  Submodule.traceDual A K I =
    { toAddSubmonoid := ((Algebra.traceForm K L).dualSubmodule (Submodule.restrictScalars A I)).toAddSubmonoid,
      smul_mem' := ⋯ }
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLTD : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → α → α
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The `BicategoricalCoherence` instance.  -/
Mathlib.Tactic.BicategoryLike.CoherenceHom.inst : Mathlib.Tactic.BicategoryLike.CoherenceHom → Lean.Expr
-- Lean.Elab.Quotation.Precheck
_private.Lean.Elab.Quotation.Precheck.0.Lean.Elab.Term.Quotation.isSectionVariable : Lean.Expr → Lean.Elab.TermElabM Bool
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {α₁ β₁ : Type u_1} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type u_1} →
        (it : Std.IterM m (β₁ × β₂)) →
          (motive : it.internalState.left.Step → Sort u_3) →
            (x : it.internalState.left.Step) →
              ((it₁' : Std.IterM m β₁) →
                  (out : β₁) →
                    (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it₁' out)) →
                      motive ⟨Std.IterStep.yield it₁' out, hp⟩) →
                ((it₁' : Std.IterM m β₁) →
                    (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.skip it₁')) →
                      motive ⟨Std.IterStep.skip it₁', hp⟩) →
                  ((hp : it.internalState.left.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩) →
                    motive x
-- Mathlib.CategoryTheory.Monad.Basic
/-- Construct a comonad isomorphism from a natural isomorphism of functors where the forward
direction is a comonad morphism.  -/
CategoryTheory.ComonadIso.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {M N : CategoryTheory.Comonad C} →
      (f : M.toFunctor ≅ N.toFunctor) →
        autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X)
            CategoryTheory.ComonadIso.mk._auto_1 →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) =
                  CategoryTheory.CategoryStruct.comp (M.δ.app X)
                    (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X))))
              CategoryTheory.ComonadIso.mk._auto_3 →
            (M ≅ N)
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.Limits.isLimitOfPreserves.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cone K} (t t_1 : CategoryTheory.Limits.IsLimit c),
  t = t_1 →
    ∀ [inst_3 : CategoryTheory.Limits.PreservesLimit K F],
      CategoryTheory.Limits.isLimitOfPreserves F t = CategoryTheory.Limits.isLimitOfPreserves F t_1
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddGrpCat AddMonCat
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.ne : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos → startPos ≠ endPos
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_of_empty_codomain : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [IsEmpty β] (f : α → β),
  Measurable f
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.mk.injEq : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (parts : Finset (Finset V)) (card_parts : parts.card = r ∨ t = 0)
  (card_mem_parts : ∀ {p : Finset V}, p ∈ parts → p.card = t)
  (isCompleteBetween : (↑parts).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2) (parts_1 : Finset (Finset V))
  (card_parts_1 : parts_1.card = r ∨ t = 0) (card_mem_parts_1 : ∀ {p : Finset V}, p ∈ parts_1 → p.card = t)
  (isCompleteBetween_1 : (↑parts_1).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2),
  ({ parts := parts, card_parts := card_parts, card_mem_parts := card_mem_parts,
        isCompleteBetween := isCompleteBetween } =
      { parts := parts_1, card_parts := card_parts_1, card_mem_parts := card_mem_parts_1,
        isCompleteBetween := isCompleteBetween_1 }) =
    (parts = parts_1)
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.Hom.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    {D : Type u_4} →
      [inst_1 : CategoryTheory.Category.{u_2, u_4} D] →
        (motive : CategoryTheory.Join C D → CategoryTheory.Join C D → Sort u_5) →
          (x x_1 : CategoryTheory.Join C D) →
            ((x y : C) → motive (CategoryTheory.Join.left x) (CategoryTheory.Join.left y)) →
              ((x y : D) → motive (CategoryTheory.Join.right x) (CategoryTheory.Join.right y)) →
                ((a : C) → (a_1 : D) → motive (CategoryTheory.Join.left a) (CategoryTheory.Join.right a_1)) →
                  ((a : D) → (a_1 : C) → motive (CategoryTheory.Join.right a) (CategoryTheory.Join.left a_1)) →
                    motive x x_1
-- Mathlib.Combinatorics.Graph.Basic
/-- The edge set.  -/
Graph.edgeSet : {α : Type u_3} → {β : Type u_4} → Graph α β → Set β
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instAddMemClass : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M], AddMemClass (ConvexCone R M) M
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.forget₂AddCommMon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ SemiRingCat AddCommMonCat)
-- Lean.Meta.LazyDiscrTree
/-- Find values that match `e` in `root`.
 -/
Lean.Meta.LazyDiscrTree.getMatchCore : {α : Type} →
  Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex →
    Lean.Expr → Lean.Meta.LazyDiscrTree.MatchM α (Lean.Meta.LazyDiscrTree.MatchResult α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.isIso_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.right
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The final vertex of a 2-simplex in a 2-truncated simplicial set.  -/
SSet.Truncated.ev2₂ : {V : SSet.Truncated 2} →
  V.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }) → SSet.OneTruncation₂ V
-- Std.Data.TreeSet.Basic
Std.TreeSet.instRepr : {α : Type u} → {cmp : α → α → Ordering} → [Repr α] → Repr (Std.TreeSet α cmp)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.indep_iff_forall_closure_ssubset_of_ssubset : ∀ {α : Type u_2} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.indep_iff_forall_closure_ssubset_of_ssubset._auto_1 →
    (M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I)
-- Mathlib.Algebra.Order.Monoid.Lex
MonoidHom.fst_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  Monotone ⇑(MonoidHom.fst α β)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- The family of 2-morphisms into a right Kan lift.  -/
CategoryTheory.Bicategory.RightLift.IsKan.desc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.RightLift f g} →
            t.IsKan → (s : CategoryTheory.Bicategory.RightLift f g) → s.lift ⟶ t.lift
-- Mathlib.MeasureTheory.Measure.MeasureSpace
Antitone.measure_iUnion : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α}, Antitone s → μ (⋃ i, s i) = ⨆ i, μ (s i)
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_add_two : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R) (n : ℕ),
  Polynomial.dickson k a (n + 2) =
    Polynomial.X * Polynomial.dickson k a (n + 1) - Polynomial.C a * Polynomial.dickson k a n
-- Mathlib.Topology.Constructions.SumProd
instTopologicalSpaceProd.eq_1 : ∀ {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y],
  instTopologicalSpaceProd = TopologicalSpace.induced Prod.fst t₁ ⊓ TopologicalSpace.induced Prod.snd t₂
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.instPartialOrder : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → PartialOrder (NonUnitalSubsemiring R)
-- Mathlib.Order.Antichain
isAntichain_insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b ∧ ¬r b a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_of_ae_le_mul : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {c : ℝ} {f : α →ₘ[μ] E} {g : ↥(MeasureTheory.Lp F p μ)},
  (∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ c * ‖↑↑g x‖) → f ∈ MeasureTheory.Lp E p μ
-- Mathlib.LinearAlgebra.Span.Defs
/-- A module is principal if it is generated by a single element.  -/
Module.IsPrincipal : (R : Type u_1) → (M : Type u_4) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_of_mem : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {m n : ℕ} {p : MvPolynomial σ R},
  p ∈ MvPolynomial.homogeneousSubmodule σ R n → (MvPolynomial.homogeneousComponent m) p = if m = n then p else 0
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Monotone convergence theorem**, version with `AEMeasurable` functions.  -/
MeasureTheory.lintegral_iSup' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) → ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.forgetStalk_inv_comp_eval : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)),
  CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv
      (TypeCat.ofHom ⇑(CommRingCat.Hom.hom (smoothSheafCommRing.evalHom IM I M R x))) =
    smoothSheaf.evalHom IM I R x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.getKey? a = t_1.getKey? a_1
-- Mathlib.Order.Basic
Preorder.toLE_injective : ∀ {α : Type u_2}, Function.Injective (@Preorder.toLE α)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- A prepartition `π` of `I` is a partition if the boxes of `π` cover the whole `I`.  -/
BoxIntegral.Prepartition.IsPartition : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → Prop
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instZero.eq_1 : ∀ {α : Type u_1} [inst : Zero α], Colex.instZero = inst
-- Lean.DocString.Extension
/-- A block element with a deferred check. The `index` is a 0-based index into the current docstring's
deferred checks, in source order. Block and inline deferred elements share a counter.
 -/
Lean.Doc.Block.deferred : ℕ → Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) → Lean.Doc.Block Lean.ElabInline Lean.ElabBlock
-- Mathlib.Order.Basic
le_iff_eq_or_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b ↔ a = b ∨ a < b
-- Mathlib.Data.Quot
Quot.induction_on₃ : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  {δ : Quot r → Quot s → Quot t → Prop} (q₁ : Quot r) (q₂ : Quot s) (q₃ : Quot t),
  (∀ (a : α) (b : β) (c : γ), δ (Quot.mk r a) (Quot.mk s b) (Quot.mk t c)) → δ q₁ q₂ q₃
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_usize : ∀ (x : USize), ↑x = ↑x.toNat
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.primesOverFinset`.

---

The finite set of all prime factors of the pushforward of `p`.  -/
primesOverFinset : {A : Type u_4} →
  [inst : CommRing A] →
    Ideal A → (B : Type u_5) → [inst_1 : CommRing B] → [IsDedekindDomain B] → [Algebra A B] → Finset (Ideal B)
-- Mathlib.Topology.NhdsSet
/-- **Alias** of the reverse direction of `nhdsSet_eq_principal_iff`. -/
IsOpen.nhdsSet_eq : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → nhdsSet s = Filter.principal s
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instPosSMulReflectLE : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : Preorder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → Preorder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), PosSMulReflectLE α (β i)], PosSMulReflectLE α (Π₀ (i : ι), β i)
-- Mathlib.Data.Fin.SuccPred
Fin.cast_le_cast : ∀ {n m : ℕ} (eq : n = m) {a b : Fin n}, Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b