mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Sublist
List.Sublist.getLast_mem : ∀ {α : Type u_1} {ys xs : List α}, ys.Sublist xs → ∀ (h : ys ≠ []), ys.getLast h ∈ xs
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toUniformConvergenceCLM_continuous : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_4}
  (F : Type u_5) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F],
  ∀ 𝔖 ⊆ {S | Bornology.IsVonNBounded 𝕜₁ S}, Continuous ⇑(ContinuousLinearMap.toUniformConvergenceCLM σ F 𝔖)
-- Mathlib.Computability.Partrec
Partrec₂.unpaired' : ∀ {f : ℕ → ℕ →. ℕ}, Nat.Partrec (Nat.unpaired f) ↔ Partrec₂ f
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.not_isSolvable : ∀ (G : Type u_1) [inst : Group G] [Nontrivial G] [Group.IsPerfect G], ¬Group.IsSolvable G
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.evalTactic : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.map_obj_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
  (g : CategoryTheory.MonoOver X),
  ((CategoryTheory.MonoOver.map f).obj g).arrow = CategoryTheory.CategoryStruct.comp g.arrow f
-- Mathlib.Algebra.Ring.Equiv
/-- Reinterpret a ring equivalence as a monoid homomorphism.  -/
RingEquiv.toMonoidHom : {R : Type u_4} → {S : Type u_5} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R ≃+* S → R →* S
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed_le_div_measure_closedBall_rIn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (x : E),
  f.normed μ x ≤ 1 / μ.real (Metric.closedBall c f.rIn)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_eq_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel (α × β) γ}
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  κ.compProd η = 0 ↔ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
-- Mathlib.Geometry.Manifold.SmoothEmbedding
Manifold.IsSmoothEmbedding.isEmbedding : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₃] [inst_4 : NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E₁ H}
  {J : ModelWithCorners 𝕜 E₃ G} {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSmoothEmbedding I J n f → Topology.IsEmbedding f
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂'_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (H : CategoryTheory.Functor C V)
  [inst_5 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {Y : CategoryTheory.Functor C V},
  (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂' F G H).homEquiv =
    (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).homEquiv.trans
      ((CategoryTheory.MonoidalCategory.externalProduct (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
            H).homEquivOfIsLeftKanExtension
        (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft
          (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
          (CategoryTheory.MonoidalCategory.DayConvolution.unit F G) H)
        (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).obj Y))
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X) ((t.eTruncGE.obj i).map f) =
    CategoryTheory.CategoryStruct.comp f ((t.eTruncGEπ i).app Y)
-- Mathlib.Topology.Order.LeftRightNhds
/-- If `S` is order-connected and contains two points `x < y`, then `S` is a punctured left
neighbourhood of `y`.  -/
Set.OrdConnected.mem_nhdsLT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {S : Set α} {x y : α},
  S.OrdConnected → x ∈ S → y ∈ S → x < y → S ∈ nhdsWithin y (Set.Iio y)
-- Mathlib.GroupTheory.Coset.Basic
/-- A group is made up of a disjoint union of cosets of a subgroup.  -/
QuotientGroup.univ_eq_iUnion_smul : ∀ {α : Type u_1} [inst : Group α] (H : Subgroup α), Set.univ = ⋃ x, Quotient.out x • ↑H
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : One α] [inst_3 : OfNat α 2] [inst_4 : Invertible 2]
  (a b : αˢʸᵐ), SymAlg.unsym (a * b) = ⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.sumNodes_T_eq : ∀ (n : ℕ),
  Polynomial.Chebyshev.sumNodes n (Polynomial.Chebyshev.leadingCoeffC✝ n) (Polynomial.Chebyshev.T ℝ ↑n) = 2 ^ (n - 1)
-- Init.Data.SInt.Lemmas
Int32.toNat_toUInt32_of_le : ∀ {x : Int32}, 0 ≤ x → x.toUInt32.toNat = x.toNatClampNeg
-- Mathlib.Data.FP.Basic
FP.Float.sign : [C : FP.FloatCfg] → FP.Float → Bool
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.lift_algebraMap_eq_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [IsScalarTower R Rₘ Sₘ] [inst_11 : IsScalarTower R S Sₘ], IsLocalization.lift ⋯ = algebraMap Rₘ Sₘ
-- Mathlib.Data.Rat.Init
Rat.cast_eq_id : Rat.cast = id
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inl_snd_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : L.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Lean.Meta.Tactic.Backtrack
/-- Configuration structure to control the behaviour of `backtrack`:
* control the maximum depth and behaviour (fail or return subgoals) at the maximum depth,
* and hooks allowing
  * modifying intermediate goals before running the external tactic,
  * 'suspending' goals, returning them in the result, and
  * discharging subgoals if the external tactic fails.
 -/
Lean.Meta.Tactic.Backtrack.BacktrackConfig : Type
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If A is an R-algebra all of whose elements are integral over R,
and B is an A-algebra all of whose elements are integral over A,
then all elements of B are integral over R.  -/
Algebra.IsIntegral.trans : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra A B] [inst_4 : Algebra R B] [inst_5 : Algebra R A] [IsScalarTower R A B] [Algebra.IsIntegral R A]
  [Algebra.IsIntegral A B], Algebra.IsIntegral R B
-- Mathlib.Algebra.Group.Action.Pi
Pi.vadd_def' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → VAdd (α i) (β i)] (s : (i : ι) → α i)
  (x : (i : ι) → β i), s +ᵥ x = fun i => s i +ᵥ x i
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.smul : {m : Type u_2} → {n : Type u_3} → {R : Type u_7} → {α : Type v} → [SMul R α] → SMul R (Matrix m n α)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.set_index_subset : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s)
  (ht : t ∈ l), s ↑(h.index t ht) ⊆ t
-- Mathlib.Algebra.Order.Group.Cone
PartialOrder.mkOfGroupCone_le_iff : ∀ {S : Type u_3} {G : Type u_4} [inst : CommGroup G] [inst_1 : SetLike S G] [inst_2 : GroupConeClass S G] {C : S}
  {a b : G}, a ≤ b ↔ b / a ∈ C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : β → β} {he : (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false},
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey he =
    if compare (t.maxKey ⋯) k = Ordering.eq then k else t.maxKey ⋯
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop.eq_1 : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gᵐᵒᵖ),
  H.unop = { carrier := MulOpposite.op ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.isProbabilityMeasure_expMeasure : ∀ {r : ℝ}, 0 < r → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.expMeasure r)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
with Haar measure. Then the `Lᵖ` norm of `u`, where `p := n / (n - 1)`, is bounded above by
a constant times the `L¹` norm of the Fréchet derivative of `u`.  -/
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_4} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] {u : E → F},
  ContDiff ℝ 1 u →
    HasCompactSupport u →
      ∀ {p : NNReal},
        (↑(Module.finrank ℝ E)).HolderConjugate p →
          MeasureTheory.eLpNorm u (↑p) μ ≤
            ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) 1 μ
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.nonneg' : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 ≤ r
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLE.toContravariantClass : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : PosMulReflectLE α],
  ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- `L` is a left adjoint  -/
CategoryTheory.Coreflective.adj : {C : Type u₁} →
  {D : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {L : CategoryTheory.Functor C D} → [self : CategoryTheory.Coreflective L] → L ⊣ CategoryTheory.Coreflective.R L
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x y : CategoryTheory.Meq P S),
  (∀ (I : S.Arrow), ↑x I = ↑y I) → x = y
-- Mathlib.Algebra.MonoidAlgebra.Opposite
AddMonoidAlgebra.opRingEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Add M] (a : AddMonoidAlgebra Rᵐᵒᵖ Mᵃᵒᵖ),
  AddMonoidAlgebra.opRingEquiv.symm a =
    MulOpposite.op
      ((AddMonoidAlgebra.mapDomainAddEquiv R AddOpposite.opEquiv.symm)
        ((AddMonoidAlgebra.mapAddEquiv Mᵃᵒᵖ MulOpposite.opAddEquiv.symm) a))
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffOn.coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_20 : MemTrivializationAtlas e] [inst_21 : MemTrivializationAtlas e'] {s : Set M} {f : M → B},
  ContMDiffOn IM IB n f s →
    Set.MapsTo f s e.baseSet →
      Set.MapsTo f s e'.baseSet →
        ContMDiffOn IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n
          (fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))) s
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_hom_associator : ∀ {R : Type u} [inst : CommSemiring R] {M N K : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom = ↑(TensorProduct.assoc R ↑M ↑N ↑K)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.funBinderTypes : Lean.Option Bool
-- Mathlib.SetTheory.Ordinal.Family
/-- The least strict upper bound of a family of ordinals.  -/
Ordinal.lsub : {ι : Type u} → (ι → Ordinal.{max u v}) → Ordinal.{max u v}
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.constantCoeff_inv : ∀ {k : Type u_2} [inst : Field k] (φ : PowerSeries k), PowerSeries.constantCoeff φ⁻¹ = (PowerSeries.constantCoeff φ)⁻¹
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- An auxiliary cocone used in the lemma `pointwiseLeftKanExtension_desc_app`  -/
CategoryTheory.Functor.costructuredArrowMapCocone : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                (G : CategoryTheory.Functor D H) →
                  (F ⟶ L.comp G) →
                    (Y : D) → CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Expand `⟪x + y, x + y⟫`  -/
InnerProductSpace.Core.inner_add_add_self : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F),
  inner 𝕜 (x + y) (x + y) = inner 𝕜 x x + inner 𝕜 x y + inner 𝕜 y x + inner 𝕜 y y
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.π_relation : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M) (r : relations.R), solution.π (relations.relation r) = 0
-- Mathlib.Algebra.Homology.Single
/-- The functor `V ⥤ CochainComplex V ℕ` creating a cochain complex supported in degree zero.  -/
CochainComplex.single₀ : (V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [CategoryTheory.Limits.HasZeroObject V] → CategoryTheory.Functor V (CochainComplex V ℕ)
-- Mathlib.Topology.Algebra.FilterBasis
/-- A `ModuleFilterBasis` on a module is a `FilterBasis` satisfying some additional axioms.
Example : if `M` is a topological module then the neighbourhoods of zero are a
`ModuleFilterBasis`. Conversely given a `ModuleFilterBasis` one can define a topology
compatible with the module structure on `M`.  -/
ModuleFilterBasis : (R : Type u_1) →
  (M : Type u_2) → [inst : Semiring R] → [TopologicalSpace R] → [inst_2 : AddCommGroup M] → [Module R M] → Type u_2
-- Init.Core
Array.mk.inj : ∀ {α : Type u} {toList toList_1 : List α}, { toList := toList } = { toList := toList_1 } → toList = toList_1
-- Mathlib.Topology.Algebra.Algebra
/-- The topological closure of the subalgebra generated by a single element.  -/
Algebra.elemental : (R : Type u_1) →
  [inst : CommSemiring R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Semiring A] → [inst_3 : Algebra R A] → [IsSemitopologicalSemiring A] → A → Subalgebra R A
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.semireducible : Lean.ReducibilityStatus
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The morphism of presheaves of `R`-modules `free I ⟶ free J` induced by
a map `f : I → J`.  -/
SheafOfModules.freeMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {I J_1 : Type u} → (I → J_1) → (SheafOfModules.free I ⟶ SheafOfModules.free J_1)
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The equivalence `Arrow (Discrete S) ≃ S`.  -/
CategoryTheory.Arrow.discreteEquiv : (S : Type u) → CategoryTheory.Arrow (CategoryTheory.Discrete S) ≃ S
-- Mathlib.LinearAlgebra.FreeModule.PID
eq_bot_of_generator_maximal_map_eq_zero : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_1}
  (b : Module.Basis ι R M) {N : Submodule R M} {ϕ : M →ₗ[R] R},
  (∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N) →
    ∀ [inst_3 : (Submodule.map ϕ N).IsPrincipal], Submodule.IsPrincipal.generator (Submodule.map ϕ N) = 0 → N = ⊥
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.succFn_spec : ∀ {ι : Type u_1} [inst : LinearOrder ι] (i : ι), IsGLB (Set.Ioi i) (LinearLocallyFiniteOrder.succFn i)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.id_s₀`. -/
AlgebraicGeometry.Scheme.Cover.id_idx_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (a : E.I₀),
  (CategoryTheory.CategoryStruct.id E).s₀ a = a
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.le_weightedOrder_subst : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} (w : τ → ℕ),
  PowerSeries.HasSubst a →
    ∀ (f : PowerSeries R),
      f.order * MvPowerSeries.weightedOrder w a ≤ MvPowerSeries.weightedOrder w (PowerSeries.subst a f)
-- Mathlib.Order.MinMax
min_right_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), min (min a b) c = min (min a c) b
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `Nat.sub a b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalNatSub : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorNat : LawfulXor ℕ
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step_done : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {upper : α},
  { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }.step = Std.IterStep.done
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.pushoutCocone_inr : ∀ (R A B : Type u) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A]
  [inst_4 : Algebra R B],
  (CommRingCat.pushoutCocone R A B).inr = CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_image_le_of_one_le : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} {ι' : Type u_9}
  [inst_2 : DecidableEq ι'] [MulLeftMono N] {g : ι → ι'} {f : ι' → N},
  (∀ u ∈ Finset.image g s, 1 ≤ f u) → ∏ u ∈ Finset.image g s, f u ≤ ∏ u ∈ s, f (g u)
-- Mathlib.Tactic.Ring.RingNF
/-- The normalization style for `ring_nf`.  -/
Mathlib.Tactic.RingNF.RingMode : Type
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.eq_2 : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n → α → α) (a : α) (m : ℕ) (h : m.succ ≤ n),
  Nat.foldTR.loop✝ n f m.succ h a = Nat.foldTR.loop✝ n f m ⋯ (f (n - m.succ) ⋯ a)
-- Lean.MonadEnv
Lean.isInductiveCore? : Lean.Environment → Lean.Name → Option Lean.InductiveVal
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_div : ∀ (a b : BitVec 64), { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Function.Surjective ⇑Monoid.Coprod.snd
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_neg : ∀ {x : ℝ*}, ¬x.Infinite → ¬(-x).Infinite
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- *Faa di Bruno* formula: If two functions `g` and `f` have Taylor series up to `n` given by
`q` and `p`, then `g ∘ f` also has a Taylor series, given by `q.taylorComp p`.  -/
HasFTaylorSeriesUpToOn.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {t : Set F}
  {q : F → FormalMultilinearSeries 𝕜 F G} {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} {g : F → G}
  {f : E → F},
  HasFTaylorSeriesUpToOn n g q t →
    HasFTaylorSeriesUpToOn n f p s →
      Set.MapsTo f s t → HasFTaylorSeriesUpToOn n (g ∘ f) (fun x => (q (f x)).taylorComp (p x)) s
-- Mathlib.RingTheory.ChainOfDivisors
factor_orderIso_map_one_eq_bot : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [IsCancelMulZero N] {m : Associates M} {n : Associates N} (d : { l // l ≤ m } ≃o { l // l ≤ n }), ↑(d ⟨1, ⋯⟩) = 1