mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Parser
/-- A non-`meta` copy of `Lean.Doc.Syntax.metadataContents`.  -/
Lean.Doc.Parser.metadataContents : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vsub_midpoint_same_right : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ p₃ : P), midpoint R p₁ p₃ -ᵥ midpoint R p₂ p₃ = ⅟2 • (p₁ -ᵥ p₂)
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_castAdd : ∀ {n m : ℕ} (i : Fin n), (Fin.castAdd m i).castSucc = Fin.castAdd (m + 1) i
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  (i : Fin (n + 1)), s.excenterWeightsUnnorm signs i = (if i ∈ signs then -1 else 1) * (s.height i)⁻¹
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_val_assemble₃ : ∀ {w x y : UInt8} (c : Char),
  ByteArray.utf8DecodeChar?.assemble₃ w x y = some c →
    c.val.toBitVec =
      BitVec.setWidth 32 (BitVec.setWidth 4 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec ++ BitVec.setWidth 6 y.toBitVec)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable.  -/
VectorField.mlieBracket_zero_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {W : (x : M) → TangentSpace I x},
  VectorField.mlieBracket I 0 W = 0
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverEolWithAtErrPos : Array Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.le_map_apply_image : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → ∀ (s : Set α), μ s ≤ (MeasureTheory.Measure.map f μ) (f '' s)
-- Init.Data.Option.Lemmas
Option.guard_eq_none_iff : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Option.guard p a = none ↔ p a = false
-- Lean.Level
Lean.Level.isAlreadyNormalizedCheap : Lean.Level → Bool
-- Lean.Environment
/-- Mapping from constant name to module (index) where constant has been declared.
Recall that a Lean file has a header where previously compiled modules can be imported.
Each imported module has a unique `ModuleIdx`.
Many extensions use the `ModuleIdx` to efficiently retrieve information stored in imported modules.

Remark: this mapping also contains auxiliary constants, created by the code generator, that are **not** in
the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator.
Only the code generator uses them.
 -/
Lean.Kernel.Environment.const2ModIdx : Lean.Kernel.Environment → Std.HashMap Lean.Name Lean.ModuleIdx
-- Mathlib.Tactic.GRewrite.Core
/-- The metavariables that appear in the lemma. We do the slightly dodgy thing of
modifying their local context in order to be able to unify with bound variables.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.mvarIds : Mathlib.Tactic.GRewrite.GRewriteLemma✝ → Array (Lean.MVarId × Array Lean.LocalDecl)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.ExtTreeMap.ofList l cmp).getKey? k = none
-- Mathlib.Algebra.Quaternion
Quaternion.re_nnratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ≥0), (↑q).re = ↑q
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.evenKernel_functional_equation : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.evenKernel a x = 1 / x ^ (1 / 2) * HurwitzZeta.cosKernel a (1 / x)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.numCases : Lean.Meta.Grind.SplitCandidateWithAnchor → ℕ
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- A bijection on index sets.  -/
RootPairing.Hom.indexEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                {P : RootPairing ι R M N} → {Q : RootPairing ι₂ R M₂ N₂} → P.Hom Q → ι ≃ ι₂
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.group : {α : Type u} → [AddGroup α] → Group (Multiplicative α)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.exp_half : ∀ (x : ℝ), Real.exp (x / 2) = √(Real.exp x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
/-- The adjunction between the subdivision functor `sd` and `ex`.  -/
SSet.sdExAdjunction : SSet.sd ⊣ SSet.ex
-- Mathlib.Data.Set.Lattice
Set.iUnion_exists : ∀ {α : Type u_1} {ι : Sort u_5} {p : ι → Prop} {f : Exists p → Set α}, ⋃ (x : Exists p), f x = ⋃ i, ⋃ (h : p i), f ⋯
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- The integral closure of a subset in a field is the intersection of all valuation subrings
containing it.  -/
iInf_valuationSubring_superset : ∀ {K : Type u_3} [inst : Field K] {s : Set K},
  ⨅ V, (↑V).toSubring = (integralClosure (↥(Subring.closure s)) K).toSubring
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_filter_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {a : α}, a +ᵥ ⊥ = ⊥
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDerivWithin_clm_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {c : F} {s : Set E} {x : E}
  {N : WithTop ℕ∞} {n : ℕ},
  ContDiffWithinAt 𝕜 N f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s → ↑n ≤ N → ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- API for PushoutCocone.IsColimit.lift for `IsPushout`  -/
CategoryTheory.IsPushout.desc : {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} →
              CategoryTheory.IsPushout f g inl inr →
                {W : C} →
                  (h : X ⟶ W) →
                    (k : Y ⟶ W) →
                      CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k → (P ⟶ W)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.instInhabitedHom : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      (X : F.CoGrothendieck) → Inhabited (X.Hom X)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.leftInverse.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f f_1 : E →L[R] F} (e_f : f = f_1) (h : f.HasLeftInverse), h.leftInverse = ⋯.leftInverse
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroup_eq : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀),
  (MonoidWithZeroHom.ofClass Valued.v).valueGroup = (MonoidWithZeroHom.ofClass v).valueGroup
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.recF.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β),
  MvQPF.recF g = (MvQPF.P F).wRec fun a f' _f rec => g (MvQPF.abs ⟨a, TypeVec.splitFun f' rec⟩)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.bot_isCompleteMultipartite : ∀ {α : Type u}, ⊥.IsCompleteMultipartite
-- Mathlib.Lean.Expr.Basic
/-- Erase proofs in an expression by replacing them with `sorry`s.

This function replaces all proofs in the expression
and in the types that appear in the expression
by `sorryAx`s.
The resulting expression has the same type as the old one.

It is useful, e.g., to verify if the proof-irrelevant part of a definition depends on a variable.
 -/
Lean.Expr.eraseProofs : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.zeroCokernelCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.cokernel.zeroCokernelCofork f) = 0
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Core of the uniform structure of uniform convergence.  -/
UniformFun.uniformCore : (α : Type u_1) → (β : Type u_2) → [UniformSpace β] → UniformSpace.Core (UniformFun α β)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_inv_left`. -/
AntivaryOn.of_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f⁻¹ g s → MonovaryOn f g s
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.instIsTopologicalRing : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [IsTopologicalRing A] (s : NonUnitalSubalgebra R A), IsTopologicalRing ↥s
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.mk.inj : ∀ {α : Type} {promise : IO.Promise Bool} {waiter : Option (Std.Async.Waiter (Option α))} {promise_1 : IO.Promise Bool}
  {waiter_1 : Option (Std.Async.Waiter (Option α))},
  { promise := promise, waiter := waiter } = { promise := promise_1, waiter := waiter_1 } →
    promise = promise_1 ∧ waiter = waiter_1
-- Mathlib.RingTheory.Valuation.ExtendToLocalization
Valuation.extendToLocalization_apply_map_apply : ∀ {A : Type u_1} [inst : CommRing A] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ)
  {S : Submonoid A} (hS : S ≤ v.supp.primeCompl) (B : Type u_3) [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsLocalization S B] (a : A), (v.extendToLocalization hS B) ((algebraMap A B) a) = v a
-- Mathlib.Data.Setoid.Partition
Setoid.eqv_class_mem' : ∀ {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) {x : α}, {y | (Setoid.mkClasses c H) x y} ∈ c
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instAdditiveCoind₁Functor : ∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type v} [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G], (TopRep.coind₁Functor k G).Additive
-- Init.Data.Vector.Algebra
/-- Componentwise addition of vectors.  -/
Vector.add : {α : Type u_1} → {n : ℕ} → [Add α] → Vector α n → Vector α n → Vector α n
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mkOfAdjoinEqTop.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsDomain S] [inst_5 : Module.IsTorsionFree R S] [inst_6 : IsIntegrallyClosed R] {α : S}
  (hα : IsIntegral R α) (hα₂ : R[α] = ⊤), IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂ = IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂
-- Mathlib.RingTheory.NormalClosure
Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S] [PerfectField (FractionRing R)],
  Algebra.IsSeparable (FractionRing S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_two_mul : ∀ {z : ℂ}, Complex.tan (2 * z) = 2 * Complex.tan z / (1 - Complex.tan z ^ 2)
-- Mathlib.Algebra.Lie.Submodule
/-- The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules.  -/
LieSubmodule.incl : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → (N : LieSubmodule R L M) → ↥N →ₗ⁅R,L⁆ M
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernel_R : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤),
  (pres₂.cokernel data hg₁).R = (pres₂.R ⊕ ι)
-- Mathlib.MeasureTheory.PiSystem
generateFrom_piiUnionInter_measurableSet : ∀ {α : Type u_3} {ι : Type u_4} (m : ι → MeasurableSpace α) (S : Set ι),
  MeasurableSpace.generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i
-- Mathlib.Data.Nat.Totient
Nat.eq_or_eq_of_totient_eq_totient : ∀ {a b : ℕ}, a ∣ b → a.totient = b.totient → a = b ∨ 2 * a = b
-- Batteries.Data.List.Lemmas
List.countPBefore_cons : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ} {a : α},
  List.countPBefore p (a :: xs) i =
    if i = 0 then 0 else if p a = true then List.countPBefore p xs (i - 1) + 1 else List.countPBefore p xs (i - 1)
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.IsContPerfPair.continuous_uncurry : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst : CommRing R} {inst_1 : TopologicalSpace R}
  {inst_2 : AddCommGroup M} {inst_3 : Module R M} {inst_4 : TopologicalSpace M} {inst_5 : AddCommGroup N}
  {inst_6 : Module R N} {inst_7 : TopologicalSpace N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsContPerfPair],
  Continuous fun x =>
    match x with
    | (x, y) => (p x) y
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : DistribMulAction S A] [inst_6 : DistribMulAction S B] [inst_7 : DistribMulAction R A]
  [inst_8 : DistribMulAction R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B] (f : A →ₙₐ[S] B)
  (x : A), (NonUnitalAlgHom.restrictScalars R f) x = f x
-- Mathlib.Data.Fin.Tuple.Basic
Fin.init_def : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {q : (i : Fin (n + 1)) → α i}, (Fin.init fun k => q k) = fun k => q k.castSucc
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsShortNF.a₁ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsShortNF], W.a₁ = 0
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Zipper α β → Sort u_3) (k : α) (v : β k)
  (tree : Std.DTreeMap.Internal.Impl α β) (next : Std.DTreeMap.Internal.Zipper α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Zipper.done)
  (h_2 :
    (k : α) →
      (v : β k) →
        (tree : Std.DTreeMap.Internal.Impl α β) →
          (next : Std.DTreeMap.Internal.Zipper α β) → motive (Std.DTreeMap.Internal.Zipper.cons k v tree next)),
  (match Std.DTreeMap.Internal.Zipper.cons k v tree next with
    | Std.DTreeMap.Internal.Zipper.done => h_1 ()
    | Std.DTreeMap.Internal.Zipper.cons k v tree next => h_2 k v tree next) =
    h_2 k v tree next
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.IsIso.comp_right_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) [CategoryTheory.IsIso g], CategoryTheory.CategoryStruct.comp f g = 0 ↔ f = 0
-- Mathlib.Data.Stream.Init
Stream'.mem_of_mem_even : ∀ {α : Type u} (a : α) (s : Stream' α), a ∈ s.even → a ∈ s
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.inner_map_map_of_mem_unitary : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {u : H →L[𝕜] H}, u ∈ unitary (H →L[𝕜] H) → ∀ (x y : H), inner 𝕜 (u x) (u y) = inner 𝕜 x y
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.IsHashSelf.replicate : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ},
  Std.DHashMap.Internal.IsHashSelf (Array.replicate c Std.DHashMap.Internal.AssocList.nil)
-- Mathlib.CategoryTheory.Subterminal
/-- The (full sub)category of subterminal objects.
TODO: If `C` is the category of sheaves on a topological space `X`, this category is equivalent
to the lattice of open subsets of `X`. More generally, if `C` is a topos, this is the lattice of
"external truth values".
 -/
CategoryTheory.Subterminals : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type u₁
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Util.0.Lean.Grind.Linarith.Poly.pickVarToElim?.go : ℤ → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → ℤ × Lean.Grind.Linarith.Var
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_of_append_right : ∀ {V : Type u_1} {G : SimpleGraph V} {v w u : V} {p₁ : G.Walk v w} {p₂ : G.Walk w u} {p₃ : G.Walk v u},
  p₃ = p₁.append p₂ → p₂.IsSubwalk p₃
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
/-- The tensor product of two morphisms of presheaves of modules.  -/
PresheafOfModules.Monoidal.tensorHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      {M₁ M₂ M₃ M₄ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
        (M₁ ⟶ M₂) →
          (M₃ ⟶ M₄) → (PresheafOfModules.Monoidal.tensorObj M₁ M₃ ⟶ PresheafOfModules.Monoidal.tensorObj M₂ M₄)
-- Mathlib.Algebra.Algebra.Operations
Submodule.instCovariantClassHSMulLe_1 : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M],
  CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C}
  (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) h) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₂ c₁₂ i₁ i₂ i₁₂) h)
-- Lean.Meta.Sym.Canon
/-- Return type for the `shouldCanon` function.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult : Type
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H1Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 1)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H1Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.π h)
-- Init.Data.ByteArray.Basic
ByteArray.findFinIdx?.loop.eq_def : ∀ (a : ByteArray) (p : UInt8 → Bool) (i : ℕ),
  ByteArray.findFinIdx?.loop a p i =
    if h : i < a.size then if p a[i] = true then some ⟨i, h⟩ else ByteArray.findFinIdx?.loop a p (i + 1) else none
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.prodRight_symm_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (B : Type u_6)
  (C : Type u_7) [inst_7 : Semiring B] [inst_8 : Semiring C] [inst_9 : Algebra R B] [inst_10 : Algebra R C] (a : A)
  (b : B) (c : C), (Algebra.TensorProduct.prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c) = a ⊗ₜ[R] (b, c)
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Multipliable.eventually_bounded_finsetProd : ∀ {ι : Type u_1} {v : ι → ℝ}, Multipliable v → ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.spanCarrier.brecOn : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)}
  {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} {a : Projectivization K V}
  (t : Projectivization.Subspace.spanCarrier S a),
  (∀ (a : Projectivization K V) (t : Projectivization.Subspace.spanCarrier S a),
      Projectivization.Subspace.spanCarrier.below t → motive a t) →
    motive a t
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
surjective_of_nonzero_of_finrank_eq_one : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Type u_1}
  {A : Type u_2} [inst_3 : Semiring A] [inst_4 : Module A V] [inst_5 : AddCommGroup W] [inst_6 : Module K W]
  [inst_7 : Module A W] [LinearMap.CompatibleSMul V W K A],
  Module.finrank K W = 1 → ∀ {f : V →ₗ[A] W}, f ≠ 0 → Function.Surjective ⇑f
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.top_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊤.toSubsemiring = ⊤
-- Mathlib.CategoryTheory.CommSq
/-- A `LiftStruct` for a commutative square in the opposite category
gives a `LiftStruct` for the corresponding square in the original category.  -/
CategoryTheory.CommSq.LiftStruct.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : Cᵒᵖ} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → {sq : CategoryTheory.CommSq f i p g} → sq.LiftStruct → ⋯.LiftStruct
-- Mathlib.Algebra.Order.GroupWithZero.Basic
posMulReflectLE_iff_posMulReflectLT : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsLeftCancelMulZero α],
  PosMulReflectLE α ↔ PosMulReflectLT α