mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpToOn_univ_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p Set.univ ↔ HasFTaylorSeriesUpTo n f p
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.eventuallyEq_one : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], ↑f =ᶠ[nhds c] 1
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.minpoly_powerBasis_gen_of_monic : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f.Monic) (hf' : optParam (f ≠ 0) ⋯),
  minpoly K (AdjoinRoot.powerBasis hf').gen = f
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.add.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J RingCat}
  {a a_1 a_2 a_3 : RingCat.Colimits.Prequotient F}, a.add a_1 = a_2.add a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isSpanningSubgraph_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G ≤s ⊥ ↔ G = ⊥
-- Mathlib.Topology.Order.ProjIcc
continuous_IccExtend_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} {h : a ≤ b} [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] {f : ↑(Set.Icc a b) → β},
  Continuous (Set.IccExtend h f) ↔ Continuous f
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Ico_iff_Iio : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  a < b → (ContinuousWithinAt f (Set.Ico a b) b ↔ ContinuousWithinAt f (Set.Iio b) b)
-- Mathlib.Data.Finsupp.Basic
Finsupp.coe_sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ),
  ⇑(f.sumElim g) = Sum.elim ⇑f ⇑g
-- Mathlib.Order.Closure
/-- Predicate for an element to be closed.

By default, this is defined as `c.IsClosed x := (c x = x)` (see `isClosed_iff`).
We allow an override to fix definitional equalities.  -/
ClosureOperator.IsClosed : {α : Type u_1} → [inst : Preorder α] → ClosureOperator α → α → Prop
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.instInhabitedParamKind : Inhabited Lean.PrettyPrinter.Delaborator.ParamKind
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- A `MeasurableSpace` structure on the product of two measurable spaces.  -/
MeasurableSpace.prod : {α : Type u_6} → {β : Type u_7} → MeasurableSpace α → MeasurableSpace β → MeasurableSpace (α × β)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.isoMk_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Oplax.StrongTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Oplax.StrongTrans.isoMk app naturality).hom.as.app a = (app a).hom
-- Mathlib.RingTheory.Localization.Basic
/-- `IsLocalization.map` applied to a projection homomorphism from a product ring.  -/
Localization.mapPiEvalRingHom : {ι : Type u_1} →
  {R : ι → Type u_2} →
    [inst : (i : ι) → CommSemiring (R i)] →
      {i : ι} → (S : Submonoid (R i)) → Localization (Submonoid.comap (Pi.evalRingHom R i) S) →+* Localization S
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_iInf : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {ι : Sort u_1} [Nonempty ι] (f : K →+* L)
  (s : ι → Subfield K), Subfield.map f (iInf s) = ⨅ i, Subfield.map f (s i)
-- Mathlib.Analysis.Normed.Group.Real
Real.ofReal_le_enorm : ∀ (r : ℝ), ENNReal.ofReal r ≤ ‖r‖ₑ
-- Lean.Environment
/-- Returns debug output about the asynchronous state of the environment.  -/
Lean.Environment.dbgFormatAsyncState : Lean.Environment → BaseIO String
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- The submonoid of nonnegative elements.  -/
AddSubmonoid.nonneg : (M : Type u_1) → [inst : AddMonoid M] → [inst_1 : Preorder M] → [AddLeftMono M] → AddSubmonoid M
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesAt_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {c : F} {e : E},
  HasFPowerSeriesAt (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a_one_pow_n : ∀ {n : ℕ}, QuaternionGroup.a 1 ^ (2 * n) = 1
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Icc_left_eq_Icc_sub_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α},
  a - 1 ≤ b → insert (a - 1) (Set.Icc a b) = Set.Icc (a - 1) b
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_ne_zero : ∀ {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : Zero α] [NoZeroDivisors α] {a b : n → α},
  a ≠ 0 → b ≠ 0 → Matrix.vecMulVec a b ≠ 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_min?_eq_not_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.min?.isSome = !t.isEmpty
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `d ↦ d ⊙ᵣ c` as a functor.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight : {C : Type u_1} →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] → C → CategoryTheory.Functor D D
-- Mathlib.Data.Finset.Empty
/-- The property `s.Nonempty` expresses the fact that the finset `s` is not empty. It should be used
in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives access to a nice API thanks
to the dot notation.  -/
Finset.Nonempty : {α : Type u_1} → Finset α → Prop
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSeq.mk : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)},
  a ≤ o.cof.ord → StrictMono f → IsCofinal (Set.range f) → Ordinal.IsFundamentalSeq f
-- Std.Async.System
Std.Async.System.instReprOSInfo.repr : Std.Async.System.OSInfo → ℕ → Std.Format
-- Mathlib.GroupTheory.Congruence.Defs
Con.comap_comp : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (c : Con P) (g : N → P)
  (f : M → N) (hg : ∀ (x y : N), g (x * y) = g x * g y) (hf : ∀ (x y : M), f (x * y) = f x * f y),
  Con.comap (g ∘ f) ⋯ c = Con.comap f hf (Con.comap g hg c)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Multiset.recOn.congr_simp : ∀ {α : Type u_1} {C : Multiset α → Sort u_3} (m : Multiset α) (C_0 C_0_1 : C 0),
  C_0 = C_0_1 →
    ∀ (C_cons C_cons_1 : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) (e_C_cons : C_cons = C_cons_1)
      (C_cons_heq :
        ∀ (a a' : α) (m : Multiset α) (b : C m),
          C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)),
      m.recOn C_0 C_cons C_cons_heq = m.recOn C_0_1 C_cons_1 ⋯
-- Lean.Meta.MkIffOfInductiveProp
Lean.Meta.mkSumOfProducts : Lean.Name → Lean.MetaM Unit
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- If the target space is inhabited, so is the space of bounded continuous functions.  -/
BoundedContinuousFunction.instInhabited : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → [Inhabited β] → Inhabited (BoundedContinuousFunction α β)
-- Init.Data.SInt.Lemmas
Int8.toInt16_toInt64 : ∀ (n : Int8), n.toInt64.toInt16 = n.toInt16
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y} (hf : Φ.prop f), hf.arrowIso.hom.left = CategoryTheory.CategoryStruct.id X
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  Function.Injective fun x => (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj x
-- Mathlib.Topology.JacobsonSpace
instDiscreteTopologyOfFiniteOfJacobsonSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Finite X] [JacobsonSpace X], DiscreteTopology X
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.measurableSet_le : ∀ {α : Type u_1} {E : Type u_5} {m : MeasurableSpace α} {f g : α → E} [inst : TopologicalSpace E] [inst_1 : Preorder E]
  [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasurableSet {a | f a ≤ g a}
-- Mathlib.Algebra.Group.Basic
add_add_add_comm' : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c d : G), a + b + c + d = a + c + b + d
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Infinite-dimensional version of 7.64(b) in [axler2024].  -/
ContinuousLinearMap.ker_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (T : E →L[𝕜] F),
  (↑(ContinuousLinearMap.adjoint T ∘SL T)).ker = (↑T).ker
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankPosMap : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RankPos] {f : α → β} (hf : Set.InjOn f M.E), (M.map f hf).RankPos
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toBitVec = BitVec.ofNat 32 n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  m.WF → (Std.DHashMap.Raw.map f m).getKey? k = m.getKey? k
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.ComplexConfig.mk.sizeOf_spec : ∀ (out ctx : Type) (trigger : Option ctx → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx)
  (test : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx → Lean.MVarId → Lean.Elab.Command.CommandElabM out)
  (tell : Lean.Syntax → List Lean.MVarId → ℕ → out → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)),
  sizeOf { out := out, ctx := ctx, trigger := trigger, test := test, tell := tell } = 1 + sizeOf out + sizeOf ctx
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLoopAt.not_isNonloopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsLoopAt e x → ∀ (y : α), ¬G.IsNonloopAt e y
-- Mathlib.CategoryTheory.Limits.Unit
CategoryTheory.Limits.instHasLimitsOfSizeDiscretePUnit : CategoryTheory.Limits.HasLimitsOfSize.{v', v, u_1, u_1} (CategoryTheory.Discrete PUnit.{u_1 + 1})
-- Mathlib.Data.Nat.Nth
Nat.nth_add_eq_sub : ∀ {p : ℕ → Prop} {m n : ℕ}, (∀ k < m, ¬p k) → Nat.nth p n ≠ 0 → Nat.nth (fun i => p (i + m)) n = Nat.nth p n - m
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_neg : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Neg G] (a : G), ↑(-a) = -↑a
-- Mathlib.CategoryTheory.Pi.Basic
/-- The natural isomorphism between pulling back then evaluating, and just evaluating.  -/
CategoryTheory.Pi.comapEvalIsoEval : {I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₁} →
        (h : J → I) →
          (j : J) →
            (CategoryTheory.Pi.comap C h).comp (CategoryTheory.Pi.eval (C ∘ h) j) ≅ CategoryTheory.Pi.eval C (h j)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerRight.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] {X₁ X₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom X₂)
  (Y : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (f.whiskerRight Y) = 1 + sizeOf X₁ + sizeOf X₂ + sizeOf f + sizeOf Y
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLattice.toInfSet : {α : Type u_5} → [self : ConditionallyCompleteLattice α] → InfSet α
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.not_add : ∀ {w : ℕ} (a : BitVec w), ~~~a + a = -1#w
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionHom`, the bifunctorial action of morphisms in `C` and
`D` on `- ⊙ -`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊙ᵣₘ_» : Lean.TrailingParserDescr
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.toExpr.go : {α : Type u_1} → Lean.Expr → (α → Lean.Expr) → Lean.Expr → Lean.Expr → Lean.RArray α → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.mem_irrelevant_of_mem : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {x : A} {i : ι}, 0 < i → x ∈ 𝒜 i → x ∈ HomogeneousIdeal.irrelevant 𝒜
-- Mathlib.MeasureTheory.Constructions.Projective
/-- A family of measures indexed by finite sets of `ι` is projective if, for finite sets `J ⊆ I`,
the projection from `∀ i : I, α i` to `∀ i : J, α i` maps `P I` to `P J`.  -/
MeasureTheory.IsProjectiveMeasureFamily : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (α i)] → ((J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)) → Prop
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.extensionProductIter 0 = P
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toArray_eq_if_rco : ∀ {α : Type u} {r : Std.Rco α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLT α],
  r.toArray =
    if r.lower < r.upper then
      match Std.PRange.succ? r.lower with
      | none => #[r.lower]
      | some next => #[r.lower] ++ (next...r.upper).toArray
    else #[]
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.lift_fst_assoc : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z_1 : CompHausLike P}
  (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w)
      (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp a h
-- Init.Data.SInt.Lemmas
ISize.toUSize_le : ∀ {a b : ISize}, 0 ≤ a → a ≤ b → a.toUSize ≤ b.toUSize
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
hasFDerivAt_of_tendstoLocallyUniformlyOn : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G}
  {g' : E → E →L[𝕜] G} {x : E} [l.NeBot] {s : Set E},
  IsOpen s →
    TendstoLocallyUniformlyOn f' g' l s →
      (∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasFDerivAt g (g' x) x
-- Init.System.FilePath
System.instHashableFilePath : Hashable System.FilePath
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Adding a vector to a point in a subspace produces a point in the subspace if and only if the
vector is in the direction.  -/
AffineSubspace.vadd_mem_iff_mem_direction : ∀ {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 : AffineSubspace k P} (v : V) {p : P}, p ∈ s → (v +ᵥ p ∈ s ↔ v ∈ s.direction)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraMap_eq : ∀ {R : Type u_2} [inst : CommSemiring R], algebraMap R (PowerSeries R) = PowerSeries.C
-- Init.Prelude
Lean.Name.brecOn.go : {motive : Lean.Name → Sort u} →
  (t : Lean.Name) → ((t : Lean.Name) → Lean.Name.below t → motive t) → motive t ×' Lean.Name.below t
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- We have
`cyclotomic n R = (X ^ k - 1) /ₘ (∏ i ∈ Nat.properDivisors k, cyclotomic i K)`.  -/
Polynomial.cyclotomic_eq_X_pow_sub_one_div : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ},
  0 < n → Polynomial.cyclotomic n R = (Polynomial.X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i R
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_option_iff : ∀ (X : Type u) (κ : Cardinal.{w}), Cardinal.aleph0 ≤ κ → (HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ)
-- Mathlib.Data.EReal.Inv
EReal.strictAnti_div_right_of_neg : ∀ {b : EReal}, b < 0 → b ≠ ⊥ → StrictAnti fun a => a / b
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.mk.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (toSignature : Lean.Compiler.LCNF.Signature pu)
  (value : Lean.Compiler.LCNF.DeclValue pu) (recursive : Bool) (inlineAttr? : Option Lean.Compiler.InlineAttributeKind)
  (toSignature_1 : Lean.Compiler.LCNF.Signature pu) (value_1 : Lean.Compiler.LCNF.DeclValue pu) (recursive_1 : Bool)
  (inlineAttr?_1 : Option Lean.Compiler.InlineAttributeKind),
  ({ toSignature := toSignature, value := value, recursive := recursive, inlineAttr? := inlineAttr? } =
      { toSignature := toSignature_1, value := value_1, recursive := recursive_1, inlineAttr? := inlineAttr?_1 }) =
    (toSignature = toSignature_1 ∧ value = value_1 ∧ recursive = recursive_1 ∧ inlineAttr? = inlineAttr?_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom.eq_3 : ∀ (y₁_2 a y₂_2 : SimplexCategory) (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of y₁_2)
  (f₂_2 : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of y₂_2),
  AugmentedSimplexCategory.tensorHom x f₂_2 =
    CategoryTheory.CategoryStruct.comp f₂_2
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.mkHom (Fin.natAddOrderEmb (y₁_2.len + 1)).toOrderHom)
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.le_sup_toSubalgebra : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L), E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Error.eof.sizeOf_spec : sizeOf Std.Internal.Parsec.Error.eof = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonTypeDefinitionParams : Lean.FromJson Lean.Lsp.TypeDefinitionParams
-- Mathlib.Data.List.Lattice
List.bagInter_cons_of_not_mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} [inst : DecidableEq α] (l₂ : List α),
  a ∉ l₁ → l₁.bagInter (a :: l₂) = l₁.bagInter l₂
-- Mathlib.Data.Set.Image
Set.image_pair : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α), f '' {a, b} = {f a, f b}
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instSeparableSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.SeparableSpace α],
  TopologicalSpace.SeparableSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.equivQuotTensor_naturality_mk : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (x : M),
  (QuotSMulTop.equivQuotTensor r M') (((QuotSMulTop.map r) f) (Submodule.Quotient.mk x)) =
    (LinearMap.lTensor (R ⧸ Ideal.span {r}) f) ((QuotSMulTop.equivQuotTensor r M) (Submodule.Quotient.mk x))
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Last element of the composition  -/
CompositionAsSet.getLast_mem : ∀ {n : ℕ} (self : CompositionAsSet n), Fin.last n ∈ self.boundaries
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The functions whose Mellin transform we study  -/
WeakFEPair.g : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ → E
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.embDomain_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : PartialOrder Γ']
  (f : Γ ↪o Γ') (r : R) (x : HahnSeries Γ R), HahnSeries.embDomain f (r • x) = r • HahnSeries.embDomain f x
-- Lean.Meta.Tactic.Backtrack
Lean.Meta.Tactic.Backtrack.BacktrackConfig.mk : ℕ →
  (List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) →
    (Lean.MVarId → Lean.MetaM Bool) →
      (Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) → Bool → Lean.Meta.Tactic.Backtrack.BacktrackConfig
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (f g : PadicSeq p), (f * g).norm = f.norm * g.norm
-- Lean.Meta.ExprLens
/-- `view visit p e` runs `visit fvars s` where `s : Expr` is the subexpression of `e` at `p`.
and `fvars` are the free variables for the binders that `s` is under.
`s` is already instantiated with respect to these.
The role of the `visit` function is analogous to the `k` function in `Lean.Meta.forallTelescope`.  -/
Lean.Meta.viewSubexpr : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] →
        [Lean.MonadError M] → {α : Type} → (Array Lean.Expr → Lean.Expr → M α) → Lean.SubExpr.Pos → Lean.Expr → M α
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A version of `Matroid.IsCircuit.strong_multi_elimination` that is phrased using insertion.  -/
Matroid.IsCircuit.strong_multi_elimination_insert : ∀ {α : Type u_1} {M : Matroid α} {ι : Type u_2} {J : Set α} (x : ι → α) (I : ι → Set α) (z : α),
  (∀ (i : ι), x i ∉ I i) →
    (∀ (i : ι), M.IsCircuit (insert (x i) (I i))) →
      M.IsCircuit (J ∪ Set.range x) → z ∈ J → (∀ (i : ι), z ∉ I i) → ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- An injective object admits a trivial injective resolution: itself in degree 0.  -/
CategoryTheory.InjectiveResolution.self : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (Z : C) → [CategoryTheory.Injective Z] → CategoryTheory.InjectiveResolution Z
-- Batteries.Data.MLList.Basic
/-- A monadic lazy list, controlled by an arbitrary monad.  -/
MLList : (Type u → Type u) → Type u → Type u
-- Mathlib.Data.Nat.Init
Nat.leRec_eq_leRec : @Nat.leRec = @Nat.le.rec
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
inv_le_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), a⁻¹ ≤ |a|ₘ
-- Mathlib.Logic.Relation
Relation.TransGen.closed : ∀ {α : Type u_1} {r p : α → α → Prop}, r ≤ Relation.TransGen p → Relation.TransGen r ≤ Relation.TransGen p
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instIsMultiplicativeSchemeLocallyQuasiFinite : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.LocallyQuasiFinite