mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
/-- A node in the E-matching diagnostics hyper-graph.
 -/
Lean.Meta.Grind.EMatchDiagNode : Type
-- Mathlib.Topology.Order.Basic
/-- **Alias** of `tendsto_of_tendsto_of_tendsto_of_le_of_le`.

---

**Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold everywhere.  -/
Filter.Tendsto.squeeze : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f g h : β → α}
  {b : Filter β} {a : α},
  Filter.Tendsto g b (nhds a) → Filter.Tendsto h b (nhds a) → g ≤ f → f ≤ h → Filter.Tendsto f b (nhds a)
-- Mathlib.Topology.LocallyFinite
LocallyFinite.comp_injOn : ∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} {g : ι' → ι},
  LocallyFinite f → Set.InjOn g {i | (f (g i)).Nonempty} → LocallyFinite (f ∘ g)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.localization_comap_isEmbedding : ∀ {R : Type u} (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Submonoid R)
  [IsLocalization M S], Topology.IsEmbedding (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.CategoryTheory.Localization.Opposite
/-- If `L : C ⥤ D` satisfies the universal property of the localisation
for `W : MorphismProperty C`, then `L.op` also does.  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.op : {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] →
        {L : CategoryTheory.Functor C D} →
          {W : CategoryTheory.MorphismProperty C} →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W Eᵒᵖ →
                  CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L.op W.op E
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.snd_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.AddMon C),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd M N).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X
-- Mathlib.Order.WithBot
WithBot.instBoundedOrder.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α],
  WithBot.instBoundedOrder = { toOrderTop := WithBot.instOrderTop, toOrderBot := WithBot.instOrderBot }
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.span_singleton_mem_isPrincipalSubmonoid : ∀ {R : Type u_1} [inst : CommRing R] (a : R), Ideal.span {a} ∈ Ideal.isPrincipalSubmonoid R
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInverseAssociator_inv_app_down_down : ∀ (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),
  ((CategoryTheory.sum.inlCompInverseAssociator C D E).inv.app X).down.down = CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instAdd : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Add (WittVector p R)
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instOrderTopOfOrderBot : (α : Type u) → [inst : LE α] → [h : OrderBot α] → OrderTop αᵒᵈ
-- Mathlib.Logic.Function.Basic
/-- A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`.  -/
Std.Symm.forall_existsUnique_iff' : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r],
  (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ r = fun x1 x2 => f x1 = x2
-- Mathlib.Data.PNat.Basic
OrderIso.pnatIsoNat_apply : ⇑OrderIso.pnatIsoNat = PNat.natPred
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_le_card_biUnion_add_one : ∀ {ι : Type u_1} {α : Type u_2} [inst : DecidableEq α] {s : Finset ι} {f : ι → Finset α},
  Function.Injective f → (↑s).PairwiseDisjoint f → s.card ≤ (s.biUnion f).card + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.has_cokernel_pair_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  CategoryTheory.Limits.HasPushout f f
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments by duplicating the first argument. Used for `pow`.  -/
Simps.copyFirst : Simps.findArgType
-- Mathlib.Tactic.Widget.StringDiagram
/-- Help function for displaying two string diagrams in an equality.  -/
Mathlib.Tactic.Widget.StringDiagram.mkEqHtml : ProofWidgets.Html → ProofWidgets.Html → ProofWidgets.Html
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_zero : ∀ {x y : NNReal}, x.agmSequences y 0 = (NNReal.sqrt (x * y), (x + y) / 2)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.propSet_singleton : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (j : ↑J.obj), J.PropSet {j}
-- Mathlib.Computability.Language
Language.mem_sub : ∀ {α : Type u_1} (l m : Language α) (x : List α), x ∈ l - m ↔ x ∈ l ∧ x ∉ m
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, k ∈ m → m.getKey? k = some k
-- Mathlib.Order.CompleteLattice.Basic
iInf_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] (f : β → γ → α),
  ⨅ i, ⨅ j, f i j = ⨅ x, f x.1 x.2
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.preservesFiniteBiproductsOfPreservesBiproducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproducts F],
  CategoryTheory.Limits.PreservesFiniteBiproducts F
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- An injective linear map sends linearly independent families of vectors to linearly independent
families of vectors. See also `LinearIndependent.map` for a more general statement.  -/
LinearIndependent.map' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M'] [inst_3 : Module R M] [inst_4 : Module R M'],
  LinearIndependent R v → ∀ (f : M →ₗ[R] M'), f.ker = ⊥ → LinearIndependent R (⇑f ∘ v)
-- Lean.Meta.Tactic.Grind.Beta
/-- Returns the root of the functions in the equivalence class containing `e`.
That is, if `f a` is in `root`s equivalence class, results contains the root of `f`.
 -/
Lean.Meta.Grind.getFnRoots : Lean.Expr → Lean.Meta.Grind.GoalM (Array Lean.Expr)
-- Mathlib.RingTheory.AdicCompletion.Completeness
/-- Given an element `x` in the adic completion of `M` whose projection to `M / I ^ n • M` is zero,
`ofValEqZero` constructs the corresponding element in the adic completion of `I ^ n • M`.  -/
AdicCompletion.ofValEqZero : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_2} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → {n : ℕ} → {x : AdicCompletion I M} → ↑x n = 0 → AdicCompletion I ↥(I ^ n • ⊤)
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The restriction of a continuous representation along a monoid homomorphism.  -/
ContRepresentation.restrict : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] →
                [inst_5 : Module R V] →
                  {H : Type u_6} → [inst_6 : Monoid H] → ContRepresentation R G V → (H →* G) → ContRepresentation R H V
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_exp_mul_of_le_of_le : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t a b : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp (a * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp (b * X ω)) μ →
      a ≤ t → t ≤ b → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
even_abs : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a : α}, Even |a| ↔ Even a
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Return all applicable library rewrites of `e`.
Note that the result may contain duplicate rewrites. These can be removed with `filterRewrites`.  -/
Mathlib.Tactic.LibraryRewrite.getImportRewrites : Lean.Expr → Lean.MetaM (Array (Array (Mathlib.Tactic.LibraryRewrite.Rewrite × Lean.Name)))
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bind_const : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (q : PMF β), (p.bind fun x => q) = q
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.addRightCancelInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_extend_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {R : CategoryTheory.Presieve X},
  CategoryTheory.Presieve.functorPushforward F (CategoryTheory.Sieve.generate R).arrows =
    CategoryTheory.Presieve.functorPushforward F R
-- Mathlib.GroupTheory.PGroup
/-- A group of order `p ^ 2` is commutative. See also `IsPGroup.commGroupOfCardEqPrimeSq`
for the `CommGroup` instance.  -/
IsPGroup.isMulCommutative_of_card_eq_prime_sq : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)], Nat.card G = p ^ 2 → IsMulCommutative G
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_injOn : Set.InjOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosedMap_comap_of_isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.IsIntegral → IsClosedMap (PrimeSpectrum.comap f)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_rankFinite : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E : Set α} [N.RankFinite], (N.comapOn E f).RankFinite
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.TreeMap.Raw.minEntryD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α × β → α × β
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasFiniteWidePullbacks_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasFiniteWidePullbacks Cᵒᵖ ↔ CategoryTheory.Limits.HasFiniteWidePushouts C
-- Mathlib.Logic.Nontrivial.Defs
/-- See Note [lower instance priority]

Note that since this and `instNonemptyOfInhabited` are the most "obvious" way to find a nonempty
instance if no direct instance can be found, we give this a higher priority than the usual `100`.
 -/
Nontrivial.to_nonempty : ∀ {α : Type u_1} [Nontrivial α], Nonempty α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_eq_zero_iff : ∀ {θ : ℂ}, Complex.cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑Real.pi / 2
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddSemigroup M],
  Filter.Germ.instAddSemigroup = { toAdd := Filter.Germ.instAdd, add_assoc := ⋯ }
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.coe_mk : ∀ {R : Type u_1} [inst : Zero R] (f : ℕ → R) (hf : f 0 = 0), ⇑{ toFun := f, map_zero' := hf } = f
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.mk.sizeOf_spec : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf Ω] [inst_2 : SizeOf C]
  (obj : Set Ω) (hom : ↑obj → ↑obj → Set Ω) (objEquiv : ↑obj ≃ C)
  (homEquiv : {X Y : ↑obj} → ↑(hom X Y) ≃ (objEquiv X ⟶ objEquiv Y)),
  sizeOf { obj := obj, hom := hom, objEquiv := objEquiv, homEquiv := homEquiv } = 1 + sizeOf objEquiv
-- Mathlib.Order.SupClosed
supClosed_range : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : FunLike F α β] [SupHomClass F α β] (f : F), SupClosed (Set.range ⇑f)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Wedge F) {i j : J}
  (f : i ⟶ j) {Z : C} (h : (F.obj (Opposite.op i)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c i)
      (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j)
      (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
-- Init.Data.UInt.Lemmas
UInt64.neg_mul : ∀ (a b : UInt64), -a * b = -(a * b)
-- Mathlib.Data.Fintype.Card
univ_eq_singleton_of_card_one : ∀ {α : Type u_4} [inst : Fintype α] (x : α), Fintype.card α = 1 → Finset.univ = {x}
-- Mathlib.Topology.Order.Hom.Esakia
/-- `id` as an `EsakiaHom`.  -/
EsakiaHom.id : (α : Type u_2) → [inst : TopologicalSpace α] → [inst_1 : Preorder α] → EsakiaHom α α
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.inner_normalize_ortho : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  inner ℝ y (NormedSpace.normalize (InnerProductGeometry.ortho✝ y x)) = 0
-- Mathlib.RingTheory.Polynomial.Subring
/-- Given a polynomial whose coefficients are in some subring, return
the corresponding polynomial whose coefficients are in the ambient ring.  -/
Polynomial.ofSubring : {R : Type u_1} → [inst : Ring R] → (T : Subring R) → Polynomial ↥T → Polynomial R
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [Nonempty ι] {α : Type u_1} [Finite α]
  (x : α → FirstOrder.Language.DirectLimit G f), ∃ i y, x = fun a => ⟦FirstOrder.Language.Structure.Sigma.mk f i (y a)⟧
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_inverse_obj_X : ∀ (X : TwoP), (TwoP.swapEquiv.inverse.obj X).X = X.X
-- Mathlib.Algebra.Group.Subgroup.Lattice
Multiplicative.mem_toSubgroup : ∀ {A : Type u_2} [inst : AddGroup A] (S : AddSubgroup A) (a : Multiplicative A),
  a ∈ AddSubgroup.toSubgroup S ↔ Multiplicative.toAdd a ∈ S
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.iUnion_skeleton_eq_complex`. -/
Topology.CWComplex.iUnion_skeleton_eq_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ⋃ n, ↑(Topology.RelCWComplex.skeleton C ↑n) = C
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.forEachVar : Array Lean.Syntax → (Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subRight_toEquiv : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G),
  (IsometryEquiv.subRight c).toEquiv = Equiv.subRight c
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasSum.hasSum_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {a₁ a₂ : α} {s : Set β}, HasSum (f ∘ Subtype.val) a₁ → (HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂))
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.instIsRightAdjointΓ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_4, u_2} C] (J : CategoryTheory.GrothendieckTopology C)
  (A : Type u_3) [inst_1 : CategoryTheory.Category.{u_1, u_3} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A], (CategoryTheory.Sheaf.Γ J A).IsRightAdjoint
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Get the `BinderInfo`s for the arguments of `mkAppN fn args`.  -/
_private.Mathlib.Tactic.ClickSuggestions.Util.0.Mathlib.Tactic.ClickSuggestions.isExplicitEq.getBinderInfos : Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.BinderInfo)
-- Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
SeparableClosure.hasEnoughRootsOfUnity_pow : ∀ (F : Type u_1) [inst : Field F] (n k : ℕ) [NeZero ↑n], HasEnoughRootsOfUnity (SeparableClosure F) (n ^ k)
-- Std.Internal.Parsec.String
/-- Parse an ASCII digit `0-9` as a `Char`.
 -/
Std.Internal.Parsec.String.digit : Std.Internal.Parsec.String.Parser Char
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The functor `ι : Fib S ⥤ 𝒳`.  -/
HasFibers.ι : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳} →
        {p : CategoryTheory.Functor 𝒳 𝒮} → [self : HasFibers p] → (S : 𝒮) → CategoryTheory.Functor (HasFibers.Fib p S) 𝒳
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] (s : Set E), Bornology.IsVonNBounded 𝕜 s = ∀ ⦃V : Set E⦄, V ∈ nhds 0 → Absorbs 𝕜 V s
-- Mathlib.Analysis.BoundedVariation
/-- Eta-expanded form of `LocallyBoundedVariationOn.mul` -/
LocallyBoundedVariationOn.fun_mul : ∀ {α : Type u_2} [inst : LinearOrder α] {f g : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s → LocallyBoundedVariationOn g s → LocallyBoundedVariationOn (fun i => f i * g i) s
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.drop.match_1.eq_1 : ∀ {σ : Type u_1} {α : Type u_2} (motive : Option (α × σ) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (fst : α) → (s : σ) → motive (some (fst, s))),
  (match none with
    | none => h_1 ()
    | some (fst, s) => h_2 fst s) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
/-- The preimage of a null measurable set under a (quasi-)measure-preserving map is a null
measurable set.  -/
MeasureTheory.NullMeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {s : Set β},
  MeasureTheory.NullMeasurableSet s μb →
    MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → MeasureTheory.NullMeasurableSet (f ⁻¹' s) μa
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instEpiGShortComplexOpcyclesThreeδ₂Toδ₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Epi (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst.eq_1 : ∀ (G₀ : Type u_1) (H₀ : Type u_2) [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀],
  MonoidWithZeroHom.fst G₀ H₀ = WithZero.lift' ((Units.coeHom G₀).comp (MonoidHom.fst G₀ˣ H₀ˣ))
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_ι_image_ι_isoImage_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens),
  CategoryTheory.CategoryStruct.comp (f ∣_ (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
      (AlgebraicGeometry.Scheme.Hom.isoImage U.ι V).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯)
        (AlgebraicGeometry.Scheme.Hom.isoImage ((TopologicalSpace.Opens.map f.base).obj U).ι
            ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V)).inv)
      (f ∣_ U ∣_ V)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Convert a `PreDiscrTree` to a `RefinedDiscrTree`.  -/
Lean.Meta.RefinedDiscrTree.PreDiscrTree.toRefinedDiscrTree : {α : Type} → Lean.Meta.RefinedDiscrTree.PreDiscrTree α → Lean.Meta.RefinedDiscrTree α
-- Mathlib.Data.Matrix.Reflection
_private.Mathlib.Data.Matrix.Reflection.0.Matrix.transposeᵣ.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x x_1 : ℕ) → Matrix (Fin x) (Fin x_1) α → Sort u_2) (x : ℕ) (x_1 : Matrix (Fin x) (Fin 0) α)
  (h_1 : (x : ℕ) → (x_2 : Matrix (Fin x) (Fin 0) α) → motive x 0 x_2)
  (h_2 : (x n : ℕ) → (A : Matrix (Fin x) (Fin (n + 1)) α) → motive x n.succ A),
  (match x, 0, x_1 with
    | x, 0, x_2 => h_1 x x_2
    | x, n.succ, A => h_2 x n A) =
    h_1 x x_1
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct an isomorphism of group objects by giving an isomorphism between the underlying
objects and checking compatibility with unit and multiplication only in the forward direction.  -/
CategoryTheory.Grp.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : CategoryTheory.Grp C} →
        (e : G.X ≅ H.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
              CategoryTheory.Grp.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                    CategoryTheory.MonObj.mul)
                CategoryTheory.Grp.mkIso._auto_3 →
              (G ≅ H)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_right_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).inv h))))
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.top_sub_coe : ∀ {α : Type u_1} [inst : Sub α] [inst_1 : Bot α] {a : α}, ⊤ - ↑a = ⊤
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ShowDocumentClientCapabilities.mk.injEq : ∀ (support support_1 : Bool), ({ support := support } = { support := support_1 }) = (support = support_1)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Inversion of a unit monomial.  -/
Tactic.ComputeAsymptotics.UnitMonomial.inv : Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.UnitMonomial
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_fromOpenSubsetsGlue : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : J),
  CategoryTheory.CategoryStruct.comp ((TopCat.GlueData.ofOpenSubsets U).ι i) (TopCat.GlueData.fromOpenSubsetsGlue U) =
    (U i).inclusion'