mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.failure.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (code : Lean.JsonRpc.ErrorCode) (message : String),
  sizeOf (Lean.Server.ServerRequestResponse.failure code message) = 1 + sizeOf code + sizeOf message
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.inl_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsLimit t.toCone),
  t.inl = CategoryTheory.Limits.BinaryFan.IsLimit.lift ht (CategoryTheory.CategoryStruct.id X) 0
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_apply : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] (s : Finset ι) (v r : ι → F),
  (Lagrange.interpolate s v) r = ∑ i ∈ s, Polynomial.C (r i) * Lagrange.basis s v i
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.toEquiv_inj : ∀ {𝕜 : 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_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {h h' : Diffeomorph I I' M M' n}, h.toEquiv = h'.toEquiv ↔ h = h'
-- Mathlib.Analysis.Complex.Basic
RCLike.im_tsum : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜},
  Summable f L → RCLike.im (∑'[L] (a : α), f a) = ∑'[L] (a : α), RCLike.im (f a)
-- Std.Async.System
_private.Std.Async.System.0.Std.Async.System.Environment.mk.injEq : ∀ (toHashMap toHashMap_1 : Std.HashMap String String),
  ({ toHashMap := toHashMap } = { toHashMap := toHashMap_1 }) = (toHashMap = toHashMap_1)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulOfMulOpposite : {M : Type u_1} → [Mul Mᵐᵒᵖ] → Mul Mᵈᵐᵃ
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.ext : ∀ {A : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {x y : WithCStarModule A ((i : ι) → E i)},
  (∀ (i : ι), x i = y i) → x = y
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_ι_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) [inst_2 : CategoryTheory.IsFiltered J] (j : J), h.cocone.ι.app j = h.coconeιApp j
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Remove and return the minimum element from the heap.  -/
Batteries.BinomialHeap.deleteMin : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Option (α × Batteries.BinomialHeap α le)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCloseds_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (x : α), {x}.toCloseds = {x}
-- Mathlib.Data.Set.Subset
Set.image_val_inter : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, Subtype.val '' (D ∩ E) = Subtype.val '' D ∩ Subtype.val '' E
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranObjObjIsoLimit_inv_π : ∀ {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) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H)
  [inst_4 : L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L),
  CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv
      (CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)) =
    CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Attempts to verify that c can be added to f via unit propagation. If it can, it returns
`((f.insert c), true)`. If it can't, it returns false as the second part of the tuple
(and no guarantees are made about what formula is returned).
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRupAdd : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n →
      Array ℕ → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (Φ : J.Point),
  CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber (CategoryTheory.CategoryStruct.id Φ) =
    CategoryTheory.CategoryStruct.id Φ.presheafFiber
-- Mathlib.RingTheory.Noetherian.Basic
LinearIndependent.set_finite_of_isNoetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  [Nontrivial R] {s : Set M}, LinearIndependent R Subtype.val → s.Finite
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.power_nat_le : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.aleph0 ≤ c → c ^ n ≤ c
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.restrictScalars_fieldEquivOfAlgEquiv : ∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) [inst_5 : Field FA]
  [inst_6 : Field FB] [inst_7 : Field FC] [inst_8 : Algebra A FA] [inst_9 : Algebra B FB] [inst_10 : Algebra C FC]
  [inst_11 : IsFractionRing A FA] [inst_12 : IsFractionRing B FB] [inst_13 : IsFractionRing C FC]
  [inst_14 : Algebra A FB] [inst_15 : IsScalarTower A B FB] [inst_16 : Algebra A FC] [inst_17 : IsScalarTower A C FC]
  [inst_18 : Algebra FA FB] [inst_19 : IsScalarTower A FA FB] [inst_20 : Algebra FA FC]
  [inst_21 : IsScalarTower A FA FC] (f : B ≃ₐ[A] C),
  AlgEquiv.restrictScalars A (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f) = IsFractionRing.algEquivOfAlgEquiv f
-- Mathlib.Topology.MetricSpace.Similarity
/-- Reversing the order of vertices preserves similarity.  -/
Similar.reverse_of_three : ∀ {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] {a b c : P₁}
  {a' b' c' : P₂}, Similar ![a, b, c] ![a', b', c'] → Similar ![c, b, a] ![c', b', a']
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.u_csInf_of_directedOn' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] {l : α → β} {u : β → α},
  GaloisConnection u l →
    ∀ {s : Set α}, DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → BddBelow s → l (sInf s) = sInf (l '' s)
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.eventuallyConst_neg_set_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant],
  Filter.EventuallyConst (-s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.GroupTheory.OrderOfElement
finite_multiples : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {a : G}, (↑(AddSubmonoid.multiples a)).Finite ↔ IsOfFinAddOrder a
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  nhdsSet (Set.Ioo a b) = Filter.principal (Set.Ioo a b)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.map : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x))
    (RingCat.Colimits.Prequotient.of j x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I),
  (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Data.Multiset.UnionInter
Multiset.le_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.orbitRel_conjAct : ∀ {G : Type u_3} [inst : Group G], ⇑(MulAction.orbitRel (ConjAct G) G) = IsConj
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.rhs : Lean.Meta.Grind.AC.EqCnstr → Lean.Grind.AC.Seq
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.range_comp : ∀ {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (g : Y ⟶ Z),
  SSet.Subcomplex.range (CategoryTheory.CategoryStruct.comp f g) = (SSet.Subcomplex.range f).image g
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.diagonal_kronecker_diagonal : ∀ {α : Type u_3} {m : Type u_10} {n : Type u_11} [inst : MulZeroClass α] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n] (a : m → α) (b : n → α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (Matrix.diagonal a) (Matrix.diagonal b) =
    Matrix.diagonal fun mn => a mn.1 * b mn.2
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT!_eq_get!_getEntryGT? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α}
  [inst_1 : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.getEntryGT! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t).get!
-- Mathlib.Data.ENat.Lattice
ENat.iSup_natCast_lt_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨆ i, ↑(f i) < ⊤ ↔ BddAbove (Set.range f)
-- Mathlib.NumberTheory.PythagoreanTriples
/-- Three integers `x`, `y`, and `z` form a Pythagorean triple if `x * x + y * y = z * z`.  -/
PythagoreanTriple : ℤ → ℤ → ℤ → Prop
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairId_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x : CategoryTheory.Join C D),
  CategoryTheory.Join.mapPairId.hom.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- The `IndepMatroid` whose independent sets are the independent subsets of `R`.  -/
Matroid.restrictIndepMatroid : {α : Type u_1} → Matroid α → Set α → IndepMatroid α
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The Dirichlet character mod `0` corresponds to `δ`.  -/
DirichletCharacter.modZero_eq_delta : ∀ {χ : DirichletCharacter ℂ 0}, (fun n => χ ↑n) = LSeries.delta
-- Mathlib.CategoryTheory.Category.KleisliCat
/-- The Kleisli category on the (type-)monad `m`. Note that the monad is not assumed to be lawful
yet.  -/
CategoryTheory.KleisliCat : (Type u → Type v) → Type (u + 1)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.mk'_mul_T : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ),
  IsLocalization.mk' (LaurentPolynomial R) p ⟨Polynomial.X ^ n, ⋯⟩ * LaurentPolynomial.T ↑n = Polynomial.toLaurent p
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))) =
    CategoryTheory.Limits.pullback.snd i₁ i₂
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instNatCast : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] → (ρ : Representation A G V) → NatCast (ρ.IntertwiningMap ρ)
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- Any surjective linear map from `Rⁿ` to `Rᵐ` guarantees `m ≤ n`.  -/
RankCondition.le_of_fin_surjective : ∀ {R : Type u} {inst : Semiring R} [self : RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
  Function.Surjective ⇑f → m ≤ n
-- Mathlib.Order.Grade
GradeMaxOrder.mk : {𝕆 : Type u_5} →
  {α : Type u_6} →
    [inst : Preorder 𝕆] →
      [inst_1 : Preorder α] →
        [toGradeOrder : GradeOrder 𝕆 α] → (∀ ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a)) → GradeMaxOrder 𝕆 α
-- Mathlib.Order.Hom.Basic
OrderHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f g : α →o β), ⇑f = ⇑g → f = g
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A bicone morphism between two bicones for the same diagram is a morphism of the bicone points
which commutes with the cone and cocone legs.  -/
CategoryTheory.Limits.BiconeMorphism : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Limits.Bicone F → CategoryTheory.Limits.Bicone F → Type uC'
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- Given a left adjoint to `G`, we can construct an initial object in each structured arrow
category on `G`.  -/
CategoryTheory.mkInitialOfLeftAdjoint : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          {F : CategoryTheory.Functor C D} →
            (h : F ⊣ G) → (A : C) → CategoryTheory.Limits.IsInitial (CategoryTheory.StructuredArrow.mk (h.unit.app A))
-- Mathlib.Topology.Algebra.Group.Basic
IsClosed.inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {s : Set G},
  IsClosed s → IsClosed s⁻¹
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The bare function of a `GroupSeminorm`.  -/
GroupSeminorm.toFun : {G : Type u_6} → [inst : Group G] → GroupSeminorm G → G → ℝ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.d_pOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j] {Z : C}
  (h : K.opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- The natural transformation between left-derived functors induced by a natural transformation.  -/
CategoryTheory.NatTrans.leftDerived : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {F G : CategoryTheory.Functor C D} →
                [inst_5 : F.Additive] → [inst_6 : G.Additive] → (F ⟶ G) → (n : ℕ) → F.leftDerived n ⟶ G.leftDerived n
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData)
  [inst_2 : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)],
  (CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).iso =
    CategoryTheory.asIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- If the derivatives of `g` at `f x` are bounded by `C`, and the `i`-th derivative
of `f` at `x` is bounded by `D^i` for all `1 ≤ i ≤ n`, then the `n`-th derivative
of `g ∘ f` is bounded by `n! * C * D^n`.

Version with the iterated derivative of `g` only bounded on the range of `f`.  -/
norm_iteratedFDeriv_comp_le' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {N : WithTop ℕ∞}
  {t : Set F},
  Set.range f ⊆ t →
    UniqueDiffOn 𝕜 t →
      ContDiffOn 𝕜 N g t →
        ContDiff 𝕜 N f →
          ↑n ≤ N →
            ∀ (x : E) {C D : ℝ},
              (∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
                (∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) →
                  ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n.factorial * C * D ^ n
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_ofReal : ∀ {α : Type u_1} {f : Filter α} {m : α → ℝ} {a : ℝ},
  Filter.Tendsto m f (nhds a) → Filter.Tendsto (fun a => ENNReal.ofReal (m a)) f (nhds (ENNReal.ofReal a))
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.LawfulMapOperator.mk : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α}
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f],
  (∀ (aig : Std.Sat.AIG α) (input1 input2 : aig.Ref) (h : aig.decls.size ≤ (f aig input1).aig.decls.size)
      (assign : α → Bool), ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧) →
    Std.Sat.AIG.RefVec.LawfulMapOperator α f
-- Mathlib.FieldTheory.FinTrdeg
FinTrdeg.of_isTranscendenceBasis : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_3} [Finite ι]
  {x : ι → L}, IsTranscendenceBasis K x → FinTrdeg K L
-- Init.Data.Array.Find
Array.findSomeRev?_push : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {a : α} {f : α → Option β},
  Array.findSomeRev? f (xs.push a) = (f a).or (Array.findSomeRev? f xs)
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_mul_index : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → H.relIndex K * K.index = H.index
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.lift_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} [inst_4 : F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (F.map f) (F.map g))
      (CategoryTheory.Functor.LaxMonoidal.μ F Y Z) =
    F.map (CategoryTheory.CartesianMonoidalCategory.lift f g)
-- Lean.Compiler.LCNF.Basic
/-- This type is used to index the fundamental LCNF IR data structures. Depending on its value different
constructors are available for the different semantic phases of LCNF.

Notably in order to save memory we never index the IR types over `Purity`. Instead the type is
parametrized by the phase and the individual constructors might carry a proof (that will be erased)
that they are only allowed in a certain phase.
 -/
Lean.Compiler.LCNF.Purity : Type
-- Mathlib.Geometry.Manifold.Notation
/-- `HasMFDerivAt% f x f'` elaborates to `HasMFDerivAt I J f x f'`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termHasMFDerivAt%______» : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instMin.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instMin = { min := fun s t => { carrier := ↑s ∩ ↑t, smul_mem' := ⋯ } }
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φK : ∀ {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] (h : S.LeftHomologyData) (τ : F ⟶ G),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φK = τ.app h.K
-- Mathlib.Order.RelSeries
/-- A `<`-series with length `n` if the relation is infinite dimensional  -/
LTSeries.withLength : (α : Type u_1) → [inst : Preorder α] → [InfiniteDimensionalOrder α] → ℕ → LTSeries α
-- Mathlib.Order.Lattice.Nat
Nat.sInf_add' : ∀ {n : ℕ} {p : ℕ → Prop}, 0 < sInf {m | p m} → sInf {m | p m} + n = sInf {m | p (m - n)}
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_sub_pure : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (a b : α), NonemptyInterval.pure a - NonemptyInterval.pure b = NonemptyInterval.pure (a - b)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- Given an adjunction `F ⊣ G` such that `F` preserves monomorphisms and is faithful,
then any injective presentation of `F(X)` can be pulled back to an injective presentation of `X`.
This is similar to `mapInjectivePresentation`.  -/
CategoryTheory.Adjunction.injectivePresentationOfMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              [F.PreservesMonomorphisms] →
                [F.ReflectsMonomorphisms] →
                  (X : C) → CategoryTheory.InjectivePresentation (F.obj X) → CategoryTheory.InjectivePresentation X
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOps.mk : (Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) →
  (Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) →
    (Lean.Expr → Option Lean.Expr) →
      (Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr))) →
        (Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) → Lean.Elab.Do.DoOps