mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Basic
/-- Decodes an array of bytes that encode a string as [UTF-8](https://en.wikipedia.org/wiki/UTF-8) into
the corresponding string, or panics if the array is not a valid UTF-8 encoding of a string.
 -/
String.fromUTF8! : ByteArray → String
-- Mathlib.NumberTheory.ModularForms.Petersson
SlashInvariantFormClass.norm_petersson_smul : ∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] {k : ℤ}
  {g : GL (Fin 2) ℝ} {τ : UpperHalfPlane} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne]
  [SlashInvariantFormClass F Γ k] {f : F} [SlashInvariantFormClass F' Γ k] {f' : F'},
  g ∈ Γ → ‖UpperHalfPlane.petersson k (⇑f) (⇑f') (g • τ)‖ = ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_sub : ∀ {R : Type u_1} {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {f : α → α} {g g' : α → M},
  birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g'
-- Init.Data.Vector.Algebra
Vector.neg_add_cancel : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α] [inst_2 : Neg α],
  (∀ (x : α), -x + x = 0) → ∀ (xs : Vector α n), -xs + xs = 0
-- Init.Tactics
/-- `(tacs)` executes a list of tactics in sequence, without requiring that
the goal be closed at the end like `· tacs`. Like `by` itself, the tactics
can be either separated by newlines or `;`.
 -/
Lean.Parser.Tactic.paren : Lean.ParserDescr
-- Mathlib.Topology.Order.DenselyOrdered
IsMin.of_disjoint_nhds_Iio : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {x : α}
  {u : Set α}, u ∈ nhds x → Disjoint u (Set.Iio x) → IsMin x
-- Init.Data.UInt.Lemmas
UInt32.toNat_one : UInt32.toNat 1 = 1
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenConj_neg : Real.goldenConj < 0
-- Aesop.Script.Tactic
Aesop.Script.STactic.run : Aesop.Script.STactic → Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousWithinAt_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α},
  UpperSemicontinuousWithinAt f Set.univ x ↔ UpperSemicontinuousAt f x
-- Init.Data.BitVec.Bitblast
BitVec.add_eq_adc : ∀ (w : ℕ) (x y : BitVec w), x + y = (x.adc y false).2
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instGeometricallyReducedFiberToSpecResidueField : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyReduced f],
  AlgebraicGeometry.GeometricallyReduced (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.not.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Std.Tactic.BVDecide.BoolExpr α), sizeOf a.not = 1 + sizeOf a
-- Mathlib.Combinatorics.Matroid.Circuit
/-- In a finitary matroid, every element spanned by a set `X` is in fact
spanned by a finite independent subset of `X`.  -/
Matroid.exists_mem_finite_closure_of_mem_closure : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} [M.Finitary],
  e ∈ M.closure X → ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.below.blackL : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : RBTree.RBNode.Path α) →
      (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop}
  {y : RBTree.RBNode α} {c₂ : RBTree.RBColor} {n : ℕ} {parent : RBTree.RBNode.Path α} {v : α} {c₁ : RBTree.RBColor}
  (a : y.Balanced c₂ n) (a_1 : RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.black (n + 1)),
  RBTree.RBNode.Path.Balanced.below a_1 →
    motive parent RBTree.RBColor.black (n + 1) a_1 → RBTree.RBNode.Path.Balanced.below ⋯
-- Mathlib.LinearAlgebra.Ray
RayVector.coe : {R : Type u_1} → {M : Type u_2} → [inst : Zero M] → CoeOut (RayVector R M) M
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.zpow_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H)
  [CategoryTheory.IsMonHom g], CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  Neg.neg '' Set.Iic a = Set.Ici (-a)
-- Std.Tactic.Do.Syntax
/-- A hint tactic that expands to `mvcgen invariants?`.
 -/
Lean.Parser.Tactic.mvcgenHint : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The diagram of the filtered colimit presentation  -/
CategoryTheory.Limits.IndObjectPresentation.F : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (self : CategoryTheory.Limits.IndObjectPresentation A) → CategoryTheory.Functor self.I C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_minKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {f : β → β}, t.WF → (Std.DTreeMap.Raw.Const.modify t k f).minKey?.isSome = !t.isEmpty
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.comp_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ {X Y : C} {a : X ⟶ S.X₂},
      CategoryTheory.CategoryStruct.comp a S.g = 0 →
        ∀ {b : S.X₂ ⟶ Y}, CategoryTheory.CategoryStruct.comp S.f b = 0 → CategoryTheory.CategoryStruct.comp a b = 0
-- Mathlib.Algebra.Group.Defs
nsmulBinRec.go.eq_1 : ∀ {M : Type u_2} [inst : Add M] (k : ℕ),
  nsmulBinRec.go k =
    Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y + x else y) (x + x)) k
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.mk.inj : ∀ {numNodes numNull numCollisions maxDepth numNodes_1 numNull_1 numCollisions_1 maxDepth_1 : ℕ},
  { numNodes := numNodes, numNull := numNull, numCollisions := numCollisions, maxDepth := maxDepth } =
      { numNodes := numNodes_1, numNull := numNull_1, numCollisions := numCollisions_1, maxDepth := maxDepth_1 } →
    numNodes = numNodes_1 ∧ numNull = numNull_1 ∧ numCollisions = numCollisions_1 ∧ maxDepth = maxDepth_1
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFinitePresentation f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- For quadratic forms on finite-dimensional spaces, the maximal finrank of a positive-definite
subspace of `M`. (Defined as `0` if `M` is infinite-dimensional).  -/
sigPos : {R : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommGroup M] → [inst_1 : CommRing R] → [LinearOrder R] → [inst_3 : Module R M] → QuadraticForm R M → ℕ
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instCoeSortType : CoeSort SemiNormedGrp₁ (Type u_1)
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_neg : ∀ (a : UInt32), (-a).toUInt64 = -a.toUInt64 % 4294967296
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_norm_tendsto_zero : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : NormedField β],
  Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Filter.Tendsto (fun a => ‖k a ^ n * f a‖) l (nhds 0)
-- Mathlib.Order.Partition.Basic
Partition.mem_iff_mem_partOf_mem : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, x ∈ u ↔ x ∈ P.partOf x ∧ P.partOf x ∈ P
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.locallyLinear_comap : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph β} {e : α ≃ β},
  (SimpleGraph.comap (⇑e) G).LocallyLinear ↔ G.LocallyLinear
-- Mathlib.Analysis.CStarAlgebra.Classes
instCommCStarAlgebraComplex : CommCStarAlgebra ℂ
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.toMessageData : Lean.Meta.Grind.Result → Lean.MetaM Lean.MessageData
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_div_left : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k) μ
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_eq_top : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y},
  eHolderNorm r f = ⊤ ↔ ¬MemHolder r f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineEquiv.linear_ofEq : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [inst_4 : Nonempty ↥S₁] [inst_5 : Nonempty ↥S₂]
  (h : S₁ = S₂), (AffineEquiv.ofEq S₁ S₂ h).linear = LinearEquiv.ofEq S₁.direction S₂.direction ⋯
-- Mathlib.Analysis.Convex.Gauge
gauge_mono : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s t : Set E}, Absorbent ℝ s → s ⊆ t → gauge t ≤ gauge s
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasProductsOfShape_of_hasBiproductsOfShape : ∀ {J : Type w} (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C],
  CategoryTheory.Limits.HasProductsOfShape J C
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_conjTranspose : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] (A : Matrix m n 𝕜), ‖A.conjTranspose‖ = ‖A‖
-- Mathlib.Data.Finset.Prod
Finset.filter_product_card : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop) [inst : DecidablePred p]
  [inst_1 : DecidablePred q],
  {x ∈ s ×ˢ t | p x.1 = q x.2}.card =
    (Finset.filter p s).card * (Finset.filter q t).card + {x ∈ s | ¬p x}.card * {x ∈ t | ¬q x}.card
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetGE : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
  (n : ℕ), MeasureTheory.SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsWeakLimit t) {W : C} (h : W ⟶ X)
  (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C}
  (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w)
      (CategoryTheory.CategoryStruct.comp t.fst h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Init.Data.List.Basic
List.nodupDecidable : {α : Type u} → [DecidableEq α] → (l : List α) → Decidable l.Nodup
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_eq_setToL1S : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.integral f = MeasureTheory.L1.SimpleFunc.setToL1S (MeasureTheory.weightedSMul μ) f
-- Qq.Macro
Qq.Impl.macro : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan.eq_def : ∀ (x : ℕ),
  catalan x =
    match x with
    | 0 => 1
    | n.succ => ∑ i, catalan ↑i * catalan (n - ↑i)
-- Init.Grind.ToInt
Lean.Grind.ToInt.Zero.wrap_zero : ∀ {α : Type u_1} (I : Lean.Grind.IntInterval) [inst : Zero α] [inst_1 : Lean.Grind.ToInt α I]
  [Lean.Grind.ToInt.Zero α I], I.wrap 0 = 0
-- Mathlib.Lean.MessageData.ForExprs
/-- Get all the expressions in a message, in order.

If you need the context of the expressions, prefer iterating over the expressions via
`for (ppCtx, e) in msg.exprs do` directly.  -/
Lean.MessageData.getExprs : {m : Type → Type u} → [Monad m] → [MonadLiftT BaseIO m] → Lean.MessageData → m (Array Lean.Expr)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mk.injEq : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (toAddSubmonoid : AddSubmonoid R)
  (mul_mem' : ∀ {a b : R}, a ∈ toAddSubmonoid.carrier → b ∈ toAddSubmonoid.carrier → a * b ∈ toAddSubmonoid.carrier)
  (toAddSubmonoid_1 : AddSubmonoid R)
  (mul_mem'_1 :
    ∀ {a b : R}, a ∈ toAddSubmonoid_1.carrier → b ∈ toAddSubmonoid_1.carrier → a * b ∈ toAddSubmonoid_1.carrier),
  ({ toAddSubmonoid := toAddSubmonoid, mul_mem' := mul_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, mul_mem' := mul_mem'_1 }) =
    (toAddSubmonoid = toAddSubmonoid_1)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing.eq_1 : ∀ (R : Type u) (ι : Type v) {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M] (z : M),
  ContinuousMultilinearMap.mkPiRing R ι z = (ContinuousMultilinearMap.mkPiAlgebra R ι R).smulRight z
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.IsMinimal.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W W_1 : WeierstrassCurve K),
  W = W_1 → WeierstrassCurve.IsMinimal R W = WeierstrassCurve.IsMinimal R W_1
-- Mathlib.Geometry.Convex.Hull
Convexity.IsConvexSet.convexHull_subset_iff : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {C s : Set X},
  Convexity.IsConvexSet R C → ((Convexity.convexHull R) s ⊆ C ↔ s ⊆ C)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Icc_add_one_left_eq_Ioc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a : α},
  ¬IsMax a → ∀ (b : α), Set.Icc (a + 1) b = Set.Ioc a b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.isEmpty_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- The order isomorphism between Lie ideals and invariant root submodules.  -/
LieAlgebra.IsKilling.lieIdealOrderIso : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : CharZero K] →
        [inst_2 : LieRing L] →
          [inst_3 : LieAlgebra K L] →
            [inst_4 : FiniteDimensional K L] →
              [inst_5 : LieAlgebra.IsKilling K L] →
                (H : LieSubalgebra K L) →
                  [inst_6 : H.IsCartanSubalgebra] →
                    [inst_7 : LieModule.IsTriangularizable K (↥H) L] →
                      LieIdeal K L ≃o ↥(LieAlgebra.IsKilling.rootSystem H).invtRootSubmodule
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.top_prod_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ⊤.prod ⊤ = ⊤
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.isUnit_one_sub_smul_of_lt_inv_radius : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  {a : A} {z : 𝕜}, ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹ → IsUnit (1 - z • a)
-- Mathlib.Topology.MetricSpace.ProperSpace
ProperSpace.isCompact_closedBall : ∀ {α : Type u} {inst : PseudoMetricSpace α} [self : ProperSpace α] (x : α) (r : ℝ), IsCompact (Metric.closedBall x r)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instLargeCategory : CategoryTheory.LargeCategory NonemptyFinLinOrd
-- Mathlib.Topology.Compactness.Compact
/-- Cantor's intersection theorem for `iInter`:
the intersection of a directed family of nonempty compact closed sets is nonempty.  -/
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X),
  Directed (fun x1 x2 => x1 ⊇ x2) t →
    (∀ (i : ι), (t i).Nonempty) → (∀ (i : ι), IsCompact (t i)) → (∀ (i : ι), IsClosed (t i)) → (⋂ i, t i).Nonempty
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.zpow` -/
MeromorphicOn.fun_zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn s U → ∀ (n : ℤ), MeromorphicOn (fun i => s i ^ n) U
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `Divisionsemiring α`, if it
exists.  -/
Mathlib.Meta.NormNum.inferCharZeroOfDivisionSemiring? : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(DivisionSemiring «$α») Mathlib.Meta.NormNum.inferCharZeroOfDivisionSemiring?._auto_1) →
      Lean.MetaM (Option Q(CharZero «$α»))
-- Std.Time.Duration
/-- Adds a `Week.Offset` to a `Duration`
 -/
Std.Time.Duration.addWeeks : Std.Time.Duration → Std.Time.Week.Offset → Std.Time.Duration
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_eq_zero : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)]
  (f : (i : ι) → M₂ →ₗ[R] φ i), LinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.leadingCoeff 0 = 0
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- `ordinaryHypergeometric (a b c : 𝕂) : 𝔸 → 𝔸`, denoted `₂F₁`, is the ordinary hypergeometric map,
defined as the sum of the `FormalMultilinearSeries` `ordinaryHypergeometricSeries 𝔸 a b c`.

Note that this takes the junk value `0` outside the radius of convergence.
 -/
ordinaryHypergeometric : {𝕂 : Type u_1} →
  {𝔸 : Type u_2} →
    [inst : Field 𝕂] →
      [inst_1 : Ring 𝔸] → [Algebra 𝕂 𝔸] → [inst : TopologicalSpace 𝔸] → [IsTopologicalRing 𝔸] → 𝕂 → 𝕂 → 𝕂 → 𝔸 → 𝔸
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- The underlying function  -/
MeasureTheory.SimpleFunc.toFun : {α : Type u} → [inst : MeasurableSpace α] → {β : Type v} → MeasureTheory.SimpleFunc α β → α → β
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Composition of a conjugate square with a square between right adjoints.  -/
CategoryTheory.Bicategory.rightAdjointConjugateSquare.vcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {g : a ⟶ c} →
        {h : b ⟶ d} →
          {r₁ r₂ : b ⟶ a} →
            {r₃ : d ⟶ c} →
              (r₁ ⟶ r₂) →
                (CategoryTheory.CategoryStruct.comp r₂ g ⟶ CategoryTheory.CategoryStruct.comp h r₃) →
                  (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₃)
-- Mathlib.RepresentationTheory.Coinduced
/-- If `φ : G →* H` and  `A : Rep k G` then `coind φ A` is the coinduction of `A` along `φ`,
defined by letting `H` act on the `G`-equivariant functions `H → A` by `(h • f) h₁ := f (h₁ * h)`.
 -/
Rep.coind : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → (G →* H) → Rep.{u_1, u, v} k G → Rep.{max w u_1, u, w} k H
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.lintegral_tendsto_of_countably_generated : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ENNReal},
      AEMeasurable f μ → Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (nhds (∫⁻ (x : α), f x ∂μ))
-- Mathlib.CategoryTheory.Grothendieck
/-- The functor to build the equivalence `compAsSmallFunctorEquivalence`.  -/
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) →
      CategoryTheory.Functor (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor))
        (CategoryTheory.Grothendieck F)
-- Mathlib.Topology.Separation.Basic
instR0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], R0Space X
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.comp_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsStableUnderComposition]
  [inst_4 : W.IsStableUnderComposition] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X.Hom Y)
  (g : Y.Hom Z), (f.comp g).right = CategoryTheory.CategoryStruct.comp f.right g.right
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
IsTopologicallyNilpotent.mem_topologicalNilradical_iff : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [inst_2 : IsLinearTopology R R] {a : R},
  a ∈ topologicalNilradical R ↔ IsTopologicallyNilpotent a
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_eq_zero_of_le_right : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, K ≤ L → H.relIndex K = 0 → H.relIndex L = 0
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateL.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk)
  (rr : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.rotateL k v l rk rv Std.DTreeMap.Internal.Impl.leaf rr =
    if Std.DTreeMap.Internal.Impl.leaf.size < Std.DTreeMap.Internal.ratio * rr.size then
      Std.DTreeMap.Internal.Impl.singleL k v l rk rv Std.DTreeMap.Internal.Impl.leaf rr
    else Std.DTreeMap.Internal.Impl.singleL k v l rk rv Std.DTreeMap.Internal.Impl.leaf rr
-- Init.System.IO
IO.FS.instInhabitedStream : Inhabited IO.FS.Stream
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_unitIso : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U),
  (TopCat.Presheaf.generateEquivalenceOpensLe U hY).unitIso = CategoryTheory.eqToIso ⋯
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toPresheafedSpace_map : ∀ (R S : CommRingCatᵒᵖ) (f : R ⟶ S),
  AlgebraicGeometry.Spec.toPresheafedSpace.map f = (AlgebraicGeometry.Spec.sheafedSpaceMap f.unop).hom
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.mk : {M : Type u_10} →
  {N : Type u_11} →
    [inst : Mul M] → [inst_1 : Mul N] → (toFun : M → N) → (∀ (x y : M), toFun (x * y) = toFun x * toFun y) → M →ₙ* N
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_inv : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α), σ⁻¹.cycleType = σ.cycleType