mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
hasFDerivAt_of_restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {f' : E →L[𝕜'] F}
  {x : E} {g' : E →L[𝕜] F}, HasFDerivAt f g' x → ContinuousLinearMap.restrictScalars 𝕜 f' = g' → HasFDerivAt f f' x
-- Init.Data.Nat.Basic
Nat.add_one_mul : ∀ (n m : ℕ), (n + 1) * m = n * m + m
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.mkNatTrans_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  (h₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ =
        CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
      _auto_160✝)
  (h₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ =
        CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      _auto_162✝)
  (h₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
        CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion))
      _auto_164✝),
  (CategoryTheory.Limits.reflexivePair.mkNatTrans e₀ e₁ h₁ h₂ h₃).app CategoryTheory.Limits.WalkingReflexivePair.one =
    e₁
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_single' : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : Zero R] [inst_2 : DecidableEq m]
  {i j : m}, b j ≤ b i → ∀ (c : R), (Matrix.single i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_gcd_mul_left_right : ∀ (m n k : ℕ), m.gcd n ∣ m.gcd (k * n)
-- Mathlib.Data.FP.Basic
FP.Float.neg : [C : FP.FloatCfg] → FP.Float → FP.Float
-- Mathlib.Order.InitialSeg
PrincipalSeg.range_eq_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : LT α] (f : α <i β),
  Set.range ⇑f.toRelEmbedding = Set.Iio f.top
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.diagram.injEq : ∀ {J : Type u₁} (val val_1 : J),
  (CategoryTheory.Bicone.diagram val = CategoryTheory.Bicone.diagram val_1) = (val = val_1)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.ofTensorProduct_eq : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (ι : Type u_4) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  AdicCompletion.ofTensorProduct I (ι → R) =
    ↑(AdicCompletion.piEquivOfFintype I fun x => R).symm ∘ₗ
      ↑(TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)
-- Mathlib.Order.LiminfLimsup
liminf_finset_inf : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : ConditionallyCompleteLinearOrder β] [inst_1 : OrderTop β]
  {f : Filter α} {F : ι → α → β} {s : Finset ι},
  autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (F i)) liminf_finset_inf._auto_1 →
    autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (F i)) liminf_finset_inf._auto_3 →
      Filter.liminf (fun a => s.inf fun i => F i a) f = s.inf fun i => Filter.liminf (F i) f
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.hom_inv_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (x : ↥X), e.inv (e.hom x) = x
-- Mathlib.Data.Int.GCD
Nat.xgcdAux_rec : ∀ {r : ℕ} {s t : ℤ} {r' : ℕ} {s' t' : ℤ},
  0 < r → r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getNatValue? : Lean.Expr → OptionT Id ℕ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_inter_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.measure_of_restrictNonposSeq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    ∀ (n : ℕ),
      ¬MeasureTheory.VectorMeasure.restrict s
              (i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k) ≤
            MeasureTheory.VectorMeasure.restrict 0
              (i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k) →
        0 < s (MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n)
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedSMul.smul_le_smul_left : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : SMul G P} [self : IsOrderedSMul G P] (a b : P),
  a ≤ b → ∀ (c : G), c • a ≤ c • b
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.contains_iff_find? : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBMap α β cmp},
  t.contains x = true ↔ ∃ v, t.find? x = some v
-- Mathlib.Algebra.Group.Irreducible.Defs
Irreducible.eq_one_or_eq_one : ∀ {M : Type u_1} [inst : Monoid M] {a b : M} [Subsingleton Mˣ], Irreducible (a * b) → a = 1 ∨ b = 1
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy cofiber if for all
indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X j ⊞ G.X i` exists.  -/
HomologicalComplex.HasHomotopyCofiber : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} → {c : ComplexShape ι} → {F G : HomologicalComplex C c} → (F ⟶ G) → Prop
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.fineSubfamilyOn_of_frequently : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (f : X → Set (Set X)) (s : Set X),
  (∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x) → v.FineSubfamilyOn f s
-- Batteries.Classes.Order
Std.OrientedOrd.instOrdLex' : ∀ {α : Type u_1} (ord₁ ord₂ : Ord α) [Std.OrientedOrd α] [Std.OrientedOrd α], Std.OrientedOrd α
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Convenience function for restricting the linearity of a bilinear map.  -/
ContinuousLinearMap.bilinearRestrictScalars : (𝕜 : Type u_1) →
  {E : Type u_4} →
    {F : Type u_6} →
      {G : Type u_8} →
        {𝕜' : Type u_11} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NontriviallyNormedField 𝕜'] →
              [inst_2 : NormedAlgebra 𝕜 𝕜'] →
                [inst_3 : SeminormedAddCommGroup E] →
                  [inst_4 : NormedSpace 𝕜 E] →
                    [inst_5 : NormedSpace 𝕜' E] →
                      [IsScalarTower 𝕜 𝕜' E] →
                        [inst_7 : SeminormedAddCommGroup F] →
                          [inst_8 : NormedSpace 𝕜 F] →
                            [inst_9 : NormedSpace 𝕜' F] →
                              [IsScalarTower 𝕜 𝕜' F] →
                                [inst_11 : SeminormedAddCommGroup G] →
                                  [inst_12 : NormedSpace 𝕜 G] →
                                    [inst_13 : NormedSpace 𝕜' G] →
                                      [IsScalarTower 𝕜 𝕜' G] → (E →L[𝕜'] F →L[𝕜'] G) → E →L[𝕜] F →L[𝕜] G
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of the forward direction of `continuousWithinAt_insert`. -/
ContinuousWithinAt.of_insert : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] {x y : X}
  {s : Set X} {f : X → Y}, ContinuousWithinAt f (insert y s) x → ContinuousWithinAt f s x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Ult
Std.Tactic.BVDecide.BVPred.mkUlt_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (input : aig.BinaryRefVec w) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ⟦assign, Std.Tactic.BVDecide.BVPred.mkUlt aig input⟧ = lhs.ult rhs
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableAdd` if `(c + ·)` and `(· + c)` are measurable functions.
For a typeclass assuming measurability of `uncurry (· + ·)` see `MeasurableAdd₂`.  -/
MeasurableAdd : (M : Type u_2) → [MeasurableSpace M] → [Add M] → Prop
-- Mathlib.Tactic.FunProp.Theorems
/-- Tag for one of the 5 basic lambda theorems  -/
Mathlib.Meta.FunProp.LambdaTheoremType : Type
-- Mathlib.Algebra.Order.Module.Defs
IsOrderedModule.toSMulPosMono : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  {inst_4 : Zero β} [self : IsOrderedModule α β], SMulPosMono α β
-- Mathlib.Data.Sym.Basic
Sym.cons_erase : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s), a ::ₛ s.erase a h = s
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_epi_comp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  {Z : V} (h : Z ⟶ A) [inst_4 : CategoryTheory.Epi h]
  (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f) g = 0),
  imageToKernel (CategoryTheory.CategoryStruct.comp h f) g w =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE
        (CategoryTheory.Limits.imageSubobject f) ⋯)
      (imageToKernel f g ⋯)
-- Mathlib.Order.RelSeries
RelSeries.isChain_toList : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x.toList
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.lift_of_apply : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (f : X → A) (x : X),
  ((FreeNonUnitalNonAssocAlgebra.lift R) f) (FreeNonUnitalNonAssocAlgebra.of R x) = f x
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- Embedding of `(pathGraph 3)ᶜ` into `G` that is not complete-multipartite.  -/
SimpleGraph.pathGraph3ComplEmbeddingOf : {α : Type u} → {G : SimpleGraph α} → ¬G.IsCompleteMultipartite → (SimpleGraph.pathGraph 3)ᶜ ↪g G
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_inter : ∀ {α : Type u_2} {x : Bornology α} {s t : Set α},
  Bornology.IsCobounded (s ∩ t) ↔ Bornology.IsCobounded s ∧ Bornology.IsCobounded t
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = (Std.Internal.List.getKey? a l).isSome
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_self : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  (P.reflectionPerm i) ((P.reflectionPerm i) j) = j
-- Std.Http.Protocol.H1.Config
/-- Maximum number of extensions on a single chunk-size line (default: 16).
 -/
Std.Http.Protocol.H1.Config.maxChunkExtensions : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The modular form of weight `k_1 + k_2` given by the product of two modular forms of weights
`k_1` and `k_2`.  -/
ModularForm.mul : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k_1 k_2 : ℤ} → [Γ.HasDetPlusMinusOne] → ModularForm Γ k_1 → ModularForm Γ k_2 → ModularForm Γ (k_1 + k_2)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_apply_toFun : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  [inst_3 : CompactSpace α] (f : C(α, β)) (a : α), (ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty f) a = f a
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `exists` is adjoint to `pullback` when images exist  -/
CategoryTheory.MonoOver.existsPullbackAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
            CategoryTheory.MonoOver.exists f ⊣ CategoryTheory.MonoOver.pullback f
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank : ∀ {R S : CommRingCat} {f : R ⟶ S},
  (CommRingCat.Hom.hom f).Finite →
    (CommRingCat.Hom.hom f).Flat →
      AlgebraicGeometry.Scheme.Hom.finrank (AlgebraicGeometry.Spec.map f) = (CommRingCat.Hom.hom f).finrank
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The derivative of the Fourier transform is given by the Fourier transform of the multiplication
with `-(2 * π * Complex.I) • innerSL ℝ`.  -/
SchwartzMap.fderivCLM_fourier_eq : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : SMulCommClass ℂ 𝕜 E] {V : Type u_3} [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : FiniteDimensional ℝ V] [inst_8 : MeasurableSpace V] [inst_9 : BorelSpace V]
  (f : SchwartzMap V E),
  (SchwartzMap.fderivCLM 𝕜 V E) (FourierTransform.fourier f) =
    FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulRightCLM ℂ E (innerSL ℝ)) f)
-- Lean.Meta.MethodSpecs
Lean.instInhabitedMethodSpecsAttrData : Inhabited Lean.MethodSpecsAttrData
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- An `AddSubmonoid` of an ordered additive monoid is an ordered additive monoid.  -/
AddSubmonoidClass.toIsOrderedAddMonoid : ∀ {M : Type u_1} {S : Type u_2} [inst : SetLike S M] [inst_1 : AddCommMonoid M] [inst_2 : Preorder M]
  [IsOrderedAddMonoid M] [inst_4 : AddSubmonoidClass S M] (s : S), IsOrderedAddMonoid ↥s
-- Init.Data.Nat.ToString
Nat.d_eq_digitChar : ∀ {n : ℕ}, 'd' = n.digitChar ↔ n = 13
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
/-- `κ(I[X]) ≃ₐ[κ(I)] κ(I)(X)`.  -/
Polynomial.residueFieldMapCAlgEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      [inst_1 : I.IsPrime] →
        (J : Ideal (Polynomial R)) →
          [inst_2 : J.IsPrime] →
            [inst_3 : J.LiesOver I] →
              [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)] →
                [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] →
                  J = Ideal.map Polynomial.C I → J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofPartialTermInfo.sizeOf_spec : ∀ (i : Lean.Elab.PartialTermInfo), sizeOf (Lean.Elab.Info.ofPartialTermInfo i) = 1 + sizeOf i
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- If `f_n → g` pointwise and the derivatives `(f_n)' → h` _uniformly_ converge, then
in fact for a fixed `y`, the difference quotients `‖z - y‖⁻¹ • (f_n z - f_n y)` converge
_uniformly_ to `‖z - y‖⁻¹ • (g z - g y)`  -/
difference_quotients_converge_uniformly : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_5} [inst : NormedAddCommGroup E] {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_7} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {f : ι → E → G}
  {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E},
  TendstoUniformlyOnFilter f' g' l (nhds x) →
    (∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
      (∀ᶠ (y : E) in nhds x, Filter.Tendsto (fun n => f n y) l (nhds (g y))) →
        TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l
          (nhds x)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.comp_bfamilyOfFamily' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → α) (g : α → β),
  (fun i hi => g (Ordinal.bfamilyOfFamily' r f i hi)) = Ordinal.bfamilyOfFamily' r (g ∘ f)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
-- Mathlib.Algebra.Star.Unitary
Unitary.star_eq_inv' : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R], star = Inv.inv
-- Lean.IdentifierSuggestion
Lean.Elab.Term.hintAutoImplicitFailure : Lean.Expr → optParam String "a function" → Lean.Elab.TermElabM Lean.MessageData
-- Mathlib.Algebra.Order.Group.Defs
LinearOrderedCommGroup.to_noMaxOrder : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [Nontrivial α], NoMaxOrder α
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (s : Set α) (t : Set β),
  (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- The yoneda embedding for `AddGrp C` is fully faithful.  -/
CategoryTheory.yonedaAddGrpFullyFaithful : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.yonedaAddGrp.FullyFaithful
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_empty_of_one_mem : ∀ {R : Type u} [inst : CommSemiring R] {s : Set R}, 1 ∈ s → PrimeSpectrum.zeroLocus s = ∅
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.zero_left : ∀ {G₀ : Type u_2} [inst : MulZeroClass G₀] (a : G₀), Commute 0 a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.assert : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.GoalM Unit
-- Init.Data.Array.Basic
/-- Checks whether `a` is an element of `as`, using `==` to compare elements.

`Array.elem` is a synonym that takes the element before the array.

Examples:
* `#[1, 4, 2, 3, 3, 7].contains 3 = true`
* `Array.contains #[1, 4, 2, 3, 3, 7] 5 = false`
 -/
Array.contains : {α : Type u} → [BEq α] → Array α → α → Bool
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_dist_eq_add : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : Dist α] [inst_1 : Dist β],
  0 < p.toReal →
    ∀ (f g : WithLp p (α × β)), dist f g = (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsZeroOrMarkovKernel (κ n)] (a b : ℕ),
  ProbabilityTheory.IsZeroOrMarkovKernel (ProbabilityTheory.Kernel.partialTraj κ a b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f},
  (t.modify k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ⋯ (f (t.get k ⋯)) else t.get k' ⋯
-- Mathlib.Data.PNat.Xgcd
Nat.succPNat.eq_1 : ∀ (n : ℕ), n.succPNat = ⟨n.succ, ⋯⟩
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D]
  [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ], CategoryTheory.HasSheafify J D
-- Lean.DocString
/-- Finds the docstring for a name, taking the current namespace and open declarations from the ambient
monad. Tactic alternate forms and documentation extensions are taken into account.

Docstrings are rendered with the default options.
 -/
Lean.findMarkdownDocString? : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadResolveName m] → [MonadLiftT IO m] → Lean.Name → optParam Bool true → m (Option String)
-- Mathlib.Topology.Order.LeftRight
continuousWithinAt_iff_continuous_left'_right' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
  {s : Set α} {a : α} {f : α → β},
  ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Set.Iio a) a ∧ ContinuousWithinAt f (s ∩ Set.Ioi a) a
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Auxiliary definition for `stalkToFiber`.  -/
TopCat.LocalPredicate.cocone : {X : TopCat} →
  {T : ↑X → Type u_1} →
    (P : TopCat.LocalPredicate T) →
      (x : ↑X) →
        CategoryTheory.Limits.Cocone
          ((TopologicalSpace.OpenNhds.inclusion x).op.comp (TopCat.subpresheafToTypes P.toPrelocalPredicate))
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableDSimpCacheKey.hash : Lean.Elab.Tactic.Grind.DSimpCacheKey → UInt64
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_bsup_of_limit : ∀ {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}},
  (∀ {a a' : Ordinal.{u_3}} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha') →
    (∀ a < o, Order.succ a < o) → ∀ (i : Ordinal.{u_3}) (h : i < o), f i h < o.bsup f
-- Mathlib.Analysis.Normed.Operator.Conformal
isConformalMap_id : ∀ {R : Type u_1} {M : Type u_2} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup M] [inst_2 : NormedSpace R M],
  IsConformalMap (ContinuousLinearMap.id R M)
-- Batteries.Data.DList.Basic
Batteries.DList.instEmptyCollection : {α : Type u} → EmptyCollection (Batteries.DList α)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- **Alias** of `tendsto_seminormFromConst_seq_atTop`.

---

We prove that `seminormFromConst' c f x` is the limit of the sequence
`seminormFromConst_seq c f x` as `n` tends to infinity.  -/
seminormFromConst_isLimit : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 →
    f c ≠ 0 →
      IsPowMul ⇑f →
        ∀ (x : R), Filter.Tendsto (seminormFromConst_seq c f x) Filter.atTop (nhds (seminormFromConst' c f x))