mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.mk.inj : ∀ {R : Type u} {S : Type u₁} {inst : Monoid R} {inst_1 : Monoid S} {φ : R →* S} {A : Type v} {B : Type w}
  {inst_2 : NonUnitalNonAssocSemiring A} {inst_3 : DistribMulAction R A} {inst_4 : NonUnitalNonAssocSemiring B}
  {inst_5 : DistribMulAction S B} {toDistribMulActionHom : A →ₑ+[φ] B}
  {map_mul' :
    ∀ (x y : A), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y}
  {toDistribMulActionHom_1 : A →ₑ+[φ] B}
  {map_mul'_1 :
    ∀ (x y : A),
      toDistribMulActionHom_1.toFun (x * y) = toDistribMulActionHom_1.toFun x * toDistribMulActionHom_1.toFun y},
  { toDistribMulActionHom := toDistribMulActionHom, map_mul' := map_mul' } =
      { toDistribMulActionHom := toDistribMulActionHom_1, map_mul' := map_mul'_1 } →
    toDistribMulActionHom = toDistribMulActionHom_1
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is lower semicontinuous at `x` within a set `s` if, for any `ε > 0`, for all
`x'` close enough to `x` in `s`, then `f x'` is at least `f x - ε`. We formulate this in a general
preordered space, using an arbitrary `y < f x` instead of `f x - ε`.  -/
LowerSemicontinuousWithinAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → α → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.strictMono_leastExt : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E],
  StrictMono (Field.Emb.Cardinal.leastExt F E)
-- Mathlib.Data.List.Permutation
List.mem_foldr_permutationsAux2 : ∀ {α : Type u_1} {t : α} {ts : List α} {r L : List (List α)} {l' : List α},
  l' ∈ List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompAssociator_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : C ⊕ D),
  (CategoryTheory.sum.inlCompAssociator C D E).hom.app X =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Sum.inl_ C (D ⊕ E)).sum'
            ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))).obj
        X)
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The standard etale algebra `R[X][Y]/⟨f, Yg-1⟩` associated to a `StandardEtalePair R`.
Also see
`equivPolynomialQuotient   : P.Ring ≃ R[X][Y]/⟨f, Yg-1⟩`
`equivAwayAdjoinRoot       : P.Ring ≃ (R[X]/f)[1/g]`
`equivAwayQuotient         : P.Ring ≃ R[X][1/g]/f`
`equivMvPolynomialQuotient : P.Ring ≃ R[X, Y]/⟨f, Yg-1⟩`  -/
StandardEtalePair.Ring : {R : Type u_1} → [inst : CommRing R] → StandardEtalePair R → Type u_1
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instMembershipOfBEqOfHashable : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Membership α (Std.DHashMap.Raw α β)
-- Lean.Util.CollectLevelParams
_private.Lean.Util.CollectLevelParams.0.Lean.CollectLevelParams.State.getUnusedLevelParam.loop : Lean.CollectLevelParams.State → Lean.Name → ℕ → Lean.Level
-- Init.Data.SInt.Lemmas
Int8.le_of_lt : ∀ {a b : Int8}, a < b → a ≤ b
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F) (n : ℕ)
  (α : A₁ ⟶ A₂), (n • α).f = n • α.f
-- Mathlib.Data.Setoid.Partition
IndexedPartition.piecewise_apply : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} {f : ι → α → β} (x : α),
  hs.piecewise f x = f (hs.index x) x
-- Mathlib.RingTheory.SimpleModule.Basic
Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M}
  (R₀ : Type u_6) (P : Type u_7) [inst_3 : Semiring R₀] [inst_4 : AddCommMonoid P] [inst_5 : Module R P]
  [inst_6 : Module R₀ P] [inst_7 : SMulCommClass R R₀ P] [Module.Finite R₀ (M →ₗ[R] P)] [IsSemisimpleModule R M],
  Module.Finite R₀ (↥m →ₗ[R] P)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_η_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal] {Z : C}
  (h : (F.obj n).obj ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor n).hom).app X) h)
-- Mathlib.Analysis.Fourier.AddCircle
fourier_coe_apply' : ∀ {T : ℝ} {n : ℤ} {x : ℝ}, ↑(AddCircle.toCircle (n • ↑x)) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x / ↑T)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.neg_point : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point), (-P).point = W.negMap P.point
-- Mathlib.Algebra.GroupWithZero.Basic
instIsDedekindFiniteMonoidOfIsRightCancelMulZero : ∀ {M₀ : Type u_3} [inst : MonoidWithZero M₀] [IsRightCancelMulZero M₀], IsDedekindFiniteMonoid M₀
-- Mathlib.Order.Types.Arithmetic
OrderType.card_zero : OrderType.card 0 = 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_left_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Almost non-definitionally equal to `normalizeIsoApp`, but has a better definitional property
in the proof of `normalize_naturality`.  -/
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' : (C : Type u) →
  (X : CategoryTheory.FreeMonoidalCategory C) →
    (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.FreeMonoidalCategory.inclusionObj n) X ≅
        CategoryTheory.FreeMonoidalCategory.inclusionObj (X.normalizeObj n)
-- Mathlib.Topology.NhdsSet
bUnion_mem_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {t : X → Set X},
  (∀ x ∈ s, t x ∈ nhds x) → ⋃ x ∈ s, t x ∈ nhdsSet s
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Monoid α] [inst_2 : AddGroup β]
  [inst_3 : DistribMulAction α β] (a : α) (t : Finset β), a • -t = -(a • t)
-- Mathlib.Data.Nat.Log
Nat.clog_mono : ∀ {b c m n : ℕ}, 1 < c → c ≤ b → m ≤ n → Nat.clog b m ≤ Nat.clog c n
-- Std.Http.Data.Request
/-- Creates a new HTTP OPTIONS Request builder with the specified URI.
Use `Request.options (RequestTarget.asteriskForm)` for server-wide OPTIONS.
 -/
Std.Http.Request.options : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.Data.Sym.Sym2
Sym2.fromRelNdrec_mk : ∀ {α : Type u_1} {r : α → α → Prop} {motive : Sort u_4} {sym : Std.Symm r} {a b : α} (hz : r a b)
  (f : (a b : α) → r a b → motive) (h : ∀ (a b : α) (h : r a b), f a b h = f b a ⋯),
  Sym2.fromRelNdrec s(a, b) hz f h = f a b hz
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.apply_comp_inclusion : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {T S_1 : E →ₛₗ.[σ] F}
  (h : T ≤ S_1) (x : ↥T.domain), ↑T x = ↑S_1 ((Submodule.inclusion ⋯) x)
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.zeroLocus_singleton : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))), X.zeroLocus {f} = (X.basicOpen f).carrierᶜ
-- Mathlib.Algebra.Group.Defs
three'_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 3 • a = a + a + a
-- Lean.Parser.Syntax
Lean.Parser.Syntax.nonReserved.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_hom_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom.app X_1).snd.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj X_2)
-- Mathlib.GroupTheory.Congruence.Defs
Con.gi.eq_1 : ∀ (M : Type u_1) [inst : Mul M], Con.gi M = { choice := fun r x => conGen r, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- For natural numbers `n`, the proximity function of `f ^ n` at `0` equals `n` times the proximity
function of `f` at `0`.
 -/
ValueDistribution.proximity_pow_zero : ∀ {f : ℂ → ℂ} {n : ℕ}, ValueDistribution.proximity (f ^ n) 0 = n • ValueDistribution.proximity f 0
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.nonneg_of_isNat' : ∀ {A : Type u_1} {e : A} {n : ℕ} [inst : AddMonoidWithOne A] [inst_1 : PartialOrder A] [AddLeftMono A]
  [ZeroLEOneClass A], Mathlib.Meta.NormNum.IsNat e n → 0 ≤ e
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.μ_bddAbove : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 →
    ∀ {s : ℕ → ℕ},
      (∀ (n : ℕ), s n ≤ n) → ∀ (x : R) (ψ : ℕ → ℕ), BddAbove (Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- The weak pullback cone built from the weak pullback projections is a weak pullback.  -/
CategoryTheory.Limits.weakPullbackIsWeakPullback : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] →
            CategoryTheory.Limits.IsWeakLimit
              (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.weakPullback.fst f g)
                (CategoryTheory.Limits.weakPullback.snd f g) ⋯)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.Handler : Type
-- Init.Data.List.Lemmas
List.partition.loop.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as bs cs : List α),
  List.partition.loop p (a :: as) (bs, cs) =
    match p a with
    | true => List.partition.loop p as (a :: bs, cs)
    | false => List.partition.loop p as (bs, a :: cs)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_mul_one_sub_succ : ∀ {F : Type u_1} [inst : Field F] [CharZero F] (p : Polynomial F) (d : ℕ),
  (p * (1 - Polynomial.X)).hilbertPoly (d + 1) = p.hilbertPoly d
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- Construct a `Mor₂` term from a Lean expression.  -/
Mathlib.Tactic.Bicategory.Mor₂OfExpr : Lean.Expr → Mathlib.Tactic.Bicategory.BicategoryM Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Data.Seq.Computation
/-- Assertion that a `Computation` limits to a given value  -/
Computation.Mem : {α : Type u} → Computation α → α → Prop
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp_bitVecToInt : ∀ (n : BitVec 64), Int64.ofIntClamp n.toInt = Int64.ofBitVec n
-- Lean.Meta.SizeOf
/-- Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName`
The resulting array contains the generated functions names. The `NameMap` maps recursor names into the generated function names.
There is a function for each element of the mutual inductive declaration, and for auxiliary recursors for nested inductive types.
 -/
Lean.Meta.mkSizeOfFns : Lean.Name → Lean.MetaM (Array Lean.Name × Lean.NameMap Lean.Name)
-- Mathlib.Algebra.Lie.SkewAdjoint
/-- Given an `R`-module `M`, equipped with a bilinear form, the skew-adjoint endomorphisms form a
Lie subalgebra of the Lie algebra of endomorphisms.  -/
skewAdjointLieSubalgebra : {R : Type u} →
  {M : Type v} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → LieSubalgebra R (Module.End R M)
-- Mathlib.Order.Basic
forall_gt_imp_ne_iff_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a < c → c ≠ b) ↔ b ≤ a
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_eqOn_left : ∀ {𝕜 : 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} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), Set.EqOn (↑hf.localInverse.toPartialEquiv ∘ f) id hf.localInverse.target
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`.  -/
BitVec.reduceGetMsb : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.replaceUniformity_eq : ∀ {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α),
  m.replaceUniformity H = m
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.isCancelMulZero_iff : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α], IsCancelMulZero αᵐᵒᵖ ↔ IsCancelMulZero α
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_sSup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s : Set (Submodule R M)} {m : M}, m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.altViews : Lean.Elab.Term.GeneralizeResult → Array Lean.Elab.Term.TermMatchAltView
-- Mathlib.Topology.Constructions
instCompactSpaceMultiplicative : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X], CompactSpace (Multiplicative X)
-- Std.Internal.Do.Order.PreservesSup
/-- A right adjoint is monotone.  -/
Lean.Order.PreservesSup.upperAdjoint_mono : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (f : α → α) [Lean.Order.PreservesSup f] {b b' : α},
  Lean.Order.PartialOrder.rel b b' →
    Lean.Order.PartialOrder.rel (Lean.Order.PreservesSup.upperAdjoint f b) (Lean.Order.PreservesSup.upperAdjoint f b')
-- Mathlib.Geometry.Manifold.Instances.Real
/-- Definition of the model with corners `(EuclideanSpace ℝ (Fin n), EuclideanQuadrant n)`, used as a
model for manifolds with corners  -/
modelWithCornersEuclideanQuadrant : (n : ℕ) → ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.comp_whiskerRight : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {E : Type u₂} [inst_4 : CategoryTheory.EnrichedCategory V E] {F G H : CategoryTheory.EnrichedFunctor V C D}
  (α : F ⟶ G) (β : G ⟶ H) (I : CategoryTheory.EnrichedFunctor V D E),
  CategoryTheory.EnrichedCat.whiskerRight { out := CategoryTheory.CategoryStruct.comp α.out β.out } I =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α I)
      (CategoryTheory.EnrichedCat.whiskerRight β I)
-- Mathlib.NumberTheory.ModularForms.NormTrace
/-- The trace of a modular form, as a modular form.  -/
ModularForm.trace : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F →
        [inst : FunLike F UpperHalfPlane ℂ] →
          {k : ℤ} → [𝒢.IsFiniteRelIndex ℋ] → [ModularFormClass F 𝒢 k] → ModularForm ℋ k
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.ext : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  {f g : BoxIntegral.BoxAdditiveMap ι M I₀}, (∀ (J : BoxIntegral.Box ι), f J = g J) → f = g
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instMulOneClass : {α : Type u_1} → [MulOneClass α] → MulOneClass αᵒᵈ
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The additive submonoid of elements `x : M` such that `f x = g x`  -/
AddMonoidHom.eqLocusM : {M : Type u_1} →
  {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (M →+ N) → (M →+ N) → AddSubmonoid M
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.injective_opcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) [CategoryTheory.Injective (K.X n₀)] [CategoryTheory.Injective (K.X n₁)]
  [K.IsStrictlyGE n₀],
  HomologicalComplex.ExactAt K n₀ →
    autoParam (n₀ + 1 = n₁) CochainComplex.injective_opcycles._auto_1 →
      CategoryTheory.Injective (HomologicalComplex.opcycles K n₁)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_sub_union_subset_union : ∀ {α : Type u_2} [inst : Sub α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.forget₂_map_ofHom : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y] (f : X →* Y),
  (CategoryTheory.forget₂ CommMonCat MonCat).map (CommMonCat.ofHom f) = MonCat.ofHom f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.Quotient.trans_assoc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} (γ₀ : Path.Homotopic.Quotient x₀ x₁)
  (γ₁ : Path.Homotopic.Quotient x₁ x₂) (γ₂ : Path.Homotopic.Quotient x₂ x₃),
  (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)
-- Mathlib.Order.RelIso.Basic
/-- Convert a `RelIso` to a `RelEmbedding`. This function is also available as a coercion
but often it is easier to write `f.toRelEmbedding` than to write explicitly `r` and `s`
in the target type.  -/
RelIso.toRelEmbedding : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → r ↪r s
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.bitraverse_eq_bimap_id' : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {α α' β β' : Type u}
  (f : α → β) (f' : α' → β'), bitraverse (pure ∘ f) (pure ∘ f') = pure ∘ bimap f f'
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_mono_left' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''}
  {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : α → E), MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T' hT' f
-- Mathlib.Data.PNat.Order
PNat.instSuccAddOrder : SuccAddOrder ℕ+
-- Init.Data.Array.Lemmas
Array.size_filterMap_lt_size_iff_exists : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β},
  (Array.filterMap f xs).size < xs.size ↔ ∃ x, ∃ (_ : x ∈ xs), f x = none
-- Mathlib.Logic.Equiv.Prod
/-- `PEmpty` type is a right absorbing element for type product up to an equivalence.  -/
Equiv.prodPEmpty : (α : Type u_9) → α × PEmpty.{u_10 + 1} ≃ PEmpty.{u_11}
-- Init.Data.Array.Zip
Array.lt_size_left_of_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : ℕ} {as : Array α} {bs : Array β},
  i < (Array.zipWith f as bs).size → i < as.size
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- zero-smoothness is equivalent to continuity.  -/
contMDiff_zero_iff : ∀ {𝕜 : 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 : M → M'},
  ContMDiff I I' 0 f ↔ Continuous f
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.instFunLike : (X : UniformSpaceCat) → (Y : UniformSpaceCat) → FunLike { f // UniformContinuous f } X.carrier Y.carrier
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_erase_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.get? k = none
-- Mathlib.RingTheory.DedekindDomain.Different
/-- A prime divides the different ideal iff it is ramified.  -/
dvd_differentIdeal_iff : ∀ {A : Type u_1} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B}
  [inst_9 : P.IsPrime], P ∣ differentIdeal A B ↔ ¬Algebra.IsUnramifiedAt A P
-- Mathlib.Analysis.ODE.ExistUnique
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local flow and that it is Lipschitz continuous in the initial point.  -/
IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∃ α,
      (∀ x ∈ Metric.closedBall x₀ ↑r,
          α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧
        ∃ L', ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith L' (fun x => α x t) (Metric.closedBall x₀ ↑r)
-- Init.Data.Array.Attach
Array.reverse_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (H : ∀ a ∈ xs, P a),
  (Array.pmap f xs H).reverse = Array.pmap f xs.reverse ⋯
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
_private.Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv.0.coe_auxContinuousLinearEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] [inst_4 : NormedAddCommGroup W]
  [inst_5 : InnerProductSpace 𝕜 W] [inst_6 : CompleteSpace W] (e : V ≃L[𝕜] W) {α α' : 𝕜} (hα : α ≠ 0)
  (hα2 : α' * α' = α⁻¹) (he : ContinuousLinearMap.adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V)
  (he' : ↑e ∘SL ContinuousLinearMap.adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W),
  ↑(auxContinuousLinearEquiv✝ e hα hα2 he he') = α' • ↑e