mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.strFn.go.eq_def : ∀ (str : String) (c : Lean.Parser.ParserContext) (iter : str.Pos) (s : Lean.Parser.ParserState),
  Lean.Doc.Parser.strFn.go✝ str c iter s =
    if h : iter.IsAtEnd then s
    else
      have ch := iter.get h;
      Lean.Doc.Parser.strFn.go✝ str c (iter.next h) (Lean.Parser.satisfyFn (fun x => x == ch) ch.toString c s)
-- Mathlib.SetTheory.ZFC.PSet
PSet.instInhabited : Inhabited PSet.{u_1}
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- A local site is a site that has a terminal object with only a single covering sieve.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Prop
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely as `x` tends to `b` from the right or from the left,
then `u ↦ ∫ x in a..u, f x` has right (resp., left) derivative `c` at `b`.  -/
intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
      StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
        Filter.Tendsto f (nhdsWithin b t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
          HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) c s b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_filterMap!_eq_size_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filterMap! f t).size = t.size ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true),
        (f (t.getKey a h) (Std.DTreeMap.Internal.Impl.Const.get t a h)).isSome = true)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.star_apply_of_isSelfAdjoint : ∀ {n : Type u_2} {A : Type u_5} [inst : Star A] {f : CStarMatrix n n A},
  IsSelfAdjoint f → ∀ {i j : n}, star (f i j) = f j i
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.invRotate_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.invRotate.mor₂ = T.mor₁
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.coe_nonneg : ∀ {H : Type u_1} [inst : AddCommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedAddMonoid H],
  ↑(AddGroupCone.nonneg H) = {x | 0 ≤ x}
-- Mathlib.Topology.Sheaves.MayerVietoris
Opens.coe_mayerVietorisSquare_X₁ : ∀ {T : Type u} [inst : TopologicalSpace T] (U V : TopologicalSpace.Opens T),
  ↑(Opens.mayerVietorisSquare U V).X₁ = ↑U ∩ ↑V
-- Mathlib.Analysis.Calculus.ContDiff.Basic
LinearIsometryEquiv.contDiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (f : E ≃ₗᵢ[𝕜] F), ContDiff 𝕜 n ⇑f
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- Polarization identity for symmetric linear maps.
See `inner_map_polarization` for the complex version without the symmetric assumption.  -/
LinearMap.IsSymmetric.inner_map_polarization : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E},
  T.IsSymmetric →
    ∀ (x y : E),
      inner 𝕜 (T x) y =
        (inner 𝕜 (T (x + y)) (x + y) - inner 𝕜 (T (x - y)) (x - y) -
              RCLike.I * inner 𝕜 (T (x + RCLike.I • y)) (x + RCLike.I • y) +
            RCLike.I * inner 𝕜 (T (x - RCLike.I • y)) (x - RCLike.I • y)) /
          4
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- Compose two isomorphisms in a monoidal category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.MonoidalCategory.«term_≪⊗≫_» : Lean.TrailingParserDescr
-- Init.Data.Vector.Basic
Vector.flatten : {α : Type u_1} → {n m : ℕ} → Vector (Vector α n) m → Vector α (m * n)
-- Lean.Meta.Eqns
Lean.Meta.eqnThmSuffixBasePrefix : String
-- Lean.DocString.Markdown
Lean.Doc.MdRendererState.mk : Lean.NameMap Lean.Name → Lean.NameMap Lean.Name → Lean.Doc.MdRendererState
-- Mathlib.Algebra.Category.Ring.Limits
/-- The chosen cone is a limit cone. (Generally, you'll just want to use `limit.cone F`.)  -/
CommRingCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] →
        CategoryTheory.Limits.IsLimit (CommRingCat.limitCone F)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAdd : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Add Y] → Add (LocallyConstant X Y)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.of_hasKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {Y Z : C} (g : Y ⟶ Z) (X : C) [CategoryTheory.Limits.HasKernel g],
  { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := g, zero := ⋯ }.HasLeftHomology
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.conjContinuousAlgEquiv_apply : ∀ {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup G] [inst_1 : AddCommGroup H]
  [inst_2 : NormedField 𝕜] [inst_3 : Module 𝕜 G] [inst_4 : Module 𝕜 H] [inst_5 : TopologicalSpace G]
  [inst_6 : TopologicalSpace H] [inst_7 : IsTopologicalAddGroup G] [inst_8 : IsTopologicalAddGroup H]
  [inst_9 : ContinuousConstSMul 𝕜 G] [inst_10 : ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) (f : G →L[𝕜] G),
  e.conjContinuousAlgEquiv f = ↑e ∘SL f ∘SL ↑e.symm
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ),
  (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.obj X = X.unmop.unmop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      l.contains k = false →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = true → m.contains k = true
-- Lean.Environment
Lean.instInhabitedConstantKind : Inhabited Lean.ConstantKind
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Contains a `PreDiscrTree` and any errors occurring during initialization of
the library search tree.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults : Type → Type
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.decidableLT : {α : Type u} →
  (self : Std.Packages.PreorderOfLEArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    let this := self.lt;
    have this_1 := ⋯;
    DecidableLT α
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.exp_arsinh : ∀ (x : ℝ), Real.exp (Real.arsinh x) = x + √(1 + x ^ 2)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeftIso_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h),
  (CategoryTheory.Bicategory.whiskerLeftIso f η).hom = CategoryTheory.Bicategory.whiskerLeft f η.hom
-- Init.Data.AC
Lean.Data.AC.instBEqExpr.beq : Lean.Data.AC.Expr → Lean.Data.AC.Expr → Bool
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.natEnd.eq_1 : Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.Γ'.consₗ = true
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_div : ∀ {a b : UInt16}, (a / b).toBitVec = a.toBitVec / b.toBitVec
-- Lean.Syntax
/-- Like `structRangeEq` but prints trace on failure if `trace.Elab.reuse` is activated.  -/
Lean.Syntax.structRangeEqWithTraceReuse : Lean.Options → Lean.Syntax → Lean.Syntax → Bool
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral over simple functions in L1 space as a continuous linear map.  -/
MeasureTheory.L1.SimpleFunc.integralCLM' : (α : Type u_1) →
  (E : Type u_2) →
    (𝕜 : Type u_4) →
      [inst : NormedAddCommGroup E] →
        {m : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) →
            [inst_1 : NormedRing 𝕜] →
              [inst_2 : Module 𝕜 E] →
                [inst_3 : IsBoundedSMul 𝕜 E] →
                  [inst_4 : NormedSpace ℝ E] → [SMulCommClass ℝ 𝕜 E] → ↥(α →₁ₛ[μ] E) →L[𝕜] E
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
le_eventuallyMeasurableSpace : ∀ {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [inst : CountableInterFilter l],
  m ≤ eventuallyMeasurableSpace m l
-- Lean.Meta.Tactic.Cases
Lean.Meta.CasesSubgoal.mk.injEq : ∀ (toInductionSubgoal : Lean.Meta.InductionSubgoal) (ctorName : Option Lean.Name)
  (toInductionSubgoal_1 : Lean.Meta.InductionSubgoal) (ctorName_1 : Option Lean.Name),
  ({ toInductionSubgoal := toInductionSubgoal, ctorName := ctorName } =
      { toInductionSubgoal := toInductionSubgoal_1, ctorName := ctorName_1 }) =
    (toInductionSubgoal = toInductionSubgoal_1 ∧ ctorName = ctorName_1)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.finrank_dualCoannihilator_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {Φ : Subspace K (Module.Dual K V)},
  Module.finrank K ↥(Submodule.dualCoannihilator Φ) = Module.finrank K ↥(Submodule.dualAnnihilator Φ)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.subset_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  S ⊆ ↑(IntermediateField.adjoin F S)
-- Mathlib.Data.Fin.Fin2
Fin2.castSucc.eq_2 : ∀ (n_1 : ℕ) (i : Fin2 n_1), i.fs.castSucc = i.castSucc.fs
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.hyp.sizeOf_spec : sizeOf Mathlib.Tactic.ClickSuggestions.SectionKind.hyp = 1
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Recurrence formula for the Beta function.  -/
Complex.betaIntegral_recurrence : ∀ {u v : ℂ}, 0 < u.re → 0 < v.re → u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_div_sq_add_sq : ∀ {a b c : ℝ}, ∫ (x : ℝ) in a..b, c / (c ^ 2 + x ^ 2) = Real.arctan (b / c) - Real.arctan (a / c)
-- Init.Data.Array.Lemmas
Array.replace_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a b : α} {xs ys : Array α},
  (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_π : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d)
  (x_1 : SSet.relativeCellComplexOfMono.Cell i d), ((SSet.relativeCellComplexOfMono i).attachCells d x).π x_1 = ()
-- Mathlib.Probability.Kernel.Category.Stoch
instIsStableUnderComonoidSFinKerStochHom : ∀ {X : SFinKer}, StochHom.IsStableUnderComonoid X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.right = iZ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'
-- Mathlib.Data.Setoid.Basic
/-- Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose
induced map from the quotient of α to β is injective.  -/
Setoid.ker_eq_lift_of_injective : ∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} (f : α → β) (H : r ≤ Setoid.ker f),
  Function.Injective (Quotient.lift f H) → Setoid.ker f = r
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- Morphisms into the chosen end are determined by their composites with `chosenEnd.π`.  -/
CategoryTheory.Limits.chosenEnd.hom_ext : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {X : C} {f g : X ⟶ CategoryTheory.Limits.chosenEnd F},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.chosenEnd.π F j) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.chosenEnd.π F j)) →
    f = g
-- Init.Data.UInt.Lemmas
UInt8.add_comm : ∀ (a b : UInt8), a + b = b + a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.uniqueHomToTrivial : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] →
      (A : CategoryTheory.Mon D) → Unique (A ⟶ CategoryTheory.Mon.trivial D)
-- Mathlib.Order.SymmDiff
bihimp_bihimp_cancel_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a (bihimp a b) = b
-- Mathlib.Analysis.InnerProductSpace.Continuous
Continuous.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → E},
  Continuous f → Continuous g → Continuous fun t => inner 𝕜 (f t) (g t)
-- Mathlib.Order.Disjoint
isCompl_comm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y ↔ IsCompl y x
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncContext.mkRaw.inj : ∀ {declPrefix : Lean.Name} {realizingStack : List Lean.Name} {declPrefix_1 : Lean.Name}
  {realizingStack_1 : List Lean.Name},
  { declPrefix := declPrefix, realizingStack := realizingStack } =
      { declPrefix := declPrefix_1, realizingStack := realizingStack_1 } →
    declPrefix = declPrefix_1 ∧ realizingStack = realizingStack_1
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.comp.eq_3 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (_x : C) (_y _z : D) (x_5 : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y))
  (x_6 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)),
  CategoryTheory.Join.comp x_5 x_6 = PUnit.unit
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coeToZeroHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N],
  AddMonoidHom.coeToZeroHom = { coe := AddMonoidHom.toZeroHom }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.WF → t₂.WF → (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁.Equiv t₂
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
/-- If `f : ∀ (j : Fin (n + 2)) (_ : j ≠ i), Δ[n] ⟶ X` is a compatible family
of morphisms (which defines a morphism `Λ[n + 1, i] ⟶ X`), `p : X ⟶ Y` a Kan fibration
and `b : Δ[n + 1] ⟶ Y` such that for all `j ≠ i`, `f j _ ≫ p = stdSimplex.δ j ≫ b`,
then this is a lifting `Δ[n + 1] ⟶ X`.  -/
SSet.horn.IsCompatible.lift : {X : SSet} →
  {n : ℕ} →
    {i : Fin (n + 2)} →
      {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)} →
        SSet.horn.IsCompatible f →
          {Y : SSet} →
            (p : X ⟶ Y) →
              [HomotopicalAlgebra.Fibration p] →
                (b : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y) →
                  (∀ (j : Fin (n + 2)) (hj : j ≠ i),
                      CategoryTheory.CategoryStruct.comp (f j hj) p =
                        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b) →
                    (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₁ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (i₁ i₂ : data.I₀),
  data.toPreOneHypercover.I₁ i₁ i₂ = data.I₁ i₁ i₂
-- Mathlib.Order.Category.PartOrdEmb
/-- The underlying `OrderEmbedding`.  -/
PartOrdEmb.Hom.hom' : {X Y : PartOrdEmb} → X.Hom Y → ↑X ↪o ↑Y
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.ne_zero_of_ne : ∀ {R : Type u} [inst : Semiring R], 0 ≠ 1 → ∀ {p : Polynomial R}, p.Monic → p ≠ 0
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F` and `G` are naturally isomorphic, then `F.mapCone c` being a limit implies
`G.mapCone c` is also a limit.
 -/
CategoryTheory.Limits.IsLimit.mapConeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {K : CategoryTheory.Functor J C} →
              {F G : CategoryTheory.Functor C D} →
                (F ≅ G) →
                  {c : CategoryTheory.Limits.Cone K} →
                    CategoryTheory.Limits.IsLimit (F.mapCone c) → CategoryTheory.Limits.IsLimit (G.mapCone c)
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_support : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (p : Polynomial S), (IsLocalization.integerNormalization M p).support ⊆ p.support
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsRelIffEmbeddingUp'Add : ∀ {A : Type u_3} [inst : AddCommSemigroup A] [inst_1 : IsRightCancelAdd A] (a b : A),
  (ComplexShape.embeddingUp'Add a b).IsRelIff
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_mono : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Multiset α},
  s₁ ⊆ s₂ → s₂.gcd ∣ s₁.gcd
-- Mathlib.Topology.MetricSpace.Algebra
/-- Class `LipschitzMul M` says that the multiplication `(*) : X × X → X` is Lipschitz jointly
in the two arguments.  -/
LipschitzMul : (β : Type u_2) → [PseudoMetricSpace β] → [Monoid β] → Prop
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.toAddSubgroup_closedBall : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] (c : FiniteArchimedeanClass M),
  (FiniteArchimedeanClass.closedBall K c).toAddSubgroup = c.closedBallAddSubgroup
-- Mathlib.Order.Disjoint
codisjoint_of_subsingleton : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α} [Subsingleton α], Codisjoint a b
-- Mathlib.Topology.Algebra.Group.TopologicalAbelianization
/-- The topological abelianization of `absoluteGaloisGroup`, that is, the quotient of
`absoluteGaloisGroup` by the topological closure of its commutator subgroup.  -/
TopologicalAbelianization : (G : Type u_1) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → Type u_1
-- Mathlib.Analysis.Convolution
/-- `(φ i ⋆ g i) (k i)` tends to `z₀` as `i` tends to some filter `l` if
* `φ` is a sequence of nonnegative functions with integral `1` as `i` tends to `l`;
* The support of `φ` tends to small neighborhoods around `(0 : G)` as `i` tends to `l`;
* `g i` is `mu`-a.e. strongly measurable as `i` tends to `l`;
* `g i x` tends to `z₀` as `(i, x)` tends to `l ×ˢ 𝓝 x₀`;
* `k i` tends to `x₀`.

See also `ContDiffBump.convolution_tendsto_right`.
 -/
MeasureTheory.convolution_tendsto_right : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G]
  [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] [inst_7 : NormedSpace ℝ E'] [CompleteSpace E'] {ι : Type u_1}
  {g : ι → G → E'} {l : Filter ι} {x₀ : G} {z₀ : E'} {φ : ι → G → ℝ} {k : ι → G},
  (∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x) →
    (∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1) →
      Filter.Tendsto (fun n => Function.support (φ n)) l (nhds 0).smallSets →
        (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ) →
          Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀) →
            Filter.Tendsto k l (nhds x₀) →
              Filter.Tendsto (fun i => MeasureTheory.convolution (φ i) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i)) l
                (nhds z₀)
-- Mathlib.Algebra.Group.Conj
AddConjClasses.eq_1 : ∀ (α : Type u_1) [inst : AddMonoid α], AddConjClasses α = Quotient (IsAddConj.setoid α)
-- Init.SimpLemmas
Lean.true_arrow_congr_right : ∀ (q q' : Prop), q = q' → Lean.Arrow True q = q'
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.mem_so : ∀ (n : Type u_1) (R : Type u₂) [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (A : Matrix n n R),
  A ∈ LieAlgebra.Orthogonal.so n R ↔ A.transpose = -A
-- Mathlib.Combinatorics.Enumerative.Bell
/-- The `n`th standard Bell number,
which counts the number of partitions of a set of cardinality `n`.
 -/
Nat.bell : ℕ → ℕ
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If `f` is meromorphic, then the divisor of `f ^ n` is `n` times the divisor of `f`.
 -/
MeromorphicOn.divisor_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicOn f U → ∀ (n : ℕ), MeromorphicOn.divisor (f ^ n) U = n • MeromorphicOn.divisor f U
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer : Type
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.mono_iff_mono_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasPullbacks A]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G]
  {Y Z : CategoryTheory.StructuredArrow X G} (f : Y ⟶ Z),
  CategoryTheory.Mono f ↔ CategoryTheory.Mono (CategoryTheory.StructuredArrow.Hom.right f)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F),
  ((ContinuousLinearMap.toLinearMap₁₂ L) v) w = (L v) w
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.aeval_primPart_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {S : Type u_2} [inst_2 : Ring S] [IsDomain S]
  [inst_4 : Algebra R S] [Module.IsTorsionFree R S] {p : Polynomial R} {s : S},
  p ≠ 0 → (Polynomial.aeval s) p = 0 → (Polynomial.aeval s) p.primPart = 0