mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source_of_isClosed : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] {s : Set M},
  IsClosed s → ∃ f, f.IsSubordinate fun x => (chartAt H ↑x).source
-- Mathlib.Data.ENNReal.Inv
ENNReal.orderIsoIicCoe_apply_coe : ∀ (a : NNReal) (a_1 : ↑(Set.Iic ↑a)), ↑((ENNReal.orderIsoIicCoe a) a_1) = (↑a_1).toNNReal
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.apply_apply : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f g : α → α}, P.IsRepFun f → P.IsRepFun g → ∀ (x : α), f (g x) = f x
-- Mathlib.LinearAlgebra.Projection
/-- Given an idempotent linear operator `q`,
we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`.  -/
LinearMap.IsIdempotentElem.comp_eq_right_iff : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {q : M →ₗ[S] M},
  IsIdempotentElem q →
    ∀ {E : Type u_7} [inst_3 : AddCommMonoid E] [inst_4 : Module S E] (p : E →ₗ[S] M), q ∘ₗ p = p ↔ p.range ≤ q.range
-- Init.Data.String.Defs
String.Pos.mk : {s : String} → (offset : String.Pos.Raw) → String.Pos.Raw.IsValid s offset → s.Pos
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_reflectionPerm_self_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] (i j : ι),
  P.pairingIn S ((P.reflectionPerm i) i) j = -P.pairingIn S i j
-- Mathlib.Algebra.Algebra.Basic
Algebra.mul_sub_algebraMap_pow_commutes : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A) (r : R)
  (n : ℕ), x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.instLawfulGetElemMem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  LawfulGetElem (Std.ExtHashMap α β) α β fun m a => a ∈ m
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_of_essentiallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C],
  CategoryTheory.LocallySmall.{w, v, u} C
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the right unitor `ρ_ f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.rightUnitorM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
/-- `Finset.Nat.antidiagonalTuple k n` is a finset of `k`-tuples summing to `n`  -/
Finset.Nat.antidiagonalTuple : (k : ℕ) → ℕ → Finset (Fin k → ℕ)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonFileEvent : Lean.ToJson Lean.Lsp.FileEvent
-- Init.Data.List.Sublist
List.prefix_iff_exists_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ ∃ l₃, l₂ = l₁ ++ l₃
-- Init.Data.Char.Lemmas
Char.not_le : ∀ {a b : Char}, ¬a ≤ b ↔ b < a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.minD fallback = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Not an instance, to avoid loops with `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono`.  -/
MulLeftStrictMono.toIsLeftCancelMul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulLeftStrictMono α], IsLeftCancelMul α
-- Mathlib.Topology.LocallyFinsupp
/-- If `X` is T2 and if `U` is compact, then the support of a function with locally finite support
within `U` is finite.
 -/
Function.locallyFinsuppWithin.finiteSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [T2Space X] [inst_2 : Zero Y]
  (D : Function.locallyFinsuppWithin U Y), IsCompact U → D.support.Finite
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.injective_of_map_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  {N : Type u_6} [inst_6 : AddCommMonoid N] [inst_7 : Module R N] {g : M' →ₗ[R] N},
  (∀ {x y : M}, g (f x) = g (f y) → f x = f y) → Function.Injective ⇑g
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.toList_split_of_isEmpty : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_3 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_4 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice},
  s.isEmpty = true → List.map String.Slice.copy (s.split pat).toList = [""]
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBot_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (a : WithBot α),
  f.withBot a = WithBot.map (⇑f) a
-- Init.Grind.Ring.Field
Lean.Grind.Field.zpow_natCast : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (n : ℕ), a ^ ↑n = a ^ n
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in an array.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toArray`.
 -/
Std.Iter.Total.toArray : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.Iterators.Finite α Id] → Std.Iter.Total β → Array β
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instFunLike : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → FunLike (SchwartzMap E F) E F
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.isAtEnd : Lean.Server.Snapshots.Snapshot → Bool
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The distance from the circumcenter to the reflection of the orthocenter in a side equals the
circumradius.  -/
Affine.Triangle.dist_circumcenter_reflection_orthocenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ : Fin 3},
  i₁ ≠ i₂ →
    dist (Affine.Simplex.circumcenter t)
        ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) t.orthocenter) =
      Affine.Simplex.circumradius t
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorph.isLocalDiffeomorphOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f → ∀ (s : Set M), IsLocalDiffeomorphOn I J n f s
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_mul_self : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : Invertible 2] (a : αˢʸᵐ),
  SymAlg.unsym (a * a) = SymAlg.unsym a * SymAlg.unsym a
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn_2.go : {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u} →
    {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
      {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
        (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
          ((t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t) →
            ((t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
                Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t) →
              ((t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
                  Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t) →
                ((t : Task Lean.Language.Lean.CommandParsedSnapshot) →
                    Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t) →
                  motive_3 t ×' Lean.Language.Lean.CommandParsedSnapshot.below_2 t
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_eq_max_of_aleph0_le_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≠ 0 → a * b = max a b
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_le_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {a : α},
  BddAbove (Set.range f) → (iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a)
-- Init.Prelude
EStateM.instOrElseOfBacktrackable : {ε σ α δ : Type u} → [EStateM.Backtrackable δ σ] → OrElse (EStateM ε σ α)
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
/-- An `R`-algebra `A` is geometrically reduced iff for every prime ideal `p` of R`
the base change to `AlgebraicClosure p.ResidueField` is reduced.  -/
Algebra.IsGeometricallyReduced : (R : Type u_3) → (A : Type u_4) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Prop
-- Lean.Meta.SynthInstance
/-- Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthInstance.main` into an `Expr`.
This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.applyCachedAbstractResult? : Lean.Expr → Option Lean.Meta.AbstractMVarsResult → Lean.MetaM (Option Lean.Expr)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ t.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Iic_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iic ↑a = WithBot.some '' Set.Iic a ∪ {⊥}
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.symm : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → MeasureTheory.AEDisjoint μ t s
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_nil : Lean.Omega.IntList.gcd [] = 0
-- Std.Data.DHashMap.Raw
/-- Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.DHashMap.Raw.Const.unitOfArray : {α : Type u} → [BEq α] → [Hashable α] → Array α → Std.DHashMap.Raw α fun x => Unit
-- Mathlib.CategoryTheory.Sites.Pullback
CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat : ∀ {C : Type v₁} [inst : CategoryTheory.SmallCategory C] {D : Type v₁} [inst_1 : CategoryTheory.SmallCategory D]
  (G : CategoryTheory.Functor C D) (A : Type u₁) [inst_2 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {FA : A → A → Type u_1}
  {CA : A → Type v₁} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA]
  [inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [inst_6 : CategoryTheory.Limits.HasColimits A] [inst_7 : CategoryTheory.Limits.HasLimits A]
  [inst_8 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
  [inst_9 : (CategoryTheory.forget A).ReflectsIsomorphisms] [inst_10 : G.IsContinuous J K]
  [CategoryTheory.RepresentablyFlat G], CategoryTheory.Limits.PreservesFiniteLimits (G.sheafPullback A J K)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.coprod.desc
          (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iU f))
          (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iV f)))
        h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization f) h
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.ofArrowIso_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  {F : CategoryTheory.Limits.MonoFactorisation f.hom} (hF : CategoryTheory.Limits.IsImage F) (sq : f ⟶ g)
  [inst_1 : CategoryTheory.IsIso sq] (F' : CategoryTheory.Limits.MonoFactorisation g.hom),
  (hF.ofArrowIso sq).lift F' = hF.lift (F'.ofArrowIso (CategoryTheory.inv sq))
-- Mathlib.LinearAlgebra.Projection
Submodule.mk_quotientEquivOfIsCompl_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : E ⧸ p), Submodule.Quotient.mk ↑((p.quotientEquivOfIsCompl q h) x) = x
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_of_dvd_of_not_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, a ^ k ∣ b → ¬a ^ (k + 1) ∣ b → emultiplicity a b = ↑k
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) (i : ι), CategoryTheory.CategoryStruct.comp (s.π i) (f i) = s.base
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.forIn_filterMapWithPostcondition.match_1.splitter : {β₂ : Type u_1} →
  (motive : Option β₂ → Sort u_2) →
    (__do_lift : Option β₂) → ((c : β₂) → motive (some c)) → (Unit → motive none) → motive __do_lift
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.funLike : {α : Type u_2} → {β : Type u_3} → [inst : MulZeroOneClass α] → [inst_1 : MulZeroOneClass β] → FunLike (α →*₀ β) α β
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd_hom_app : ∀ {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] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C),
  (CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).hom.app X =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X))
      (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X))
          ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X))))
-- Std.Http.Protocol.H1
/-- Common body-chunk emission helper.

Updates size accounting and reader state, optionally emits `.closeBody`, and
returns an optional pulled chunk (suppressed when body is being internally
drained).
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.emitBodyChunk : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    Std.Http.Protocol.H1.Reader.State dir →
      Bool →
        Bool →
          Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) →
            ByteSlice →
              optParam Bool false → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_quotient_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), Module.supportDim R (R ⧸ I) = ringKrullDim (R ⧸ I)
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.le_iff_le : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S}, v.IsEquiv w → ∀ {x y : R}, v x ≤ v y ↔ w x ≤ w y
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_one_cancel : ∀ {a b : WithBot ℕ∞}, a + 1 = b + 1 ↔ a = b
-- Mathlib.RingTheory.Flat.Basic
/-- If `M` is a flat module, then `f ⊗ 𝟙 M` is injective for all injective linear maps `f`.  -/
Module.Flat.rTensor_preserves_injective_linearMap : ∀ {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] [Module.Flat R M] (f : N →ₗ[R] P),
  Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.cast.eq_1 : ∀ {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d), s.cast hd = { dim := d, simplex := cast ⋯ s.simplex }
-- Init.Data.SInt.Lemmas
Int32.ofInt_lt_iff_lt : ∀ {a b : ℤ},
  Int32.minValue.toInt ≤ a →
    a ≤ Int32.maxValue.toInt →
      Int32.minValue.toInt ≤ b → b ≤ Int32.maxValue.toInt → (Int32.ofInt a < Int32.ofInt b ↔ a < b)
-- Mathlib.Algebra.Category.Ring.Limits
RingCat.hasLimits : CategoryTheory.Limits.HasLimits RingCat
-- Mathlib.Order.Concept
Order.IsExtent.lowerPolar_upperPolar_subset : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s s' : Set α},
  Order.IsExtent r s → s' ⊆ s → lowerPolar r (upperPolar r s') ⊆ s
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.liftAddHom.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {F : Type u_10} [inst_3 : AddCommMonoid F] (φ : R × ((i : ι) → s i) → F)
  (C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0) (C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0)
  (C_add :
    ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
      φ (r, Function.update f i m₁) + φ (r, Function.update f i m₂) = φ (r, Function.update f i (m₁ + m₂)))
  (C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f))
  (C_smul :
    ∀ [inst_4 : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R),
      φ (r, Function.update f i (r' • f i)) = φ (r' * r, f)),
  PiTensorProduct.liftAddHom φ C0 C0' C_add C_add_scalar C_smul =
    (addConGen (PiTensorProduct.Eqv R s)).lift (FreeAddMonoid.lift φ) ⋯
-- Mathlib.RingTheory.Derivation.Basic
Derivation.toFun_eq_coe : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M),
  (↑D).toFun = ⇑D
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_dblZ : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblZ (⇑f ∘ P) = f ((W'.baseChange A).dblZ P)
-- Mathlib.Order.Max
not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a : α), ¬IsMax a
-- Std.Do.SPred.SPred
Std.Do.SPred.bientails_cons : ∀ {σs : List (Type u)} {σ : Type u} {P Q : Std.Do.SPred (σ :: σs)}, (P ⊣⊢ₛ Q) = ∀ (s : σ), P s ⊣⊢ₛ Q s
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_0 : ∀ {R : Type u} [inst : Semiring R], Polynomial.C 0 = 0
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- **Alias** of `Ideal.finite_setOfPred_absNorm_eq`. -/
Ideal.finite_setOf_absNorm_eq : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  [CharZero S] (n : ℕ), {I | Ideal.absNorm I = n}.Finite
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_iff_tendsto_smallSets_nhds : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {S : Set E},
  Bornology.IsVonNBounded 𝕜 S ↔ Filter.Tendsto (fun x => x • S) (nhds 0) (nhds 0).smallSets
-- Mathlib.Dynamics.Minimal
AddAction.dense_orbit : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α] (x : α), Dense (AddAction.orbit M x)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker_fst : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mker (AddMonoidHom.fst M N) = ⊥.prod ⊤
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.pi.eq_1 : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {γ : Type w} [inst_1 : Mul γ] (g : (i : I) → γ →ₙ* f i),
  MulHom.pi g = { toFun := fun x i => (g i) x, map_mul' := ⋯ }
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType : Type
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instAddCommMonoidWithOne : {Γ : Type u_1} →
  {R : Type u_3} →
    [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : AddCommMonoidWithOne R] → AddCommMonoidWithOne (HahnSeries Γ R)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_mul_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R),
  m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f + m.withBotDegree g)
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Mon.forgetMapConeLimitConeIso F c hc).inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Algebra.Order.Monovary
Antivary.mul_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g₁ g₂ : ι → β},
  0 ≤ g₁ → 0 ≤ g₂ → Antivary f g₁ → Antivary f g₂ → Antivary f (g₁ * g₂)
-- Std.Http.Transport
/-- Send all data through the client connection.
 -/
Std.Http.Transport.sendAll : {α : Type} → [self : Std.Http.Transport α] → α → Array ByteArray → Std.Async.Async Unit