mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ofFn_blocksFun : ∀ {n : ℕ} (c : Composition n), List.ofFn c.blocksFun = c.blocks
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.find?_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Bool},
  it.find? f =
    match ↑it.step with
    | Std.IterStep.yield it' out => if f out = true then some out else it'.find? f
    | Std.IterStep.skip it' => it'.find? f
    | Std.IterStep.done => none
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.Nat.unaryCast.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.Iterators.Basic
Std.IterM.internalState_mk : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (it : α), { internalState := it }.internalState = it
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.M.isubtree.match_1.eq_2 : ∀ {F : PFunctor.{u_1, u_2}} (motive : PFunctor.Approx.Path F → F.M → Sort u_3) (a : F.A) (i : F.B a) (ps : List F.Idx)
  (x : F.M) (h_1 : (x : F.M) → motive [] x)
  (h_2 : (a : F.A) → (i : F.B a) → (ps : List F.Idx) → (x : F.M) → motive (⟨a, i⟩ :: ps) x),
  (match ⟨a, i⟩ :: ps, x with
    | [], x => h_1 x
    | ⟨a, i⟩ :: ps, x => h_2 a i ps x) =
    h_2 a i ps x
-- Mathlib.Data.Finset.Image
/-- **Alias** of the reverse direction of `Finset.map_nonempty`. -/
Finset.Nonempty.map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, s.Nonempty → (Finset.map f s).Nonempty
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixedField.isScalarTower : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E),
  IsScalarTower (↥K) (↥(IntermediateField.fixedField K.fixingSubgroup)) E
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  ↑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).obj A) = CategoryTheory.Aut A.obj
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.isUnit_one_sub_self_of_mem_nonunits : ∀ {R : Type u_1} [inst : CommRing R] [IsLocalRing R], ∀ a ∈ nonunits R, IsUnit (1 - a)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_four : CartanMatrix.D 4 = !![2, -1, 0, 0; -1, 2, -1, -1; 0, -1, 2, 0; 0, -1, 0, 2]
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  t.WF → (Std.DTreeMap.Raw.filter f t).contains k = Option.any (f k) (t.get? k)
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Typecheck an `AlgHom` as a morphism in `AlgCat`.  -/
AlgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {A B : Type v} →
      [inst_1 : Ring A] →
        [inst_2 : Ring B] →
          [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → (AlgCat.of R A ⟶ AlgCat.of R B)
-- Mathlib.Order.Bounds.Basic
lowerBounds_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β},
  s.Nonempty → t.Nonempty → lowerBounds (s ×ˢ t) = lowerBounds s ×ˢ lowerBounds t
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Hom.hom₂_apply : ∀ {R : Type u_1} [inst : CommRing R] {M N P : ModuleCat R} (f : M ⟶ ModuleCat.of R (N ⟶ P)) (x : ↑M),
  (ModuleCat.Hom.hom₂ f) x = (ModuleCat.ofHom ↑ModuleCat.homLinearEquiv).hom' (f.hom' x)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonTextDocumentClientCapabilities.toJson : Lean.Lsp.TextDocumentClientCapabilities → Lean.Json
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.toPiFork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (K : CategoryTheory.Limits.Multifork I), (CategoryTheory.Limits.Multifork.toPiFork hc hd K).pt = K.pt
-- Mathlib.Control.ULift
/-- Monadic bind.  -/
ULift.bind : {α : Type u} → {β : Type v} → ULift.{u_1, u} α → (α → ULift.{u_2, v} β) → ULift.{u_2, v} β
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_list : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs, suffix := [], property := ⋯ } b; epost ⦄
-- Init.Data.Rat.Lemmas
Rat.num_mul : ∀ (a b : ℚ), (a * b).num = a.num * b.num / ↑((a.num * b.num).natAbs.gcd (a.den * b.den))
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_le_subst_cert : Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.Data.List.ReduceOption
List.reduceOption_nil : ∀ {α : Type u_1}, [].reduceOption = []
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H2Iso.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.H2Iso A =
    (HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 2).leftHomologyIso.symm ≪≫
      CategoryTheory.ShortComplex.leftHomologyMapIso' (groupCohomology.isoShortComplexH2 A)
        (HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 2).leftHomologyData
        (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData
-- Batteries.Data.String.Legacy
/-- Auxuliary definition for `String.Legacy.posOf`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
String.Legacy.posOfAux : String → Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
indicator_iUnion_of_pairwise_disjoint_on_support : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α),
  Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.support f) →
    ∀ (i : β), (⋃ d, s d).indicator f i = ∑' (d : γ), (s d).indicator f i
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Construct a natural isomorphism between functors out of a walking multispan from its
components.  -/
CategoryTheory.Limits.WalkingMultispan.functorExt : {J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan J) C} →
        (left :
            (i : J.L) →
              F.obj (CategoryTheory.Limits.WalkingMultispan.left i) ≅
                G.obj (CategoryTheory.Limits.WalkingMultispan.left i)) →
          (right :
              (i : J.R) →
                F.obj (CategoryTheory.Limits.WalkingMultispan.right i) ≅
                  G.obj (CategoryTheory.Limits.WalkingMultispan.right i)) →
            autoParam
                (∀ (i : J.L),
                  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i))
                      (right (J.fst i)).hom =
                    CategoryTheory.CategoryStruct.comp (left i).hom
                      (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i)))
                CategoryTheory.Limits.WalkingMultispan.functorExt._auto_1 →
              autoParam
                  (∀ (i : J.L),
                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i))
                        (right (J.snd i)).hom =
                      CategoryTheory.CategoryStruct.comp (left i).hom
                        (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i)))
                  CategoryTheory.Limits.WalkingMultispan.functorExt._auto_3 →
                (F ≅ G)
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
Lean.Meta.Grind.Arith.Linear.getStructId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.Data.List.Intervals
List.Ico.filter_lt_of_succ_bot : ∀ {n m : ℕ}, n < m → List.filter (fun x => decide (x < n + 1)) (List.Ico n m) = [n]
-- Init.Data.String.Defs
/-- Predicate for validity of positions inside a `String`.

There are multiple equivalent definitions for validity.

We say that a position is valid if the string obtained by taking all of the bytes up to, but
excluding, the given position, is valid UTF-8; see `Pos.isValid_iff_isValidUTF8_extract_zero`.

Similarly, a position is valid if the string obtained by taking all of the bytes starting at the
given position is valid UTF-8; see `Pos.isValid_iff_isValidUTF8_extract_utf8ByteSize`.

An equivalent condition is that the position is the length of the UTF-8 encoding of
some prefix of the characters of the string; see `Pos.isValid_iff_exists_append` and
`Pos.isValid_iff_exists_take_data`.

Another equivalent condition that can be checked efficiently is that the position is either the
end position or strictly smaller than the end position and the byte at the position satisfies
`UInt8.IsUTF8FirstByte`; see `Pos.isValid_iff_isUTF8FirstByte`.

Examples:
 * `String.Pos.IsValid "abc" ⟨0⟩`
 * `String.Pos.IsValid "abc" ⟨1⟩`
 * `String.Pos.IsValid "abc" ⟨3⟩`
 * `¬ String.Pos.IsValid "abc" ⟨4⟩`
 * `String.Pos.IsValid "𝒫(A)" ⟨0⟩`
 * `¬ String.Pos.IsValid "𝒫(A)" ⟨1⟩`
 * `¬ String.Pos.IsValid "𝒫(A)" ⟨2⟩`
 * `¬ String.Pos.IsValid "𝒫(A)" ⟨3⟩`
 * `String.Pos.IsValid "𝒫(A)" ⟨4⟩`
 -/
String.Pos.Raw.IsValid : String → String.Pos.Raw → Prop
-- Std.Data.HashMap.Basic
Std.HashMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (inner inner_1 : Std.DHashMap α fun x => β),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.vle_one_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x : R}, x ≤ᵥ 1 ↔ v x ≤ 1
-- Mathlib.GroupTheory.Exponent
/-- If two commuting elements `x` and `y` of an additive monoid have order `n` and
`m`, then there is an element of order `lcm n m` that lies in the additive subgroup generated by `x`
and `y`.  -/
AddCommute.exists_addOrderOf_eq_lcm : ∀ (G : Type u) [inst : AddMonoid G] {x y : G},
  AddCommute x y → ∃ z ∈ AddSubmonoid.closure {x, y}, addOrderOf z = (addOrderOf x).lcm (addOrderOf y)
-- Init.Data.List.Impl
/-- Pairs each element of a list with its index, optionally starting from an index other than `0`.

`O(|l|)`. This is a tail-recursive version of `List.zipIdx` that's used at runtime.

Examples:
* `[a, b, c].zipIdxTR = [(a, 0), (b, 1), (c, 2)]`
* `[a, b, c].zipIdxTR 5 = [(a, 5), (b, 6), (c, 7)]`
 -/
List.zipIdxTR : {α : Type u_1} → List α → optParam ℕ 0 → List (α × ℕ)
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.instBEqMorApplication : BEq Mathlib.Meta.FunProp.MorApplication
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_id : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.id.ker = ⊥
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- If `v : ι → E` is an orthonormal family, then `Subtype.val : (range v) → E` is an orthonormal
family.  -/
Orthonormal.toSubtypeRange : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → Orthonormal 𝕜 Subtype.val
-- Init.Data.Array.Lemmas
Array.filterMap_filter : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → Option β} {xs : Array α},
  Array.filterMap f (Array.filter p xs) = Array.filterMap (fun x => if p x = true then f x else none) xs
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.meas_biInter : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ι → Set Ω},
  ProbabilityTheory.iIndepSet f μ → ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w n : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec n → ℕ → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.CategoryTheory.Center.Preadditive
CategoryTheory.CatCenter.app_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (z₁ z₂ : CategoryTheory.CatCenter C) (X : C), (z₁ - z₂).app X = z₁.app X - z₂.app X
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The ring homomorphism `R[W] →+* S[W.map f]` induced by a ring homomorphism `f : R →+* S`.  -/
WeierstrassCurve.Affine.CoordinateRing.map : {R : Type r} →
  {S : Type s} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (W' : WeierstrassCurve.Affine R) → (f : R →+* S) → W'.CoordinateRing →+* (W'.map f).CoordinateRing
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.toLex_monotone : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → PartialOrder (α i)], Monotone ⇑toLex
-- Mathlib.Topology.Compactness.CompactSystem
/-- The set of sets which are either compact and closed, or `univ`, is a compact system.  -/
isCompactSystem_insert_univ_isCompact_isClosed : ∀ (α : Type u_2) [inst : TopologicalSpace α], IsCompactSystem (insert Set.univ {s | IsCompact s ∧ IsClosed s})
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- A complete equipartite subgraph gives rise to a copy of a complete equipartite graph.  -/
SimpleGraph.CompleteEquipartiteSubgraph.toCopy : {V : Type u_1} →
  {G : SimpleGraph V} →
    {r t : ℕ} → G.CompleteEquipartiteSubgraph r t → (SimpleGraph.completeEquipartiteGraph r t).Copy G
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommGroupContinuousMap : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : CommGroup β] → [IsTopologicalGroup β] → CommGroup C(α, β)
-- Batteries.Data.Fin.Lemmas
Fin.prod_succ : ∀ {α : Type u_1} {n : ℕ} [inst : One α] [inst_1 : Mul α] (x : Fin (n + 1) → α),
  Fin.prod x = x 0 * Fin.prod fun x_1 => x x_1.succ
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.backward.dsimp.useDefEqAttr : Lean.Option Bool
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_eq_one_iff : ∀ {R : Type u_1} [inst : Semiring R] {φ : Polynomial R}, ↑φ = 1 ↔ φ = 1
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- `2α + β` is short.  -/
RootPairing.EmbeddedG2.twoShortAddLongRoot_shortRoot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.EmbeddedG2] (B : P.InvariantForm),
  (B.form (RootPairing.EmbeddedG2.twoShortAddLongRoot P)) (RootPairing.EmbeddedG2.twoShortAddLongRoot P) =
    (B.form (RootPairing.EmbeddedG2.shortRoot P)) (RootPairing.EmbeddedG2.shortRoot P)
-- Init.Data.Float.Model.Unpacked.Operations.Sqrt
/-- Computes the square root of a floating-point number and rounds the result according to the given
specification.
 -/
Float.Model.UnpackedFloat.sqrt : Float.Model.Format → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.inter : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsLocalMaxOn f s a → ∀ (t : Set α), IsLocalMaxOn f (s ∩ t) a
-- Lean.Meta.Basic
/-- Backtrackable state for the `MetaM` monad.
 -/
Lean.Meta.SavedState : Type
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.div : ∀ {α : Type u} {β : Type v} [inst : Div β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → f / f' =ᶠ[l] g / g'
-- Init.System.ST
Void.instNonempty : ∀ {σ : Type}, Nonempty (Void σ)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.zeroBasis_repr_apply : ∀ {𝕜 : Type u_1} {α : Type u_3} [inst : NormedRing 𝕜] (x : ↥(lp (fun x => 𝕜) 0)),
  lp.zeroBasis.repr x = Finsupp.ofSupportFinite ↑x ⋯
-- Mathlib.Order.Filter.Extr
IsMaxOn.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → ∀ {g : β → γ}, Monotone g → IsMaxOn (g ∘ f) s a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  [inst_1 : SizeOf ι] (s : ↑P.II) (rank_s : f.rank s = i),
  sizeOf { s := s, rank_s := rank_s } = 1 + sizeOf s + sizeOf rank_s
-- Mathlib.Data.Finset.Slice
Set.Sized.subsingleton : ∀ {α : Type u_1} {A : Set (Finset α)}, Set.Sized 0 A → A.Subsingleton
-- Aesop.Forward.State
Aesop.instInhabitedForwardState.default : Aesop.ForwardState
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq : ∀ {c : Char} {s : String.Slice},
  String.Slice.Pattern.ForwardPattern.skipPrefix? c s =
    String.Slice.Pattern.ForwardPattern.skipPrefix? (fun x => x == c) s
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] {f g : M →+ N}, f = g ↔ ∀ (x : M), f x = g x
-- Lean.Parser.Command
Lean.Parser.Command.moduleDoc.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.equivIsoLimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (i : r ≅ t),
  CategoryTheory.Limits.IsLimit.equivIsoLimit i =
    { toFun := fun h => h.ofIsoLimit i, invFun := fun h => h.ofIsoLimit i.symm, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_mul : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t : Set α}, (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.foldlM_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  t₁.Equiv t₂ → Std.DTreeMap.foldlM f init t₁ = Std.DTreeMap.foldlM f init t₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
isAddFundamentalDomain_Ioc' : ∀ {T : ℝ},
  0 < T →
    ∀ (t : ℝ) (μ : autoParam (MeasureTheory.Measure ℝ) isAddFundamentalDomain_Ioc'._auto_1),
      MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T).op) (Set.Ioc t (t + T)) μ
-- Mathlib.Order.Notation
Top.ext : ∀ {α : Type u_1} {x y : Top α}, ⊤ = ⊤ → x = y
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.fromSigma.eq_1 : ∀ {C : Type u} (F : C → Type v) (c : CategoryTheory.Limits.CofanTypes F) (x : (i : C) × F i),
  CategoryTheory.Limits.CofanTypes.fromSigma F c x = c.inj x.fst x.snd
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  (Std.ExtDHashMap.filter f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => f x_2 (Std.ExtDHashMap.Const.get m x_2 ⋯)
-- Mathlib.Topology.MetricSpace.Pseudo.Real
Real.dist_right_le_of_mem_uIcc : ∀ {x y z : ℝ}, y ∈ Set.uIcc x z → dist y z ≤ dist x z
-- Lean.LibrarySuggestions.Basic
/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs.  -/
Lean.Expr.relevantConstants : Lean.Expr → Lean.MetaM (Array Lean.Name)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_lt_ncard_iff_ncard_sdiff_lt_ncard_sdiff`. -/
Set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_lt_ncard_iff_ncard_sdiff_lt_ncard_sdiff._auto_1 →
    autoParam t.Finite Set.ncard_lt_ncard_iff_ncard_sdiff_lt_ncard_sdiff._auto_3 →
      (s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard)
-- Mathlib.Topology.Order.LocalExtr
IsMinOn.isLocalMin : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → s ∈ nhds a → IsLocalMin f a
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toMultilinearMap_injective : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂],
  Function.Injective ContinuousMultilinearMap.toMultilinearMap
-- Mathlib.Algebra.Group.Commute.Defs
IsRightRegular.commute_mul_right_iff : ∀ {S : Type u_3} [inst : Semigroup S] {a b : S}, IsRightRegular a → (Commute (b * a) a ↔ Commute a b)