mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function which is continuous on a separable set `s` is almost everywhere strongly measurable
with respect to `μ.restrict s`.  -/
ContinuousOn.aestronglyMeasurable_of_isSeparable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α]
  [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α] [inst_3 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
  ContinuousOn f s →
    MeasurableSet s → TopologicalSpace.IsSeparable s → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.Order.Directed
directedOn_image : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : Set β} {f : β → α},
  DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.iInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {W : ι → CategoryTheory.MorphismProperty C}
  [∀ (i : ι), (W i).IsStableUnderComposition], (⨅ i, W i).IsStableUnderComposition
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- `Real.tan` as an `OrderIso` between `(-(π / 2), π / 2)` and `ℝ`.  -/
Real.tanOrderIso : ↑(Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) ≃o ℝ
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteVerts_isLink : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (G : Graph α β) (X : Set α),
  (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AState.mk.injEq : ∀ (generalizations : Array (Lean.Expr × Lean.Expr)) (propToProof : Lean.ExprMap Lean.Expr)
  (generalizations_1 : Array (Lean.Expr × Lean.Expr)) (propToProof_1 : Lean.ExprMap Lean.Expr),
  ({ generalizations := generalizations, propToProof := propToProof } =
      { generalizations := generalizations_1, propToProof := propToProof_1 }) =
    (generalizations = generalizations_1 ∧ propToProof = propToProof_1)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instIsOrderedAddMonoid : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [IsOrderedAddMonoid β], IsOrderedAddMonoid (BoundedContinuousFunction α β)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.instPullback₂Scheme : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  {T : AlgebraicGeometry.Scheme} (f : T ⟶ S),
  AlgebraicGeometry.QuasiCompactCover (CategoryTheory.PreZeroHypercover.pullback₂ f 𝒰)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.apply : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  (f : Module.Dual R V) (v x : V), (LinearMap.transvection f v) x = x + f x • v
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algHom_ext : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {F G : SymmetricAlgebra R M →ₐ[R] A},
  ↑F ∘ₗ SymmetricAlgebra.ι R M = ↑G ∘ₗ SymmetricAlgebra.ι R M → F = G
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α),
  t.getKey? k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k' v l r =>
      match compare k k' with
      | Ordering.lt => l.getKey? k
      | Ordering.gt => r.getKey? k
      | Ordering.eq => some k'
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.unit_mem_mul_comm : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a b : A} {r : Rˣ},
  ↑r ∈ spectrum R (a * b) ↔ ↑r ∈ spectrum R (b * a)
-- Lean.Data.Json.Basic
Lean.Json.Structured.obj.injEq : ∀ (kvPairs kvPairs_1 : Std.TreeMap.Raw String Lean.Json compare),
  (Lean.Json.Structured.obj kvPairs = Lean.Json.Structured.obj kvPairs_1) = (kvPairs = kvPairs_1)
-- Aesop.Options.Internal
Aesop.instInhabitedOptions' : Inhabited Aesop.Options'
-- Mathlib.Analysis.Normed.Group.Basic
pow_mem_ball : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ},
  0 < n → a ∈ Metric.ball b r → a ^ n ∈ Metric.ball (b ^ n) (n • r)
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.recordTheoremWithBadKeys.unsafe_impl_2 : Lean.Meta.SimpTheorem → Lean.Meta.Simp.Diagnostics → Bool
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipBlock : Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ofπ_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b ⟶ P)
  (w :
    ∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst a) (π (J.fst a)) =
        CategoryTheory.CategoryStruct.comp (I.snd a) (π (J.snd a)))
  (x : CategoryTheory.Limits.WalkingMultispan J),
  (CategoryTheory.Limits.Multicofork.ofπ I P π w).ι.app x =
    match x with
    | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.CategoryStruct.comp (I.fst a) (π (J.fst a))
    | CategoryTheory.Limits.WalkingMultispan.right a => π a
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.empty : Aesop.Script.StepTree
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom α.base) x ∈ U) {Z : C} (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom α.base) x) hx)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x) h) =
    CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map α.base).obj U) x hx) h)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Embedding.sum_comp_sumComm : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H'),
  (g.sum f).comp SimpleGraph.Iso.sumComm.toEmbedding = SimpleGraph.Iso.sumComm.toEmbedding.comp (f.sum g)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : SizeOf C] (toPrecoverage : CategoryTheory.Precoverage C)
  (has_isos :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ toPrecoverage.coverings X)
  (pullbacks :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage.coverings Y)
  (transitive :
    ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
      S ∈ toPrecoverage.coverings X →
        (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage.coverings Y) → S.bind Ti ∈ toPrecoverage.coverings X),
  sizeOf { toPrecoverage := toPrecoverage, has_isos := has_isos, pullbacks := pullbacks, transitive := transitive } =
    1 + sizeOf toPrecoverage
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) h_1))
-- Aesop.Search.Expansion
Aesop.runRegularRuleTac : Aesop.Goal →
  Aesop.RuleTac →
    Aesop.RuleName →
      Array Aesop.IndexMatchLocation →
        Option (Array Aesop.Substitution) → Aesop.Options' → Aesop.BaseM (Except Lean.Exception Aesop.RuleTacOutput)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β},
  MeasureTheory.MemLp f 1 μ →
    ∀ {ε : ℝ}, 0 < ε → ∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.kind? : Lean.Lsp.InlayHint → Option Lean.Lsp.InlayHintKind
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instTransOrd : Std.TransOrd Std.Time.Weekday
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendScalars_δ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat R),
  CategoryTheory.Functor.OplaxMonoidal.δ (ModuleCat.extendScalars f) M₁ M₂ =
    ModuleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R S ↑M₁ ↑M₂)
-- Mathlib.Data.Sigma.Order
Sigma.LE.fiber : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] (i : ι) (a b : α i), a ≤ b → ⟨i, a⟩.LE ⟨i, b⟩
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceXor : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Fractional operation is symmetric.  -/
FractionalOperation.IsSymmetric : {D : Type u_1} → {m : ℕ} → FractionalOperation D m → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_zero : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S), f 0 = 0
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphUnitSphereProd_apply_snd_coe : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : ↑{0}ᶜ),
  ↑((homeomorphUnitSphereProd E) x).2 = ‖↑x‖
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.mk : Lean.Ident →
  Option Lean.ConstructorVal →
    Bool →
      Bool →
        Array (Lean.Name × Lean.BinderInfo) →
          ℕ →
            Array Lean.Elab.Term.NamedArg →
              Std.HashSet Lean.Name →
                List Lean.Elab.Term.Arg → Array Lean.Term → Lean.Elab.Term.CollectPatternVars.Context
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_of_countable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {s : L.Substructure M} [h : Countable ↥s], s.CG
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.h₀_assoc : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (self : f.Homotopy g) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₀ (CategoryTheory.CategoryStruct.comp self.h h) =
    CategoryTheory.CategoryStruct.comp f.map h
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.charFn.eq_1 : ∀ {X : Type u_1} (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : MulZeroOneClass Y] {U : Set X} (hU : IsClopen U),
  LocallyConstant.charFn Y hU = LocallyConstant.indicator 1 hU
-- Mathlib.Geometry.Manifold.Instances.Real
modelWithCornersEuclideanHalfSpace_zero : ∀ {n : ℕ} [inst : NeZero n], ↑(modelWithCornersEuclideanHalfSpace n) 0 = 0
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Taking a product over `f : α →₀ M` is the same as multiplying the value on a single element
`y ∈ f.support` by the product over `erase y f`.  -/
Finsupp.mul_prod_erase : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) (y : α)
  (g : α → M → N), y ∈ f.support → g y (f y) * (Finsupp.erase y f).prod g = f.prod g
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_inter_support_eq' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s t : Set α),
  (∀ x ∈ Function.support f, x ∈ s ↔ x ∈ t) → ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.contains_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.contains k = t₂.contains k
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A set in a σ-finite space has zero measure if and only if its intersection with
all members of the countable family of finite measure spanning sets has zero measure.  -/
MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ]
  (s : Set α), (∀ (n : ℕ), μ (s ∩ MeasureTheory.spanningSets μ n) = 0) ↔ μ s = 0
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given an expression `e : Q($M)`, construct an expression which is morally "± `e`", with the
choice between + and - determined by an object `g : Sign M`.  -/
Mathlib.Tactic.FieldSimp.Sign.expr : {v : Lean.Level} → {M : Q(Type v)} → Mathlib.Tactic.FieldSimp.Sign M → Q(«$M») → Q(«$M»)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↥X) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (X.evaluation U x hx)) f = 0 ↔ x ∉ X.basicOpen f
-- Mathlib.Data.Stream.Init
Stream'.get_tails : ∀ {α : Type u} (n : ℕ) (s : Stream' α), s.tails.get n = Stream'.drop n s.tail
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_4 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f fs : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont') (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.cons fs, k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_4 f fs k
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from variables to their "upper" bounds. We say a relational constraint `c` is a upper bound for a variable `x`
if `x` is the maximal variable in `c`, and `x` coefficient in `c` is positive.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.uppers : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr)
-- Mathlib.Algebra.FiniteSupport.Defs
Function.HasFiniteSupport.eq_1 : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), Function.HasFiniteSupport f = (Function.support f).Finite
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.idealOrderIsoENat_symm_apply_coe_of_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (n : ℕ) {ϖ : R},
  Irreducible ϖ → (IsDiscreteValuationRing.idealOrderIsoENat R).symm ↑n = Ideal.span {ϖ ^ n}
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addCommMonoid.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddCommMonoid G] [inst_10 : TopologicalSpace G]
  [inst_11 : ChartedSpace H' G] [inst_12 : ContMDiffAdd I' n G],
  ContMDiffMap.addCommMonoid = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Order.Hom.Ring
/-- Reinterpret an ordered ring homomorphism as an order homomorphism.  -/
OrderRingHom.toOrderMonoidWithZeroHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → α →+*o β → α →*₀o β
-- Std.Internal.Parsec.ByteArray
/-- Convert a byte representing `'0'..'9'` to a `Nat`.
 -/
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.digitToNat : UInt8 → ℕ
-- Mathlib.LinearAlgebra.FreeModule.Norm
/-- For a nonzero element `f` in a `F[X]`-module `S`, the dimension of $S/\langle f \rangle$ as an
`F`-vector space is the degree of the norm of `f` relative to `F[X]`.  -/
finrank_quotient_span_eq_natDegree_norm : ∀ {S : Type u_2} {ι : Type u_3} [inst : CommRing S] [IsDomain S] {F : Type u_4} [inst_2 : Field F]
  [inst_3 : Algebra (Polynomial F) S] [Finite ι] [inst_5 : Algebra F S] [IsScalarTower F (Polynomial F) S]
  (b : Module.Basis ι (Polynomial F) S) {f : S},
  f ≠ 0 → Module.finrank F (S ⧸ Ideal.span {f}) = ((Algebra.norm (Polynomial F)) f).natDegree
-- Mathlib.Analysis.Convex.Between
affineSegment_subset_affineSpan : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), affineSegment R x y ⊆ ↑line[R, x, y]
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The forgetful functor from the full subcategory of `Comma L R` defined by `P` is
fully faithful.  -/
CategoryTheory.MorphismProperty.Comma.forgetFullyFaithful : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (P : CategoryTheory.MorphismProperty T) →
                  (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤).FullyFaithful
-- Std.Http.Data.URI.Config
/-- Maximum total byte length of the path (all segments combined, including separating slashes).
 -/
Std.Http.URI.Config.maxTotalPathLength : Std.Http.URI.Config → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The intersection of two subgraphs.  -/
SimpleGraph.Subgraph.instMin : {V : Type u} → {G : SimpleGraph V} → Min G.Subgraph
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.instInhabited : (α : Type u_2) → [inst : Preorder α] → [inst_1 : Mul α] → Inhabited (α ≃*o α)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_ae : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    MeasurableSet t →
      (∀ᵐ (x : X) ∂μ.variation.restrict t, f x = 0) → ∫ᵛ (x : X) in s ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.shortestPrefixDiff_pos : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)}, IsClosed s → s.Nonempty → ∀ {x : (n : ℕ) → E n}, x ∉ s → 0 < PiNat.shortestPrefixDiff x s
-- Mathlib.RingTheory.PicardGroup
/-- Every ring homomorphism between commutative semirings induces a homomorphism between
Picard groups.  -/
CommRing.Pic.mapRingHom : {R : Type u} →
  [inst : CommSemiring R] → {S : Type u_7} → [inst_1 : CommSemiring S] → (R →+* S) → CommRing.Pic R →* CommRing.Pic S
-- Mathlib.NumberTheory.PrimeCounting
Nat.notMem_primesBelow : ∀ (n : ℕ), n ∉ n.primesBelow
-- Std.Time.Zoned.RecurringRule
/-- Standard UTC offset (east-positive).
 -/
Std.Time.TimeZone.RecurringRule.stdOffset : Std.Time.TimeZone.RecurringRule → Std.Time.TimeZone.Offset
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblU_ne_zero_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.dblU P ≠ 0
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesLimitsOfSize0.createsFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedDoOps : Inhabited Lean.Elab.Do.DoOps
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_univ : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : ConditionallyCompleteLattice ι] {u : ι → Ω → β} (n : ι),
  MeasureTheory.hittingAfter u Set.univ n = fun x => ↑n
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- An ideal consisting of zero divisors in a commutative Noetherian ring is annihilated by
some nonzero element. This is not true in general for finitely generated modules in commutative
rings, see https://math.stackexchange.com/q/1189814 and http://dx.doi.org/10.2140/pjm.1979.83.375
(keywords: Property (A), Quentel's Condition (C)).

It is also not true that every finitely generated module over every commutative Noetherian ring
is annihilated by some nonzero element if each element is annihilated by some nonzero element,
see https://math.stackexchange.com/a/3187153.  -/
Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors : ∀ {A : Type u} [inst : CommRing A] [IsNoetherianRing A] {I : Ideal A},
  Disjoint ↑I ↑(nonZeroDivisors A) → ⊥ < Module.annihilator A ↥I
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt.eq_1 : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D),
  L.HasPointwiseLeftKanExtensionAt F Y =
    CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Monotone.image_uIcc_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  Monotone f → f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonName : Lean.ToJson Lean.Name
-- Init.Prelude
Nat.not_le_of_not_ble_eq_true : ∀ {n m : ℕ}, ¬n.ble m = true → ¬n ≤ m
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.union : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s ≤ᶠ[l] t → s' ≤ᶠ[l] t' → s ∪ s' ≤ᶠ[l] t ∪ t'