mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Basic
Lean.Parser.withAntiquotFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn → optParam Bool false → Lean.Parser.ParserFn
-- Mathlib.Topology.Compactness.Compact
IsCompact.nonempty_inter_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ {t : Set (Set X)}, (∀ a ∈ t, IsClosed a) → (∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty) → (s ∩ ⋂₀ t).Nonempty
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_same : ∀ {ι : 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] (P : RootPairing ι R M N) (i : ι) (x : M),
  (P.reflection i) ((P.reflection i) x) = x
-- Mathlib.CategoryTheory.Sites.Types
/-- The sheaf condition for `yoneda'`.  -/
CategoryTheory.Presieve.isSheaf_yoneda' : ∀ {α : Type u}, CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda.obj α)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mkIso'_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} (e : G ≅ H) [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H]
  [inst_4 : CategoryTheory.IsAddMonHom e.hom], (CategoryTheory.AddGrp.mkIso' e).hom.hom.hom = e.hom
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.mapEdgeSet_coe : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑G.edgeSet),
  ↑(f.mapEdgeSet e) = Sym2.map ⇑f ↑e
-- Mathlib.Data.List.Basic
List.head?.eq_2 : ∀ {α : Type u} (a : α) (as : List α), (a :: as).head? = some a
-- Mathlib.Topology.Order.PartialSups
ContinuousOn.partialSups_apply : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ} {s : Set X},
  (∀ k ≤ n, ContinuousOn (f k) s) → ContinuousOn (fun a => (partialSups fun x => f x a) n) s
-- Mathlib.Tactic.FunProp.Core
/-- Get candidate theorems from the environment for function property `funPropDecl` and
function `funName`.  -/
Mathlib.Meta.FunProp.getDeclTheorems : Mathlib.Meta.FunProp.FunPropDecl → Lean.Name → Array ℕ → ℕ → Lean.MetaM (Array Mathlib.Meta.FunProp.FunctionTheorem)
-- Mathlib.Order.Category.DistLat
/-- The type of morphisms in `DistLat R`.  -/
DistLat.Hom : DistLat → DistLat → Type u
-- Std.Time.Format.Modifier
/-- `W`: Week of month (e.g., 4).
 -/
Std.Time.Modifier.W : Std.Time.Number → Std.Time.Modifier
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.instInhabited : (α : Type u_2) → [inst : TopologicalSpace α] → Inhabited (α →CO α)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofIso_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞 : CategoryTheory.Subobject.Classifier C) {Ω₀ Ω : C}
  (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω)
  (ht :
    autoParam (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
      CategoryTheory.Subobject.Classifier.ofIso._auto_1)
  {F G : C} (m : F ⟶ G) (x : CategoryTheory.Mono m),
  (𝒞.ofIso eΩ eΩ₀ from' t ht).χ m = CategoryTheory.CategoryStruct.comp (𝒞.χ m) eΩ.hom
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousGeneratedBy.continuousMap_coe : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {g : Y → Z} (hg : Topology.ContinuousGeneratedBy X g),
  ⇑hg.continuousMap = ⇑Topology.WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑Topology.WithGeneratedByTopology.equiv
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.exists_presentation_fin : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S], ∃ n m, Nonempty (Algebra.Presentation R S (Fin n) (Fin m))
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- Append `a` to `x : Fin n ↪ ofStabilizer G a`  to get an element of `Fin n.succ ↪ α`.  -/
SubAddAction.ofStabilizer.snoc : {G : Type u_1} →
  [inst : AddGroup G] →
    {α : Type u_2} →
      [inst_1 : AddAction G α] → {a : α} → {n : ℕ} → (Fin n ↪ ↥(SubAddAction.ofStabilizer G a)) → Fin n.succ ↪ α
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.domRestrictHom_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {S : Type u_3} [inst_1 : SetLike S R] [inst_2 : SubmonoidClass S R] (T : S)
  (R'' : Type u_4) [inst_3 : CommMonoidWithZero R''] (χ : MulChar R R''),
  (MulChar.domRestrictHom T R'') χ = MulChar.domRestrict T χ
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.unitaryGroup.toGL` is the map from the unitary group to the general linear group  -/
Matrix.UnitaryGroup.toGL : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} →
        [inst_2 : CommRing α] →
          [inst_3 : StarRing α] → ↥(Matrix.unitaryGroup n α) → LinearMap.GeneralLinearGroup α (n → α)
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- A function `f` has the gradient `f'` as derivative along the filter `L` if
`f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` when `x'` converges along the filter `L`.  -/
HasGradientAtFilter : {𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → F → F → Filter F → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_same : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p : P1), AffineMap.lineMap p p = AffineMap.const k k p
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.set_next_add.foo : ∀ (i : String.Pos.Raw) (c : Char) (cs : List Char) (a : String.Pos.Raw) (b₁ b₂ : ℕ),
  (String.Pos.Raw.utf8GetAux cs a i).utf8Size + b₁ = String.utf8ByteSize'.go✝ cs + b₂ →
    (String.Pos.Raw.utf8GetAux (String.Pos.Raw.utf8SetAux c cs a i) a i).utf8Size + b₁ =
      String.utf8ByteSize'.go✝ (String.Pos.Raw.utf8SetAux c cs a i) + b₂
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_eq_generate : ∀ {α : Type u_1} {f : Filter α}, f.smallSets = Filter.generate (Set.powerset '' f.sets)
-- Mathlib.Topology.Defs.Filter
/-- A function between topological spaces is continuous at a point `x₀`
if `f x` tends to `f x₀` when `x` tends to `x₀`.  -/
ContinuousAt : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → X → Prop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_le_iff_add_nonneg' : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b : α}, -a ≤ b ↔ 0 ≤ a + b
-- Mathlib.Logic.Equiv.List
Encodable.decodeList.eq_def : ∀ {α : Type u_1} [inst : Encodable α] (x : ℕ),
  Encodable.decodeList x =
    match x with
    | 0 => some []
    | v.succ =>
      match Nat.unpair v, ⋯ with
      | (v₁, v₂), h =>
        have this := ⋯;
        (fun x1 x2 => x1 :: x2) <$> Encodable.decode v₁ <*> Encodable.decodeList v₂
-- Mathlib.Algebra.Homology.CommSq
/-- The kernel fork attached to a commutative square in a preadditive category.  -/
CategoryTheory.CommSq.kernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {fst : X₁ ⟶ X₂} →
            {snd : X₁ ⟶ X₃} →
              {f : X₂ ⟶ X₄} →
                {g : X₃ ⟶ X₄} →
                  CategoryTheory.CommSq fst snd f g →
                    CategoryTheory.Limits.KernelFork (CategoryTheory.Limits.biprod.desc f (-g))
-- Mathlib.Algebra.Group.Conj
isAddConj_zero_right : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, IsAddConj 0 a ↔ a = 0
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftK_π_eq_zero_of_boundary : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂) (x : A ⟶ S.X₁)
  (hx : k = CategoryTheory.CategoryStruct.comp x S.f), CategoryTheory.CategoryStruct.comp (h.liftK k ⋯) h.π = 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder] (i j : ι)
  (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij)
      ((HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij)
      ((CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) -
            CategoryTheory.CategoryStruct.id K.cylinder).f
        j)
-- Mathlib.RingTheory.TwoSidedIdeal.Instances
instNonUnitalSubringClassTwoSidedIdeal : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], NonUnitalSubringClass (TwoSidedIdeal R) R
-- Mathlib.FieldTheory.Perfect
injective_pow_p : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [ExpChar R p] [PerfectRing R p] {x y : R}, x ^ p = y ^ p → x = y
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compression.eq_1 : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  [inst_3 : DecidableEq α] (u v : α) (s : Finset α),
  UV.compression u v s = {a ∈ s | UV.compress u v a ∈ s} ∪ {a ∈ Finset.image (UV.compress u v) s | a ∉ s}
-- Init.Data.Array.Attach
List.unattach_toArray : ∀ {α : Type u_1} {p : α → Prop} {xs : List { x // p x }}, xs.toArray.unattach = xs.unattach.toArray
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.inr_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc h k w) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.instSetLike : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → SetLike (L.Substructure M) M
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.addQuotDepth : ℤ → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Action.Basic
/-- The object this action acts on  -/
Action.V : {V : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} V] → {G : Type u_2} → [inst_1 : Monoid G] → Action V G → V
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ),
  UniformConcaveOn s φ f =
    (Convex ℝ s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y + a * b * φ ‖x - y‖ ≤ f (a • x + b • y))
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_concat : ∀ {w t : ℕ} {x : BitVec (w + 1)} {y : Bool},
  BitVec.extractLsb' 0 (t + 1) (x.concat y) = (BitVec.extractLsb' 0 t x).concat y
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Presieve S), F.IsPrestackFor R ↔ Nonempty (F.toDescentData fun f => f.obj.hom).FullyFaithful
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.sin_le : ∀ {x : ℝ}, 0 ≤ x → Real.sin x ≤ x
-- Init.Meta.Defs
/-- Return substring of original input covering `stx`.
Result is meaningful only if all involved `SourceInfo.original`s refer to the same string (as is the case after parsing).  -/
Lean.Syntax.getSubstring? : Lean.Syntax → optParam Bool true → optParam Bool true → Option Substring.Raw
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.ae_eq_of_dirac : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} [MeasurableSingletonClass 𝓧] {x : 𝓧},
  ProbabilityTheory.HasLaw X (MeasureTheory.Measure.dirac x) P → X =ᵐ[P] fun x_1 => x
-- Mathlib.Data.Setoid.Basic
Setoid.le_def : ∀ {α : Type u_1} {r s : Setoid α}, r ≤ s ↔ ∀ {x y : α}, r x y → s x y
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_one : ∀ {R : Type u} [inst : Monoid R] {A : Type v} [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A],
  ⇑1 = id
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2Space : ∀ {R : Type u_1} [inst : CommSemiring R] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : TopologicalSpace B]
  [inst_3 : Algebra R B] {D : Type u_5} [inst_4 : UniformSpace D] [CompleteSpace D] [inst_6 : Semiring D]
  [inst_7 : Algebra R D] [T2Space B] (f g : D →A[R] B), CompleteSpace ↥((↑f).equalizer ↑g)
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.fintype_card_le_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {ι : Type u_1} [inst_5 : Fintype ι] {b : ι → M},
  LinearIndependent R b → Fintype.card ι ≤ Module.finrank R M
-- Mathlib.CategoryTheory.Filtered.Small
/-- The first part of a factoring of a functor from a small category to a cofiltered category
through a small filtered category.  -/
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            CategoryTheory.Functor D (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
RCLike.nonUnitalContinuousFunctionalCalculusIsClosedEmbedding : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop},
  (∀ {x : A}, p₁ ↑x ↔ p x) →
    ∀ [ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] [CompleteSpace A] [CStarRing A],
      NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instPartialOrder : {α : Type u_2} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.Closeds α)
-- Mathlib.LinearAlgebra.DFinsupp
iSupIndep_iff_linearIndependent_of_ne_zero : ∀ {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] [IsDomain R]
  [Module.IsTorsionFree R N] {ι : Type u_7} {v : ι → N},
  (∀ (i : ι), v i ≠ 0) → ((iSupIndep fun x => R ∙ v x) ↔ LinearIndependent R v)
-- Mathlib.CategoryTheory.Adjunction.Comma
CategoryTheory.isRightAdjoint_iff_hasInitial_structuredArrow : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor D C},
  G.IsRightAdjoint ↔ ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v), w.reverse = w.reverseAux SimpleGraph.Walk.nil
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance_eq_inner : ∀ {α : Type u} {β : α → Type v} [Ord α] {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β}
  (hl : (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced)
  {h :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balance k v l r ⋯ ⋯ h = Std.DTreeMap.Internal.Impl.inner sz k v l r
-- Mathlib.Util.TermReduce
/-- `delta% t` elaborates to a head-delta reduced version of `t`.  -/
Mathlib.Util.TermReduce.elabDelta : Lean.Elab.Term.TermElab
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNNNorm_mul_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R]
  (x : R), ‖(ContinuousLinearMap.mul 𝕜 R) x‖₊ = ‖x‖₊
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The coercion from multivariate polynomials to multivariate power series
as an algebra homomorphism.
 -/
MvPolynomial.coeToMvPowerSeries.algHom : {σ : Type u_1} →
  {R : Type u_2} →
    [inst : CommSemiring R] →
      (A : Type u_3) → [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → MvPolynomial σ R →ₐ[R] MvPowerSeries σ A
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {X : Type u_8} [inst_5 : TopologicalSpace X] {g : M → X}
  {s : Set M} {x : M},
  ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(f.extend I) x) ↔
    ContinuousWithinAt (g ∘ ↑f.symm) (↑f.symm ⁻¹' s) (↑f x)
-- Mathlib.Topology.Algebra.Affine
/-- The line map is continuous in all arguments.  -/
AffineMap.lineMap_continuous_uncurry : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V],
  Continuous fun pqt => (AffineMap.lineMap pqt.1 pqt.2.1) pqt.2.2
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonzero, nonnegative, multiplicatively bounded function, then `f 1 ≠ 0`.  -/
map_one_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  f ≠ 0 → 0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → f 1 ≠ 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass.mk' : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {γ : Type u_1}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (∀ (c : γ), Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation (op c)) →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op
-- Mathlib.Analysis.Convex.Join
convexJoin_union_right : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s t₁ t₂ : Set E), convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂
-- Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Algebra.isIntegral_def : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.IsIntegral R A ↔ ∀ (x : A), IsIntegral R x
-- Mathlib.Order.Filter.Ker
Filter.pi.eq_1 : ∀ {ι : Type u_3} {α : ι → Type u_4} (f : (i : ι) → Filter (α i)),
  Filter.pi f = ⨅ i, Filter.comap (Function.eval i) (f i)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_of_le_of_coeff_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.natDegree ≤ n → p.coeff n ≠ 0 → p.natDegree = n
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp : ∀ {a b c : CategoryTheory.LocallyDiscrete CommRingCat} (x : a ⟶ b) (x_1 : b ⟶ c),
  CommRingCat.moduleCatExtendScalarsPseudofunctor.mapComp x x_1 =
    CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom x.as) (CommRingCat.Hom.hom x_1.as))
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves kernels  -/
CategoryTheory.Functor.PreservesHomology.preservesKernels : ∀ {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.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {F : CategoryTheory.Functor C D}
  {inst_4 : F.PreservesZeroMorphisms} [self : F.PreservesHomology] ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F
-- Mathlib.Order.Directed
IsDirectedOrder.eq_1 : ∀ (α : Type u_5) [inst : LE α], IsDirectedOrder α = IsDirected α fun x1 x2 => x1 ≤ x2
-- Mathlib.Tactic.GRewrite.Core
/-- The state used in `GRewriteM`.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State : Type
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- **Conditional Jensen's inequality**: in a Banach space `E` with a measure `μ` that is σ-finite
on a sub-σ-algebra `m`, if `φ : E → ℝ` is convex and lower-semicontinuous on a closed set `s`, then
for any `f : α → E` such that `f` and `φ ∘ f` are integrable, and `f` lies in `s` a.e., we have
`φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m]`.  -/
ConvexOn.map_condExp_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConvexOn ℝ s φ →
    LowerSemicontinuousOn φ s →
      (∀ᵐ (a : α) ∂μ, f a ∈ s) →
        IsClosed s → MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_iff_exists_orderOf_eq_natCard : ∀ {α : Type u_1} [inst : Group α] [Finite α], IsCyclic α ↔ ∃ g, orderOf g = Nat.card α
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.Raw.Const.minEntry! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → α × β
-- Mathlib.RingTheory.RingInvo
RingInvo.coe_ringEquiv : ∀ {R : Type u_2} [inst : Semiring R] (f : RingInvo R) (a : R), f.toRingEquiv a = f a
-- Mathlib.Data.Set.Lattice
/-- This rather trivial consequence of `subset_iUnion₂` is convenient with `apply`, and has `i` and
`j` explicit for this purpose.  -/
Set.subset_iUnion₂_of_subset : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
  s ⊆ t i j → s ⊆ ⋃ i, ⋃ j, t i j
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.exists_toScheme : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {P : ↥↑U → Prop}, (∃ x, P x) ↔ ∃ x, ∃ (hx : x ∈ U), P ⟨x, hx⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.unop_π_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.unop.π.app CategoryTheory.Limits.WalkingParallelPair.zero =
    (c.ι.app CategoryTheory.Limits.WalkingParallelPair.one).unop
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.finiteAt_principal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ.FiniteAtFilter (Filter.principal s) ↔ μ s < ⊤