mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Nilpotent
/-- A custom induction principle for nilpotent groups. The base case is a trivial group
(`subsingleton G`), and in the induction step, one can assume the hypothesis for
the group quotiented by its center.  -/
Group.nilpotent_center_quotient_ind : ∀ {P : (G : Type u_2) → [inst : Group G] → [Group.IsNilpotent G] → Prop} (G : Type u_2) [inst : Group G]
  [inst_1 : Group.IsNilpotent G],
  (∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G) →
    (∀ (G : Type u_2) [inst : Group G] [inst_2 : Group.IsNilpotent G], P (G ⧸ Subgroup.center G) → P G) → P G
-- Lean.Data.PrefixTree
Lean.PrefixTree.find? : {α : Type u_1} → {β : Type u_2} → {p : α → α → Ordering} → Lean.PrefixTree α β p → List α → Option β
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.inv_mk : ∀ {G : Type u_2} [inst : CategoryTheory.Groupoid G] (r : HomRel G) {X Y : CategoryTheory.Quotient r} (f : X.as ⟶ Y.as),
  CategoryTheory.Quotient.inv r (Quot.mk (CategoryTheory.HomRel.CompClosure r) f) =
    Quot.mk (CategoryTheory.HomRel.CompClosure r) (CategoryTheory.Groupoid.inv f)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.toLegacyIterator.match_1.splitter : (motive : Substring.Raw → Sort u_1) →
  (x : Substring.Raw) →
    ((s : String) → (b stopPos : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := stopPos }) → motive x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  m.insertManyIfNewUnit (k :: l) = (m.insertIfNew k ()).insertManyIfNewUnit l
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.preservesColimitsOfShape_fst : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B]
  [CategoryTheory.Limits.PreservesColimitsOfShape J L],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Comma.fst L R)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformly.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l → TendstoUniformly f' g' l → TendstoUniformly (f * f') (g * g') l
-- Init.Data.Order.Ord
Std.OrientedCmp.isGT_eq_isLT : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp a b).isGT = (cmp b a).isLT
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_none : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∉ m → Std.DHashMap.Raw.Const.get? m a = none
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.add_neg_of_eq : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑u = a → a + ↑(-u) = 0
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instOrderedRingQOfLawfulOrderLTOfExistsAddOfLT : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedRing α] [Lean.Grind.ExistsAddOfLT α],
  Lean.Grind.OrderedRing (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂)
      (CategoryTheory.CategoryStruct.comp i₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)},
  (∀ {Y : C}, Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x) → F.IsRepresentedBy x
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.describeMVar.collectAwaiting : Lean.Expr → Lean.MetaM String
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupport.mk.injEq : ∀ (codeActionKind codeActionKind_1 : Lean.Lsp.CodeActionLiteralSupportValueSet),
  ({ codeActionKind := codeActionKind } = { codeActionKind := codeActionKind_1 }) = (codeActionKind = codeActionKind_1)
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.eulerPoint_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)),
  (s.reindex e).eulerPoint = s.eulerPoint ∘ ⇑e.symm
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.equicontinuousWithinAt_iff_right : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X},
  (uniformity α).HasBasis p s →
    (EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in nhdsWithin x₀ S, ∀ (i : ι), (F i x₀, F i x) ∈ s k)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isIntTangentAt_self_iff_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P}, s.IsIntTangentAt s p ↔ p ∈ s
-- Mathlib.Algebra.Order.Hom.Basic
/-- The image of zero is zero.  -/
AddGroupSeminormClass.map_zero : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : AddGroup α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : AddGroupSeminormClass F α β] (f : F), f 0 = 0
-- Init.Data.BitVec.Basic
/-- Transforms a bitvector of length `w` into a bitvector of length `v`, padding with `0` as needed.

The specific behavior depends on the relationship between the starting width `w` and the final width
`v`:
 * If `v > w`, it is zero-extended; the high bits are padded with zeroes until the bitvector has `v`
   bits.
 * If `v = w`, the bitvector is returned unchanged.
 * If `v < w`, the high bits are truncated.

`BitVec.setWidth`, `BitVec.zeroExtend`, and `BitVec.truncate` are aliases for this operation.

SMT-LIB name: `zero_extend`.
 -/
BitVec.zeroExtend : {w : ℕ} → (v : ℕ) → BitVec w → BitVec v
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_comap_comap_eq_relrank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : L →ₐ[F] E),
  B ≤ f.fieldRange → (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank B
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andIntro.sizeOf_spec : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p₁ p₂ : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.andIntro ak p₁ p₂) = 1 + sizeOf ak + sizeOf p₁ + sizeOf p₂
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSpace_two_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  α.IsNonZero → LieAlgebra.rootSpace H (2 • ⇑α) = ⊥
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk.injEq : ∀ (coe : ℂ) (coe_im_pos : 0 < coe.im) (coe_1 : ℂ) (coe_im_pos_1 : 0 < coe_1.im),
  ({ coe := coe, coe_im_pos := coe_im_pos } = { coe := coe_1, coe_im_pos := coe_im_pos_1 }) = (coe = coe_1)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ}
  (x : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg))
  (hx : CategoryTheory.CategoryStruct.comp x ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0)
  {Z : C} (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.liftOpcycles f g fg h x hx)
      (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) h_1) =
    CategoryTheory.CategoryStruct.comp x h_1
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.num.sizeOf_spec : sizeOf Lean.Meta.Grind.Result.num✝ = 1
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε_up_ℤ : ∀ (n : ℤ), (ComplexShape.up ℤ).ε n = n.negOnePow
-- Mathlib.Data.List.Intervals
List.Ico.inter_consecutive : ∀ (n m l : ℕ), List.Ico n m ∩ List.Ico m l = []
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_eq_zero_iff : ∀ {ι : Type u_3} (f : ι → Ordinal.{max v u_3}), Ordinal.lsub f = 0 ↔ IsEmpty ι
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBoundP?_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBTree.RBSet α cmp},
  t.upperBoundP? cut = some x → x ∈ t.toList
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblenWith f o₁ a < veblenWith f o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a < b`
* `o₁ < o₂` and `a < veblenWith f o₂ b`
* `o₁ > o₂` and `veblenWith f o₁ a < b`  -/
Ordinal.veblenWith_lt_veblenWith_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}},
  Order.IsNormal f →
    (Ordinal.veblenWith f o₁ a < Ordinal.veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < Ordinal.veblenWith f o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblenWith f o₁ a < b)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkChainResult : Lean.TSyntax `tactic → Array (Lean.TSyntax `tactic) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- A monoidal equivalence between monoidal categories induces a monoid isomorphism between
the skeleta.  -/
CategoryTheory.Skeleton.mulEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (e : C ≌ D) → [e.functor.Monoidal] → CategoryTheory.Skeleton C ≃* CategoryTheory.Skeleton D
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIsScalarTower : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {S : Type u_3}
  {P : Type u_4} [inst_2 : SMul S P] [inst_3 : SMul R S] [inst_4 : SMul R P] [IsScalarTower R S P] (v : Valuation R Γ₀),
  IsScalarTower (WithVal v) S P
-- Init.Data.SInt.Lemmas
ISize.toISize_toUSize : ∀ (x : ISize), x.toUSize.toISize = x
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_toArray : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  [inst_6 : Std.LawfulDeterministicIterator α Id] {γ : Type x} {it : Std.Iter β} {init : γ}
  {f : (out : β) → out ∈ it.toArray → γ → m (ForInStep γ)},
  forIn' it.toArray init f = forIn' it init fun out h acc => f out ⋯ acc
-- Lean.Parser.Term
Lean.Parser.Tactic.quot.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating compatibility between `PatternModel` and `ToForwardSearcher`.

We require the searcher to always match the longest match at the first position where the pattern
matches; see `IsValidSearchFrom`.
 -/
String.Slice.Pattern.Model.LawfulToForwardSearcherModel : {ρ : Type} →
  (pat : ρ) →
    [String.Slice.Pattern.Model.PatternModel pat] →
      {σ : String.Slice → Type} →
        [String.Slice.Pattern.ToForwardSearcher pat σ] →
          [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
            [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] → Prop
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.getD_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.filterMap f t) k fallback =
    ((Std.ExtDTreeMap.Const.get? t k).bind (f k)).getD fallback
-- Std.Data.ExtDHashMap.Basic
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.ExtDHashMap.Const.insertMany : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [EquivBEq α] →
        [LawfulHashable α] →
          {β : Type v} →
            {ρ : Type w} → [ForIn Id ρ (α × β)] → (Std.ExtDHashMap α fun x => β) → ρ → Std.ExtDHashMap α fun x => β
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_xor_odd : ∀ (n : ℤ), Xor (Even n) (Odd n)
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.instDecidableEqProd.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} → (motive : α × β → Sort u_3) → (x : α × β) → ((a' : α) → (b' : β) → motive (a', b')) → motive x
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.to_topologicalGroup : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], IsTopologicalGroup α
-- Mathlib.Topology.Separation.Basic
/-- A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair
`x ≠ y`, there is an open set containing one but not the other. We formulate the definition in terms
of the `Inseparable` relation.  -/
T0Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.RingTheory.Flat.Rank
PrimeSpectrum.comap_surjective_iff_injective_of_finite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S], Function.Surjective (PrimeSpectrum.comap (algebraMap R S)) ↔ Function.Injective ⇑(algebraMap R S)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat iX],
  AlgebraicGeometry.IsAffineOpen US →
    AlgebraicGeometry.IsAffineOpen UX →
      IsCompact ↑UT → IsQuasiSeparated ↑UT → CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wpRec_eq : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_2} n} {C : Sort u_1}
  (g : (a : P.A) → (f : P.last.B a → P.last.W) → TypeVec.Arrow (P.WPath (WType.mk a f)) α → (P.last.B a → C) → C)
  (a : P.A) (f : P.last.B a → P.last.W) (f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α),
  P.wpRec g (WType.mk a f) f' = g a f f' fun i => P.wpRec g (f i) (P.wPathDestRight f' i)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.exact : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] (ita itb : Std.BundledIterM m β),
  Quot.mk (Std.BundledIterM.Equiv m β) ita = Quot.mk (Std.BundledIterM.Equiv m β) itb →
    Std.BundledIterM.Equiv m β ita itb
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_prod_le_of_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal},
  (∀ b ∈ s, ‖f b‖₊ ≤ n b) → ‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b
-- Mathlib.Data.Finset.Prod
Finset.diag_union : ∀ {α : Type u_1} (s t : Finset α) [inst : DecidableEq α], (s ∪ t).diag = s.diag ∪ t.diag
-- Lean.Structure
/-- The direct fields of a structure, sorted by position in the structure.
For example, the `s.3` notation refers to `fieldNames[3 - 1]`.  -/
Lean.StructureInfo.fieldNames : Lean.StructureInfo → Array Lean.Name
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.mapRingHom_tmul : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {R' : Type u_6} {S' : Type u_7} {T' : Type u_8} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T]
  [inst_5 : CommSemiring R'] [inst_6 : CommSemiring S'] [inst_7 : CommSemiring T'] [inst_8 : Algebra R' S']
  [inst_9 : Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T')
  (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR)
  (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR) (s : S) (t : T),
  (Algebra.TensorProduct.mapRingHom fR fS fT HS HT) (s ⊗ₜ[R] t) = fS s ⊗ₜ[R'] fT t
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.indTypes : Lean.Elab.Command.AddAndFinalizeContext✝ → List Lean.InductiveType
-- Mathlib.Topology.Homotopy.Basic
/-- If each `f₀ i : C(X, Y i)` is homotopic to `f₁ i : C(X, Y i)`, then `ContinuousMap.pi f₀` is
homotopic to `ContinuousMap.pi f₁`.  -/
ContinuousMap.Homotopic.piMap : ∀ {ι : Type u_2} {X : ι → Type u_3} {Y : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (Y i)] {f₀ f₁ : (i : ι) → C(X i, Y i)},
  (∀ (i : ι), (f₀ i).Homotopic (f₁ i)) → (ContinuousMap.piMap f₀).Homotopic (ContinuousMap.piMap f₁)
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_le : ∀ {w acc : ℕ} {x : BitVec w} (n : ℕ), x.cpopNatRec n acc ≤ acc + n
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.edist_ofSnowflaking_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : EDist X] (x y : Metric.Snowflaking X α hα₀ hα₁),
  edist (Metric.Snowflaking.ofSnowflaking x) (Metric.Snowflaking.ofSnowflaking y) = edist x y ^ α⁻¹
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_neg : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), UpperHalfPlane.denom (-g) z = -UpperHalfPlane.denom g z
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Given a pair of isomorphisms between the summands of a pair of binary biproducts,
we obtain an isomorphism between the binary biproducts.  -/
CategoryTheory.Limits.biprod.mapIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {W X Y Z : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] → (W ≅ Y) → (X ≅ Z) → (W ⊞ X ≅ Y ⊞ Z)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.comp_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasColimit G], CategoryTheory.Limits.HasColimit (F.comp G)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- A bicategory is locally groupoidal if the categories of 1-morphisms are groupoids.  -/
CategoryTheory.Bicategory.IsLocallyGroupoid : (B : Type u₁) → [CategoryTheory.Bicategory B] → Prop
-- Mathlib.Logic.Equiv.Basic
Equiv.instIdempotentOpCoeForallForallArrowCongr : ∀ {α₁ : Type u_11} {β₁ : Type u_12} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.IdempotentOp f],
  Std.IdempotentOp ((e.arrowCongr (e.arrowCongr e)) f)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.associated_det_comp_equiv : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N),
  Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))
-- Init.Data.Int.Linear
Int.Internal.Linear.abs : ℤ → ℤ
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], ⌊a⌋₊ = 0 ↔ a < 1
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.finalizeImport : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → σ → σ
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft'.eq_1 : ∀ {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β),
  Equiv.piCongrLeft' P e =
    { toFun := fun f x => f (e.symm x), invFun := fun f x => ⋯ ▸ f (e x), left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_ediv_le_natAbs : ∀ (a b : ℤ), (a / b).natAbs ≤ a.natAbs
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.EventuallyEq.of_eventually_mem_of_forall_separating_mem_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → β} (p : Set β → Prop) {s : Set β}
  [h' : HasCountableSeparatingOn β p s],
  (∀ᶠ (x : α) in l, f x ∈ s) →
    (∀ᶠ (x : α) in l, g x ∈ s) → (∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U) → f =ᶠ[l] g
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_of_pairing_eq_zero : ∀ {ι : 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} {i j : ι},
  P.pairing j i = 0 → (P.reflectionPerm i) j = j
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.isExpansionOn_reduct : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [inst : L'.Structure M],
  ϕ.IsExpansionOn M
-- Init.Data.String.TakeDrop
/-- Checks whether the string \(`s`\) ends with the pattern \(`pat`\).

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".endsWith "blue" = true`

* `"red green blue".endsWith "green" = false`

* `"red green blue".endsWith "" = true`

* `"red green blue".endsWith 'e' = true`

* `"red green blue".endsWith Char.isLower = true`
 -/
String.endsWith : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Bool
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCover_f : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x x_1 : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).f x x_1 = CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f x_1)