mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (x x_1 : G ⟶ H) (Γ : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.whiskerLeft η Γ).as.app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_coeff_degree_ne : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {i : ℕ},
  p.degree ≠ ↑i → p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedUnameInfo : Inhabited Std.Internal.UV.System.UnameInfo
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.cauchy : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} (f : CauSeq β abv) {ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, abv (↑f j - ↑f i) < ε
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α},
  k ∈ m → m.getKey? k = some k
-- Lean.Server.References
/-- Result of `filterMapIdent`.  -/
Lean.Server.References.MatchedDefinition.ident : {α : Type} → Lean.Server.References.MatchedDefinition α → α
-- Lean.Elab.Util
Lean.Elab.throwErrorWithNestedErrors : {m : Type → Type} →
  {α : Type} → [Lean.MonadError m] → [Monad m] → [Lean.MonadLog m] → Lean.MessageData → Array Lean.Exception → m α
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategory} (i : Δ' ⟶ Δ)
  [inst_3 : CategoryTheory.Mono i] {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj (Opposite.op Δ') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ)))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map i.op) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
      (CategoryTheory.CategoryStruct.comp
        (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj
          (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ')))
        h)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.compClosure_eq_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C)
  [CategoryTheory.HomRel.IsStableUnderPrecomp r] [CategoryTheory.HomRel.IsStableUnderPostcomp r],
  CategoryTheory.HomRel.CompClosure r = r
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonWorkDoneProgressOptions : Lean.FromJson Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_le_limsSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f g : Filter α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) Filter.limsSup_le_limsSup._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) g) Filter.limsSup_le_limsSup._auto_3 →
      (∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → ∀ᶠ (n : α) in f, n ≤ a) → f.limsSup ≤ g.limsSup
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (A : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf adj).obj A).str = (adj.homEquiv A.a A.a) A.str
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyze : Lean.Options → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.trans_sub : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f g : β → α}, Summable g L → Summable (fun b => f b - g b) L → Summable f L
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.modify.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering) (f : α → α) (t : RBTree.RBNode α),
  RBTree.RBNode.modify cut f t =
    match RBTree.RBNode.zoom cut t with
    | (RBTree.RBNode.nil, snd) => t
    | (RBTree.RBNode.node c a x b, path) => path.fill (RBTree.RBNode.node c a (f x) b)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.instInhabited : {L : FirstOrder.Language} → Inhabited (L ≃ᴸ L)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The `R₁`-algebra structure on `A/I` for an `R₁`-algebra `A`  -/
Ideal.Quotient.algebra : (R₁ : Type u_1) →
  {A : Type u_3} →
    [inst : CommSemiring R₁] →
      [inst_1 : Ring A] → [Algebra R₁ A] → {I : Ideal A} → [inst_3 : I.IsTwoSided] → Algebra R₁ (A ⧸ I)
-- Init.Data.Int.Order
Int.add_pos_of_nonneg_of_pos : ∀ {a b : ℤ}, 0 ≤ a → 0 < b → 0 < a + b
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A version of `Filter.eventually_prod_iff` where the first filter consists of neighborhoods
in a pseudo-metric space.  -/
Metric.eventually_nhds_prod_iff : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : α × ι → Prop},
  (∀ᶠ (x : α × ι) in nhds x₀ ×ˢ f, p x) ↔
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)
-- Mathlib.Algebra.Group.Defs
/-- A `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) -/
Group : Type u → Type u
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.lift_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  (X : CategoryTheory.Mat_ C), (CategoryTheory.Mat_.lift F).obj X = ⨁ fun i => F.obj (X.X i)
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans : ∀ (K : Type u_4) {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {κ : Type w} (E : Type z)
  [inst_3 : Field E] [inst_4 : Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L)
  [inst_8 : Fintype κ] (e : κ ≃ (L →ₐ[K] E)),
  (Algebra.traceMatrix K b).map ⇑(algebraMap K E) =
    Algebra.embeddingsMatrixReindex K E b e * (Algebra.embeddingsMatrixReindex K E b e).transpose
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α → β)
  (h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y), ⇑{ toFun := f, edist_eq' := h } = f
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoalParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.faithful_preadditiveCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.preadditiveCoyoneda.Faithful
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instIsTopologicalAddGroup : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommRing 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : IsTopologicalAddGroup 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  IsTopologicalAddGroup (WeakDual 𝕜 E)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.apply_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂), e (e.symm x) = x
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_compl_comm : ∀ {α : Type u_1} {s t : Set α}, s ⊆ tᶜ ↔ t ⊆ sᶜ
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftAdjointMate.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y),
  (ᘁf) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ᘁY).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ (ᘁX) X) ᘁY)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁX) f)
            ᘁY)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (ᘁX) Y ᘁY).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁX) (ε_ (ᘁY) Y))
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor ᘁX).hom))))
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the sum of two formal power series
is the minimum of their orders if their orders differ.  -/
MvPowerSeries.order_add_of_order_ne : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R},
  f.order ≠ g.order → (f + g).order = min f.order g.order
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_units_zsmul : ∀ {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.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℤˣ), (n • α).app X = n • α.app X
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- If `x ≠ y` belong to the same closed ball, then a convex combination of `x` and `y` with
positive coefficients belongs to the corresponding open ball.  -/
combo_mem_ball_of_ne : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y z : E}
  {a b r : ℝ},
  x ∈ Metric.closedBall z r →
    y ∈ Metric.closedBall z r → x ≠ y → 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ Metric.ball z r
-- Mathlib.Data.Nat.Log
Nat.log_lt_self : ∀ (b : ℕ) {x : ℕ}, x ≠ 0 → Nat.log b x < x
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_inc : ∀ {p : String.Pos.Raw}, p.inc.byteIdx = p.byteIdx + 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
/-- Replace the coefficient of an element `f` of a skew monoid algebra at a given point `a : α` by
a given value `b : M`.
If `b = 0`, this amounts to removing `a` from the support of `f`.
Otherwise, if `a` was not in the `support` of `f`, it is added to it.  -/
SkewMonoidAlgebra.update : {M : Type u_4} → {α : Type u_5} → [inst : AddCommMonoid M] → SkewMonoidAlgebra M α → α → M → SkewMonoidAlgebra M α
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.isPretransitive_of_isMultiplyPretransitive' : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  AddAction.IsMultiplyPretransitive G α n → AddAction.IsPretransitive G ↑(Set.powersetCard α n)
-- Mathlib.Data.FinEnum
List.Pi.finEnum : {α : Type u_1} → [FinEnum α] → {β : α → Type u_2} → [(a : α) → FinEnum (β a)] → FinEnum ((a : α) → β a)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} (hτ : MeasureTheory.IsStoppingTime ℱ τ) (i : ι)
  [MeasureTheory.SigmaFinite (μ.trim ⋯)],
  μ[f | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ ↑i}] μ[f | hτ.measurableSpace]
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.CategoryTheory.GlueData
/-- The inclusion maps of the intersection into the object.  -/
CategoryTheory.GlueData'.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (self : CategoryTheory.GlueData' C) → (i j : self.J) → (h : i ≠ j) → self.V i j h ⟶ self.U i
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go.eq_2 : ∀ (c : Char) (cs : List Char), String.utf8ByteSize'.go✝ (c :: cs) = String.utf8ByteSize'.go✝ cs + c.utf8Size
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittMul.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → WittVector.wittMul p a = WittVector.wittMul p_1 a_1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {X : C} (Z : ι → C) (f : (i : ι) → Z i ⟶ X)
  (R : (i : ι) → CategoryTheory.Presieve (Z i)),
  (CategoryTheory.Sieve.bind (CategoryTheory.Sieve.ofArrows Z f).arrows fun x x_1 hg =>
      CategoryTheory.Sieve.pullback (CategoryTheory.Sieve.ofArrows.h hg)
        (CategoryTheory.Sieve.generate (R (CategoryTheory.Sieve.ofArrows.i hg)))) ≤
    CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows Z f R)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.type : Lean.Elab.Command.PreElabHeaderResult → Lean.Expr
-- Std.Http.Data.URI.Basic
/-- Replaces all path segments. Segments will be automatically percent-encoded when building.
 -/
Std.Http.URI.Builder.setPath : Std.Http.URI.Builder → Array String → Std.Http.URI.Builder
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRevM f init ↑m = Array.foldrM (fun a b => f b a.fst a.snd) init (↑m).toArray
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rco_eq_mkSlice_rco_min : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Rco.Sliceable.mkSlice xs lo...hi) = Std.Rco.Sliceable.mkSlice xs (min lo (min hi xs.size))...min hi xs.size
-- Mathlib.Algebra.Group.End
/-- The monoid of endomorphisms.

Note that this is generalized by `CategoryTheory.End` to categories other than `Type u`.  -/
Function.End : Type u_4 → Type u_4
-- Init.Data.Array.Basic
/-- Folds a monadic function over a list from the left, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in order, using `f`.

The optional parameters `start` and `stop` control the region of the array to be folded. Folding
proceeds from `start` (inclusive) to `stop` (exclusive), so no folding occurs unless `start < stop`.
By default, the entire array is folded.

Examples:
```lean example
example [Monad m] (f : α → β → m α) :
    Array.foldlM (m := m) f x₀ #[a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure x₃)
  := by rfl
```

```lean example
example [Monad m] (f : α → β → m α) :
    Array.foldlM (m := m) f x₀ #[a, b, c] (start := 1) = (do
      let x₁ ← f x₀ b
      let x₂ ← f x₁ c
      pure x₂)
  := by rfl
```
 -/
Array.foldlM : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (β → α → m β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m β
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_neg_nat : ∀ (S : Type u_3) [inst : NonAssocRing S] [inst_1 : Pow S ℕ] [NatPowAssoc S] (q : Polynomial ℕ) (n : ℕ),
  q.smeval (-↑n) = ↑(q.smeval (-↑n))
-- Mathlib.Topology.Algebra.Group.Basic
nhds_translation_sub : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (x : G),
  Filter.comap (fun x_1 => x_1 - x) (nhds 0) = nhds x
-- Mathlib.LinearAlgebra.Dimension.Localization
IsLocalization.finrank_eq : ∀ {R : Type uR} (S : Type uS) {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] [inst_4 : Algebra R S] [inst_5 : Module S N] [IsScalarTower R S N] (p : Submonoid R)
  [IsLocalization p S], p ≤ nonZeroDivisors R → Module.finrank S N = Module.finrank R N
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.div : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [inst_2 : (i : ι) → Div (β i)]
  [∀ (i : ι), MeasurableDiv₂ (β i)],
  MeasureTheory.Adapted f u → MeasureTheory.Adapted f v → MeasureTheory.Adapted f (u / v)
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n →
    (UInt32.ofNatClamp n).toUInt64 = UInt64.ofNatLT (UInt32.size - 1) UInt32.toUInt64_ofNatClamp_of_le._proof_1
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (f : CategoryTheory.Arrow C) {X Y : SimplexCategoryᵒᵖ} (g : X ⟶ Y),
  (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.map g =
    CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom)
      (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.instIsSemitopologicalSemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [IsSemitopologicalSemiring A] (s : NonUnitalSubalgebra R A), IsSemitopologicalSemiring ↥s
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.single_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_22}
  [inst_3 : DecidableEq ι] {M : ι → Type u_23} [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι),
  Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l l'' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.Tree α β (l.size + l''.size) → Sort u_3) (ℓ : Std.DTreeMap.Internal.Impl α β)
  (hℓ₁ : ℓ.Balanced) (hℓ₂ : ℓ.size = l.size + l''.size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = l.size + l''.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Algebra.Quaternion
Quaternion.imI_neg : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (-a).imI = -a.imI
-- Lean.Parser.Basic
Lean.Parser.identFn : Lean.Parser.ParserFn
-- Mathlib.Topology.UniformSpace.Defs
/-- A uniform space is a generalization of the "uniform" topological aspects of a
metric space. It consists of a filter on `α × α` called the "uniformity", which
satisfies properties analogous to the reflexivity, symmetry, and triangle properties
of a metric.

A metric space has a natural uniformity, and a uniform space has a natural topology.
A topological group also has a natural uniformity, even when it is not metrizable.  -/
UniformSpace : Type u → Type u
-- Init.Prelude
instMonadStateOfOfMonadLift : {σ : Type u} → {m : Type u → Type v} → {n : Type u → Type w} → [MonadLift m n] → [MonadStateOf σ m] → MonadStateOf σ n
-- Mathlib.Data.List.Basic
List.append_eq_has_append : ∀ {α : Type u} {L₁ L₂ : List α}, L₁.append L₂ = L₁ ++ L₂
-- Mathlib.Data.Set.Lattice
Set.iInter_exists : ∀ {α : Type u_1} {ι : Sort u_5} {p : ι → Prop} {f : Exists p → Set α}, ⋂ (x : Exists p), f x = ⋂ i, ⋂ (h : p i), f ⋯
-- Mathlib.Geometry.Polygon.Basic
/-- Convert a polygon with 3 nondegenerate vertices to an `Affine.Triangle`.  -/
Polygon.toTriangle : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module R V] →
            [inst_3 : AddTorsor V P] → (p : Polygon P 3) → Polygon.HasNondegenerateVertices R p → Affine.Triangle R P
-- Init.Data.Range.Polymorphic.UInt
UInt64.instHasSize_1 : Std.Rxo.HasSize UInt64
-- Init.Data.Vector.Lemmas
Vector.findSomeRev?.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → Option β) (as : Vector α n),
  Vector.findSomeRev? f as = Array.findSomeRev? f as.toArray
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.exists_companion : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N),
  ∃ B, ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
-- Mathlib.Order.Sublattice
Sublattice.prodEquiv_toEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice α) (M : Sublattice β),
  (L.prodEquiv M).toEquiv = Equiv.Set.prod ↑L ↑M
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.SimpTheorems.addSimpTheorem.updateLemmaNames : Lean.Meta.SimpTheorem → Lean.PHashSet Lean.Meta.Origin → Lean.PHashSet Lean.Meta.Origin
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of a maximal ideal as an element of `ℝ≥0` is `> 1`  -/
NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], 1 < ↑(Ideal.absNorm v.asIdeal)
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.mk.inj : ∀ {wp x y zp ap bp wp_1 x_1 y_1 zp_1 ap_1 bp_1 : ℕ},
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      { wp := wp_1, x := x_1, y := y_1, zp := zp_1, ap := ap_1, bp := bp_1 } →
    wp = wp_1 ∧ x = x_1 ∧ y = y_1 ∧ zp = zp_1 ∧ ap = ap_1 ∧ bp = bp_1
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.mk_left : ∀ {S : AlgebraicGeometry.Scheme} {R : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ S)
  [inst : AlgebraicGeometry.Etale f], (AlgebraicGeometry.Scheme.AffineEtale.mk f).left = Opposite.op R
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.sum : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace H] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : TopologicalSpace M'] → [cm : ChartedSpace H M] → [cm' : ChartedSpace H M'] → ChartedSpace H (M ⊕ M')
-- Mathlib.Algebra.AddConstMap.Basic
/-- The underlying function of an `AddConstMap`.
Use automatic coercion to function instead.  -/
AddConstMap.toFun : {G : Type u_1} → {H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → AddConstMap G H a b → G → H
-- Batteries.Tactic.Lint.Simp
/-- Returns the list of elements in the discrimination tree.  -/
Lean.Meta.DiscrTree.elements : {α : Type} → Lean.Meta.DiscrTree α → Array α
-- Lean.Elab.Tactic.Doc
/-- Any docstring extensions that have been specified  -/
Lean.Elab.Tactic.Doc.TacticDoc.extensionDocs : Lean.Elab.Tactic.Doc.TacticDoc → Array String