mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Flow
Flow.ext : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  {ϕ₁ ϕ₂ : Flow τ α}, (∀ (t : τ) (x : α), ϕ₁.toFun t x = ϕ₂.toFun t x) → ϕ₁ = ϕ₂
-- Init.Prelude
/-- The homogeneous version of `HMod`: `a % b : α` where `a b : α`.  -/
Mod : Type u → Type u
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformLeft e x).1 = x.1 ∩ (AddOpposite.op e +ᵥ x.1)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isEmbedding_restrictScalars : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5}
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : (i : ι) → Module 𝕜' (E i)]
  [inst_12 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  Topology.IsEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.isOpen_iff_image_isOpen : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → ∀ {s : Set X}, IsOpen s ↔ IsOpen (f '' s)
-- Mathlib.RingTheory.Valuation.Integral
Valuation.Integers.isIntegrallyClosed_integers : ∀ {K : Type u} {Γ₀ : Type v} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀),
  IsIntegrallyClosed ↥v.integer
-- Lean.Elab.PreDefinition.Structural.IndPred
/-- Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
The `value` is the function with (only) the fixed parameters moved into the context,
The `FType` is the expected type of the argument.
The `recArgInfos` is used to transform the body of the function to replace recursive calls with
uses of the `below` induction hypothesis.
Returns the functional argument and any matchers that were created as side effects.
The matchers are created inside `withoutModifyingEnv` and need to be replayed afterwards.
 -/
Lean.Elab.Structural.mkIndPredBRecOnF : Array Lean.Elab.Structural.RecArgInfo →
  Lean.Elab.Structural.Positions →
    Lean.Elab.Structural.RecArgInfo →
      Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM (Lean.Expr × Array (Lean.MetaM Unit))
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_right : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β),
  Set.IccExtend h f b = f ⟨b, ⋯⟩
-- Mathlib.LinearAlgebra.Dual.Defs
/-- See also `Subspace.dualAnnihilator_iInf_eq` for vector subspaces when `ι` is finite.  -/
Submodule.iSup_dualAnnihilator_le_iInf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_3}
  (U : ι → Submodule R M), ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.swap : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (f ∘ Prod.swap) (ν.prod μ)
-- Mathlib.Analysis.Convex.Extreme
/-- A set `B` is an extreme subset of `A` if `B ⊆ A` and all points of `B` only belong to open
segments whose ends are in `B`.

Our definition only requires that the left endpoint of the segment lies in `B`,
but by symmetry of open segments, the right endpoint must also lie in `B`.
See `IsExtreme.right_mem_of_mem_openSegment`.  -/
IsExtreme : (𝕜 : Type u_1) →
  {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → Set E → Set E → Prop
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_weightedHomogeneousComponent : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R),
  (MvPowerSeries.coeff d) ((MvPowerSeries.weightedHomogeneousComponent w p) f) =
    if (Finsupp.weight w) d = p then (MvPowerSeries.coeff d) f else 0
-- Mathlib.Order.CompleteLattice.Basic
iSup_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {b : β}, ⨆ x ∈ {b}, f x = f b
-- Mathlib.Order.WithBot
WithTop.IsWellOrder.lt : ∀ {α : Type u_1} [inst : Preorder α] [IsWellOrder α fun x1 x2 => x1 < x2], IsWellOrder (WithTop α) fun x1 x2 => x1 < x2
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_one_le_zero_iff : ∀ (n : WithBot ℕ∞), n + 1 ≤ 0 ↔ n = ⊥
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.disjointUnion_eq_piecewise : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
  (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x ∈ e.source)]
  [inst_1 : (y : β) → Decidable (y ∈ e.target)], e.disjointUnion e' hs ht = e.piecewise e' e.source e.target ⋯ ⋯
-- Mathlib.Data.Seq.Defs
/-- Corecursor for `Seq α` as a coinductive type. Iterates `f` to produce new elements
of the sequence until `none` is obtained.  -/
Stream'.Seq.corec : {α : Type u} → {β : Type v} → (β → Option (α × β)) → β → Stream'.Seq α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_maxKeyD_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {fallback : α},
  cmp ((Std.ExtDTreeMap.Const.modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.isometry_compMeasurePreserving : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β}
  [inst_2 : Fact (1 ≤ p)] (hf : MeasureTheory.MeasurePreserving f μ μb),
  Isometry ⇑(MeasureTheory.Lp.compMeasurePreserving f hf)
-- Mathlib.Data.Num.ZNum
Num.gcdAux.eq_2 : ∀ (x : Num) (n : ℕ), Num.gcdAux n.succ Num.zero x = x
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslateData.mk.sizeOf_spec : ∀ (ignoreArgsAttr : Lean.NameMapExtension (List ℕ)) (doTranslateAttr : Lean.NameMapExtension Bool)
  (unfoldBoundaries? : Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt)
  (translations : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo) (attrName : Lean.Name)
  (changeNumeral isDual : Bool) (guessNameExt : Mathlib.Tactic.GuessName.GuessNameExt),
  sizeOf
      { ignoreArgsAttr := ignoreArgsAttr, doTranslateAttr := doTranslateAttr, unfoldBoundaries? := unfoldBoundaries?,
        translations := translations, attrName := attrName, changeNumeral := changeNumeral, isDual := isDual,
        guessNameExt := guessNameExt } =
    1 + sizeOf ignoreArgsAttr + sizeOf doTranslateAttr + sizeOf unfoldBoundaries? + sizeOf translations +
            sizeOf attrName +
          sizeOf changeNumeral +
        sizeOf isDual +
      sizeOf guessNameExt
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.hasNatScalar : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → SMul ℕ (TruncatedWittVector p n R)
-- Mathlib.GroupTheory.Generators
/-- The generators of a group are given by a generating family indexed by `ι` and an assignment
`val : ι → G` such that `Subgroup.closure (Set.range val) = ⊤`.  -/
Group.Generators : (G : Type u_5) → [Group G] → Type u_6 → Type (max u_5 u_6)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- A precoverage is `w`-small, if every `0`-hypercover is `w`-small.  -/
CategoryTheory.Precoverage.Small : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop
-- Mathlib.Data.Finite.Sigma
Finite.instPSigma : ∀ {ι : Sort u_2} {π : ι → Sort u_3} [Finite ι] [∀ (i : ι), Finite (π i)], Finite ((i : ι) ×' π i)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The pole divisor of `f₁ + f₂` is smaller than or equal to the maximum of the pole divisors of `f₁`
and `f₂`, respectively.
 -/
MeromorphicOn.negPart_divisor_add_le_max : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (MeromorphicOn.divisor (f₁ + f₂) U)⁻ ≤ (MeromorphicOn.divisor f₁ U)⁻ ⊔ (MeromorphicOn.divisor f₂ U)⁻
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CochainComplex.plus_cylinder : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (K : CochainComplex C ℤ),
  CochainComplex.plus C K → CochainComplex.plus C (HomologicalComplex.cylinder K)
-- Std.Http.Data.Body.Full
/-- Returns the known size of the remaining data.
Returns `some (.fixed n)` with the current byte count, or `some (.fixed 0)` if the body has
already been consumed or closed.
 -/
Std.Http.Body.Full.getKnownSize : Std.Http.Body.Full → Std.Async.Async (Option Std.Http.Body.Length)
-- Mathlib.RingTheory.LocalProperties.FinitePresentation
/-- If there exists a set `{ r }` of `R` that generates the unit ideal and such that
`Mᵣ` is a finitely presented `Rᵣ`-module for each `r`, then `M` is a finitely presented
`R`-module.  -/
Module.FinitePresentation.of_localizationSpan : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    (∀ (g : ↑s), Module.FinitePresentation (Localization.Away ↑g) (LocalizedModule.Away (↑g) M)) →
      Module.FinitePresentation R M
-- Mathlib.LinearAlgebra.PiTensorProduct.Generators
MultilinearMap.ext_of_span_eq_top : ∀ {R : Type u_1} {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {N : Type u_4} {γ : ι → Type u_5} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] {g : ⦃i : ι⦄ → γ i → M i},
  (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
    ∀ {φ φ' : MultilinearMap R M N}, (∀ (j : (i : ι) → γ i), (φ fun i => g (j i)) = φ' fun i => g (j i)) → φ = φ'
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.e : {X : Type u} → {inst : TopologicalSpace X} → [self : HSpace X] → X
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.liftSupQuotQuotMkₐ_toRingHom : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ↑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = DoubleQuot.liftSupQuotQuotMk I J
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_sub : ∀ (m n : ℕ), ↑(m - n) = ↑m - ↑n
-- Init.Data.UInt.Lemmas
UInt64.le_total : ∀ (a b : UInt64), a ≤ b ∨ b ≤ a
-- Mathlib.Data.ENat.Pow
ENat.epow_top : ∀ {x : ℕ∞}, 1 < x → x ^ ⊤ = ⊤
-- Mathlib.Algebra.Order.Group.PosPart
inf_eq_sub_posPart_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), a ⊓ b = a - (a - b)⁺
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α} {v : β k},
      (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Function index of callee  -/
Lean.Elab.WF.GuessLex.RecCallWithContext.callee : Lean.Elab.WF.GuessLex.RecCallWithContext → ℕ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.isStableUnderLimitsOfShape_iff_limitsOfShape_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J], W.IsStableUnderLimitsOfShape J ↔ W.limitsOfShape J ≤ W
-- Init.Data.BitVec.Bitblast
BitVec.divSubtractShift.eq_1 : ∀ {w : ℕ} (qr : BitVec.DivModState w) (n d : BitVec w),
  BitVec.divSubtractShift { n := n, d := d } qr =
    if qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) < d then
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat false, r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) }
    else
      { wn := qr.wn - 1, wr := qr.wr + 1, q := qr.q.shiftConcat true,
        r := qr.r.shiftConcat (n.getLsbD (qr.wn - 1)) - d }
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_eq_zero : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : α → M),
  (∀ (a : α), f a = 0) → ∑ a, f a = 0
-- Mathlib.CategoryTheory.Galois.Basic
/-- Fiber functors preserve quotients by finite groups in arbitrary universes.  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {G : Type u_1}
  [inst_3 : Group G] [Finite G], CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftEq.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l')
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom)),
  CategoryTheory.MorphismProperty.Comma.mapLeftEq R l l' h hl =
    CategoryTheory.MorphismProperty.Comma.mapLeftEq R l l' h hl
-- Init.Data.Int.Order
Int.ofNat_le : ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.Data.Ordmap.Invariants
Ordnode.toList.eq_1 : ∀ {α : Type u_1} (t : Ordnode α), t.toList = Ordnode.foldr List.cons t []
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ) (a : α),
  hf.vectorMeasure (Set.Ioi a) = Filter.atTop.limUnder f - Function.rightLim f a
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddGrpCat.tensorObj_eq : ∀ (G H : AddGrpCat), CategoryTheory.MonoidalCategoryStruct.tensorObj G H = AddGrpCat.of (↑G × ↑H)
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- An injective semilinear map of vector spaces induces a map on projective spaces.  -/
Projectivization.map : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {L : Type u_3} →
            {W : Type u_4} →
              [inst_3 : DivisionRing L] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module L W] →
                    {σ : K →+* L} →
                      (f : V →ₛₗ[σ] W) → Function.Injective ⇑f → Projectivization K V → Projectivization L W
-- Mathlib.Order.UpperLower.Hom
UpperSet.coe_icisSupHom : ∀ {α : Type u_1} [inst : CompleteLattice α], ⇑UpperSet.icisSupHom = UpperSet.Ici
-- Mathlib.Data.FinEnum
FinEnum.instInt8 : FinEnum Int8
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A point in the mulAntidiagonal is determined by its first co-ordinate (subtype version of
`Finset.mulAntidiagonal_congr`). This lemma is used by the `ext` tactic.  -/
Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_ext : ∀ {A : Type u_1} [inst : CancelMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {n : A}
  {p q : ↥(Finset.HasMulAntidiagonal.mulAntidiagonal n)}, (↑p).1 = (↑q).1 → p = q
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instNonUnitalCommSemiring : {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalCommSemiring β] → NonUnitalCommSemiring (α →₀ β)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceTo_le_sliceTo_iff : ∀ {s : String.Slice} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀}, p₀.sliceTo q h₁ ≤ p₀.sliceTo r h₂ ↔ q ≤ r
-- Init.Data.Bool
Bool.lt_irrefl : ∀ (x : Bool), ¬x < x
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_forget : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.forget G) =
    CategoryTheory.Pseudofunctor.CoGrothendieck.forget F
-- Batteries.Data.Array.Match
/-- Make a KMP matcher for a given a pattern stream  -/
Array.Matcher.ofStream : {α : Type u_1} → {σ : Type u_2} → [BEq α] → [Std.Stream σ α] → σ → Array.Matcher α
-- Mathlib.Order.Concept
gc_lowerPolar_upperPolar : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop),
  GaloisConnection (⇑OrderDual.toDual ∘ lowerPolar r) (upperPolar r ∘ ⇑OrderDual.ofDual)
-- Mathlib.Probability.Process.Filtration
/-- Given a filtration `𝓕`, its **right continuation** is the filtration `𝓕₊` defined as follows:
- If `i` is isolated on the right, then `𝓕₊ i := 𝓕 i`;
- Otherwise, `𝓕₊ i := ⨅ j > i, 𝓕 j`.

It is sometimes simply defined as `𝓕₊ i := ⨅ j > i, 𝓕 j` when the index type is `ℝ`. In the
general case this is not ideal however. If `i` is maximal for instance, then `𝓕₊ i = ⊤`, which
is inconvenient because `𝓕₊` is not a `Filtration ι m` anymore. If the index type
is discrete (such as `ℕ`), then we would have `𝓕 = 𝓕₊` (i.e. `𝓕` is right-continuous) only if
`𝓕` is constant.

To avoid requiring a `TopologicalSpace` instance on `ι` in the definition, we endow `ι` with
the order topology `Preorder.topology` inside the definition. Say you write a statement about
`𝓕₊` which does not require a `TopologicalSpace` structure on `ι`,
but you wish to use a statement which requires a topology (such as `rightCont_apply`).
Then you can endow `ι` with the order topology by writing
```lean
  letI := Preorder.topology ι
  haveI : OrderTopology ι := ⟨rfl⟩
```  -/
MeasureTheory.Filtration.«term_₊» : Lean.TrailingParserDescr
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instIsUniversalLinearOrderTheory : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered], L.linearOrderTheory.IsUniversal
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_zero_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L), h.d 0 1 = L.d 0 1
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.powers.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R),
  HahnSeries.SummableFamily.powers x =
    { toFun := fun n => (if 0 < x.orderTop then x else 0) ^ n, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instMul.eq_1 : ∀ {α : Type u_1} [inst : Mul α], Lex.instMul = inst
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] (P : CategoryTheory.MorphismProperty D)
  (F : CategoryTheory.Functor C D) (X : D) [F.Full],
  (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P F X).Full
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- The underlying function `C → A` of a functor `C ⥤ Codiscrete A`.  -/
CategoryTheory.Codiscrete.invFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} → CategoryTheory.Functor C (CategoryTheory.Codiscrete A) → C → A
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- Finite sets are bounded.  -/
Set.Finite.isVonNBounded : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E}, s.Finite → Bornology.IsVonNBounded 𝕜 s
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk_le_mk : ∀ {R : Type u} [inst : NonAssocRing R] {S S' : Subsemiring R} (h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier)
  (h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier),
  { toSubsemiring := S, neg_mem' := h₁ } ≤ { toSubsemiring := S', neg_mem' := h₂ } ↔ S ≤ S'
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.fromFreeYonedaCoproduct_app_mk : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (m : M.Elements),
  (CategoryTheory.ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst)) (M.freeYonedaCoproductMk m) = m.snd
-- Mathlib.Data.Matrix.Basic
/-- `LinearMap.mapMatrix` is itself linear in the map being applied.

Alternative, this is `Matrix.map` as a bilinear map.  -/
LinearMap.mapMatrixLinear : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_7} →
      {S : Type u_8} →
        (A : Type u_10) →
          {α : Type u_11} →
            {β : Type u_12} →
              [inst : Semiring R] →
                [inst_1 : Semiring S] →
                  {σᵣₛ : R →+* S} →
                    [inst_2 : AddCommMonoid α] →
                      [inst_3 : AddCommMonoid β] →
                        [inst_4 : Module R α] →
                          [inst_5 : Module S β] →
                            [inst_6 : Semiring A] →
                              [inst_7 : Module A β] →
                                [inst_8 : SMulCommClass S A β] → (α →ₛₗ[σᵣₛ] β) →ₗ[A] Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.instContinuousMapClassSomeENatTop : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N], ContinuousMapClass (Diffeomorph I J M N ↑⊤) M N
-- Mathlib.GroupTheory.PushoutI
/-- The normal form for words in the pushout. Every element of the pushout is the product of an
element of the base group and a word made up of letters each of which is in the transversal.  -/
Monoid.PushoutI.NormalWord : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} → Monoid.PushoutI.NormalWord.Transversal φ → Type (max (max u_1 u_2) u_3)
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.divRadical_dvd_self : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  (a : E), EuclideanDomain.divRadical a ∣ a