mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toCommRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → CommRing ↥S
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.alternatingFaceMapComplex_map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ),
  ((AlgebraicTopology.alternatingFaceMapComplex C).map f).f n = f.app (Opposite.op { len := n })
-- Init.Data.List.Lemmas
List.mem_iff_append : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l ↔ ∃ s t, l = s ++ a :: t
-- Mathlib.Topology.Homotopy.Equiv
/-- If `X` is homotopy equivalent to `Y`, then `Y` is homotopy equivalent to `X`.
 -/
ContinuousMap.HomotopyEquiv.symm : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → ContinuousMap.HomotopyEquiv X Y → ContinuousMap.HomotopyEquiv Y X
-- Mathlib.Data.ZMod.Basic
ZMod.subsingleton_ringEquiv : ∀ {n : ℕ} {R : Type u_1} [inst : Semiring R], Subsingleton (ZMod n ≃+* R)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.DifferentialsConstruction.instHasDifferentials : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  (φ' : S' ⟶ R), PresheafOfModules.HasDifferentials φ'
-- Mathlib.Data.Matrix.Diagonal
Matrix.col_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α) (i : n),
  (Matrix.diagonal d).col i = Pi.single i (d i)
-- Lean.Widget.Types
/-- An instance of a widget component:
the identifier of a widget module and the hash of its JS source code
together with props.

See the [manual entry](https://lean-lang.org/documentation/widgets/)
for more information about widgets.  -/
Lean.Widget.WidgetInstance : Type
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.nat_power_eq : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 ≤ c → ∀ {n : ℕ}, 2 ≤ n → ↑n ^ c = 2 ^ c
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder α]
  [inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) (a : α),
  (f.comp g) a = f (g a)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.instHasFiniteBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  CategoryTheory.Limits.HasFiniteBiproducts C
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- In a barrelled space, all lower semicontinuous seminorms on `E` are actually continuous.  -/
BarrelledSpace.continuous_of_lowerSemicontinuous : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : SeminormedRing 𝕜} {inst_1 : AddGroup E} {inst_2 : SMul 𝕜 E}
  {inst_3 : TopologicalSpace E} [self : BarrelledSpace 𝕜 E] (p : Seminorm 𝕜 E), LowerSemicontinuous ⇑p → Continuous ⇑p
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.evalOmega : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Complex.tsum_exp_neg_mul_int_sq : ∀ {a : ℂ},
  0 < a.re →
    ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2) =
      1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * ↑n ^ 2)
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.bddBelow_range : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] {a : α} [IsCodirectedOrder α]
  {u : ℕ → α}, Filter.Tendsto u Filter.atTop (nhds a) → BddBelow (Set.range u)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.ediam_image : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕)
  (s : Set E), Metric.ediam (⇑f '' s) = Metric.ediam s
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
Submodule.map_dualAnnihilator_linearEquiv_flip_symm : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M)
  (p : Submodule R N), Submodule.map (↑e.flip.symm) p.dualAnnihilator = (Submodule.map (↑e) p).dualCoannihilator
-- Init.Data.Float.Model.Unpacked.Operations.Mul
/-- Computes the product of two floating-point numbers and rounds the result according to
the given specification.
 -/
Float.Model.UnpackedFloat.mul : Float.Model.Format → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- If `f` and `f'` are isomorphic morphisms and the target of `f`
is obtained by attaching cells to the source of `f`,
then the same holds for `f'`.  -/
HomotopicalAlgebra.AttachCells.ofArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              HomotopicalAlgebra.AttachCells g f →
                {Y₁ Y₂ : C} →
                  {f' : Y₁ ⟶ Y₂} →
                    (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → HomotopicalAlgebra.AttachCells g f'
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.right.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MulticospanShape} (a : J.R),
  sizeOf (CategoryTheory.Limits.WalkingMulticospan.right a) = 1 + sizeOf a
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeStringRequestID : Coe String Lean.JsonRpc.RequestID
-- Std.Time.Duration
Std.Time.Duration.ext : ∀ {x y : Std.Time.Duration}, x.second = y.second → x.nano = y.nano → x = y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.id? : Lean.Lsp.ResolvableCompletionItemData → Option Lean.Lsp.CompletionIdentifier
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.alter : {α : Type u_1} →
  {β : Type u_2} →
    {x : BEq α} →
      {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → (Option β → Option β) → Lean.PersistentHashMap α β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.TreeMap.foldrM f init t = Array.foldrM (fun a b => f a.1 a.2 b) init t.toArray
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.elemExponent_min : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] {a : L} {n : ℕ},
  n < IsPurelyInseparable.elemExponent K a → a ^ ringExpChar K ^ n ∉ (algebraMap K L).range
-- Batteries.Data.AssocList
/-- The implementation of `ForIn`, which enables `for (k, v) in aList do ...` notation.  -/
Batteries.AssocList.forIn : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} → {δ : Type u_1} → [Monad m] → Batteries.AssocList α β → δ → (α × β → δ → m (ForInStep δ)) → m δ
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mem_ker : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (v : V),
  v ∈ Representation.IntertwiningMap.ker ρ σ f ↔ f v = 0
-- Mathlib.NumberTheory.ModularForms.Basic
SlashInvariantForm.const.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetOne] (x x_1 : ℂ),
  x = x_1 → SlashInvariantForm.const x = SlashInvariantForm.const x_1
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coe_div : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K},
  J ≠ 0 → ↑(I / J) = ↑I / ↑J
-- Init.Data.Fin.Fold
Fin.foldr_rev : ∀ {α : Sort u_1} {n : ℕ} (f : α → Fin n → α) (x : α), Fin.foldr n (fun i x => f x i.rev) x = Fin.foldl n f x
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.primPart_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R], Polynomial.primPart 0 = 1
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeAddMonoid.symbols_zero : ∀ {α : Type u_1} [inst : DecidableEq α], FreeAddMonoid.symbols 0 = ∅
-- Mathlib.Order.Category.Frm
Frm.of.injEq : ∀ (carrier : Type u_1) [str : Order.Frame carrier] (carrier_1 : Type u_1) (str_1 : Order.Frame carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Topology.Order.OrderClosed
instClosedIicTopology : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α], ClosedIicTopology α
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.residueFieldMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} [inst_2 : IsLocalRing R]
  [inst_3 : IsLocalRing S] [inst_4 : IsLocalHom f], f.EssFiniteType → (IsLocalRing.ResidueField.map f).EssFiniteType
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If an equalizer of `f` and `g` exists, we can access an arbitrary choice of such by
saying `equalizer f g`.  -/
CategoryTheory.Limits.equalizer : {C : Type u} →
  {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (f g : X ⟶ Y) → [CategoryTheory.Limits.HasEqualizer f g] → C
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.instAddCommGroup.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : IsAddCommutative G],
  IsAddCommutative.instAddCommGroup = { toAddGroup := inst, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If a wide equalizer of `f` exists, we can access an arbitrary choice of such by
saying `wideEqualizer f`.  -/
CategoryTheory.Limits.wideEqualizer : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} → (f : J → (X ⟶ Y)) → [CategoryTheory.Limits.HasWideEqualizer f] → C
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_biSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), LowerSemicontinuousOn (f i hi) s) →
    LowerSemicontinuousOn (fun x' => ⨆ i, ⨆ (hi : p i), f i hi x') s
-- Std.Http.Data.Method
Std.Http.Method.post.sizeOf_spec : sizeOf Std.Http.Method.post = 1
-- Mathlib.MeasureTheory.Function.EssSup
essSup_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] (c : β), μ ≠ 0 → essSup (fun x => c) μ = c
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : HomotopicalAlgebra.ModelCategory C} {X Y : C}
  {f : X ⟶ Y}
  {toMapFactorizationData :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f}
  {r : toMapFactorizationData.Z ⟶ X}
  {i_r :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData.i r = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam}
  {fibration_r :
    autoParam (HomotopicalAlgebra.Fibration r) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam}
  {toMapFactorizationData_1 :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f}
  {r_1 : toMapFactorizationData_1.Z ⟶ X}
  {i_r_1 :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData_1.i r_1 = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam}
  {fibration_r_1 :
    autoParam (HomotopicalAlgebra.Fibration r_1) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam},
  { toMapFactorizationData := toMapFactorizationData, r := r, i_r := i_r, fibration_r := fibration_r } =
      { toMapFactorizationData := toMapFactorizationData_1, r := r_1, i_r := i_r_1, fibration_r := fibration_r_1 } →
    toMapFactorizationData = toMapFactorizationData_1 ∧ r ≍ r_1
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.equiv : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), Filter.TendstoCofinite ⇑e
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instIsScalarTower : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M}
  [inst_1 : OreLocalization.OreSet S] [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M]
  [inst_5 : IsScalarTower R M M] [inst_6 : IsScalarTower R M X] [inst_7 : SMul R' X] [inst_8 : SMul R' M]
  [inst_9 : IsScalarTower R' M M] [inst_10 : IsScalarTower R' M X] [inst_11 : SMul R R'] [IsScalarTower R R' M],
  IsScalarTower R R' (OreLocalization S X)
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.Context.mk.inj : ∀ {steps steps_1 : Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step)},
  { steps := steps } = { steps := steps_1 } → steps = steps_1
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.leftHomologyData_π : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).LeftHomologyData),
  (HomologicalComplex.extend.leftHomologyData K e hj' hi hi' hk hk' h).π = h.π
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.prec : ∀ {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ},
  Nat.RecursiveIn O f →
    Nat.RecursiveIn O h →
      Nat.RecursiveIn O fun p =>
        match Nat.unpair p with
        | (a, n) =>
          Nat.rec (f a)
            (fun y IH => do
              let i ← IH
              h (Nat.pair a (Nat.pair y i)))
            n
-- Lean.Meta.Tactic.Assert
/-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`.  -/
Lean.MVarId.note : Lean.MVarId → Lean.Name → Lean.Expr → optParam (Option Lean.Expr) none → Lean.MetaM (Lean.FVarId × Lean.MVarId)
-- Mathlib.Order.Concept
Order.IsExtent.iInter₂ : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} {r : α → β → Prop} (f : (i : ι) → κ i → Set α),
  (∀ (i : ι) (j : κ i), Order.IsExtent r (f i j)) → Order.IsExtent r (⋂ i, ⋂ j, f i j)
-- Mathlib.Data.ZMod.QuotientGroup
MulAction.zpowersQuotientStabilizerEquiv_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Group α] (a : α) [inst_1 : MulAction α β] (b : β)
  (n : ZMod (Function.minimalPeriod (fun x => a • x) b)),
  (MulAction.zpowersQuotientStabilizerEquiv a b).symm n = ↑⟨a, ⋯⟩ ^ n.cast
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {fallback : β} {f : β → β},
      (t.modify k f).getD k' fallback =
        if cmp k k' = Ordering.eq then (Option.map f t[k]?).getD fallback else t.getD k' fallback
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {fallback : β a}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_coe' : ∀ {α : Type u_1} (l : List α), (↑l).powerset = ↑(List.map Multiset.ofList l.sublists')
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.fst.eq_1 : ∀ {R : Type u} {M : Type v} (x : TrivSqZeroExt R M), x.fst = x.1
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.mk : {X Y : Pointed} → (toFun : X.X → Y.X) → toFun X.point = Y.point → X.Hom Y
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeriesBilinear.match_1.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) →
    (Unit → motive 0) →
      (Unit → motive 1) →
        (Unit → motive 2) → ((x : ℕ) → (x = 0 → False) → (x = 1 → False) → (x = 2 → False) → motive x) → motive x
-- Lean.Meta.LitValues
/-- Recognize a non-negated `Float` literal: an `OfScientific` or `OfNat` application.  -/
_private.Lean.Meta.LitValues.0.Lean.Meta.getFloatLit? : Lean.Expr → Lean.MetaM (Option Float)
-- Mathlib.Topology.Homotopy.Contractible
/-- The product of two contractible spaces is contractible.  -/
ContractibleSpace.instProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ContractibleSpace X]
  [ContractibleSpace Y], ContractibleSpace (X × Y)
-- Mathlib.Order.Hom.Bounded
OrderIsoClass.toBoundedOrderHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : LE α] [inst_2 : BoundedOrder α]
  [inst_3 : PartialOrder β] [inst_4 : BoundedOrder β] [OrderIsoClass F α β], BoundedOrderHomClass F α β
-- Mathlib.Analysis.MeanInequalities
/-- **Weighted Hölder inequality**.  -/
Real.inner_le_weight_mul_Lp_of_nonneg : ∀ {ι : Type u} (s : Finset ι) {p : ℝ},
  1 ≤ p →
    ∀ (w f : ι → ℝ),
      (∀ (i : ι), 0 ≤ w i) →
        (∀ (i : ι), 0 ≤ f i) → ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_add_filter_not : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α →₀ M) (p : α → Prop) [inst_1 : DecidablePred p],
  Finsupp.filter p f + Finsupp.filter (fun x => ¬p x) f = f
-- Mathlib.Order.Filter.Defs
/-- The set `Set.univ` belongs to any filter.  -/
Filter.univ_sets : ∀ {α : Type u_1} (self : Filter α), Set.univ ∈ self.sets
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instHasPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Limits.HasPullback f g
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.toMonoidHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f = ↑f
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instIsStableUnderSupQcPrecoverage : AlgebraicGeometry.Scheme.qcPrecoverage.IsStableUnderSup
-- Mathlib.Order.Category.Frm
_private.Mathlib.Order.Category.Frm.0.Frm.Hom.mk.inj : ∀ {X Y : Frm} {hom' hom'_1 : FrameHom ↑X ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app._auto_1),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.opOp C) n).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X)))
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op
-- Mathlib.Data.Fintype.Inv
/-- `bijInv f` is the unique inverse to a bijection `f`. This acts
as a computable alternative to `Function.invFun`.  -/
Fintype.bijInv : {α : Type u_1} → {β : Type u_2} → [Fintype α] → [DecidableEq β] → {f : α → β} → Function.Bijective f → β → α
-- Lean.Expr
/-- The `bvar` constructor represents bound variables, i.e. occurrences
of a variable in the expression where there is a variable binder
above it (i.e. introduced by a `lam`, `forallE`, or `letE`).

The `deBruijnIndex` parameter is the *de Bruijn* index for the bound
variable. See [the Wikipedia page on de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index)
for additional information.

For example, consider the expression `fun x : Nat => forall y : Nat, x = y`.
The `x` and `y` variables in the equality expression are constructed
using `bvar` and bound to the binders introduced by the earlier
`lam` and `forallE` constructors. Here is the corresponding `Expr` representation
for the same expression:
```lean
.lam `x (.const `Nat [])
  (.forallE `y (.const `Nat [])
    (.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0))
    .default)
  .default
```
 -/
Lean.Expr.bvar : ℕ → Lean.Expr
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- The image of a precylinder by a functor.  -/
HomotopicalAlgebra.Precylinder.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      HomotopicalAlgebra.Precylinder X →
        {D : Type u_1} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
            (F : CategoryTheory.Functor C D) → HomotopicalAlgebra.Precylinder (F.obj X)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- A particular case of Sard's Theorem. Let `f : E → F` be a map between finite-dimensional real
vector spaces. Suppose that `f` is `C¹` smooth on a convex set `s` of Hausdorff dimension strictly
less than the dimension of `F`. Then the complement of the image `f '' s` is dense in `F`.  -/
ContDiffOn.dense_compl_image_of_dimH_lt_finrank : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F} {s t : Set E},
  ContDiffOn ℝ 1 f s → Convex ℝ s → t ⊆ s → dimH t < ↑(Module.finrank ℝ F) → Dense (f '' t)ᶜ
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPDeepTermsThreshold : Lean.Options → ℕ
-- Mathlib.Algebra.Opposites
/-- Additive opposite of a type. This type inherits all multiplicative structures on `α` and
reverses left and right in addition.  -/
AddOpposite : Type u_3 → Type u_3
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ → MeasureTheory.HasFiniteIntegral (fun x => (f x).toReal) μ
-- Mathlib.Order.OrdContinuous
OrderIso.rightOrdContinuous : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), RightOrdContinuous ⇑e
-- Init.Data.RArray
Lean.instGetElemRArrayNatTrue : {α : Type u} → GetElem (Lean.RArray α) ℕ α fun x x_1 => True
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- A finitely generated submonoid of an additive monoid with a single unit has finitely many
irreducible elements.  -/
AddSubmonoid.FG.finite_addIrreducible_mem_addSubmonoidClosure : ∀ {M : Type u_1} [inst : AddCommMonoid M] [Subsingleton (AddUnits M)] {S : AddSubmonoid M},
  S.FG → {p | p ∈ S ∧ AddIrreducible p}.Finite
-- Mathlib.Data.Nat.Prime.Defs
Nat.factors_lemma : ∀ {k : ℕ}, (k + 2) / (k + 2).minFac < k + 2
-- Init.Prelude
/-- Get the starting position of the syntax, if possible.
If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying
position information.
 -/
Lean.Syntax.getPos? : Lean.Syntax → optParam Bool false → Option String.Pos.Raw
-- Init.Data.Slice.List.Basic
Std.Slice.Internal.ListSliceData.mk.injEq : ∀ {α : Type u} (list : List α) (stop : Option ℕ) (list_1 : List α) (stop_1 : Option ℕ),
  ({ list := list, stop := stop } = { list := list_1, stop := stop_1 }) = (list = list_1 ∧ stop = stop_1)