mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
/-- Evaluates `k` from within a `letTelescope`, then uses `mkLetFVars` to rebuild the telescope.
 -/
Lean.Meta.mapLetTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      [MonadLiftT Lean.MetaM n] →
        Lean.Expr →
          (Array Lean.Expr → Lean.Expr → n Lean.Expr) →
            optParam Bool false → optParam Bool true → optParam Bool false → optParam Bool true → n Lean.Expr
-- Init.Data.Bool
Bool.xor_right_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z
-- Init.Data.Array.Lemmas
Array.singleton_eq_toArray_singleton : ∀ {α : Type u_1} {a : α}, #[a] = #[a]
-- Mathlib.Control.Applicative
Applicative.ext : ∀ {F : Type u → Type u_1} {A1 A2 : Applicative F} [LawfulApplicative F] [LawfulApplicative F],
  (∀ {α : Type u} (x : α), pure x = pure x) → (∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x) → A1 = A2
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X]
  [inst_1 : SMul N Y] [inst_2 : SMul R Y] [inst_3 : SMulCommClass N R Y] (f : X →ₑ[σ] Y) (r : R), ⇑(r • f) = r • ⇑f
-- Mathlib.Algebra.Group.Invertible.Basic
Invertible.mulRight_apply : ∀ {α : Type u} [inst : Monoid α] (a : α) {b : α} (x : Invertible b) (x_1 : Invertible a),
  (Invertible.mulRight a x) x_1 = invertibleMul a b
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.equiv_apply : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (self : v.Completion),
  (NumberField.InfinitePlace.Completion.equiv v) self = self.toCompletion
-- Mathlib.Order.Defs.Unbundled
RelUpperSet.mk : {α : Type u_1} → [inst : LE α] → {P : α → Prop} → (carrier : Set α) → IsRelUpperSet carrier P → RelUpperSet P
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- A finite-product-preserving functor takes group objects to group objects.  -/
CategoryTheory.Functor.mapGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] → CategoryTheory.Functor (CategoryTheory.Grp C) (CategoryTheory.Grp D)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.value : Lean.Elab.InlayHintLabelPart → String
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.edist_lt_top : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), edist x y < ⊤
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderIsomorphisms],
  P.strictLimitsOfShape J ≤ P → P.IsClosedUnderLimitsOfShape J
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Monotone.locallyIntegrable : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ], Monotone f → MeasureTheory.LocallyIntegrable f μ
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.isPullback : ∀ {X Y : SSet} (i : X ⟶ Y) (d : ℕ),
  CategoryTheory.IsPullback (SSet.relativeCellComplexOfMono.t i d) (SSet.relativeCellComplexOfMono.l i d)
    (SSet.relativeCellComplexOfMono.r i d) (SSet.relativeCellComplexOfMono.b i d)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.BifibrantObject.ι.obj X)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `Polynomial.Gal.restrict`, when both fields are splitting fields of polynomials.  -/
Polynomial.Gal.restrictDvd : {F : Type u_1} → [inst : Field F] → {p q : Polynomial F} → p ∣ q → q.Gal →* p.Gal
-- Mathlib.Algebra.Lie.Classical
/-- The classical Lie algebra of type D as a Lie subalgebra of matrices associated to the matrix
`JD`.  -/
LieAlgebra.Orthogonal.typeD : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] → [inst_1 : CommRing R] → [inst_2 : Fintype l] → LieSubalgebra R (Matrix (l ⊕ l) (l ⊕ l) R)
-- Init.Meta.Defs
Lean.MonadNameGenerator : (Type → Type) → Type
-- Init.PropLemmas
Decidable.not_imp_symm : ∀ {a b : Prop} [Decidable a], (¬a → b) → ¬b → a
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.counit_comp_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B] [CoalgHomClass F R A B] (f : F) (x : A),
  CoalgebraStruct.counit (f x) = CoalgebraStruct.counit x
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A measure which is finite on compact sets in a locally compact space is locally finite.  -/
MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [WeaklyLocallyCompactSpace α] [MeasureTheory.IsFiniteMeasureOnCompacts μ], MeasureTheory.IsLocallyFiniteMeasure μ
-- Mathlib.Data.Matrix.DMatrix
DMatrix.add_apply : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → Add (α i j)] (M N : DMatrix m n α)
  (i : m) (j : n), (M + N) i j = M i j + N i j
-- Mathlib.Order.Lex
instCoeFunLex : {α : Type u_2} → {γ : α → Sort u_3} → [H : CoeFun α γ] → CoeFun (Lex α) γ
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.subNegMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : Neg M₁]
  [inst_4 : Sub M₁] [inst_5 : SMul ℤ M₁] [inst_6 : SubNegMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Injective.subNegMonoid f hf one mul inv div npow zpow =
    { toAddMonoid := Function.Injective.addMonoid f hf one mul npow, toNeg := inst_3, toSub := inst_4,
      zsmul := fun n x => n • x, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
powersEquivPowers.eq_1 : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Finite G] {x y : G} (h : orderOf x = orderOf y),
  powersEquivPowers h = (finEquivPowers ⋯).symm.trans ((finCongr h).trans (finEquivPowers ⋯))
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula for derivatives**, assuming `f` is differentiable on a closed ball.  -/
DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ},
  0 < R →
    ∀ (n : ℕ),
      DifferentiableOn ℂ f (Metric.closedBall c R) →
        ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
          (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
-- Init.Data.Range.Polymorphic.Basic
Std.Rcc.mem_iff : ∀ {α : Type u} [inst : LE α] {r : Std.Rcc α} {a : α}, a ∈ r ↔ r.lower ≤ a ∧ a ≤ r.upper
-- Init.Data.Option.Attach
Option.attachWith_guard : ∀ {α : Type u_1} {q : α → Bool} {x : α} {P : α → Prop} {h : ∀ (a : α), Option.guard q x = some a → P a},
  (Option.guard q x).attachWith P h = if h' : q x = true then some ⟨x, ⋯⟩ else none
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.Hom.hom.eq_1 : ∀ {X Y : CommMonCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.Topology.Algebra.ConstMulAction
Dense.smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G) {s : Set α}, Dense s → Dense (c • s)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Each element of the monoid defines an additive monoid homomorphism.  -/
DistribMulAction.toAddMonoidEnd : (M : Type u_1) →
  (A : Type u_7) → [inst : Monoid M] → [inst_1 : AddMonoid A] → [DistribMulAction M A] → M →* AddMonoid.End A
-- Mathlib.RepresentationTheory.Invariants
GroupAlgebra.average.eq_1 : ∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : Invertible ↑(Fintype.card G)], GroupAlgebra.average k G = ⅟↑(Fintype.card G) • ∑ g, (MonoidAlgebra.of k G) g
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.mk_maximalIdeal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : NumberField.FinitePlace K),
  NumberField.FinitePlace.mk w.maximalIdeal = w
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] [ContinuousInv₀ G],
  ContMDiffInv₀ I 0 G
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.leftTriple_adj₂ : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.leftTriple.adj₂ = q.adj₂
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_rcc : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
        List.filter (fun e => decide ((compare e.1 lowerBound).isGE = true ∧ (compare e.1 upperBound).isLE = true))
          (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_pointReflection_left : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (p q : P), dist ((Equiv.pointReflection p) q) p = dist p q
-- Lean.DocString.DeferredCheck
/-- A recording of the fact that some kind of check could not be carried out when a docstring was
elaborated, due to some missing information that is expected to be available in the future. This is
used for forward references.

The type of the value in `check` selects the handler that carries out the check.

Source positions are not stored because they would shift with edits. Because deferred checks are
part of the public information of a module, this would lead to needless rebuilds. The docstring is
identified by `site`, the reference within it by `index`, and `sourceString` (the reference's source
text) gives readable error messages even without an accurate location.
 -/
Lean.Doc.DeferredCheck : Type
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
/-- The ⋆-algebra equivalence version of
`ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv`.

TODO: remove the hypothesis `Continuous f`, as star-algebra equivalences between endomorphisms are
automatically continuous.  -/
StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] [inst_4 : NormedAddCommGroup W]
  [inst_5 : InnerProductSpace 𝕜 W] [inst_6 : CompleteSpace W] (f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W),
  Continuous ⇑f → ∃ U, f = U.conjStarAlgEquiv
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.instantiateForall.go.eq_def : ∀ (ps : Array Lean.Expr) (i : ℕ) (type : Lean.Expr),
  Lean.Compiler.LCNF.instantiateForall.go✝ ps i type =
    if h : i < ps.size then
      match type.headBeta with
      | Lean.Expr.forallE binderName binderType b binderInfo =>
        Lean.Compiler.LCNF.instantiateForall.go✝ ps (i + 1) (b.instantiate1 ps[i])
      | x => Lean.throwError (Lean.toMessageData "invalid instantiateForall, too many parameters")
    else pure type
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.reflectsIsomorphisms_iso_iff : ∀ {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] {F G : CategoryTheory.Functor C D} (α : F ≅ G),
  F.ReflectsIsomorphisms ↔ G.ReflectsIsomorphisms
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- `Tendsto` along `atTop` for a function precomposed with `Finset.card` reduces to `Tendsto` along
`atTop` on `ℕ`, when `α` is infinite.  -/
Filter.tendsto_comp_card_atTop_iff : ∀ {α : Type u_3} {β : Type u_4} [Infinite α] {f : ℕ → β} {l : Filter β},
  Filter.Tendsto (fun s => f s.card) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
-- Mathlib.Data.List.Intervals
List.Ico.filter_lt : ∀ (n m l : ℕ), List.filter (fun x => decide (x < l)) (List.Ico n m) = List.Ico n (min m l)
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.hasColimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasColimitsOfShape J (Type u)
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.independent_of_coprime_order : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G},
  (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) →
    ∀ [Finite ι] [inst_2 : (i : ι) → Fintype ↥(H i)],
      (Pairwise fun i j => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))) → iSupIndep H
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.toLinearMap_eq_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B), f.toLinearMap = ↑f
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasEigenvector.pow_apply : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {v : M}, f.HasEigenvector μ v → ∀ (n : ℕ), (f ^ n) v = μ ^ n • v
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.sepByFnAux : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Bool → ℕ → Bool → Lean.Parser.ParserFn
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  (E : IntermediateField K L),
  SeminormClass (AlgebraNorm K ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) K
    ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.one_le_netMaxcard_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ), 1 ≤ Dynamics.netMaxcard T F U n ↔ F.Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.comp_diagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pullback.diagonal g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor.inj : ∀ {e : Lean.Expr} {f : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr} {f_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e f =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e_1 f_1 →
    e = e_1 ∧ f = f_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.enorm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), ‖e x‖ₑ = ‖x‖ₑ
-- Mathlib.Order.Heyting.Hom
HeytingHom.id_apply : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), (HeytingHom.id α) a = a
-- Mathlib.Topology.Algebra.Ring.Basic
instIsTopologicalSemiringULift : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [IsTopologicalSemiring R],
  IsTopologicalSemiring (ULift.{u_2, u_1} R)
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
/-- **Alias** of `MvPolynomial.rTensorAlgEquiv`.

---

The algebra morphism from a tensor product of a polynomial algebra
by an algebra to a polynomial algebra  -/
MvPolynomial.rTensorAlgHom : {R : Type u} →
  {N : Type v} →
    [inst : CommSemiring R] →
      {σ : Type u_1} →
        {S : Type u_3} →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommSemiring N] →
                [inst_4 : Algebra R N] → TensorProduct R S (MvPolynomial σ N) ≃ₐ[S] MvPolynomial σ (TensorProduct R S N)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- generators  -/
SheafOfModules.Presentation.generators : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.Presentation → M.GeneratingSections
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Express `nndist` in terms of `edist`  -/
nndist_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), nndist x y = (edist x y).toNNReal
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.inv_vlt_one : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {x : K}, x ≠ 0 → (x⁻¹ <ᵥ 1 ↔ 1 <ᵥ x)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given a limit cone, `F.cones` is representable by the point of the cone.  -/
CategoryTheory.Limits.IsLimit.representableBy : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit t → F.cones.RepresentableBy t.pt
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- `cfc_le_iff` only applies to a scalar ring where `R` is an actual `Ring`, and not a `Semiring`.
However, this theorem still holds for `ℝ≥0` as long as the algebra `A` itself is an `ℝ`-algebra.  -/
cfc_nnreal_le_iff : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [IsTopologicalRing A] [inst_7 : NonnegSpectrumClass ℝ A]
  [T2Space A] [inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f g : NNReal → NNReal) (a : A),
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
    autoParam (ContinuousOn f (spectrum NNReal a)) cfc_nnreal_le_iff._auto_1 →
      autoParam (ContinuousOn g (spectrum NNReal a)) cfc_nnreal_le_iff._auto_3 →
        autoParam (0 ≤ a) cfc_nnreal_le_iff._auto_5 → (cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum NNReal a, f x ≤ g x)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β}, (cmp k (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.toLocalized₀_apply_coe : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' : Submodule R M) (c : ↥M'), ↑((Submodule.toLocalized₀ p f M') c) = f ↑c
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_injective : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → Function.Injective (Ordinal.enumOrd s)
-- Mathlib.Algebra.Group.Action.End
/-- The monoid action induced by a monoid hom to `Function.End α`

See note [reducible non-instances].  -/
MulAction.ofEndHom : {M : Type u_2} → {α : Type u_5} → [inst : Monoid M] → (M →* Function.End α) → MulAction M α
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_ciInf_eq_left_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {b : β} {f : (x : β) → x = b → α},
  ⨅ x, ⨅ (h : x = b), f x h ≤ f b ⋯
-- Init.Data.UInt.Lemmas
USize.ofNatLT_add : ∀ {a b : ℕ} (hab : a + b < 2 ^ System.Platform.numBits),
  USize.ofNatLT (a + b) hab = USize.ofNatLT a ⋯ + USize.ofNatLT b ⋯
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.revlexWF.match_1.splitter : (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) →
  (m₁ m₂ : Lean.Grind.CommRing.Mon) →
    (Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit) →
      ((p : Lean.Grind.CommRing.Power) →
          (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m)) →
        ((p : Lean.Grind.CommRing.Power) →
            (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit) →
          ((pw₁ : Lean.Grind.CommRing.Power) →
              (m₁ : Lean.Grind.CommRing.Mon) →
                (pw₂ : Lean.Grind.CommRing.Power) →
                  (m₂ : Lean.Grind.CommRing.Mon) →
                    motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
            motive m₁ m₂
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.refl_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), CategoryTheory.Iso.refl X ≪≫ α = α
-- Mathlib.Logic.Equiv.Defs
Equiv.mk : {α : Sort u_1} →
  {β : Sort u_2} →
    (toFun : α → β) →
      (invFun : β → α) →
        autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam →
          autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam → α ≃ β
-- Std.Time.Date.Unit.Year
Std.Time.Year.instNegOffset : Neg Std.Time.Year.Offset
-- Mathlib.Order.Defs.LinearOrder
le_min : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a b
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- A limit pullback cone in the category of types identifies to the explicit pullback.  -/
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj : {X Y S : Type v} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      {c : CategoryTheory.Limits.PullbackCone f g} →
        CategoryTheory.Limits.IsLimit c → c.pt ≃ CategoryTheory.Limits.Types.PullbackObj f g