mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
/-- This property implies `IsRatCondKernelCDF`. The measurability, integrability and integral
conditions are the same, but the limit properties of `IsRatCondKernelCDF` are replaced by
limits of integrals.  -/
ProbabilityTheory.IsRatCondKernelCDFAux : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (α × β → ℚ → ℝ) → ProbabilityTheory.Kernel α (β × ℝ) → ProbabilityTheory.Kernel α β → Prop
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.range_self_comp_adjoint : ∀ {𝕜 : 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 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  (A ∘ₗ LinearMap.adjoint A).range = A.range
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g) g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_iso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).iso.hom = CategoryTheory.CategoryStruct.id S.homology
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mkOfCompact_zero : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  [inst_3 : CompactSpace α], BoundedContinuousFunction.mkOfCompact 0 = 0
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.kerEquivRange.congr_simp : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) [inst_7 : LieAlgebra.IsExtension i p],
  LieAlgebra.IsExtension.kerEquivRange i p = LieAlgebra.IsExtension.kerEquivRange i p
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instDecidableLtOrdinal : {x y : Std.Time.Hour.Ordinal} → Decidable (x < y)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : D ⥤ C`, this is `F.partialLeftAdjoint` on objects: it sends
`X : C` such that `F.leftAdjointObjIsDefined X` holds to an object of `D`
which represents the functor `F ⋙ coyoneda.obj (op X.obj)`.  -/
CategoryTheory.Functor.partialLeftAdjointObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor D C) → F.PartialLeftAdjointSource → D
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelUnopOp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.cokernelUnopOp g).hom =
    CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.ite.inj : ∀ {ref : Lean.Syntax} {h? : Option Lean.Elab.Term.Do.Var} {optIdent cond : Lean.Syntax}
  {thenBranch elseBranch : Lean.Elab.Term.Do.Code} {ref_1 : Lean.Syntax} {h?_1 : Option Lean.Elab.Term.Do.Var}
  {optIdent_1 cond_1 : Lean.Syntax} {thenBranch_1 elseBranch_1 : Lean.Elab.Term.Do.Code},
  Lean.Elab.Term.Do.Code.ite ref h? optIdent cond thenBranch elseBranch =
      Lean.Elab.Term.Do.Code.ite ref_1 h?_1 optIdent_1 cond_1 thenBranch_1 elseBranch_1 →
    ref = ref_1 ∧
      h? = h?_1 ∧ optIdent = optIdent_1 ∧ cond = cond_1 ∧ thenBranch = thenBranch_1 ∧ elseBranch = elseBranch_1
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_eq_zero_of_coheight_neq_one : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {z : ↥X},
  Order.coheight z ≠ 1 → ∀ (f : ↑X.functionField), AlgebraicGeometry.Scheme.ord f z = 0
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.comp_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {X_1 Y_1 Z : CategoryTheory.Factorisation f} (f_1 : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f_1 g).h = CategoryTheory.CategoryStruct.comp f_1.h g.h
-- Lean.Data.Lsp.Extra
/-- `$/lean/rpc/keepAlive` client->server notification.

The client must send an RPC notification every 10s in order to keep the RPC session alive.
This is the simplest one. On not seeing any notifications for three 10s periods, the server
will drop the RPC session and its associated references.  -/
Lean.Lsp.RpcKeepAliveParams : Type
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮),
  (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).Full
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.mem.decidable.match_1.splitter : {α : Type u_1} →
  (motive : Lists α → Lists' α true → Sort u_2) →
    (x : Lists α) →
      (x_1 : Lists' α true) →
        ((a : Lists α) → motive a Lists'.nil) →
          ((a : Lists α) → (b : Bool) → (b_1 : Lists' α b) → (l₂ : Lists' α true) → motive a (b_1.cons' l₂)) →
            motive x x_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition of being a pointwise left Kan extension at an object `Y` is
unchanged by replacing `Y` by an isomorphic object `Y'`.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso' : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                (E : L.LeftExtension F) →
                  {Y Y' : D} → (Y ≅ Y') → E.IsPointwiseLeftKanExtensionAt Y ≃ E.IsPointwiseLeftKanExtensionAt Y'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `true` if the cutsat state is inconsistent.  -/
Lean.Meta.Grind.Arith.Cutsat.inconsistent : Lean.Meta.Grind.GoalM Bool
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))),
  (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).s =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h.i
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.compLeftId_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f : D ⟶ D} (h : Homotopy f (CategoryTheory.CategoryStruct.id D))
  (g : C ⟶ D) (i j : ι), (h.compLeftId g).hom i j = CategoryTheory.CategoryStruct.comp (g.f i) (h.hom i j)
-- Plausible.Testable
/-- Test `q` by testing `p` and proving the equivalence between the two.  -/
Plausible.TestResult.iff : {p q : Prop} → (q ↔ p) → Plausible.TestResult p → Plausible.TestResult q
-- Mathlib.Analysis.Convex.Quasiconvex
QuasilinearOn.monotoneOn_or_antitoneOn : ∀ {𝕜 : Type u_1} {β : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜}
  {f : 𝕜 → β} [inst_3 : LinearOrder β], QuasilinearOn 𝕜 s f → MonotoneOn f s ∨ AntitoneOn f s
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiableWithinAt_const_add_iff`. -/
DifferentiableWithinAt.const_add : ∀ {𝕜 : 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}
  {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun y => c + f y) s x
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (completionInfoPos : ℕ),
  sizeOf { uri := uri, pos := pos, completionInfoPos := completionInfoPos } =
    1 + sizeOf uri + sizeOf pos + sizeOf completionInfoPos
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.prodCongr_symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6}
  [inst_2 : TopologicalSpace X'] [inst_3 : TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y'),
  (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
-- Mathlib.Tactic.GCongr.ForwardAttr
_private.Mathlib.Tactic.GCongr.ForwardAttr.0.Mathlib.Tactic.GCongr.mkForwardExt.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Tactic.GCongr.ForwardExt
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.disjoint_edges_of_disjoint_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u},
  p.IsPath → p.support.tail.Disjoint q.support.tail → p.length ≠ 1 → p.edges.Disjoint q.edges
-- Mathlib.Algebra.Group.Commute.Defs
/-- Equality behind `AddCommute a b`; useful for rewriting.  -/
AddCommute.eq : ∀ {S : Type u_3} [inst : Add S] {a b : S}, AddCommute a b → a + b = b + a
-- Mathlib.CategoryTheory.Whiskering
/-- Auxiliary definition for `whiskeringLeft₃`.  -/
CategoryTheory.Functor.whiskeringLeft₃Map : {C₁ : Type u_1} →
  (C₂ : Type u_2) →
    (C₃ : Type u_3) →
      {D₁ : Type u_4} →
        (D₂ : Type u_5) →
          (D₃ : Type u_6) →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            {F₁ F₁' : CategoryTheory.Functor C₁ D₁} →
                              (F₁ ⟶ F₁') →
                                (CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁ ⟶
                                  CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁')
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFoldr_eq_foldr : ∀ {α : Type u_3} {β : Type u_4} (f : α → β → β) (s : Multiset α) [h : LeftCommutative f] (b : β),
  Multiset.noncommFoldr f s ⋯ b = Multiset.foldr f b s
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- If `f.eval x = f.val y`, then for any `z` in the domain, `x - z` can't be closer than `x - y`
in terms of Archimedean classes.  -/
HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} {y : ↥(↑f).domain},
  f.eval x = ↑↑f y → ∀ (z : ↥(↑f).domain), ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (x - ↑y)
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The ring topology on `PowerSeries` of a topological ring  -/
PowerSeries.WithPiTopology.instIsTopologicalRing : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R], IsTopologicalRing (PowerSeries R)
-- Std.Do.SPred.DerivedLaws
/-- A proof that `spred(P ∧ Q)` is logically equivalent to `PQ`. -/
Std.Do.SPred.Tactic.SimpAnd.simp_and : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs} {PQ : outParam (Std.Do.SPred σs)}
  [self : Std.Do.SPred.Tactic.SimpAnd P Q PQ], P ∧ Q ⊣⊢ₛ PQ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe.injEq : ∀ (c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Lean.DocString.Types
Lean.Doc.instOrdPart : {i : Type u_1} → {b : Type u_2} → {p : Type u_3} → [Ord i] → [Ord b] → [Ord p] → Ord (Lean.Doc.Part i b p)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- Bound for `|log x * x|` in the interval `(0, 1]`.  -/
Real.abs_log_mul_self_lt : ∀ (x : ℝ), 0 < x → x ≤ 1 → |Real.log x * x| < 1
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
Equiv.divRight₀.congr_simp : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a a_1 : G₀) (e_a : a = a_1) (ha : a ≠ 0),
  Equiv.divRight₀ a ha = Equiv.divRight₀ a_1 ⋯
-- Mathlib.FieldTheory.Normal.Defs
AlgHom.restrictNormal.congr_simp : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (ϕ ϕ_1 : K₁ →ₐ[F] K₂),
  ϕ = ϕ_1 →
    ∀ (E : Type u_6) [inst_5 : Field E] [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂]
      [inst_9 : IsScalarTower F E K₁] [inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E],
      ϕ.restrictNormal E = ϕ_1.restrictNormal E
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalHom.toLinearMap : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            {V : Type u_2} →
              [inst_4 : AddCommGroup V] →
                [inst_5 : WittVector.Isocrystal p k V] →
                  {V₂ : Type u_3} →
                    [inst_6 : AddCommGroup V₂] →
                      [inst_7 : WittVector.Isocrystal p k V₂] →
                        WittVector.IsocrystalHom p k V V₂ → V →ₗ[FractionRing (WittVector p k)] V₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.forIn'_eq_match : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_6 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    match hs : Std.PRange.succ? r.lower with
    | none => pure init
    | some next =>
      have hlt := ⋯;
      have hle := ⋯;
      do
      let __do_lift ← f next hlt init
      match __do_lift with
        | ForInStep.yield c => forIn' next<...* c fun a ha acc => f a ⋯ acc
        | ForInStep.done c => pure c
-- Mathlib.Control.Fold
Traversable.foldlm.eq_1 : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] {m : Type u → Type u} [inst_1 : Monad m] (f : α → β → m α)
  (x : α) (xs : t β), Traversable.foldlm f x xs = (Traversable.foldMap (Monoid.foldlM.mk ∘ flip f) xs).get x
-- Mathlib.Data.Quot
/-- A version of `Quotient.liftOn` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument.  -/
Quotient.liftOn' : {α : Sort u_1} → {φ : Sort u_4} → {s₁ : Setoid α} → Quotient s₁ → (f : α → φ) → (∀ (a b : α), s₁ a b → f a = f b) → φ
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its line derivative at `x₀` in the direction `v` has norm
bounded by `C * ‖v‖`. This version only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a
neighborhood of `x`.
Version using `lineDeriv`.  -/
norm_lineDeriv_le_of_lip' : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {v : E}
  {f : E → F} {x₀ : E} {C : ℝ},
  0 ≤ C → (∀ᶠ (x : E) in nhds x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) → ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖
-- Std.Sat.CNF.RelabelFin
_private.Std.Sat.CNF.RelabelFin.0.Std.Sat.CNF.numLiterals.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → (Unit → motive none) → ((n : ℕ) → motive (some n)) → motive x
-- Mathlib.Algebra.Algebra.Rat
DivisionSemiring.toNNRatAlgebra : {R : Type u_2} → [inst : DivisionSemiring R] → [CharZero R] → Algebra ℚ≥0 R
-- Mathlib.GroupTheory.OreLocalization.Cardinality
AddOreLocalization.cardinalMk_le : ∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S],
  Cardinal.mk (AddOreLocalization S R) ≤ Cardinal.mk R
-- Mathlib.Tactic.Module
/-- Augment a `Module.NF R M` object `l`, i.e. a list of pairs in `R × M`, by prepending another
pair `p : R × M`.  -/
Mathlib.Tactic.Module.NF.«term_::ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Bialgebra.Basic
/-- `counitAlgHom R A` is the counit of the `R`-bialgebra `A`, as an `R`-algebra map.  -/
Bialgebra.counitAlgHom : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → A →ₐ[R] R
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], addCommutator G = ⁅⊤, ⊤⁆
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instHashableKey : Hashable Lean.Meta.DiscrTree.Key
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.α.eq_1 : ∀ {q : ℕ}, LucasLehmer.X.α = (0, 1)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sum_univ_of : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (x : DirectSum ι fun i => β i), ∑ i, (DirectSum.of β i) (x i) = x
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.gid : Std.Internal.UV.System.GroupInfo → UInt64
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.darts_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.darts = []
-- Mathlib.Data.Setoid.Basic
/-- A bijection between an indexed product of quotients and the quotient by the product of the
equivalence relations.  -/
Setoid.piQuotientEquiv : {ι : Sort u_4} → {α : ι → Sort u_5} → (r : (i : ι) → Setoid (α i)) → ((i : ι) → Quotient (r i)) ≃ Quotient piSetoid
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.completeSpace : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)]
  [∀ (a : α), CompleteSpace (E a)], CompleteSpace ↥(lp E p)
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_iff_commutator_lt`. -/
isSolvable_iff_commutator_lt : ∀ {G : Type u_1} [inst : Group G] [WellFoundedLT (Subgroup G)],
  Group.IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
-- Mathlib.Data.List.Sigma
List.dlookup_kinsert_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b' : β a'} {l : List (Sigma β)},
  a ≠ a' → List.dlookup a (List.kinsert a' b' l) = List.dlookup a l
-- Mathlib.Data.Prod.Basic
Prod.total_left : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Total r], Std.Total (Prod.Lex r s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isSome_maxKey?_modifyKey_eq_isSome : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β}
  {l : List ((_ : α) × β)},
  (Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = (Std.Internal.List.maxKey? l).isSome
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.contains (t.minD fallback) = true
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept_add_coe : ∀ (L : PeriodPair) (l₀ z : ℂ) (l : ↥L.lattice),
  L.derivWeierstrassPExcept l₀ (z + ↑l) = L.derivWeierstrassPExcept (l₀ - ↑l) z
-- Mathlib.RingTheory.Extension.Generators
/-- An `R[X]`-algebra instance on `S`. The default is the one induced by the map `R[X] → S`,
but this causes a diamond if there is an existing instance.  -/
Algebra.Generators.algebra : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S ι → Algebra (MvPolynomial ι R) S
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_iInf : ∀ {V : Type u} {ι : Sort u_2} [Nonempty ι] {f : ι → SimpleGraph V}, (⨅ i, f i).edgeSet = ⋂ i, (f i).edgeSet
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.memP_iff_find? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t → (RBTree.RBNode.MemP cut t ↔ ∃ x, RBTree.RBNode.find? cut t = some x)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.adjoin_simple_map_algEquiv : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (f : Gal(K/k)) (x : K), FiniteGaloisIntermediateField.adjoin k {f x} = FiniteGaloisIntermediateField.adjoin k {x}
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
/-- The maximal ideal of a discrete valuation ring.  -/
IsDiscreteValuationRing.maximalIdeal : (A : Type u_1) →
  [inst : CommRing A] → [inst_1 : IsDomain A] → [IsDiscreteValuationRing A] → IsDedekindDomain.HeightOneSpectrum A
-- Mathlib.Analysis.MeanInequalities
/-- **Alias** of `Real.inner_le_Lp_mul_Lq_of_nonneg`.

---

**Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with real-valued nonnegative functions.  -/
Real.inner_le_Lp_mul_Lq_of_nonneg' : ∀ {ι : Type u} (s : Finset ι) {f g : ι → ℝ} {p q : ℝ},
  p.HolderConjugate q →
    (∀ i ∈ s, 0 ≤ f i) →
      (∀ i ∈ s, 0 ≤ g i) → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Mathlib.Order.Defs.LinearOrder
cmp_eq_compareOfLessAndEq : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), cmp a b = compareOfLessAndEq a b
-- Mathlib.Order.Ideal
Order.Ideal.IsProper.mk : ∀ {P : Type u_1} [inst : LE P] {I : Order.Ideal P}, ↑I ≠ Set.univ → I.IsProper
-- Mathlib.Data.EReal.Basic
instCompleteLinearOrderEReal : CompleteLinearOrder EReal
-- Lean.ResolveName
Lean.MonadResolveName.getCurrNamespace : {m : Type → Type} → [self : Lean.MonadResolveName m] → m Lean.Name
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_add_transpose_self : ∀ {α : Type u_1} {n : Type u_3} [inst : AddCommSemigroup α] (A : Matrix n n α), (A + A.transpose).IsSymm
-- Mathlib.Topology.Bases
/-- There exists a countable set of sets that generates the topology.  -/
SecondCountableTopology.is_open_generated_countable : ∀ {α : Type u} {t : TopologicalSpace α} [self : SecondCountableTopology α],
  ∃ b, b.Countable ∧ t = TopologicalSpace.generateFrom b
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instInfOpenSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instInfOpenSubgroup = { min := fun U V => { toSubgroup := ↑U ⊓ ↑V, isOpen' := ⋯ } }