mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.id_left : ∀ {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.ContainsIdentities]
  [inst_4 : W.ContainsIdentities] (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  X.id.left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_inv_one_sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] (𝕝 : Type u_8) [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝], AnalyticAt 𝕜 (fun x => (1 - x)⁻¹) 0
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_eq_nat_iff : ∀ {a : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} a = ↑n ↔ a = ↑n
-- Mathlib.Data.Num.ZNum
Num.gcd_to_nat : ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball`.

---

`EMetric.ball x ε` is the set of all points `y` with `edist y x < ε`  -/
EMetric.ball : {α : Type u} → [EDist α] → α → ENNReal → Set α
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- The subtype of `G.subgraph` comprising those subgraphs with finite vertex sets.  -/
SimpleGraph.Finsubgraph : {V : Type u} → SimpleGraph V → Type (max 0 u)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.isComplex : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K}, NumberField.InfinitePlace.IsRamified k w → w.IsComplex
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_zero_lt_veblen_zero : ∀ {o₁ o₂ : Ordinal.{u}}, Ordinal.veblen o₁ 0 < Ordinal.veblen o₂ 0 ↔ o₁ < o₂
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.optimalGHDist : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [CompactSpace X] →
        [Nonempty X] → [inst_3 : MetricSpace Y] → [CompactSpace Y] → [Nonempty Y] → GromovHausdorff.Cb✝ X Y
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2.match_1.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (n : Lean.Name) (d b : Lean.Expr) (binderInfo : Lean.BinderInfo)
  (h_1 :
    (n : Lean.Name) → (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE n d b binderInfo))
  (h_2 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.forallE n d b binderInfo with
    | Lean.Expr.forallE n d b binderInfo => h_1 n d b binderInfo
    | x => h_2 x) =
    h_1 n d b binderInfo
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_tensorUnit_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes : ∀ {R : Type u_1} [inst : CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R y)
      ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h) =
    AlgebraicGeometry.StructureSheaf.toStalk R x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_union_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIso.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), C.xPrevIso r = C.xPrevIso r
-- Std.Do.PostCond
Std.Do.PostShape.brecOn.go : {motive : Std.Do.PostShape → Sort u_1} →
  (t : Std.Do.PostShape) →
    ((t : Std.Do.PostShape) → Std.Do.PostShape.below t → motive t) → motive t ×' Std.Do.PostShape.below t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.cocone_inr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr), h.cocone.inr = inr
-- Mathlib.Data.List.Chain
WellFoundedRelation.asymmetricₙ : ∀ {α : Type u_1} [inst : WellFoundedRelation α] {l : List α} (hne : l ≠ []),
  List.IsChain WellFoundedRelation.rel l → ¬WellFoundedRelation.rel (l.getLast hne) (l.head hne)
-- Mathlib.Algebra.Order.Group.Defs
inv_lt_inv' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a b : α}, a < b → b⁻¹ < a⁻¹
-- Aesop.Rule.Name
Aesop.PhaseName.unsafe.sizeOf_spec : sizeOf Aesop.PhaseName.unsafe = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities.dynamicRegistration? : Lean.Lsp.InlayHintClientCapabilities → Option Bool
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_one_interval : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], ↑1 = 1
-- Mathlib.Order.GaloisConnection.Defs
/-- The Galois connection associated to a Galois coinsertion.  -/
GaloisCoinsertion.gc : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self : GaloisCoinsertion l u), GaloisConnection l u
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.ext : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : ModularForm Γ k}, (∀ (x : UpperHalfPlane), f x = g x) → f = g
-- Mathlib.LinearAlgebra.Matrix.WithConv
instIsScalarTowerWithConvMatrix : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : MulAction β α]
  [inst_2 : Mul α] [IsScalarTower β α α], IsScalarTower β (WithConv (Matrix m n α)) (WithConv (Matrix m n α))
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.instToJsonProps : Lean.ToJson ProofWidgets.MarkdownDisplay.Props
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.join.eq_1 : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)),
  f.join = { weights := f.weights.sum fun d r => r • d.weights, nonneg := ⋯, total := ⋯ }
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_self : ∀ {α : Type u_1} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α},
  la.HasBasis pa sa → (la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.instLieRingModule : {ι : Type v} →
  {L : Type w₁} →
    {M : ι → Type w} →
      [inst : LieRing L] →
        [inst_1 : (i : ι) → AddCommGroup (M i)] →
          [(i : ι) → LieRingModule L (M i)] → LieRingModule L (DirectSum ι fun i => M i)
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- If `R` is a ring, then `Rᵣ` is `R`-finitely-presented for any `r : R`.  -/
RingHom.finitePresentation_holdsForLocalizationAway : RingHom.HoldsForLocalizationAway @RingHom.FinitePresentation
-- Lean.Parser.Types
/-- Parser context parts that can be updated without invalidating the parser cache.  -/
Lean.Parser.CacheableParserContext : Type
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The image of the normalizer is equal to the normalizer of the image of a bijective
function.  -/
Subgroup.map_normalizer_eq_of_bijective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : G →* N},
  Function.Bijective ⇑f → Subgroup.map f (Subgroup.normalizer ↑H) = Subgroup.normalizer ↑(Subgroup.map f H)
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f]
  [inst : AlgebraicGeometry.IsSeparated f] [inst_1 : AlgebraicGeometry.QuasiCompact f] (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x →
    ∃ V,
      (AlgebraicGeometry.Scheme.Hom.toNormalization f) x ∈ V ∧
        CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.toNormalization f ∣_ V)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_map : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {x x_1 : CategoryTheory.Pairwise ι} (i : x ⟶ x_1),
  (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).map i =
    TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap U i
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  -/
MeasureTheory.«term∫⁻_,_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.toUnder_obj_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} S]
  (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y)
  (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) (Y : S),
  ((F.toUnder X f h).obj Y).right = F.obj Y
-- Mathlib.Topology.WithTopology
WithTopology.instMax : {X : Type u_1} → (t : TopologicalSpace X) → [Max X] → Max (WithTopology X t)
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a group if `β` is a group.  -/
FunLike.group : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Inv F] →
                [inst_5 : Div F] →
                  [inst_6 : Pow F ℤ] →
                    [inst_7 : Group β] →
                      [IsOneApply F α β] →
                        [IsMulApply F α β] →
                          [IsInvApply F α β] →
                            [IsDivApply F α β] → [IsPowApply ℕ F α β] → [IsPowApply ℤ F α β] → Group F
-- Mathlib.Algebra.Ring.Equiv
/-- Turn an element of a type `F` satisfying `RingEquivClass F α β` into an actual
`RingEquiv`. This is declared as the default coercion from `F` to `α ≃+* β`.  -/
RingEquivClass.toRingEquiv : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Mul α] →
        [inst_1 : Add α] →
          [inst_2 : Mul β] → [inst_3 : Add β] → [inst_4 : EquivLike F α β] → [RingEquivClass F α β] → F → α ≃+* β
-- Lean.Meta.Basic
Lean.Meta.instAlternativeMetaM : Alternative Lean.MetaM
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.lt_log_iff_exp_lt : ∀ {x y : ℝ}, 0 < y → (x < Real.log y ↔ Real.exp x < y)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.isScalarTower_monoidAlgebra : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_7} [inst : CommMonoid M] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] [inst_3 : Algebra R S] [inst_4 : CommSemiring T] [inst_5 : Algebra R T]
  [inst_6 : Algebra S T] [IsScalarTower R S T], IsScalarTower R (MonoidAlgebra S M) (MonoidAlgebra T M)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω)
  [inst_1 : TopologicalSpace Ω] (f : BoundedContinuousFunction Ω NNReal),
  μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isClosed_iff_of_notMem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
  OnePoint.infty ∉ s → (IsClosed s ↔ IsClosed (OnePoint.some ⁻¹' s) ∧ IsCompact (OnePoint.some ⁻¹' s))
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.fact_ramificationIdx_neZero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  NeZero (p.ramificationIdx' ↑P)
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizeUsingDefault : Lean.MVarId → Lean.Elab.TermElabM Bool
-- Std.Time.Format.Modifier
Std.Time.Modifier.V.sizeOf_spec : ∀ (presentation : Std.Time.ZoneId), sizeOf (Std.Time.Modifier.V presentation) = 1 + sizeOf presentation
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv.eq_2 : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.differentiableOn_log_log' : DifferentiableOn ℝ (fun x => Real.log (Real.log x)) {-1, 0, 1}ᶜ
-- Mathlib.Order.Category.Frm
Frm.ofHom_hom : ∀ {X Y : Frm} (f : X ⟶ Y), Frm.ofHom (Frm.Hom.hom f) = f
-- Mathlib.Logic.Equiv.Prod
Equiv.Perm.prodExtendRight_apply_eq : ∀ {α₁ : Type u_9} {β₁ : Type u_10} [inst : DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (b : β₁),
  (Equiv.Perm.prodExtendRight a e) (a, b) = (a, e b)
-- Init.Data.Function
/-- `RightInverse g f` means that `g` is a right inverse to `f`. That is, `f ∘ g = id`.  -/
Function.RightInverse : {α : Sort u_1} → {β : Sort u_2} → (β → α) → (α → β) → Prop
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.smul_sup : ∀ {R : Type u_1} {E : Type u_3} [inst : Group E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] (r : R) (p q : GroupSeminorm E), r • (p ⊔ q) = r • p ⊔ r • q
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_1 : Std.Roc.HasRcoIntersection ℕ
-- Mathlib.RingTheory.Multiplicity
pow_dvd_of_le_multiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, k ≤ multiplicity a b → a ^ k ∣ b
-- Mathlib.Algebra.Category.ModuleCat.Semi
_private.Mathlib.Algebra.Category.ModuleCat.Semi.0.SemimoduleCat.mk.inj : ∀ {R : Type u} {inst : Semiring R} {carrier : Type v} {isAddCommMonoid : AddCommMonoid carrier}
  {isModule : Module R carrier} {carrier_1 : Type v} {isAddCommMonoid_1 : AddCommMonoid carrier_1}
  {isModule_1 : Module R carrier_1},
  { carrier := carrier, isAddCommMonoid := isAddCommMonoid, isModule := isModule } =
      { carrier := carrier_1, isAddCommMonoid := isAddCommMonoid_1, isModule := isModule_1 } →
    carrier = carrier_1 ∧ isAddCommMonoid ≍ isAddCommMonoid_1 ∧ isModule ≍ isModule_1
-- Mathlib.Probability.Process.Predictable
/-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable.  -/
MeasureTheory.IsStronglyPredictable.measurable_add_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E}, MeasureTheory.IsStronglyPredictable 𝓕 u → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atTop_atTop : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} [inst_2 : Preorder β],
  Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ i, ∀ (a : α), i ≤ a → b ≤ f a
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_append_of_containsKey_right_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k l' = false →
    Std.Internal.List.eraseKey k (l ++ l') = Std.Internal.List.eraseKey k l ++ l'
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.iInf_mul_le_setLIntegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α},
  MeasurableSet s → (⨅ x ∈ s, f x) * μ s ≤ ∫⁻ (x : α) in s, f x ∂μ
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.isConj : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  σ.IsCycle → τ.IsCycle → σ.support.card = τ.support.card → IsConj σ τ
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasDerivAt.prodMk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {G : Type w} [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G},
  HasDerivAt f₁ f₁' x → HasDerivAt f₂ f₂' x → HasDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_Ioo_atBot : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X} {α : Type u_2}
  {l : Filter α} {f : α → ↑(Set.Ioo a b)},
  autoParam (Order.IsPredPrelimit a) tendsto_Ioo_atBot._auto_1 →
    (Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhdsWithin a (Set.Ioi a)))
-- Mathlib.Order.Category.HeytAlg
_private.Mathlib.Order.Category.HeytAlg.0.HeytAlg.Hom.mk.inj : ∀ {X Y : HeytAlg} {hom' hom'_1 : HeytingHom ↑X ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isTrail_rotate`. -/
SimpleGraph.Walk.IsTrail.rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  c.IsTrail → (c.rotate u hu).IsTrail
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], t.get! a = (t.get? a).get!
-- Mathlib.Order.OrderIsoNat
exists_covBy_seq_of_wellFoundedLT_wellFoundedGT : ∀ (α : Type u_2) [inst : Preorder α] [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α],
  ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesParams.mk.sizeOf_spec : ∀ (changes : Array Lean.Lsp.FileEvent), sizeOf { changes := changes } = 1 + sizeOf changes
-- Mathlib.Combinatorics.Enumerative.Composition
List.length_pos_of_mem_splitWrtComposition : ∀ {α : Type u_1} {l l' : List α} {c : Composition l.length}, l' ∈ l.splitWrtComposition c → 0 < l'.length
-- Mathlib.Order.WellFounded
/-- Let `r` be a well-founded relation on `α`, let `C : α → Prop`, and let `bot : α`.
This induction principle shows that `C bot` holds, given that
* some `a` satisfies `C a`, and
* for each `b` that satisfies `C b`, there is `c` satisfying `r c b` and `C c`.

The naming is inspired by the fact that when `r` is transitive, it follows that `bot` is
the smallest element w.r.t. `r` that satisfies `C`.  -/
WellFounded.induction_bot : ∀ {α : Sort u_4} {r : α → α → Prop},
  WellFounded r → ∀ {a bot : α} {C : α → Prop}, (∀ (b : α), b ≠ bot → C b → ∃ c, r c b ∧ C c) → C a → C bot
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_Iio_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Iio a)) (Filter.principal (Set.Iio a))
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.zero_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Zero (R i)] [inst_2 : ∀ (i : ι), ZeroMemClass (S i) (R i)] (i : ι), 0 i = 0
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.adaptationNote.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.StyleError.adaptationNote✝ = 1
-- Mathlib.Algebra.Quaternion
Quaternion.sq_eq_neg_normSq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R},
  a ^ 2 = -↑(Quaternion.normSq a) ↔ a.re = 0
-- Init.Data.UInt.Lemmas
UInt64.neg_eq_neg_one_mul : ∀ (a : UInt64), -a = -1 * a
-- Mathlib.Algebra.Group.Action.Defs
/-- Zero is a neutral element for `+ᵥ`  -/
AddAction.zero_vadd : ∀ {G : Type u_9} {P : Type u_10} {inst : AddMonoid G} [self : AddAction G P] (p : P), 0 +ᵥ p = p
-- Lean.Elab.Term.TermElabM
/-- Registers a deriving handler for the purpose of error message delivery in `synthesizeInstMVarCore`.
This should only be called by `Lean.Elab.Term.registerDerivingHandler`.
 -/
Lean.Elab.Term.registerDerivableClass : Lean.Name → IO Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂
-- Mathlib.Order.Monotone.Monovary
antivary_toDual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Antivary f (⇑OrderDual.toDual ∘ g) ↔ Monovary f g
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.instRing : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Generators R S ι) → Algebra P.Ring S
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.one : ∀ {M : Type u_1} [inst : MulOneClass M], IsIdempotentElem 1
-- Mathlib.LinearAlgebra.BilinearForm.Basic
/-- The flip of a bilinear form, obtained by exchanging the left and right arguments.  -/
LinearMap.BilinForm.flipHom : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M ≃ₗ[R] LinearMap.BilinForm R M
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_atTop_principal_Iio : ∀ {α : Type u_3} [inst : Preorder α] (x : α), Disjoint Filter.atTop (Filter.principal (Set.Iio x))
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instNatCast : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → NatCast (CentroidHom α)
-- Mathlib.Topology.MetricSpace.Dilation
/-- The `ratio` is equal to the distance ratio for any two points
with nonzero finite distance; `nndist` version  -/
Dilation.ratio_unique_of_nndist_ne_zero : ∀ {α : Type u_5} {β : Type u_6} {F : Type u_7} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
  nndist x y ≠ 0 → nndist (f x) (f y) = r * nndist x y → r = Dilation.ratio f
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The degree of a vertex in a subgraph. It's zero for vertices outside the subgraph.  -/
SimpleGraph.Subgraph.degree : {V : Type u} → {G : SimpleGraph V} → (G' : G.Subgraph) → (v : V) → [Fintype ↑(G'.neighborSet v)] → ℕ
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve inverse.

See note [hom simp lemma priority]  -/
map_inv : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
  [MonoidHomClass F G H] (f : F) (a : G), f a⁻¹ = (f a)⁻¹
-- Mathlib.Data.TypeVec
/-- arrow to remove one element of a `repeat` vector  -/
TypeVec.dropRepeat : (α : Type u_1) → {n : ℕ} → (TypeVec.repeat n.succ α).drop.Arrow (TypeVec.repeat n α)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Construct a continuous alternating map
from an alternating map satisfying a boundedness condition.  -/
AlternatingMap.mkContinuous : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] →
                  [inst_5 : Fintype ι] →
                    (f : E [⋀^ι]→ₗ[𝕜] F) → (C : ℝ) → (∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖) → E [⋀^ι]→L[𝕜] F