mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_intCast_nonneg : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] (n : ℤ),
  0 ≤ ArchimedeanClass.mk ↑n
-- Mathlib.Algebra.Group.Finsupp
Finsupp.erase_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (f f' : ι →₀ M),
  Finsupp.erase a (f + f') = Finsupp.erase a f + Finsupp.erase a f'
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.symm : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c l (fun x => f₁ x - f₂ x) g → Asymptotics.IsBigOWith c l (fun x => f₂ x - f₁ x) g
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousSubmodule_zero : ∀ (σ : Type u_1) {R : Type u_3} [inst : CommSemiring R], MvPolynomial.homogeneousSubmodule σ R 0 = 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesMk₂_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupHomology.cycles₂ A)),
  groupHomology.cyclesMk 2 1 groupHomology.cyclesMk₂_eq._proof_1
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).inv) ↑x) ⋯ =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ A).inv) x
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is strongly Cartesian if for
all morphisms `φ' : a' ⟶ b` and all diagrams of the form
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ'` lifts `g ≫ f`, there exists a lift `χ` of `g` such that `φ' = χ ≫ φ`.  -/
CategoryTheory.Functor.IsStronglyCartesian : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        CategoryTheory.Functor 𝒳 𝒮 → {R S : 𝒮} → {a b : 𝒳} → (R ⟶ S) → (a ⟶ b) → Prop
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The functor `κ.ord.ToType ⥤ C` that is the diagram of the
transfinite composition `transfiniteCompositionOfShapeReflection`.  -/
CategoryTheory.OrthogonalReflection.iteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      C →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                (κ : Cardinal.{w}) →
                  [OrderBot κ.ord.ToType] →
                    [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] → CategoryTheory.Functor κ.ord.ToType C
-- Init.Data.SInt.Lemmas
ISize.toInt_lt_two_pow_numBits : ∀ (x : ISize), x.toInt < 2 ^ (System.Platform.numBits - 1)
-- Mathlib.Algebra.Homology.Embedding.Restriction
/-- The morphism `K.restriction e ⟶ L.restriction e` induced by a morphism `φ : K ⟶ L`.  -/
HomologicalComplex.restrictionMap : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              {K L : HomologicalComplex C c'} →
                (K ⟶ L) → (e : c.Embedding c') → [inst_2 : e.IsRelIff] → K.restriction e ⟶ L.restriction e
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofNat : ℕ → Lean.LeanOptionValue
-- Lean.AuxRecursor
Lean.isNoConfusion : Lean.Environment → Lean.Name → Bool
-- Mathlib.Geometry.Manifold.Sheaf.Basic
/-- Let `P` be a `LocalInvariantProp` for functions between spaces with the groupoids `G`, `G'`
and let `M`, `M'` be charted spaces modelled on the model spaces of those groupoids.  Then there is
a sheaf of types on `M` which, to each open set `U` in `M`, associates the type of bundled
functions from `U` to `M'` satisfying the lift of `P`.  -/
StructureGroupoid.LocalInvariantProp.sheaf : {H : Type u_1} →
  [inst : TopologicalSpace H] →
    {H' : Type u_2} →
      [inst_1 : TopologicalSpace H'] →
        {G : StructureGroupoid H} →
          {G' : StructureGroupoid H'} →
            {P : (H → H') → Set H → H → Prop} →
              (M : Type u) →
                [inst_2 : TopologicalSpace M] →
                  [ChartedSpace H M] →
                    (M' : Type u) →
                      [inst_4 : TopologicalSpace M'] →
                        [ChartedSpace H' M'] → G.LocalInvariantProp G' P → TopCat.Sheaf (Type u) (TopCat.of M)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.instInhabitedSubmonoidPresheaf : {X : TopCat} → (F : TopCat.Presheaf CommRingCat X) → Inhabited F.SubmonoidPresheaf
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : CommRingCat}
  (h : Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f V).inv h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_pow_const_div_const_pow_of_one_lt : ∀ (k : ℕ) {r : ℝ}, 1 < r → Filter.Tendsto (fun n => ↑n ^ k / r ^ n) Filter.atTop (nhds 0)
-- Mathlib.Data.Setoid.Partition
IndexedPartition.equivQuotient_symm_proj_apply : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α),
  hs.equivQuotient.symm (hs.proj x) = hs.index x
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.map_op_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.map AddOpposite.op (nhds x) = nhds (AddOpposite.op x)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.continuous_toCircle : ∀ {T : ℝ}, Continuous AddCircle.toCircle
-- Mathlib.NumberTheory.Real.Irrational
Irrational.sub_intCast : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), Irrational (x - ↑m)
-- Init.Data.Nat.ToString
Nat.length_repr_le_iff : ∀ {n k : ℕ}, 0 < k → (n.repr.length ≤ k ↔ n < 10 ^ k)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The canonical projection into the colimit, as a quotient type.  -/
ModuleCat.FilteredColimits.M.mk : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → (j : J) × ↑(F.obj j) → ↑(ModuleCat.FilteredColimits.M F)
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The categorical product in `Type max v u` is the type-theoretic product `Π j, F j`.  -/
CategoryTheory.Limits.Types.productIso : {J : Type v} → (F : J → Type (max v u)) → ∏ᶜ F ≅ (j : J) → F j
-- Mathlib.Data.Set.Disjoint
Set.disjoint_empty : ∀ {α : Type u} (s : Set α), Disjoint s ∅
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α}, k ∈ t₂ → Std.ExtDTreeMap.Const.get? (t₁ ∩ t₂) k = Std.ExtDTreeMap.Const.get? t₁ k
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- A category `HasWeakPullbacks` if it has all weak limits of shape `WalkingCospan`, i.e. if it
has a weak pullback for every pair of morphisms with the same codomain.  -/
CategoryTheory.Limits.HasWeakPullbacks : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iInf.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : Finite α] (f : α → L.Formula β),
  FirstOrder.Language.Formula.iInf f = FirstOrder.Language.BoundedFormula.iInf f
-- Init.Data.SInt.Lemmas
Int8.toInt_one : Int8.toInt 1 = 1
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.elim : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α} {p : Prop},
  IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_functor_map_op_edge : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C) (d : D),
  (CategoryTheory.Join.opEquiv C D).functor.map (Opposite.op (CategoryTheory.Join.edge c d)) =
    CategoryTheory.Join.edge (Opposite.op d) (Opposite.op c)
-- Init.Data.UInt.Lemmas
UInt32.toNat_sub : ∀ (a b : UInt32), (a - b).toNat = (2 ^ 32 - b.toNat + a.toNat) % 2 ^ 32
-- Mathlib.Topology.Sheaves.Stalks
/-- The morphism `(f⁻¹ℱ)ₓ ⟶ ℱ_{f(x)}`.  -/
TopCat.Presheaf.stalkPullbackInv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        (f : X ⟶ Y) →
          (F : TopCat.Presheaf C Y) →
            (x : ↑X) →
              ((TopCat.Presheaf.pullback C f).obj F).stalk x ⟶ F.stalk ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat}
  {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {generators : M.GeneratingSections}
  {relations : (CategoryTheory.Limits.kernel generators.π).GeneratingSections} {generators_1 : M.GeneratingSections}
  {relations_1 : (CategoryTheory.Limits.kernel generators_1.π).GeneratingSections},
  { generators := generators, relations := relations } = { generators := generators_1, relations := relations_1 } →
    generators = generators_1 ∧ relations ≍ relations_1
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.TryThisInfo.mk.injEq : ∀ (edit : Lean.Lsp.TextEdit) (codeActionTitle : String) (suggestion : Lean.Meta.Tactic.TryThis.Suggestion)
  (edit_1 : Lean.Lsp.TextEdit) (codeActionTitle_1 : String) (suggestion_1 : Lean.Meta.Tactic.TryThis.Suggestion),
  ({ edit := edit, codeActionTitle := codeActionTitle, suggestion := suggestion } =
      { edit := edit_1, codeActionTitle := codeActionTitle_1, suggestion := suggestion_1 }) =
    (edit = edit_1 ∧ codeActionTitle = codeActionTitle_1 ∧ suggestion = suggestion_1)
-- Mathlib.Analysis.Matrix.Normed
_private.Mathlib.Analysis.Matrix.Normed.0.Matrix.unitOf.eq_1 : ∀ {α : Type u_5} [inst : NormedDivisionRing α] [inst_1 : NormedAlgebra ℝ α] (a : α),
  Matrix.unitOf✝ a = if a = 0 then 1 else ‖a‖ • a⁻¹
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to its zeroth line `S.L₀`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorL₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.smul : {A : Type u} → {M : Type v} → A → M → Module.Presentation.tautological.R A M
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.instInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.AddMonObj A],
  CategoryTheory.AddMod.instInhabited A = { default := CategoryTheory.AddMod.regular A }
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndep_iff_iCondIndepSets : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndep m' hm' m μ ↔ ProbabilityTheory.iCondIndepSets m' hm' (fun x => {s | MeasurableSet s}) μ
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiffOn.curry_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {s : Set (M × M')},
  ContMDiffOn (I.prod I') J n (Function.uncurry f) s → ∀ {y : M'}, ContMDiffOn I J n (fun x => f x y) {x | (x, y) ∈ s}
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instEquivLike : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : Add N] → EquivLike (M ≃+ N) M N
-- Lean.Parser.Extra
Lean.Parser.sepByIndent.formatter : Lean.PrettyPrinter.Formatter → String → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).pt = W
-- Init.Data.UInt.Lemmas
USize.size_dvd_uInt64Size : USize.size ∣ UInt64.size
-- Mathlib.LinearAlgebra.Matrix.Symmetric
/-- A version of `Matrix.ext` that unfolds the `Matrix.transpose`.  -/
Matrix.IsSymm.ext : ∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, (∀ (i j : n), A j i = A i j) → A.IsSymm
-- Mathlib.GroupTheory.Perm.Closure
Equiv.Perm.closure_isCycle : ∀ {β : Type u_3} [Finite β], Subgroup.closure {σ | σ.IsCycle} = ⊤
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ext : ∀ {Γ : Type u_1} {R : Type u_2} {inst : PartialOrder Γ} {inst_1 : Zero R} {x y : HahnSeries Γ R},
  x.coeff = y.coeff → x = y
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.of_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w},
  (SimpleGraph.Walk.cons h p).IsPath → p.IsPath
-- Mathlib.Data.Quot
Quotient.instDecidableLiftOn₂'OfDecidablePred : {α : Sort u_1} →
  {β : Sort u_2} →
    {s₁ : Setoid α} →
      {s₂ : Setoid β} →
        (q₁ : Quotient s₁) →
          (q₂ : Quotient s₂) →
            (f : α → β → Prop) →
              (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), s₁ a₁ a₂ → s₂ b₁ b₂ → f a₁ b₁ = f a₂ b₂) →
                [(a : α) → DecidablePred (f a)] → Decidable (q₁.liftOn₂' q₂ f h)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Icc : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.Icc i j = Set.Icc ↑i ↑j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = (t.getKey? a).isSome
-- Mathlib.Algebra.Order.GroupWithZero.Defs
lt_mul_of_lt_mul_of_nonneg_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [MulPosMono α],
  a < b * c → b ≤ d → 0 ≤ c → a < d * c
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Note that the topology isn't part of the discrimination key so this gets tried on every
`IsModuleTopology` goal and hence the low priority.
 -/
instIsModuleTopology : ∀ {R : Type u_3} [inst : TopologicalSpace R] {A : Type u_4} [inst_1 : Add A] [inst_2 : SMul R A], IsModuleTopology R A
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instZero : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → Zero (ContMDiffSection I F n V)
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- The underlying finite set of a `logSizeBallStruct`  -/
PairReduction.logSizeBallStruct.finset : {T : Type u_2} → PairReduction.logSizeBallStruct T → Finset T
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.distribSMul : {R : Type u_1} →
  {M : Type u_4} → {N : Type u_5} → [inst : Semiring R] → [DistribSMul N R] → DistribSMul N (AddMonoidAlgebra R M)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommSemigroupOfAddHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → AddCommSemigroup (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] → AddCommSemigroup (DirectLimit G f)
-- Mathlib.CategoryTheory.Elements
/-- The functor mapping functors `C ⥤ Type w` to their category of elements  -/
CategoryTheory.Functor.elementsFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Functor C (Type w)) CategoryTheory.Cat
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.map_mem : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {F : Type u_7} [inst_3 : FunLike F M M] {f : F}, LinearMap.IsProj m f → ∀ (x : M), f x ∈ m
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_zero : ∀ (a : Ordinal.{u_4}), a - 0 = a
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_zero : Ordinal.omega 0 = Ordinal.omega0
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linkTarget.url : Lean.Parser.ParserFn
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- A fiber of a locally constant map as a `CompHausLike P`.  -/
CompHausLike.LocallyConstant.fiber : {P : TopCat → Prop} →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {Q : CompHausLike P} →
      {Z : Type (max u w)} → (r : LocallyConstant (↑Q.toTop) Z) → Function.Fiber ⇑r → CompHausLike P
-- Std.Http.Data.Headers.Name
/-- Standard Transfer-Encoding header name
 -/
Std.Http.Header.Name.transferEncoding : Std.Http.Header.Name
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_id : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A], ⇑(BialgHom.id R A) = id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.filter_equiv_self_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Raw.filter f t).Equiv t ↔
      ∀ (a : α) (h : a ∈ t), f (t.getKey a h) (Std.DTreeMap.Raw.Const.get t a h) = true)
-- Mathlib.Algebra.Group.Units.Basic
divp_mul_divp : ∀ {α : Type u} [inst : CommMonoid α] (x y : α) (ux uy : αˣ), x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClopen_iff_mul_add_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = PrimeSpectrum.zeroLocus {e}
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstHAddInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.lipschitzWith_one_ofFun_toFun' : ∀ {α : Type u_1} {β : Type u_2} {𝔖 𝔗 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  [inst_2 : Finite ↑𝔗], ⋃₀ 𝔖 ⊆ ⋃₀ 𝔗 → LipschitzWith 1 (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑(UniformOnFun.toFun 𝔗))
-- Mathlib.ModelTheory.Definability
/-- Definable sets are subsets of finite Cartesian products of a structure such that membership is
given by a first-order formula.  -/
FirstOrder.Language.DefinableSet : (L : FirstOrder.Language) → {M : Type w} → [L.Structure M] → Set M → Type u₁ → Type (max 0 u₁ w)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.one)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero),
  (match CategoryTheory.Limits.WalkingParallelPair.zero with
    | CategoryTheory.Limits.WalkingParallelPair.one => h_1 ()
    | CategoryTheory.Limits.WalkingParallelPair.zero => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
/-- The functor from a Cartesian monoidal category to comonoids in that category,
equipping every object with the diagonal map as a comultiplication.
 -/
CategoryTheory.cartesianComon : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Functor C (CategoryTheory.Comon C)
-- Init.Data.Option.Lemmas
Option.some_ne_none : ∀ {α : Type u_1} (x : α), some x ≠ none
-- Mathlib.Data.Analysis.Filter
/-- Map a `CFilter` to an equivalent representation type.  -/
CFilter.ofEquiv : {α : Type u_1} → {σ : Type u_3} → {τ : Type u_4} → [inst : PartialOrder α] → σ ≃ τ → CFilter α σ → CFilter α τ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mem_idealLattice : ∀ (K : Type u_2) [inst : Field K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.idealLattice K I ↔ ∃ y ∈ ↑↑I, (NumberField.mixedEmbedding K) y = x
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.measurableSet_liminf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (s n)) → MeasurableSet (Filter.liminf s Filter.atTop)
-- Mathlib.Algebra.Group.Defs
div_self' : ∀ {G : Type u_1} [inst : Group G] (a : G), a / a = 1