mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The map on `FunSpace` defined by `picard`, some `n`-th iterate of which will be a contracting
map  -/
ODE.FunSpace.next : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      {f : ℝ → E → E} →
        {tmin tmax : ℝ} →
          {t₀ : ↑(Set.Icc tmin tmax)} →
            {x₀ x : E} →
              {a r L K : NNReal} →
                IsPicardLindelof f t₀ x₀ a r L K →
                  x ∈ Metric.closedBall x₀ ↑r → ODE.FunSpace t₀ x₀ r L → ODE.FunSpace t₀ x₀ r L
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- Alternative version of `domRestrict` as a linear map.  -/
LinearMap.domRestrict' : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → (p : Submodule R M) → (M →ₗ[R] M₂) →ₗ[R] ↥p →ₗ[R] M₂
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.homologyMap_mapNatTrans : ∀ {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] (S : CategoryTheory.ShortComplex C)
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  [inst_6 : F.PreservesLeftHomologyOf S] [inst_7 : G.PreservesLeftHomologyOf S] [inst_8 : F.PreservesRightHomologyOf S]
  [inst_9 : G.PreservesRightHomologyOf S] [inst_10 : S.HasHomology] (τ : F ⟶ G),
  CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ) =
    CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).hom
      (CategoryTheory.CategoryStruct.comp (τ.app S.homology) (S.mapHomologyIso G).inv)
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a non-trivial additive group is one more than its quotient
by the center  -/
AddGroup.nilpotencyClass_eq_quotient_center_plus_zero : ∀ {G : Type u_1} [inst : AddGroup G] [hH : AddGroup.IsNilpotent G] [Nontrivial G],
  AddGroup.nilpotencyClass G = AddGroup.nilpotencyClass (G ⧸ AddSubgroup.center G) + 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).i = CategoryTheory.CategoryStruct.id S.X₂
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reset.inj : ∀ {n : ℕ} {x : Lean.IR.VarId} {n_1 : ℕ} {x_1 : Lean.IR.VarId},
  Lean.IR.Expr.reset n x = Lean.IR.Expr.reset n_1 x_1 → n = n_1 ∧ x = x_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {W : D} (k : G.obj Y ⟶ W)
  (wk : CategoryTheory.CategoryStruct.comp (G.map f) k = CategoryTheory.CategoryStruct.comp (G.map g) k),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv
        (CategoryTheory.Limits.coequalizer.desc k wk)) =
    k
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) {X Y : CategoryTheory.Discrete PUnit.{w + 1}} (x : X ⟶ Y),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).map x = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_def : ∀ {α : Type u_1} [inst : PartialOrder α] (s : NonemptyInterval α), ↑s = Set.Icc s.toProd.1 s.toProd.2
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivWithinAt.const_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E} {c : ℝ},
  HasFDerivWithinAt f f' s x → 0 < c → HasFDerivWithinAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') s x
-- Init.Data.List.Lemmas
List.tail_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsContained.maxDegree_mono : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj], G.IsContained H → G.maxDegree ≤ H.maxDegree
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasBiproduct_unique : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [Subsingleton J] [Nonempty J] (f : J → C),
  CategoryTheory.Limits.HasBiproduct f
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.affineCombination_toFun : ∀ {𝕜 : 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] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] (cov cov' : CovariantDerivative I F V)
  (g : M → 𝕜) (σ : (x : M) → V x) (x : M), ↑(cov.affineCombination cov' g) σ x = (g • ↑cov σ + (1 - g) • ↑cov' σ) x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_pow : ∀ {R : Type u} [inst : Semiring R] (a : Polynomial R) (n : ℕ), (a ^ n).toFinsupp = a.toFinsupp ^ n
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_cons_div_right' : ∀ {x : ℤ} {xs : List ℤ}, ↑(Lean.Omega.IntList.gcd (x :: xs)) ∣ ↑(Lean.Omega.IntList.gcd xs)
-- Std.Http.Internal.Char
/-- Checks if a byte is a valid character in a URI query component,
excluding the typical key/value separators `&` and `=`.

Inspired by `query = *( pchar / "/" / "?" )` from RFC 3986,
but disallows `&` and `=` so they can be treated as structural separators.
 -/
Std.Http.Internal.Char.isQueryDataChar : UInt8 → Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_eq_getKey! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α} {h' : a ∈ m}, m.getKey a h' = m.getKey! a
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Sum of a list of elements in a subfield is in the subfield.  -/
Subfield.list_sum_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {l : List K}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.instMonoidalCategory.tensorObj_carrier : ∀ {R : Type u} [inst : CommRing R] (X Y : AlgCat R),
  ↑(AlgCat.instMonoidalCategory.tensorObj X Y) = TensorProduct R ↑X ↑Y
-- Mathlib.Order.Heyting.Basic
compl_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α], ⊥ᶜ = ⊤
-- Std.Internal.Parsec.String
Std.Internal.Parsec.String.instInputSigmaStringPosCharRaw : Std.Internal.Parsec.Input (Sigma String.Pos) Char String.Pos.Raw
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isPlot_id' : ∀ {n : ℕ}, Diffeology.IsPlot fun x => x
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.mk.sizeOf_spec : ∀ {α : Type w} [inst : SizeOf α] (list : List α), sizeOf { list := list } = 1 + sizeOf list
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) {n : ℕ} (y₁ : ↑(F.H' n S.X₂)) (y₂ : ↑(F.H' n S.X₃)),
  (CategoryTheory.ConcreteCategory.hom (S.fromBiprod F n))
      ((CategoryTheory.ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (y₁, y₂)) =
    (CategoryTheory.ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₂.op)) y₁ -
      (CategoryTheory.ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₃.op)) y₂
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.snd = AddMonoid.Coprod.lift 0 (AddMonoidHom.id N)
-- Mathlib.Topology.Inseparable
/-- **Alias** of the forward direction of `specializes_iff_nhds`. -/
Specializes.nhds_le_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → nhds x ≤ nhds y
-- Mathlib.Data.Matrix.Mul
Matrix.instMulOneOfFintypeOfDecidableEqOfAddCommMonoid : {n : Type u_3} → {α : Type v} → [Fintype n] → [DecidableEq n] → [MulOne α] → [AddCommMonoid α] → MulOne (Matrix n n α)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of
`ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exist `r`
such that `x = (-ζ)^r`.  -/
IsPrimitiveRoot.exists_neg_pow_of_isOfFinOrder : ∀ {n : ℕ} [NeZero n] {K : Type u} [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {n} ℚ K],
  Odd n → ∀ {ζ x : K}, IsPrimitiveRoot ζ n → IsOfFinOrder x → ∃ r, x = (-ζ) ^ r
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A product of meromorphic functions in normal form is in normal form if at most one of the factors
vanishes.
 -/
meromorphicNFAt_fun_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜},
  (∀ i ∈ s, MeromorphicNFAt (f i) x) →
    {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton → MeromorphicNFAt (fun a => ∏ i ∈ s, f i a) x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.induce_union_connected : ∀ {V : Type u} {G : SimpleGraph V} {s t : Set V},
  (SimpleGraph.induce s G).Preconnected →
    (SimpleGraph.induce t G).Preconnected → (s ∩ t).Nonempty → (SimpleGraph.induce (s ∪ t) G).Connected
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.comp_continuousLinearEquivalence : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] [inst_7 : TopologicalSpace F'] [inst_8 : AddCommMonoid F'] [inst_9 : Module R F']
  {f : E →L[R] F} {f₀ : F' ≃L[R] E}, f.HasLeftInverse → (f ∘SL ↑f₀).HasLeftInverse
-- Mathlib.Topology.SmallInductiveDimension
/-- The small inductive dimension of a topological space.  -/
smallInductiveDimension : (X : Type u_1) → [TopologicalSpace X] → WithBot ℕ∞
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- Given two adjunctions `L₁ ⊣ R₁` and `L₂ ⊣ R₂` both between categories `C`, `D`, there is a
bijection between natural transformations `L₂ ⟶ L₁` and natural transformations `R₁ ⟶ R₂`. This is
defined as a special case of `mateEquiv`, where the two "vertical" functors are identity, modulo
composition with the unitors. Corresponding natural transformations are called `conjugateEquiv`.
TODO: Generalise to when the two vertical functors are equivalences rather than being exactly `𝟭`.

Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a transformation is an iso
iff its image under the bijection is an iso, see e.g. `CategoryTheory.conjugateIsoEquiv`.
This is in contrast to the general case `mateEquiv` which does not in general have this property.
 -/
CategoryTheory.conjugateEquiv : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L₁ L₂ : CategoryTheory.Functor C D} →
          {R₁ R₂ : CategoryTheory.Functor D C} → (L₁ ⊣ R₁) → (L₂ ⊣ R₂) → (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂)
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
/-- Left multiplication by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type.  -/
Equiv.mulLeft₀ : {G₀ : Type u_1} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → Equiv.Perm G₀
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.zabbrev : Std.Time.GenericFormat.DateBuilder✝ → Option String
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp e.inv.base e.hom.base = CategoryTheory.CategoryStruct.id ↑Y.toPresheafedSpace
-- Init.Data.Rat.Lemmas
Rat.ceil_add_intCast_le_ceil_add : ∀ {x : ℚ} {y : ℤ}, (x + ↑y).ceil ≤ x.ceil + y
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_one : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  [inst_11 : One M'], ContMDiff I I' n 1
-- Mathlib.Topology.Path
/-- The reverse of a path from `x` to `y`, as a path from `y` to `x`  -/
Path.symm : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Path x y → Path y x
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.consumerNode.sizeOf_spec : ∀ (a : Lean.Meta.SynthInstance.ConsumerNode), sizeOf (Lean.Meta.SynthInstance.Waiter.consumerNode a) = 1 + sizeOf a
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Any free group is isomorphic to "the" free group.  -/
IsFreeGroup.mulEquiv : (G : Type u_2) → [inst : Group G] → [inst_1 : IsFreeGroup G] → FreeGroup (IsFreeGroup.Generators G) ≃* G
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The categorical data that is involved in a `1`-hypercover of an object `S`. This
consists of a family of morphisms `f i : X i ⟶ S` for `i : I₀`, and for each
tuple `(i₁, i₂)` of elements in `I₀`, a family of objects `Y j` indexed by
a type `I₁ i₁ i₂`, which are equipped with a map to the fibre product of `X i₁`
and `X i₂`, which is phrased here as the data of the two projections
`p₁ : Y j ⟶ X i₁`, `p₂ : Y j ⟶ X i₂` and the relation `p₁ j ≫ f i₁ = p₂ j ≫ f i₂`.
(See `GrothendieckTopology.OneHypercover` for the topological conditions.)  -/
CategoryTheory.PreOneHypercover : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type (max (max u v) (w + 1))
-- Init.Data.Nat.Lemmas
Nat.lt_div_mul_add : ∀ {a b : ℕ}, 0 < b → a < a / b * b + b
-- Lean.Server.Snapshots
/-- Use the command state in the given snapshot to run a `CommandElabM`. -/
Lean.Server.Snapshots.Snapshot.runCommandElabM : {α : Type} →
  Lean.Server.Snapshots.Snapshot → Lean.Server.DocumentMeta → Lean.Elab.Command.CommandElabM α → EIO Lean.Exception α
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq pq' : κ) (hpq : (c r₀).Rel pq pq')
  (i j k : ι) (hi : i = data.i₁ pq') (hj : j = data.i₁ pq) (hk : k = data.i₂ pq) (n n' : ℤ) (hn : n = data.deg pq)
  (hn' : autoParam (n + 1 = n') CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq._auto_1),
  ((X.spectralSequence data).page r₀ ⋯).d pq pq' =
    CategoryTheory.CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom
      (CategoryTheory.CategoryStruct.comp (X.δ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n n' hn')
        (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv)
-- Mathlib.Algebra.Ring.Associator
associator_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (x y z : R), associator x y z = x * y * z - x * (y * z)
-- Mathlib.MeasureTheory.Measure.Regular
/-- Given a weakly regular measure, any measurable set of finite mass can be approximated from
inside by closed sets.  -/
MeasurableSet.exists_lt_isClosed_of_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] ⦃A : Set α⦄, MeasurableSet A → μ A ≠ ⊤ → ∀ {r : ENNReal}, r < μ A → ∃ K ⊆ A, IsClosed K ∧ r < μ K
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  PolynomialModule.coeff 0 = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_ofList_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.DHashMap.Raw.Const.ofList l).size ≤ l.length
-- Mathlib.Tactic.Ring.Common
/-- The data used by `ring` to represent coefficients. `e` is a raw rat cast.

We include `e` as a parameter even though it is unused in this definition because it lets us use
`Qq` type annotations in the `RingCompute` structure, and so that it can be used with the `Result`
type defined below.
 -/
Mathlib.Tactic.Ring.RatCoeff : {u : Lean.Level} → {α : Q(Type u)} → Q(«$α») → Type
-- Mathlib.Data.Set.Card
Set.ncard_singleton_inter : ∀ {α : Type u_1} (a : α) (s : Set α), ({a} ∩ s).ncard ≤ 1
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.float : Lean.IR.IRType
-- Mathlib.LinearAlgebra.Trace
/-- If `S` is an `R-algebra that is free of rank `1` over `R`, the map `R →+* S` is an
isomorphism.  -/
Module.Free.bijective_algebraMap_of_finrank_eq_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Nontrivial R]
  [Module.Free R S], Module.finrank R S = 1 → Function.Bijective ⇑(algebraMap R S)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_ne_zero : ∀ {x : ℝ}, 0 ≤ x → (√x ≠ 0 ↔ x ≠ 0)
-- Mathlib.Algebra.Lie.Ideal
instBracketSubtypeMemLieIdeal : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → Bracket ↥I ↥I
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- Composing the right Kan extension of `L : C ⥤ D` with `lim` on shapes `D` is isomorphic
to `lim` on shapes `C`.  -/
CategoryTheory.Functor.ranCompLimIso : {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] →
        {H : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
            (L : CategoryTheory.Functor C D) →
              [inst_3 : ∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] →
                [inst_4 : CategoryTheory.Limits.HasLimitsOfShape C H] →
                  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape D H] →
                    L.ran.comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a b : α), UpperSet.Ici (a ⊔ b) = UpperSet.Ici a ⊔ UpperSet.Ici b
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Std.Total.trichotomous`. -/
Std.Total.isTrichotomous : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r], Std.Trichotomous r
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {g : PseudoEpimorphism β γ} {f₁ f₂ : PseudoEpimorphism α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Data.Multiset.Defs
Multiset.coe_pmap : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ a ∈ l, p a),
  Multiset.pmap f (↑l) H = ↑(List.pmap f l H)
-- Init.Data.Option.Attach
Option.pbind_eq_bind_attach : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  o.pbind f =
    o.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ => f x h
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec'_zero : ∀ {motive : ℕ → Sort u} (zero : motive 0)
  (bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)), Nat.binaryRec' zero bit 0 = zero
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inr_comp_pushoutSymmetry_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushoutSymmetry f g).hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl g f)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.equivRealProdLm_symm_apply : ∀ (p : ℝ × ℝ), Complex.equivRealProdLm.symm p = ↑p.1 + ↑p.2 * Complex.I
-- Mathlib.Algebra.Group.Action.Faithful
smul_left_injective' : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [FaithfulSMul M α], Function.Injective fun x1 x2 => x1 • x2
-- Mathlib.Topology.ContinuousOn
Function.LeftInverse.map_nhds_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {g : β → α}
  {x : β},
  Function.LeftInverse f g →
    ContinuousWithinAt f (Set.range g) (g x) → ContinuousAt g x → Filter.map g (nhds x) = nhdsWithin (g x) (Set.range g)
-- Init.Data.Nat.Div.Basic
Nat.div_eq_sub_div : ∀ {b a : ℕ}, 0 < b → b ≤ a → a / b = (a - b) / b + 1
-- Mathlib.RingTheory.Filtration
/-- The `inf` of two `I.Filtration`s is an `I.Filtration`.  -/
Ideal.Filtration.instMin : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → Min (I.Filtration M)
-- Mathlib.Order.Hom.Bounded
/-- Composition of `BotHom`s as a `BotHom`.  -/
BotHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Bot α] → [inst_1 : Bot β] → [inst_2 : Bot γ] → BotHom β γ → BotHom α β → BotHom α γ
-- Mathlib.LinearAlgebra.Determinant
LinearMap.equivOfIsUnitDet_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] {f : M →ₗ[R] M} (h : IsUnit (LinearMap.det f)) (x : M),
  (LinearMap.equivOfIsUnitDet h) x = f x
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.continuous : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F}, HasFTaylorSeriesUpTo n f p → Continuous f