mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdCongr_apply : ∀ (p : ENNReal) {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β]
  [inst_4 : Module 𝕜 β] [inst_5 : SeminormedAddCommGroup α'] [inst_6 : Module 𝕜 α'] [inst_7 : SeminormedAddCommGroup β']
  [inst_8 : Module 𝕜 β'] (f : α ≃ₗᵢ[𝕜] α') (g : β ≃ₗᵢ[𝕜] β') (x : WithLp p (α × β)),
  (LinearIsometryEquiv.withLpProdCongr p f g) x = WithLp.toLp p (f x.fst, g x.snd)
-- Mathlib.Algebra.Ring.CentroidHom
/-- The canonical isomorphism from the center of a (non-associative) semiring onto its centroid.  -/
CentroidHom.centerIsoCentroid : {α : Type u_5} → [inst : NonAssocSemiring α] → ↥(Subsemiring.center α) ≃+* CentroidHom α
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
IsUltrametricDist.algNormOfAlgEquiv.congr_simp : ∀ {K : Type u_1} [inst : NormedField K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ σ_1 : Gal(L/K)),
  σ = σ_1 → IsUltrametricDist.algNormOfAlgEquiv σ = IsUltrametricDist.algNormOfAlgEquiv σ_1
-- Init.Data.SInt.Lemmas
Int64.add_left_inj : ∀ {a b : Int64} (c : Int64), a + c = b + c ↔ a = b
-- Std.Data.HashSet.Basic
Std.HashSet.Equiv.mk : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Data.Multiset.Filter
Multiset.filter_attach' : ∀ {α : Type u_1} (s : Multiset α) (p : { a // a ∈ s } → Prop) [inst : DecidableEq α] [inst_1 : DecidablePred p],
  Multiset.filter p s.attach =
    Multiset.map (Subtype.map id ⋯) (Multiset.filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach
-- Mathlib.Algebra.Quaternion
Quaternion.im_one : ∀ {R : Type u_3} [inst : CommRing R], Quaternion.im 1 = 0
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.moduleTk : Lean.Parser.Parser
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.ι_fromFreeYonedaCoproduct_apply : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (m : M.Elements) (X : Cᵒᵖ) (x : ↑(m.freeYoneda.obj X)),
  (CategoryTheory.ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app X))
      ((CategoryTheory.ConcreteCategory.hom ((M.ιFreeYonedaCoproduct m).app X)) x) =
    (CategoryTheory.ConcreteCategory.hom (m.fromFreeYoneda.app X)) x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function `f : P.RankFunction ι` for a proper pairing
of a subcomplex of a simplicial set `X`, this is the simplex of `X`
corresponding to an element in `(Subcomplex.range (f.m j)).N`.  -/
SSet.Subcomplex.Pairing.RankFunction.mapN : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) →
            [inst_1 : P.IsProper] → [SuccOrder ι] → [NoMaxOrder ι] → {j : ι} → (SSet.Subcomplex.range (f.m j)).N → X.S
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).hom.left =
    CategoryTheory.CategoryStruct.comp ⋯.isoPushout.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left
          (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T))
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).hom)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) →
    ∀ (f : α → E), MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T' hT' f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k a : α} {v : β},
  (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.Topology.Compactness.Lindelof
NonLindelofSpace.mk : ∀ {X : Type u_2} [inst : TopologicalSpace X], ¬IsLindelof Set.univ → NonLindelofSpace X
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instMax : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Max (FractionalIdeal S P)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.monotone_upper : ∀ {ι : Type u_1}, Monotone fun I => I.upper
-- Init.System.IO
_private.Init.System.IO.0.System.FilePath.walkDir.go : (System.FilePath → IO Bool) → System.FilePath → StateT (Array System.FilePath) IO Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.map f m) k = (Option.map (f k') (Std.ExtDHashMap.Const.get? m k)).get!
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence holds if and only if all non-negative distances between points with different
indices are the same.  -/
congruent_iff_pairwise_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ => nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
-- Init.Data.ByteArray.Bootstrap
_private.Init.Data.ByteArray.Bootstrap.0.List.toByteArray.match_1.eq_2 : ∀ (motive : List UInt8 → ByteArray → Sort u_1) (b : UInt8) (bs : List UInt8) (r : ByteArray)
  (h_1 : (r : ByteArray) → motive [] r) (h_2 : (b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r),
  (match b :: bs, r with
    | [], r => h_1 r
    | b :: bs, r => h_2 b bs r) =
    h_2 b bs r
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.range : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α} (g : ↑s → ι),
  (∀ (i : ↑s), f (g i) ≤ f ↑i) → s.PairwiseDisjoint f → (Set.range g).PairwiseDisjoint f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.unop_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  (φ : W.RightFraction X Y), φ.unop.s = φ.s.unop
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvections_pow_mono : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  Monotone fun n => LinearEquiv.dilatransvections R V ^ n
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.id_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), (CategoryTheory.Monad.id C).obj X = X
-- Mathlib.Algebra.Order.Module.Defs
SMulPosStrictMono.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β],
  (∀ ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b) → SMulPosStrictMono α β
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.mul_eq_trans : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f g : M ≃ₗ[R] M),
  f * g = g ≪≫ₗ f
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wrepr_wMk : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (MvQPF.P F).A)
  (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α),
  MvQPF.wrepr ((MvQPF.P F).wMk a f' f) =
    (MvQPF.P F).wMk'
      (MvQPF.repr (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.wrepr) ⟨a, (MvQPF.P F).appendContents f' f⟩)))
-- Mathlib.Data.Option.Basic
/-- `Option.map` as a function between functions is injective.  -/
Option.map_injective' : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective Option.map
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toArray_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.toList.toArray = t.toArray
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instCStarRing : ∀ {α : Type u_1} {R : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : Zero α]
  [inst_3 : NormedCommRing R] [inst_4 : StarRing R] [inst_5 : CStarRing R], CStarRing (ContinuousMapZero α R)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
act_rel_act_of_rel : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [CovariantClass M N μ r] (m : M) {a b : N},
  r a b → r (μ m a) (μ m b)
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf_of_iInter : ∀ {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α} {I : Set ι},
  I.Finite → ∀ {V : ↑I → Set α}, (∀ (i : ↑I), V i ∈ s ↑i) → ⋂ i, V i ⊆ U → U ∈ ⨅ i, s i
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_neg : ∀ {R : Type u_3} {A : Type u_4} [inst : Neg R] [inst_1 : Neg A] (x : Unitization R A), (-x).toProd = -x.toProd
-- Init.Tactics
/-- `stop` is a helper tactic for "discarding" the rest of a proof:
it is defined as `repeat sorry`.
It is useful when working on the middle of a complex proofs,
and less messy than commenting the remainder of the proof.
 -/
Lean.Parser.Tactic.tacticStop_ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MonotoneOn.memLp_of_measure_ne_top : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {p : ENNReal} {f : X → E},
  MonotoneOn f s →
    ∀ {a b : X}, IsLeast s a → IsGreatest s b → μ s ≠ ⊤ → MeasurableSet s → MeasureTheory.MemLp f p (μ.restrict s)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.negZeroClass : {I : Type u} → {f : I → Type v₁} → [(i : I) → NegZeroClass (f i)] → NegZeroClass ((i : I) → f i)
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_apply_1 : ∀ {σ₁ : Type u_1} (p : Prop) (s₁ : σ₁), Lean.Order.CompleteLattice.ofProp p s₁ = p
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.mul_assoc : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x y z : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation F ((x.mul y).mul z) (x.mul (y.mul z))
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instAddMonoid.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddMonoid N],
  ZeroHom.instAddMonoid =
    { toAdd := ZeroHom.instAdd, add_assoc := ⋯, toZero := instZeroZeroHom, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The functor from topological spaces to light condensed sets restricted to sequential spaces.
 -/
LightCondSet.sequentialToLightCondSet : CategoryTheory.Functor Sequential LightCondSet
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.isLeast_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F),
  IsLeast {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.injective_codRestrict : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  Function.Injective ⇑(f.codRestrict S hf) ↔ Function.Injective ⇑f
-- Mathlib.ModelTheory.Complexity
/-- For any bounded formula `φ`, `φ.toPrenex` is a semantically-equivalent formula in prenex normal
form.  -/
FirstOrder.Language.BoundedFormula.toPrenex : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- An integer Hadamard matrix of order greater than two has order divisible by four.

This is the standard divisibility obstruction in [Section 2.3][deLauneyFlannery2011].  -/
Matrix.IsHadamard.four_dvd_card : ∀ {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] {A : Matrix n n ℤ},
  A.IsHadamard → 2 < Fintype.card n → 4 ∣ Fintype.card n
-- Mathlib.Algebra.Lie.Weights.Killing
/-- If a Lie algebra `L` has non-degenerate Killing form, the only element of a Cartan subalgebra
whose adjoint action on `L` is nilpotent, is the zero element.

Over a perfect field a much stronger result is true, see
`LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra`.  -/
LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra : ∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] {x : L},
  x ∈ H → IsNilpotent ((LieAlgebra.ad K L) x) → x = 0
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.clearError : Lean.ParseImports.State → Lean.ParseImports.State
-- Mathlib.CategoryTheory.Equivalence
/-- An equality of properties of objects of a category `C` induces an equivalence of the
respective induced full subcategories of `C`.  -/
CategoryTheory.ObjectProperty.fullSubcategoryCongr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P P' : CategoryTheory.ObjectProperty C} → P = P' → (P.FullSubcategory ≌ P'.FullSubcategory)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.addEquiv_symm_apply : ∀ (R : Type u_3) (A : Type u_4) [inst : Add R] [inst_1 : Add A] (toProd : R × A),
  (Unitization.addEquiv R A).symm toProd = Unitization.mk toProd
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- The integral of `sin x * cos x`, given in terms of cos².
See `integral_sin_mul_cos₁` above for the integral given in terms of sin².  -/
integral_sin_mul_cos₂ : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x * Real.cos x = (Real.cos a ^ 2 - Real.cos b ^ 2) / 2
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- Delaborator for `LinearIndependent` that suggests pretty printing with type hints
in case the family of vectors is over a `Set`.

Type hints look like `LinearIndependent fun (v : ↑s) => ↑v` or `LinearIndependent (ι := ↑s) f`,
depending on whether the family is a lambda expression or not.  -/
delabLinearIndependent : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_cons : ∀ {α : Type u} {instOrd : Ord α} {hd : α} {tl : List α},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty (hd :: tl) ⋯) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit
        (Std.DTreeMap.Internal.Impl.insertIfNew hd () Std.DTreeMap.Internal.Impl.empty ⋯).impl tl ⋯)
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- If the image under the seminorm is zero, then the argument is zero.  -/
AddGroupNorm.eq_zero_of_map_eq_zero' : ∀ {G : Type u_6} [inst : AddGroup G] (self : AddGroupNorm G) (x : G), self.toFun x = 0 → x = 0
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- The cone `coneOfHasLimitEval F` is limit.  -/
HomologicalComplex.isLimitConeOfHasLimitEval : {C : Type u_1} →
  {ι : Type u_2} →
    {J : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_3} J] →
          {c : ComplexShape ι} →
            [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (F : CategoryTheory.Functor J (HomologicalComplex C c)) →
                [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] →
                  CategoryTheory.Limits.IsLimit (HomologicalComplex.coneOfHasLimitEval F)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.one_snd : ∀ {q : ℕ}, 1.2 = 0
-- Mathlib.Topology.Algebra.Group.Pointwise
IsTopologicalGroup.regularSpace : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G], RegularSpace G
-- Mathlib.NumberTheory.ModularForms.QExpansion
CuspFormClass.exp_decay_atImInfty' : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [CuspFormClass F Γ k]
  [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)],
  ∃ c > 0, ⇑f =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-c * τ.im)
-- Mathlib.Topology.CompactOpen
/-- The continuous functions from `X` to `Y` are the same as the plain functions when `X` is
discrete.  -/
ContinuousMap.homeoFnOfDiscrete : {X : Type u_2} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [DiscreteTopology X] → C(X, Y) ≃ₜ (X → Y)
-- Lean.DocString.Parser
/-- Parses a line of text (that is, one or more inline elements).
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.textLine : optParam Bool true → Lean.Parser.ParserFn
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.add : ∀ {m : Type u_1} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [AddLeftMono R]
  {A B : Matrix m m R}, A.PosSemidef → B.PosSemidef → (A + B).PosSemidef
-- Mathlib.Control.Bitraversable.Lemmas
/-- traverse on the second functor argument  -/
Bitraversable.tsnd : {t : Type u → Type u → Type u} →
  [Bitraversable t] →
    {β : Type u} → {F : Type u → Type u} → [Applicative F] → {α α' : Type u} → (α → F α') → t β α → F (t β α')
-- Mathlib.CategoryTheory.Linear.FunctorCategory
/-- Application of a natural transformation at a fixed object,
as group homomorphism  -/
CategoryTheory.NatTrans.appLinearMap : {R : Type u_1} →
  [inst : Semiring R] →
    {C : Type u_2} →
      {D : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive D] →
              [inst_4 : CategoryTheory.Linear R D] →
                {F G : CategoryTheory.Functor C D} → (X : C) → (F ⟶ G) →ₗ[R] F.obj X ⟶ G.obj X
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.addEquiv₀_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F G : CategoryTheory.Sheaf J AddCommGrpCat}
  (f : F ⟶ G) (x : F.H 0) {Z : CategoryTheory.Sheaf J AddCommGrpCat} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Ext.addEquiv₀ ((CategoryTheory.Sheaf.H.map f 0) x)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Ext.addEquiv₀ x) (CategoryTheory.CategoryStruct.comp f h)
-- Init.Sym.Simp.SimprocDSL
/-- Rewrite using inline theorems. Optionally specify a discharger for conditional rewrites.  -/
Lean.Parser.Sym.Simp.rewriteInline : Lean.ParserDescr
-- Mathlib.Order.PartialSups
iSup_eq_iSup_of_partialSups_eq_partialSups : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : CompleteLattice α]
  {f g : ι → α}, partialSups f = partialSups g → ⨆ i, f i = ⨆ i, g i
-- Init.Data.UInt.Lemmas
UInt32.le_iff_toNat_le : ∀ {a b : UInt32}, a ≤ b ↔ a.toNat ≤ b.toNat
-- Mathlib.Data.Set.Finite.Monad
Set.Finite.bind : ∀ {α β : Type u_1} {s : Set α} {f : α → Set β}, s.Finite → (∀ a ∈ s, (f a).Finite) → (s >>= f).Finite
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_unit : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : (↥A)ˣ), A.valuation ↑↑a = 1
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic.eq_1 : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), p %ₘ q = if hq : q.Monic then (p.divModByMonicAux hq).2 else p
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.linearIndependent : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), LinearIndependent R ⇑b
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ObjectProperty.FullSubcategory.concreteCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] →
            (P : CategoryTheory.ObjectProperty C) →
              CategoryTheory.ConcreteCategory P.FullSubcategory fun X Y => FC X.obj Y.obj
-- Init.Data.Slice.Array.Iterator
instForInSubarrayOfMonad : {α : Type u} → {m : Type v → Type w} → [Monad m] → ForIn m (Subarray α) α
-- Mathlib.RingTheory.PiTensorProduct
/-- `PiTensorProduct.tprod` as a `MonoidHom`.  -/
PiTensorProduct.tprodMonoidHom : {ι : Type u_1} →
  (R : Type u_3) →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → NonAssocSemiring (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] →
              [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)] → ((i : ι) → A i) →* PiTensorProduct R fun i => A i
-- Std.Time.Zoned.ZoneRules
/-- Creates ZoneRules with a fixed offset of UTC (GMT+0).
 -/
Std.Time.TimeZone.ZoneRules.UTC : Std.Time.TimeZone.ZoneRules
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- A ring isomorphism defines an isomorphism of residue fields.  -/
IsLocalRing.ResidueField.mapEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : IsLocalRing R] →
        [inst_2 : CommRing S] →
          [inst_3 : IsLocalRing S] → R ≃+* S → IsLocalRing.ResidueField R ≃+* IsLocalRing.ResidueField S
-- Std.Data.DHashMap.Raw
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.Raw.Const.modify : {α : Type u} →
  [inst : BEq α] →
    [EquivBEq α] →
      [Hashable α] → {β : Type v} → (Std.DHashMap.Raw α fun x => β) → α → (β → β) → Std.DHashMap.Raw α fun x => β
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.piCongrLeft_apply : ∀ {ι : Type u_2} {ι' : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] {Y : ι' → Type u_4}
  [inst_2 : (j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (a : (j : ι) → Y (e.symm.symm j)) (i : ι'),
  (IsometryEquiv.piCongrLeft e) a i = ⋯ ▸ a (e.symm i)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- The shifted functors given by the shift sequence.  -/
CategoryTheory.Functor.shift : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        (F : CategoryTheory.Functor C A) →
          {M : Type u_4} →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] → [F.ShiftSequence M] → M → CategoryTheory.Functor C A
-- Mathlib.Algebra.Group.Action.Units
AddUnits.addAction'.eq_1 : ∀ {G : Type u_1} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : AddAction G M]
  [inst_3 : VAddCommClass G M M] [inst_4 : VAddAssocClass G M M],
  AddUnits.addAction' =
    { vadd := fun g m => { val := g +ᵥ ↑m, neg := -g +ᵥ ↑(-m), val_neg := ⋯, neg_val := ⋯ }, add_vadd := ⋯,
      zero_vadd := ⋯ }