mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.forget₂_map : ∀ {R S : RingCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ RingCat SemiRingCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ RingCat SemiRingCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Data.Int.Bitwise
Int.ldiff_bit : ∀ (a : Bool) (m : ℤ) (b : Bool) (n : ℤ), (Int.bit a m).ldiff (Int.bit b n) = Int.bit (a && !b) (m.ldiff n)
-- Mathlib.Algebra.Algebra.Pi
Pi.instAlgebraForall : {ι : Type u_1} →
  (A : ι → Type u_3) →
    [inst : (i : ι) → Semiring (A i)] →
      (S : ι → Type u_4) →
        [inst_1 : (i : ι) → CommSemiring (S i)] →
          [(i : ι) → Algebra (S i) (A i)] → Algebra ((i : ι) → S i) ((i : ι) → A i)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  {f : α → β → γ} {k : α} {fallback : γ},
  m.WF → (Std.HashMap.Raw.map f m).getD k fallback = (Option.map (f k) m[k]?).getD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of the zero morphism is an isomorphism  -/
CategoryTheory.Limits.cokernel.π_zero_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π 0)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.dirac_prod_dirac : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {x : α} {y : β},
  (MeasureTheory.Measure.dirac x).prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.dirac (x, y)
-- LeanSearchClient.Syntax
LeanSearchClient.queryLeanSearch : String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult)
-- Mathlib.Algebra.Notation.Prod
Prod.vadd_swap : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : VAdd E α] [inst_1 : VAdd E β] (c : E) (p : α × β),
  (c +ᵥ p).swap = c +ᵥ p.swap
-- Mathlib.Order.Hom.Lattice
SupHom.symm_dual_id : ∀ {α : Type u_2} [inst : Max α], SupHom.dual.symm (InfHom.id αᵒᵈ) = SupHom.id α
-- Mathlib.LinearAlgebra.Contraction
lTensorHomEquivHomLTensor_apply : ∀ {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M]
  (x : TensorProduct R P (M →ₗ[R] Q)),
  (lTensorHomEquivHomLTensor R M P Q) x = (TensorProduct.lTensorHomToHomLTensor (RingHom.id R) M P Q) x
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubgroup.even_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddCommGroup G], (AddSubgroup.even G).toAddSubmonoid = AddSubmonoid.even G
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
differentiableOn_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)] {f : H → PiLp p E} {t : Set H},
  DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => (f x).ofLp i) t
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.trans : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (u v w : (MvQPF.P F).W α),
  MvQPF.WEquiv u v → MvQPF.WEquiv v w → MvQPF.WEquiv u w
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_1 : ∀ {σ : Type u_1} {P Q : Std.Do.SPred [σ]}, P ⊢ₛ Q ↔ ∀ (s : σ), (P s).down → (Q s).down
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.mk.sizeOf_spec : ∀ (tree : Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry) (isEmpty : Bool),
  sizeOf { tree := tree, isEmpty := isEmpty } = 1 + sizeOf tree + sizeOf isEmpty
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of the forward direction of `SimpleGraph.colorable_zero_iff`. -/
SimpleGraph.Colorable.isEmpty : ∀ {V : Type u} {G : SimpleGraph V}, G.Colorable 0 → IsEmpty V
-- Mathlib.RingTheory.Ideal.Cotangent
AlgHom.kerSquareLift_mk : ∀ {R : Type u} [inst : CommRing R] {A : Type u_1} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (x : A),
  f.kerSquareLift ((Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2)) x) = f x
-- Mathlib.NumberTheory.NumberField.ExistsRamified
/-- If `𝒪` is a domain that is a finite and unramified extension of `ℤ`, then `𝒪 = ℤ`.  -/
bijective_algebraMap_int_of_finite_of_unramified : ∀ {𝒪 : Type u_2} [inst : CommRing 𝒪] [Module.Finite ℤ 𝒪] [Algebra.Unramified ℤ 𝒪] [IsDomain 𝒪] [FaithfulSMul ℤ 𝒪],
  Function.Bijective ⇑(algebraMap ℤ 𝒪)
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.proj_equiv₁' : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α), Tuple.graph.proj ∘ ⇑(Tuple.graphEquiv₁ f) = f
-- Mathlib.CategoryTheory.Localization.Resolution
/-- a morphism in the source category  -/
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.f : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → {L L' : Φ.LeftResolution X₂} → L.Hom L' → (L.X₁ ⟶ L'.X₁)
-- Std.Time.Date.Unit.Month
/-- Returns the cumulative size in days of each month for a non-leap year.
 -/
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.cumulativeSizes : { val // val.size = 12 }
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    FractionalIdeal.count K v I =
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors)
-- Mathlib.Data.Set.Function
Set.LeftInvOn.eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → ∀ {x : α}, x ∈ s → f' (f x) = x
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instSub : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Sub (CuspForm Γ k)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_iff_disjoint_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g ↔ Disjoint f.support g.support
-- Mathlib.Order.Basic
/-- **Alias** of `Decidable.lt_or_eq_of_le'`. -/
LE.le.lt_or_eq_dec' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} [DecidableLE α], b ≤ a → b < a ∨ a = b
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_counitIso : ∀ (A : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [inst_2 : CategoryTheory.Category.{v, u} B],
  (CategoryTheory.Sum.functorEquiv A A' B).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun F => (F.1.inlCompSum' F.2).prod (F.1.inrCompSum' F.2) ≪≫ CategoryTheory.prod.etaIso F) ⋯
-- Mathlib.Combinatorics.Quiver.Path
_private.Mathlib.Combinatorics.Quiver.Path.0.Quiver.Path.length.match_1.splitter : {V : Type u_2} →
  [inst : Quiver V] →
    {a : V} →
      (motive : (x : V) → Quiver.Path a x → Sort u_3) →
        (x : V) →
          (x_1 : Quiver.Path a x) →
            (Unit → motive a Quiver.Path.nil) →
              ((x b : V) → (p : Quiver.Path a b) → (a_1 : b ⟶ x) → motive x (p.cons a_1)) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfLeftIso_x : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f], (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt = Y
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.trans`. -/
HasSSubset.SSubset.trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumAssoc_symm_apply : ∀ {U : Type u_1} {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
  (a : V ⊕ W ⊕ U),
  (RelIso.symm SimpleGraph.Iso.sumAssoc) a = Sum.elim (Sum.inl ∘ Sum.inl) (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr) a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl), ms.tail = Stream'.Seq.tail ms
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.prop_trans : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀]
  [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (self : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j),
  P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- If `G` is locally fully faithful and locally cover dense, `G` is cover-preserving w.r.t. the
restricted topology.  -/
CategoryTheory.Functor.coverPreserving_restrictedTopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K],
  CategoryTheory.CoverPreserving (G.restrictedTopology K) K G
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Reverse
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastReverse : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.RefVec w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse aig target).vec.get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := target.get (w - 1 - idx) ⋯ }⟧
-- Lean.Language.Basic
/-- Whether it should be indicated to the user that a fatal error (which should be part of
`diagnostics`) occurred that prevents processing of the remainder of the file.
 -/
Lean.Language.Snapshot.isFatal : Lean.Language.Snapshot → Bool
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.le_radius_of_tendsto : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {r : NNReal}
  (p : FormalMultilinearSeries 𝕜 E F) {l : ℝ},
  Filter.Tendsto (fun n => ‖p n‖ * ↑r ^ n) Filter.atTop (nhds l) → ↑r ≤ p.radius
-- Lean.Linter.MissingDocs
_private.Lean.Linter.MissingDocs.0.Lean.Linter.MissingDocs.isEmptyDocString : Lean.Syntax → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.Data.List.Chain
List.IsChain.concat_induction_head : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α),
  List.IsChain r (l ++ [b]) → (l ++ [b]).head ⋯ = a → (∀ ⦃x y : α⦄, r x y → p x → p y) → p a → p b
-- Init.Data.SInt.Bitwise
Int64.shiftLeft_or : ∀ {a b c : Int64}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Init.Meta.Defs
Lean.TSyntax.Compat.instCoeTailArraySyntaxTSyntaxArray : {k : Lean.SyntaxNodeKinds} → CoeTail (Array Lean.Syntax) (Lean.TSyntaxArray k)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The medians of a simplex are concurrent at its centroid.  -/
Affine.Simplex.eq_centroid_of_forall_mem_median : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) {hn : 1 < n} {p : P},
  (∀ (i : Fin (n + 1)), p ∈ s.median i) → p = s.centroid
-- Mathlib.FieldTheory.Finite.GaloisField
instFiniteGaloisField : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (n : ℕ), Finite (GaloisField p n)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.toSigmaCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I)
  {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c)
  {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d),
  (CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K).π = CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospan.match_1.eq_3 : ∀ {J : CategoryTheory.Limits.MulticospanShape}
  (motive : (x y : CategoryTheory.Limits.WalkingMulticospan J) → (x ⟶ y) → Sort u_3) (b : J.R)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingMulticospan J) → motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x))
  (h_2 :
    (b : J.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (J.fst b))
        (CategoryTheory.Limits.WalkingMulticospan.right b) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst b))
  (h_3 :
    (b : J.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (J.snd b))
        (CategoryTheory.Limits.WalkingMulticospan.right b) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd b)),
  (match CategoryTheory.Limits.WalkingMulticospan.left (J.snd b), CategoryTheory.Limits.WalkingMulticospan.right b,
      CategoryTheory.Limits.WalkingMulticospan.Hom.snd b with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMulticospan.left (J.fst b)), .(CategoryTheory.Limits.WalkingMulticospan.right b),
      CategoryTheory.Limits.WalkingMulticospan.Hom.fst b => h_2 b
    | .(CategoryTheory.Limits.WalkingMulticospan.left (J.snd b)), .(CategoryTheory.Limits.WalkingMulticospan.right b),
      CategoryTheory.Limits.WalkingMulticospan.Hom.snd b => h_3 b) =
    h_3 b
-- Init.Data.Array.Lemmas
/-- Variant of `List.foldl_push_eq_append` specialized to `f = id`.  -/
List.foldl_push_eq_append' : ∀ {α : Type u_1} {l : List α} {xs : Array α}, List.foldl (fun xs x => xs.push x) xs l = xs ++ l.toArray
-- Lean.Language.Basic
Lean.Language.Snapshot.mk : autoParam String Lean.Language.Snapshot.desc._autoParam →
  Lean.Language.Snapshot.Diagnostics → Option Lean.Elab.InfoTree → Lean.TraceState → Bool → Lean.Language.Snapshot
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_sup : ∀ {G : Type u_2} [inst : AddGroup G] (S₁ S₂ : AddSubgroup G), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Lean.Elab.SetOption
/-- Returns the type corresponding to the given `DataValue`, or `none` if the corresponding type
cannot be specified using `set_option` notation.
 -/
_private.Lean.Elab.SetOption.0.Lean.Elab.ctorType? : Lean.DataValue → Option Lean.Expr
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformContinuous_eval : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)},
  ⋃₀ 𝔖 = Set.univ → ∀ (x : α), UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- The length on `Icc a b` of a path into a manifold, where the path is defined on the whole real
line.

We use the whole real line to avoid subtype hell in API, but this is equivalent to
considering functions on the manifold with boundary `Icc a b`, see
`lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc`.

We use `mfderiv` instead of `mfderivWithin` in the definition as these coincide (apart from the two
endpoints which have zero measure) and `mfderiv` is easier to manipulate. However, we give
a lemma `pathELength_eq_integral_mfderivWithin_Icc` to rewrite with the `mfderivWithin` form.  -/
Manifold.pathELength : {E : Type u_4} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_5} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            {M : Type u_6} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → [(x : M) → ENorm (TangentSpace I x)] → (ℝ → M) → ℝ → ℝ → ENNReal
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.isStrongLimit_iff : ∀ (c : Cardinal.{u_1}), c.IsStrongLimit ↔ c ≠ 0 ∧ c.IsStrongPrelimit
-- Mathlib.Order.Hom.Basic
/-- Given two bundled monotone maps `f`, `g`, `f.prod g` is the map `x ↦ (f x, g x)` bundled as a
`OrderHom`.  -/
OrderHom.prod : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Preorder γ] → (α →o β) → (α →o γ) → α →o β × γ
-- Mathlib.Control.Monad.Cont
LawfulMonadCont.callCC_dummy : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadCont m} [self : LawfulMonadCont m] {α β : Type u} (dummy : m α),
  (MonadCont.callCC fun x => dummy) = dummy
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.triangleOfDegreewiseSplit_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  (CochainComplex.triangleOfDegreewiseSplit S σ).mor₁ = S.f
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.Linear.mk : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  {F : CategoryTheory.Functor C D},
  autoParam (∀ {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f)
      CategoryTheory.Functor.Linear.map_smul._autoParam →
    CategoryTheory.Functor.Linear R F
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The map between darts induced by a homomorphism.  -/
SimpleGraph.Hom.mapDart : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G →g G' → G.Dart → G'.Dart
-- Mathlib.Algebra.Free
/-- Lifts an additive magma homomorphism `α → β` to an
additive semigroup homomorphism `AddMagma.AssocQuotient α → β` given an additive semigroup `β`.  -/
AddMagma.FreeAddSemigroup.lift : {α : Type u} →
  [inst : Add α] → {β : Type v} → [inst_1 : AddSemigroup β] → (α →ₙ+ β) ≃ (AddMagma.FreeAddSemigroup α →ₙ+ β)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_sq : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sqrt_sq._auto_1 → CFC.sqrt (a ^ 2) = a
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.div_add_mod' : ∀ {R : Type u} [inst : EuclideanDomain R] (m k : R), m / k * k + m % k = m
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_pow : ∀ {α : Type u} [inst : Monoid α] (n : ℕ) (a : α), Additive.ofMul (a ^ n) = n • Additive.ofMul a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorObj_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S : CategoryTheory.Over X),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).left = CategoryTheory.Limits.pullback R.hom S.hom
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_natCast_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (↑n).degree ≤ 0
-- Mathlib.Analysis.Convex.Topology
Convex.closure_interior_eq_closure_of_nonempty_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [inst_7 : TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → (interior s).Nonempty → closure (interior s) = closure s
-- Mathlib.Data.Finset.Grade
Finset.isCoatom_iff : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], IsCoatom s ↔ ∃ a, s = {a}ᶜ
-- Mathlib.Topology.MetricSpace.Gluing
/-- The canonical map from `X` to the space obtained by gluing isometric subsets in `X` and `Y`.  -/
Metric.toGlueL : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : Nonempty Z] →
        [inst_1 : MetricSpace Z] →
          [inst_2 : MetricSpace X] →
            [inst_3 : MetricSpace Y] →
              {Φ : Z → X} → {Ψ : Z → Y} → (hΦ : Isometry Φ) → (hΨ : Isometry Ψ) → X → Metric.GlueSpace hΦ hΨ
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_5.eq_1 : ∀ (motive : (n : ℕ) → (P : Fin n → Prop) → (inst : DecidablePred P) → Fin (Fin.countP fun x => decide (P x)) → Sort u_1)
  (x : Fin 0 → Prop) (x_1 : DecidablePred x) (val : ℕ) (h : val < Fin.countP fun x_2 => decide (x x_2))
  (h_1 :
    (x : Fin 0 → Prop) →
      (x_2 : DecidablePred x) → (val : ℕ) → (h : val < Fin.countP fun x_3 => decide (x x_3)) → motive 0 x x_2 ⟨val, h⟩)
  (h_2 :
    (n : ℕ) →
      (P : Fin (n + 1) → Prop) →
        (inst : DecidablePred P) →
          (k : ℕ) → (hk : k < Fin.countP fun x => decide (P x)) → motive n.succ P inst ⟨k, hk⟩),
  (match 0, x, x_1, ⟨val, h⟩ with
    | 0, x, x_2, ⟨val, h⟩ => h_1 x x_2 val h
    | n.succ, P, inst, ⟨k, hk⟩ => h_2 n P inst k hk) =
    h_1 x x_1 val h
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J) {Z : C}
  (h : Opposite.unop (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitLeftOpIsoUnopColimit F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j).unop h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.leftOp (Opposite.op j)) h
-- Init.Meta.Defs
/-- Compare syntax structures modulo source info.  -/
Lean.Syntax.structEq : Lean.Syntax → Lean.Syntax → Bool
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHomEquiv_symm_one : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], AddChar.toMonoidHomEquiv.symm 1 = 0
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk.sizeOf_spec : ∀ {B : Type u_1} {F : Type u_4} {E : B → Type u_5} [inst : SizeOf B] [inst_1 : SizeOf F]
  [inst_2 : (a : B) → SizeOf (E a)] (proj : B) (snd : E proj), sizeOf ⟨proj, snd⟩ = 1 + sizeOf proj + sizeOf snd
-- Aesop.Search.SearchM
Aesop.getTree : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Aesop.Tree
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_add_left_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (y * z + x) y → IsCoprime x y
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- An algebraic extension is purely inseparable if and only if all of its finite-dimensional
subextensions are purely inseparable.  -/
isPurelyInseparable_iff_fd_isPurelyInseparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L