mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Lattice
Set.iUnion_mono : ∀ {α : Type u_1} {ι : Sort u_5} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → ⋃ i, s i ⊆ ⋃ i, t i
-- Mathlib.Topology.Compactness.LocallyCompact
IsClosed.locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {s : Set X}, IsClosed s → LocallyCompactSpace ↑s
-- Mathlib.GroupTheory.GroupAction.Blocks
_private.Mathlib.GroupTheory.GroupAction.Blocks.0.MulAction.block_stabilizerOrderIso.match_1.splitter : (G : Type u_2) →
  [inst : Group G] →
    {X : Type u_1} →
      [inst_1 : MulAction G X] →
        (a : X) →
          (motive : { B // a ∈ B ∧ MulAction.IsBlock G B } → Sort u_3) →
            (x : { B // a ∈ B ∧ MulAction.IsBlock G B }) →
              ((B : Set X) → (ha : a ∈ B) → (hB : MulAction.IsBlock G B) → motive ⟨B, ⋯⟩) → motive x
-- Mathlib.Topology.AlexandrovDiscrete
principal_nhdsKer : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α),
  Filter.principal (nhdsKer s) = nhdsSet s
-- Mathlib.Data.Set.Card
Set.cast_ncard : ∀ {α : Type u_1} {s : Set α}, s.Finite → ↑s.ncard = Cardinal.mk ↑s
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr_comp_lsingle : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (m : M),
  (AddMonoidAlgebra.domCongr R A e).toLinearMap ∘ₗ AddMonoidAlgebra.lsingle m = AddMonoidAlgebra.lsingle (e m)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.toInv : {α : Type u_3} → [self : LinearOrderedCommGroupWithZero α] → Inv α
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The additive action `(+ᵥ) : Γ → T → T` is continuous in the second argument.  -/
ContinuousConstVAdd.continuous_const_vadd : ∀ {Γ : Type u_1} {T : Type u_2} {inst : TopologicalSpace T} {inst_1 : VAdd Γ T} [self : ContinuousConstVAdd Γ T]
  (γ : Γ), Continuous fun x => γ +ᵥ x
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a Heyting homomorphism preserves the Heyting implication.  -/
HeytingHom.map_himp' : ∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (self : HeytingHom α β) (a b : α),
  self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
-- Mathlib.Order.Hom.Basic
/-- If `α` and `β` are order-isomorphic then the two orders of order-homomorphisms
from `α` and `β` to themselves are order-isomorphic.  -/
OrderIso.conj : {α : Type u_6} → {β : Type u_7} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → (α →o α) ≃ (β →o β)
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_empty : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {c : E}, MeasureTheory.indicatorConstLp p ⋯ ⋯ c = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top : ∀ (X : SSet), ⨆ x, SSet.Subcomplex.ofSimplex ↑x.snd = ⊤
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {x : M} {f : M → E'}, mfderiv% (-f) x = -mfderiv% f x
-- Mathlib.Order.Hom.Bounded
BotHom.instMax.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β],
  BotHom.instMax = { max := fun f g => { toFun := ⇑f ⊔ ⇑g, map_bot' := ⋯ } }
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc.eq_1 : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {x : MeasurableSpace α} (T : Set α → F →L[ℝ] F')
  (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x_1 ∈ f.range, (T (⇑f ⁻¹' {x_1})) x_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)], (↑m).isEmpty = true → m.get! a = default
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback : α}, Std.Internal.List.getKeyD (Std.Internal.List.maxKey! l) l fallback = Std.Internal.List.maxKey! l
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.unbotD_zero_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : WithBot α),
  WithBot.unbotD 0 (a * b) = WithBot.unbotD 0 a * WithBot.unbotD 0 b
-- Mathlib.Order.Preorder.Finsupp
Finsupp.inf_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : SemilatticeInf M] (f g : ι →₀ M) (i : ι),
  (f ⊓ g) i = f i ⊓ g i
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
instDecidableEqDihedralGroup.decEq : {n : ℕ} → (x x_1 : DihedralGroup n) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)]
  [CategoryTheory.Presheaf.IsLocallyInjective J f₂], CategoryTheory.Presheaf.IsLocallySurjective J f₁
-- Init.Data.List.Sort.Lemmas
/-- If the ordering relation `le` is transitive and total (i.e. `le a b || le b a` for all `a, b`)
then the `merge` of two sorted lists is sorted.
 -/
List.pairwise_merge : ∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      ∀ (l₁ l₂ : List α),
        List.Pairwise (fun a b => le a b = true) l₁ →
          List.Pairwise (fun a b => le a b = true) l₂ → List.Pairwise (fun a b => le a b = true) (l₁.merge l₂ le)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The essential image of `Over.post F` where `F` is full is the same as the essential image of
`F`.  -/
CategoryTheory.Functor.essImage_overPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} [F.Full] {Y : CategoryTheory.Over (F.obj X)},
  (CategoryTheory.Over.post F).essImage Y ↔ F.essImage Y.left
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- The categorical product of a finite family in `FintypeCat` is equivalent to the product
as types.  -/
CategoryTheory.Limits.FintypeCat.productEquiv : {ι : Type u_1} → [inst : Finite ι] → (X : ι → FintypeCat) → (∏ᶜ X).obj ≃ ((i : ι) → (X i).obj)
-- Lean.Environment
_private.Lean.Environment.0.Lean.RealizationContext.mk.injEq : ∀ (env : NonScalar) (opts : Lean.Options) (realizeMapRef : IO.Ref (Lean.NameMap NonScalar)) (env_1 : NonScalar)
  (opts_1 : Lean.Options) (realizeMapRef_1 : IO.Ref (Lean.NameMap NonScalar)),
  ({ env := env, opts := opts, realizeMapRef := realizeMapRef } =
      { env := env_1, opts := opts_1, realizeMapRef := realizeMapRef_1 }) =
    (env = env_1 ∧ opts = opts_1 ∧ realizeMapRef = realizeMapRef_1)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_intCast_star : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Ring α] [inst_2 : StarRing α] (d : ℤ), (↑d).map star = ↑d
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.Injective : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] {a : α},
  AddLECancellable a → Function.Injective fun x => a + x
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.single_strictAnti : ∀ {α : Type u_1} [inst : LinearOrder α], StrictAnti fun a => toLex fun₀ | a => 1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Occurrence sets are closed.  -/
SymbolicDynamics.FullShift.isClosed_mulOccursInAt : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : Monoid G]
  [IsLeftCancelMul G] [T1Space A] (p : SymbolicDynamics.FullShift.Pattern A G) (g : G),
  IsClosed {x | p.mulOccursInAt x g}
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.SheafCondition.instInhabitedOpensLeCoverOfNonempty : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) → [h : Nonempty ι] → Inhabited (TopCat.Presheaf.SheafCondition.OpensLeCover U)
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
inf_mul₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : SemilatticeInf G₀] [MulPosReflectLT G₀] {c : G₀},
  0 ≤ c → ∀ (a b : G₀), (a ⊓ b) * c = a * c ⊓ b * c
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.hausdorffMeasure_of_finrank_lt : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {d : ℝ},
  ↑(Module.finrank ℝ E) < d → MeasureTheory.Measure.hausdorffMeasure d = 0
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (i : J) {j : J} (iter : Φ.Iteration j) (hi : i ≤ j),
  (Φ.iterationFunctor J).obj i = iter.F.obj ⟨i, hi⟩
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ord_term : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (i : I),
  Profinite.NobelingProof.ord I i = o ↔ Profinite.NobelingProof.term I ho = i
-- Mathlib.Algebra.Ring.CentroidHom
NonUnitalNonAssocCommSemiring.mem_center_iff : ∀ {α : Type u_5} [inst : NonUnitalNonAssocCommSemiring α] (a : α),
  a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (AddMonoid.End.mulLeft b) (AddMonoid.End.mulLeft a)
-- Init.System.IOError
IO.Error.unsatisfiedConstraints.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.unsatisfiedConstraints osCode details) = 1 + sizeOf osCode + sizeOf details
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.min_le_mk_sub : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a b : M),
  min (ArchimedeanClass.mk a) (ArchimedeanClass.mk b) ≤ ArchimedeanClass.mk (a - b)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.toBilinForm_diagonalStrongDualPi_apply : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ} (x y : StrongDual ℝ ((i : ι) → E i)),
  ((ContinuousLinearMap.diagonalStrongDualPi✝ L).toBilinForm x) y =
    ∑ i, ((L i).toBilinForm (x ∘SL ContinuousLinearMap.single ℝ E i)) (y ∘SL ContinuousLinearMap.single ℝ E i)
-- Std.Sat.AIG.Basic
/-- Add a new input node to the AIG in `aig`. Note that this version is only meant for proving,
for production purposes use `AIG.mkAtomCached` and equality theorems to this one.
 -/
Std.Sat.AIG.mkAtom : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → α → Std.Sat.AIG.Entrypoint α
-- Mathlib.Analysis.SumIntegralComparisons
MonotoneOn.integral_le_sum : ∀ {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ},
  MonotoneOn f (Set.Icc x₀ (x₀ + ↑a)) → ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxcHasSize : Std.Rxc.HasSize Int8
-- Mathlib.Analysis.Seminorm
Seminorm.ball_smul_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ), Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.commaObj_iff : ∀ {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) {W : CategoryTheory.MorphismProperty T}
  (Y : CategoryTheory.Comma L R), CategoryTheory.MorphismProperty.commaObj L R W Y ↔ W Y.hom
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.toClass_injective : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F],
  Function.Injective ⇑WeierstrassCurve.Affine.Point.toClass
-- Aesop.Script.UScript
Aesop.Script.UScript : Type
-- Mathlib.Topology.UnitInterval
unitInterval.mul_pos_mem_iff : ∀ {a t : ℝ}, 0 < a → (a * t ∈ unitInterval ↔ t ∈ Set.Icc 0 (1 / a))
-- Mathlib.Order.Filter.Pointwise
Filter.coe_pureZeroHom : ∀ {α : Type u_2} [inst : Zero α], ⇑Filter.pureZeroHom = pure
-- Init.Meta.Defs
/-- Decodes a quoted name literal, returning the name.

Returns `Lean.Name.anonymous` if the syntax is malformed.
 -/
Lean.TSyntax.getName : Lean.NameLit → Lean.Name
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
SubsemiringClass.toCommSemiring.congr_simp : ∀ {S : Type v} (s : S) {R : Type u_1} [inst : CommSemiring R] [inst_1 : SetLike S R] [inst_2 : SubsemiringClass S R],
  SubsemiringClass.toCommSemiring s = SubsemiringClass.toCommSemiring s
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.one_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S}, 1 ∈ MvPolynomial.coeffsIn σ M ↔ 1 ∈ M
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax'_mapComp_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).inv = F.mapComp f g
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.sub_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂), (φ - φ').τ₂ = φ.τ₂ - φ'.τ₂
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_delete : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (arr : Array ℕ),
  f.ReadyForRupAdd → (f.delete arr).ReadyForRupAdd
-- Mathlib.CategoryTheory.NatIso
/-- Horizontal composition of natural isomorphisms.  -/
CategoryTheory.NatIso.hcomp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F G : CategoryTheory.Functor C D} →
              {H I : CategoryTheory.Functor D E} → (F ≅ G) → (H ≅ I) → (F.comp H ≅ G.comp I)
-- Mathlib.Order.Hom.Basic
/-- If the images by an order embedding of two elements are disjoint,
then they are themselves disjoint.  -/
Disjoint.of_orderEmbedding : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ↪o β) [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] {a₁ a₂ : α}, Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂
-- Mathlib.Tactic.Widget.Conv
/-- A path to a subexpression from a root expression.
The constructors are chosen to be easily translatable into `conv` directions.
 -/
Mathlib.Tactic.Conv.Path : Type
-- Batteries.Data.Nat.Lemmas
Nat.recDiagOn_zero_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (n : ℕ),
  Nat.recDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ =
    zero_succ n (Nat.recDiagOn 0 n zero_zero zero_succ succ_zero succ_succ)
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialOn_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {v : F} {s : Set E},
  CPolynomialOn 𝕜 (fun x => v) s
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidCloseTextDocumentParams : Lean.FromJson Lean.Lsp.DidCloseTextDocumentParams
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type Dₙ (rank n, corresponding to so(2n)).  -/
CartanMatrix.D : (n : ℕ) → Matrix (Fin n) (Fin n) ℤ
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If one controls the norm of every `A x`, then one controls the norm of `A`.  -/
ContinuousLinearMap.opNorm_le_bound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ},
  0 ≤ M → (∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.id_apply : ∀ {R : Type u} [inst : Semiring R] (M : SemimoduleCat R) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.Analysis.Analytic.Uniqueness
/-- The *identity principle* for analytic functions: If an analytic function vanishes in a whole
neighborhood of a point `z₀`, then it is uniformly zero along a connected set. For a one-dimensional
version assuming only that the function vanishes at some points arbitrarily close to `z₀`, see
`AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero`.  -/
AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {U : Set E}, AnalyticOnNhd 𝕜 f U → IsPreconnected U → ∀ {z₀ : E}, z₀ ∈ U → f =ᶠ[nhds z₀] 0 → Set.EqOn f 0 U
-- Lean.Meta.Tactic.Grind.Arith.EvalNum
Lean.Meta.Grind.Arith.evalInt? : Lean.Expr → Lean.Meta.Grind.GrindM (Option ℤ)
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_inter : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α) (x : α),
  (s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- Transport a `HasLimitsOfSize` instance across an equivalence.  -/
CategoryTheory.Adjunction.has_limits_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C],
  CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.map_nonZeroDivisors_le : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N), Submonoid.map f (nonZeroDivisors M) ≤ nonZeroDivisors N
-- Mathlib.Data.Finset.Sups
Finset.inf_mem_infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α} {a b : α},
  a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t
-- Mathlib.Logic.Basic
Xor.or : ∀ {a b : Prop}, Xor a b → a ∨ b
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.combine.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (p₁ : Lean.Grind.Linarith.Poly)
  (h_1 : (p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂)
  (h_2 : (p₁ : Lean.Grind.Linarith.Poly) → motive p₁ Lean.Grind.Linarith.Poly.nil)
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Lean.Grind.Linarith.Var) →
        (p₁ : Lean.Grind.Linarith.Poly) →
          (a₂ : ℤ) →
            (x₂ : Lean.Grind.Linarith.Var) →
              (p₂ : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)),
  (p₁ = Lean.Grind.Linarith.Poly.nil → False) →
    (match p₁, Lean.Grind.Linarith.Poly.nil with
      | Lean.Grind.Linarith.Poly.nil, p₂ => h_1 p₂
      | p₁, Lean.Grind.Linarith.Poly.nil => h_2 p₁
      | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ => h_3 a₁ x₁ p₁ a₂ x₂ p₂) =
      h_2 p₁
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a `Cocone F.op` into a `Cone F`.  -/
CategoryTheory.Limits.Cocone.unop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cocone F.op → CategoryTheory.Limits.Cone F
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.le_topologicalClosure : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M),
  s ≤ s.topologicalClosure
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The forward direction of the left distributivity isomorphism is the cogap morphism
`coprod.desc (_ ◁ coprod.inl) (_ ◁ coprod.inr) : (X ⊗ Y) ⨿ (X ⊗ Z) ⟶ X ⊗ (Y ⨿ Z)`.  -/
CategoryTheory.leftDistrib_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C},
  (CategoryTheory.leftDistrib X Y Z).hom =
    CategoryTheory.Limits.coprod.desc
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr)
-- Mathlib.Computability.Partrec
Nat.Partrec.below : {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop} → {a : ℕ →. ℕ} → Nat.Partrec a → Prop
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over the full range in the
index type `β`.

The type of the resulting slices is `γ`.
 -/
Std.Rii.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max u w)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- Lemmas to prove the meta version of `CategoryTheory.FreeBicategory.normalize_naturality`.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality : (Type → Type) → Type
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.smul_boundedBy : ∀ {α : Type u_1} {m : Set α → ENNReal} {c : ENNReal},
  c ≠ ⊤ → c • MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.boundedBy (c • m)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isLittleO_one_exp_comp : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  ((fun x => 1) =o[l] fun x => Real.exp (f x)) ↔ Filter.Tendsto f l Filter.atTop