mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Given `ModularForm`'s `F i` of weight `k i` for `i : ι`, define the form which as a
function is a product of those indexed by `s : Finset ι` with weight `m = ∑ i ∈ s, k i`.  -/
ModularForm.prod : {ι : Type} →
  {s : Finset ι} →
    {k : ι → ℤ} →
      (m : ℤ) →
        m = ∑ i ∈ s, k i →
          {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → ((i : ι) → ModularForm Γ (k i)) → ModularForm Γ m
-- Mathlib.MeasureTheory.Order.Lattice
Measurable.const_sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : α → M} [inst_1 : Max M]
  [MeasurableSup M], Measurable f → ∀ (c : M), Measurable fun x => c ⊔ f x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- This is the natural linear isometry induced by `f : F ≃ₗᵢ G`.  -/
LinearIsometry.lTensor : {𝕜 : Type u_1} →
  (E : Type u_2) →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] → (F →ₗᵢ[𝕜] G) → TensorProduct 𝕜 E F →ₗᵢ[𝕜] TensorProduct 𝕜 E G
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMaps.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C],
  (∀ {f g : CategoryTheory.Arrow C} (st : f ⟶ g), CategoryTheory.Limits.HasImageMap st) →
    CategoryTheory.Limits.HasImageMaps C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.keyAtIdxD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keyAtIdxD i fallback = t₂.keyAtIdxD i fallback
-- Mathlib.Algebra.MonoidAlgebra.Opposite
MonoidAlgebra.opRingEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Mul M] (a : MonoidAlgebra Rᵐᵒᵖ Mᵐᵒᵖ),
  MonoidAlgebra.opRingEquiv.symm a =
    MulOpposite.op
      ((MonoidAlgebra.mapDomainAddEquiv R MulOpposite.opEquiv.symm)
        ((MonoidAlgebra.mapAddEquiv Mᵐᵒᵖ MulOpposite.opAddEquiv.symm) a))
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
CategoryTheory.Functor.preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.EnoughProjectives C] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [F.PreservesProjectiveObjects], G.PreservesEpimorphisms
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (A : Type u_1) [inst_3 : CommRing A] [inst_4 : Algebra S A] [inst_5 : Algebra P.Ring A]
  [inst_6 : IsScalarTower P.Ring S A],
  KaehlerDifferential.cotangentComplexBaseChange R S P.Ring A =
    ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ
      LinearMap.baseChange A P.cotangentComplex ∘ₗ
        ↑((TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
            LinearEquiv.baseChange S A (TensorProduct P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.isoMk_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Lax.OplaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Lax.OplaxTrans.isoMk app naturality).inv.as.app a = (app a).inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constEntryAtIdx?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.entryAtIdx? t₁ i = Std.DTreeMap.Raw.Const.entryAtIdx? t₂ i
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite products of meromorphic functions are meromorphic.  -/
MeromorphicOn.fun_prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_5} {s : Finset ι} {f : ι → 𝕜 → 𝕜'},
  (∀ σ ∈ s, MeromorphicOn (f σ) U) → MeromorphicOn (fun z => ∏ n ∈ s, f n z) U
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_3 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (w_2 start : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w_2),
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.extract start w expr) =
    BitVec.extractLsb' start w (Std.Tactic.BVDecide.BVExpr.eval assign expr)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.LocalTimeType.mk.sizeOf_spec : ∀ (gmtOffset : Std.Time.TimeZone.Offset) (isDst : Bool) (abbreviation : String) (wall : Std.Time.TimeZone.StdWall)
  (utLocal : Std.Time.TimeZone.UTLocal) (identifier : String),
  sizeOf
      { gmtOffset := gmtOffset, isDst := isDst, abbreviation := abbreviation, wall := wall, utLocal := utLocal,
        identifier := identifier } =
    1 + sizeOf gmtOffset + sizeOf isDst + sizeOf abbreviation + sizeOf wall + sizeOf utLocal + sizeOf identifier
-- Std.Http.Server.Handler
/-- Body instance required by the connection loop for receiving response chunks.
 -/
Std.Http.Server.Handler.responseBodyInstance : {σ : Type} → [self : Std.Http.Server.Handler σ] → Std.Http.Body (Std.Http.Server.Handler.ResponseBody σ)
-- Mathlib.Analysis.SpecificLimits.Basic
le_geom : ∀ {u : ℕ → ℝ} {c : ℝ}, 0 ≤ c → ∀ (n : ℕ), (∀ k < n, u (k + 1) ≤ c * u k) → u n ≤ c ^ n * u 0
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.integral_rnDeriv_smul : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {E : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite μ] {f : α → E},
  μ.AbsolutelyContinuous ν → ∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_whiskerRight : ∀ {R : Type u} [inst : CommRing R] {L M : ModuleCat R} (f : L ⟶ M) (N : ModuleCat R),
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) =
    LinearMap.rTensor (↑N) (ModuleCat.Hom.hom f)
-- Mathlib.Data.Num.Lemmas
Num.castNum_or : ∀ (m n : Num), ↑(m ||| n) = ↑m ||| ↑n
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabEnsureExpectedType : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.mul : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommSemiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {I J : Ideal A},
  Ideal.IsHomogeneous 𝒜 I → Ideal.IsHomogeneous 𝒜 J → Ideal.IsHomogeneous 𝒜 (I * J)
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuousOn_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {s : Set β},
  ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, edist (f x) (f b) < ε
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.smul_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] {S : Type u_10} [inst_7 : TopologicalSpace W] [inst_8 : Monoid S]
  [inst_9 : DistribMulAction S W] [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W]
  [inst_12 : TopologicalSpace V] [inst_13 : IsTopologicalAddTorsor P] [inst_14 : IsTopologicalAddGroup W] (t : S)
  (f : P →ᴬ[R] W), (t • f).contLinear = t • f.contLinear
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_apply : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (x : 𝕜), logDeriv f x = deriv f x / f x
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.LiftRelAux.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ Computation α → β ⊕ Computation β → Sort u_3) (a : α) (cb : Computation β)
  (h_1 : (a : α) → (b : β) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (a : α) → (cb : Computation β) → motive (Sum.inl a) (Sum.inr cb))
  (h_3 : (ca : Computation α) → (b : β) → motive (Sum.inr ca) (Sum.inl b))
  (h_4 : (ca : Computation α) → (cb : Computation β) → motive (Sum.inr ca) (Sum.inr cb)),
  (match Sum.inl a, Sum.inr cb with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl a, Sum.inr cb => h_2 a cb
    | Sum.inr ca, Sum.inl b => h_3 ca b
    | Sum.inr ca, Sum.inr cb => h_4 ca cb) =
    h_2 a cb
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.range_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (AlgHom.id R A).range = ⊤
-- Mathlib.Algebra.Lie.Sl2
/-- Given a representation of a Lie algebra with distinguished `sl₂` triple, a simultaneous
eigenvector for the action of both `h` and `e` necessarily has eigenvalue zero for `e`.  -/
IsSl2Triple.HasPrimitiveVectorWith.mk' : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] {h e f : L}
  [IsAddTorsionFree M] (t : IsSl2Triple h e f) (m : M) (μ ρ : R),
  m ≠ 0 → ⁅h, m⁆ = μ • m → ⁅e, m⁆ = ρ • m → t.HasPrimitiveVectorWith m μ
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_nnrpow_two_mul : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A)
  (x : NNReal), CFC.abs a ^ (2 * x) = (star a * a) ^ x
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_sup'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (fun a => s.sup' hne fun x => f x a) x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.isLeftAdjoint_pushforward_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [F.IsCocontinuous J K]
  [CategoryTheory.IsIso φ] [F.IsLeftAdjoint], (SheafOfModules.pushforward φ).IsLeftAdjoint
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_two_lt_three_halves : √2 < 3 / 2
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `‖f a‖ ≤ B a`;
* `f` has right derivative `f'` at every point of `[a, b)`;
* `B` has derivative `B'` everywhere on `ℝ`;
* the norm of `f'` is strictly less than `B'` whenever `‖f x‖ = B x`.

Then `‖f x‖ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
to make this theorem work for piecewise differentiable functions.
 -/
image_norm_le_of_norm_deriv_right_lt_deriv_boundary : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        ‖f a‖ ≤ B a →
          (∀ (x : ℝ), HasDerivAt B (B' x) x) →
            (∀ x ∈ Set.Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Delaborator for `mvfderiv`.  -/
Manifold.delabMVFDeriv : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- If `φ : K ⟶ L` is a morphism of cochain complexes in `C` and `G : C ⥤ D` is an
additive functor, then the image by `G` of the triangle `triangleh φ` identifies to
the triangle associated to the image of `φ` by `G`.  -/
CochainComplex.mappingCone.mapTrianglehIso : {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.Preadditive C] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            [inst_4 : CategoryTheory.Preadditive D] →
              [inst_5 : CategoryTheory.Limits.HasBinaryBiproducts D] →
                {K L : CochainComplex C ℤ} →
                  (φ : K ⟶ L) →
                    (G : CategoryTheory.Functor C D) →
                      [inst_6 : G.Additive] →
                        (G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj
                            (CochainComplex.mappingCone.triangleh φ) ≅
                          CochainComplex.mappingCone.triangleh ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
-- Aesop.Tree.Data
Aesop.Goal.setState : Aesop.GoalState → Aesop.Goal → Aesop.Goal
-- Mathlib.CategoryTheory.Shift.Linear
CategoryTheory.Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ' : ∀ (R : Type u_1) [inst : Ring R] {C : Type u_5} [inst_1 : CategoryTheory.Category.{v_1, u_5} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {M : Type u_3} [inst_4 : AddMonoid M]
  [inst_5 : CategoryTheory.HasShift C M] [∀ (n : M), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)]
  (W : CategoryTheory.MorphismProperty C) (n : M) [inst_7 : W.HasLocalization]
  [inst_8 : CategoryTheory.HasShift W.Localization' M] [W.Q'.CommShift M]
  [inst_10 : CategoryTheory.Preadditive W.Localization'] [inst_11 : CategoryTheory.Linear R W.Localization']
  [CategoryTheory.Functor.Linear R W.Q'],
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor W.Localization' n)
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_roi : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = xs.size - (lo + 1)
-- Std.Http.Data.URI
/-- Attempts to parse a URI path from the given string.
Returns `none` if the string is not a valid path.
 -/
Std.Http.URI.Path.parse? : String → Option Std.Http.URI.Path
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
cexp_neg_quadratic_isLittleO_rpow_atTop : ∀ {a : ℂ}, a.re < 0 → ∀ (b : ℂ) (s : ℝ), (fun x => Complex.exp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.atTop] fun x => x ^ s
-- Lean.Declaration
Lean.ConstantInfo.ctorInfo.inj : ∀ {val val_1 : Lean.ConstructorVal}, Lean.ConstantInfo.ctorInfo val = Lean.ConstantInfo.ctorInfo val_1 → val = val_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, (Std.ExtTreeMap.filterMap f t).contains k = true → t.contains k = true
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.refl_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] (x : P₁), (ContinuousAffineEquiv.refl k P₁) x = x
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv_char_of_ne : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], a ≠ b → (RegularExpression.char a).deriv b = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_biInf : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_5} {s : Set ι} {H : ι → Subgroup G},
  (∀ i ∈ s, (H i).Characteristic) → (⨅ i ∈ s, H i).Characteristic
-- Init.Data.List.Attach
List.pmap_reverse : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs.reverse, P a),
  List.pmap f xs.reverse H = (List.pmap f xs ⋯).reverse
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mul_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (p₁.mul_nc p₂) =
        Lean.Grind.CommRing.Poly.denoteS ctx p₁ * Lean.Grind.CommRing.Poly.denoteS ctx p₂
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A sequence of simple functions such that
`∀ x, Tendsto (fun n => hf.approx n x) atTop (𝓝 (f x))`.
That property is given by `stronglyMeasurable.tendsto_approx`.  -/
MeasureTheory.StronglyMeasurable.approx : {α : Type u_1} →
  {β : Type u_2} →
    {f : α → β} →
      [inst : TopologicalSpace β] →
        {x : MeasurableSpace α} → MeasureTheory.StronglyMeasurable f → ℕ → MeasureTheory.SimpleFunc α β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get a ⋯
-- Mathlib.Data.Int.GCD
pow_eq_pow_iff_of_coprime : ∀ {α : Type u_1} [inst : CommGroupWithZero α] {a b : α} {m n : ℕ},
  m.Coprime n → (a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m)
-- Mathlib.Topology.Compactness.SigmaCompact
iUnion_compactCovering : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X], ⋃ n, compactCovering X n = Set.univ
-- Mathlib.Data.Sym.Sym2
Sym2.out_fst_mem : ∀ {α : Type u_1} (e : Sym2 α), (Quot.out e).1 ∈ e
-- Init.Data.Order.Classes
/-- This typeclass states that the order structure on `α`, represented by an `LE α` instance,
is a linear preorder.
In other words, the less-or-equal relation is reflexive, transitive and total.
 -/
Std.IsLinearPreorder : (α : Type u) → [LE α] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.paste_vert_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ →
    CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
      (CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
          (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔
        CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁)
-- Mathlib.Logic.Basic
instDecidableXor : {a b : Prop} → [Decidable a] → [Decidable b] → Decidable (Xor a b)
-- Mathlib.Order.Bounded
Set.bounded_gt_Ici : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a : α), Set.Bounded (fun x1 x2 => x1 > x2) (Set.Ici a)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State.mk.inj : ∀ {annotations : Lean.PrettyPrinter.Delaborator.OptionsPerPos} {postponed : Array (Lean.Expr × Lean.Expr)}
  {annotations_1 : Lean.PrettyPrinter.Delaborator.OptionsPerPos} {postponed_1 : Array (Lean.Expr × Lean.Expr)},
  { annotations := annotations, postponed := postponed } = { annotations := annotations_1, postponed := postponed_1 } →
    annotations = annotations_1 ∧ postponed = postponed_1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
SupBotHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] [inst_2 : Bot α] [inst_3 : Bot β]
  (toSupHom toSupHom_1 : SupHom α β) (e_toSupHom : toSupHom = toSupHom_1) (map_bot' : toSupHom.toFun ⊥ = ⊥),
  { toSupHom := toSupHom, map_bot' := map_bot' } = { toSupHom := toSupHom_1, map_bot' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNatClamp_of_le : ∀ {n : ℕ}, UInt32.size ≤ n → (UInt32.ofNatClamp n).toNat = UInt32.size - 1
-- Batteries.Lean.Except
ExceptT.mk_run : ∀ {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (x : ExceptT ε m α), ExceptT.mk x.run = x
-- Mathlib.Algebra.Star.Unitary
val_unitarySubgroupUnitsEquiv_symm_apply_coe : ∀ {M : Type u_5} [inst : Monoid M] [inst_1 : StarMul M] (x : ↥(unitary M)), ↑↑(unitarySubgroupUnitsEquiv.symm x) = ↑x
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Auxiliary definition for `mapTrifunctor`.  -/
CategoryTheory.GradedObject.mapTrifunctorObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)) →
                  {I₁ : Type u_7} →
                    CategoryTheory.GradedObject I₁ C₁ →
                      (I₂ : Type u_8) →
                        (I₃ : Type u_9) →
                          CategoryTheory.Functor (CategoryTheory.GradedObject I₂ C₂)
                            (CategoryTheory.Functor (CategoryTheory.GradedObject I₃ C₃)
                              (CategoryTheory.GradedObject (I₁ × I₂ × I₃) C₄))
-- Mathlib.Data.List.MinMax
List.argmax_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {l : List α} {m : α},
  m ∈ List.argmax f l → m ∈ l
-- Init.Data.UInt.Lemmas
UInt8.ofFin_add : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a + b) = UInt8.ofFin a + UInt8.ofFin b
-- Mathlib.Algebra.GroupWithZero.Center
Set.zero_mem_center : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], 0 ∈ Set.center M₀
-- Lean.Elab.PreDefinition.WF.Fix
/-- Refine `F` over `PSum.casesOn`  -/
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.processSumCasesOn : Lean.Expr →
  Lean.Expr →
    Lean.Expr → (Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Data.List.Rotate
/-- If a `l : List α` is `Nodup l`, then all of its cyclic permutants are distinct.  -/
List.Nodup.cyclicPermutations : ∀ {α : Type u} {l : List α}, l.Nodup → l.cyclicPermutations.Nodup
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vadd_set_ae_le : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s t : Set α},
  c +ᵥ s ≤ᵐ[μ] c +ᵥ t ↔ s ≤ᵐ[μ] t
-- Mathlib.Analysis.Complex.CoveringMap
isQuotientCoveringMap_npow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℕ),
  ↑n ≠ 0 → (Function.Surjective fun x => x ^ n) → IsQuotientCoveringMap (fun x => x ^ n) ↥(powMonoidHom n).ker