mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural embedding `α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i`.  -/
Subgroup.quotientiInfEmbedding : {α : Type u_1} → [inst : Group α] → {ι : Type u_2} → (f : ι → Subgroup α) → α ⧸ ⨅ i, f i ↪ (i : ι) → α ⧸ f i
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
Construct the limiting coalgebra from the map `λ : L ⟶ TL` given by `lambda`. We are required to
show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of `D`
and our `commuting` lemma.
 -/
CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          {D : CategoryTheory.Functor J T.Coalgebra} →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) →
              CategoryTheory.Limits.IsLimit c →
                [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] →
                  [CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] → T.Coalgebra
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.instReprPostponeBehavior.repr : Lean.Elab.Term.PostponeBehavior → ℕ → Std.Format
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + g x) ^ x` as `(x : ℝ) → ∞` is `exp t`,
where `t : ℂ` is the limit of `x * g x`.  -/
Complex.tendsto_one_add_cpow_exp_of_tendsto : ∀ {g : ℝ → ℂ} {t : ℂ},
  Filter.Tendsto (fun x => ↑x * g x) Filter.atTop (nhds t) →
    Filter.Tendsto (fun x => (1 + g x) ^ ↑x) Filter.atTop (nhds (Complex.exp t))
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_union_right : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α]
  [inst_3 : DecidableEq α], a ∉ upperClosure ↑s → a ∈ upperClosure ↑t → (s ∪ t).truncatedInf a = t.truncatedInf a
-- Mathlib.Order.Fin.Basic
/-- `Fin.cast` as an `OrderIso`.

`castOrderIso eq i` embeds `i` into an equal `Fin` type.  -/
Fin.castOrderIso : {m n : ℕ} → n = m → Fin n ≃o Fin m
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_coeff_apply_aux_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (k : ℕ)
  (x : R), matPolyEquiv (Matrix.single i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.single i j x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The equivalence setoid for a Jacobian point representative on a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.instSetoidForallFinOfNatNat : {R : Type r} → [CommRing R] → Setoid (Fin 3 → R)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Given a symmetric bilinear form `B` on some vector space `V` over a field `K`
in which `2` is invertible, there exists an orthogonal basis with respect to `B`.  -/
LinearMap.BilinForm.exists_orthogonal_basis : ∀ {V : Type u} {K : Type v} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  [hK : Invertible 2] {B : LinearMap.BilinForm K V}, LinearMap.IsSymm B → ∃ v, LinearMap.IsOrthoᵢ B ⇑v
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotate_map_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.rotate C).map f).hom₂ = f.hom₃
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁), S.δ F n₀ n₁ h = S.δ F n₀ n₁ h
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- A restatement of `sum_ite_self_eq` with the equality test reversed.  -/
Finsupp.sum_ite_self_eq' : ∀ {α : Type u_1} [inst : DecidableEq α] {N : Type u_16} [inst_1 : AddCommMonoid N] (f : α →₀ N) (a : α),
  (f.sum fun x v => if x = a then v else 0) = f a
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), φ.order = if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.mem_face_iff : ∀ {n : ℕ} (S : Finset (Fin (n + 1))) {d : ℕ} (x : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })),
  x ∈ (SSet.stdSimplex.face S).obj (Opposite.op { len := d }) ↔ ∀ (i : Fin (d + 1)), x i ∈ S
-- Mathlib.Logic.Embedding.Basic
/-- An embedding `e : α ↪ β` defines an embedding `(γ → α) ↪ (γ → β)` that sends each `f`
to `e ∘ f`.  -/
Function.Embedding.arrowCongrRight : {α : Sort u} → {β : Sort v} → {γ : Sort w} → (α ↪ β) → (γ → α) ↪ γ → β
-- Init.Data.Option.Lemmas
Option.reflBEq_iff : ∀ {α : Type u_1} [inst : BEq α], ReflBEq (Option α) ↔ ReflBEq α
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.of_split : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {P : Type u_2}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] [Algebra.FormallySmooth R P] (f : P →ₐ[R] A)
  (g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2), f.kerSquareLift.comp g = AlgHom.id R A → Algebra.FormallySmooth R A
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.not_a_field' : ∀ {R : Type u} {inst : CommRing R} {inst_1 : IsDomain R} [self : IsDiscreteValuationRing R],
  IsLocalRing.maximalIdeal R ≠ ⊥
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- The functor `J ⥤ C` induced by `functorToMonoOver hG A₀ J : J ⥤ MonoOver X`.  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : C} →
      [inst_1 : CategoryTheory.Abelian C] →
        CategoryTheory.IsSeparator G →
          {X : C} →
            [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
              CategoryTheory.Subobject X →
                (J : Type w) →
                  [inst_3 : LinearOrder J] →
                    [OrderBot J] → [SuccOrder J] → [WellFoundedLT J] → CategoryTheory.Functor J C
-- Mathlib.Algebra.RingQuot
RingQuot.instIsScalarTower : ∀ {R : Type uR} [inst : Semiring R] {S : Type uS} [inst_1 : CommSemiring S] {T : Type uT} (r : R → R → Prop)
  [inst_2 : CommSemiring T] [inst_3 : SMul S T] [inst_4 : Algebra S R] [inst_5 : Algebra T R] [IsScalarTower S T R],
  IsScalarTower S T (RingQuot r)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_series_injective : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] [Nontrivial E], Function.Injective (FormalMultilinearSeries.ofScalars E)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_lt_of_lt_ediv : ∀ {a b c : ℤ}, 0 < c → a < b / c → a * c < b
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofNat' : ∀ {n : ℕ}, (ISize.ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_pow : ∀ (f : CircleDeg1Lift) (n : ℕ), (f ^ n).translationNumber = ↑n * f.translationNumber
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk.sizeOf_spec : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : SizeOf B] [inst_3 : SizeOf F] [inst_4 : SizeOf Z] (toPartialEquiv : PartialEquiv Z (B × F))
  (open_target : IsOpen toPartialEquiv.target) (baseSet : Set B) (open_baseSet : IsOpen baseSet)
  (source_eq : toPartialEquiv.source = proj ⁻¹' baseSet) (target_eq : toPartialEquiv.target = baseSet ×ˢ Set.univ)
  (proj_toFun : ∀ p ∈ toPartialEquiv.source, (↑toPartialEquiv p).1 = proj p),
  sizeOf
      { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
    1 + sizeOf toPartialEquiv + sizeOf open_target + sizeOf open_baseSet + sizeOf source_eq + sizeOf target_eq
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.eventually_star_eq : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {l : Filter A},
  l.IsIncreasingApproximateUnit → ∀ᶠ (x : A) in l, star x = x
-- Init.Data.Array.Nat
Array.sum_div_length_le_max_nat : ∀ {xs : Array ℕ} (h : xs ≠ #[]), xs.sum / xs.size ≤ xs.max h
-- Mathlib.Order.Irreducible
not_infPrime : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, ¬InfPrime a ↔ IsMax a ∨ ∃ b c, b ⊓ c ≤ a ∧ ¬b ≤ a ∧ ¬c ≤ a
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGE_eq_pos : ∀ {s : String.Slice} {p : String.Pos.Raw} (h : String.Pos.Raw.IsValidForSlice s p), s.posGE p ⋯ = s.pos p h
-- Init.Data.SInt.Basic
instMulInt32 : Mul Int32
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X) f
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuousAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α},
  SemicontinuousAt r x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhds x, ¬r x' y) → ¬r x y
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncTotal_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R)
  {x : σ →₀ ℕ}, n ≤ Finsupp.degree x → MvPolynomial.coeff x ((MvPowerSeries.truncTotal n) p) = 0
-- Lean.Parser.Command
Lean.Parser.Command.deriving : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Basic
add_eq_right : ∀ {M : Type u_4} [inst : AddMonoid M] [IsRightCancelAdd M] {a b : M}, a + b = b ↔ a = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : β →+o γ) (g : α →+o β) (a : α),
  (f.comp g) a = f (g a)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.finite_quotient_of_pretransitive_of_finite_quotient : ∀ {G : Type u} (X : Type v) [inst : Group G] [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {H : Subgroup G}
  [Finite (G ⧸ H)], Finite (MulAction.orbitRel.Quotient (↥H) X)
-- Mathlib.Lean.MessageData.ForExprs
Lean.MessageData.Exprs.mk.injEq : ∀ (msg msg_1 : Lean.MessageData), ({ msg := msg } = { msg := msg_1 }) = (msg = msg_1)
-- Mathlib.Testing.Plausible.Functions
/-- Produce a string for a given `InjectiveFunction`.
The output is of the form `[x₀ ↦ f x₀, .. xₙ ↦ f xₙ, x ↦ x]`.
Unlike for `TotalFunction`, the default value is not a constant
but the identity function.
 -/
Plausible.InjectiveFunction.repr : {α : Type u} → [Repr α] → Plausible.InjectiveFunction α → String
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
/-- If a perfect pairing over a field `L` takes values in a subfield `K` along two `K`-subspaces
whose `L` span is full, then these subspaces induce a `K`-structure in the sense of
[*Algebra I*, Bourbaki : Chapter II, §8.1 Definition 1][bourbaki1989].  -/
LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module L M] [inst_6 : Module L N] [inst_7 : Module K M]
  [inst_8 : Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] (M' : Submodule K M)
  (N' : Submodule K N),
  Submodule.span L ↑M' = ⊤ →
    Submodule.span L ↑N' = ⊤ →
      (∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range) → ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)
-- Lean.Syntax
Lean.Syntax.getAtomVal : Lean.Syntax → String
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ι_functorMapSrc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  (i : I) (t : A i ⟶ X) (b : B i ⟶ S)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b) (b' : B i ⟶ T)
  (hb' : CategoryTheory.CategoryStruct.comp b (CategoryTheory.Arrow.Hom.right τ) = b') (t' : A i ⟶ Y)
  (ht' : CategoryTheory.CategoryStruct.comp t (CategoryTheory.Arrow.Hom.left τ) = t'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjSrcFamily f πX)
        { i := i, t := t, b := b, w := w })
      (CategoryTheory.SmallObject.functorMapSrc f τ) =
    CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjSrcFamily f πY)
      { i := i, t := t', b := b', w := ⋯ }
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Create one measure for each (eligible) parameter of the given predefinition.   -/
Lean.Elab.WF.GuessLex.simpleMeasures : Array Lean.Elab.PreDefinition →
  Lean.Elab.FixedParamPerms → Array (Array Lean.Name) → Lean.MetaM (Array (Array Lean.Elab.WF.GuessLex.BasicMeasure))
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_neg : ∀ {R : Type u} [inst : Ring R] (a : Polynomial R), (-a).toFinsupp = -a.toFinsupp
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.inf_le_invariants_comp : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f g : α → α),
  MeasurableSpace.invariants f ⊓ MeasurableSpace.invariants g ≤ MeasurableSpace.invariants (f ∘ g)
-- Mathlib.Analysis.Complex.CoveringMap
isCoveringMapOn_npow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℕ),
  ↑n ≠ 0 → IsCoveringMapOn (fun x => x ^ n) {0}ᶜ
-- Mathlib.Topology.Convenient.Category
/-- The adjunction between the categories `ContinuousGeneratedByCat X` and `TopCat`.  -/
ContinuousGeneratedByCat.adj : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      ContinuousGeneratedByCat.toTopCat X ⊣ TopCat.toContinuousGeneratedByCat X
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.eqOn_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
  [T2Space Y] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {s : Set X} {f g : X → Y},
  f =ᵐ[μ.restrict s] g → ContinuousOn f s → ContinuousOn g s → s ⊆ closure (interior s) → Set.EqOn f g s
-- Mathlib.Data.Sigma.Basic
sigma_mk_injective : ∀ {α : Type u_1} {β : α → Type u_4} {i : α}, Function.Injective (Sigma.mk i)
-- Mathlib.GroupTheory.Order.Min
Monoid.le_minOrder : ∀ {α : Type u_2} [inst : Monoid α] {n : ℕ∞},
  n ≤ Monoid.minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.closedEBall`.

---

`Metric.closedEBall x ε` is the set of all points `y` with `edist y x ≤ ε`  -/
EMetric.closedBall : {α : Type u} → [PseudoEMetricSpace α] → α → ENNReal → Set α
-- Init.Data.Nat.Div.Basic
Nat.mod_eq_sub_div_mul : ∀ {x k : ℕ}, x % k = x - x / k * k
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.instHasKernelsFullSubcategoryOfIsClosedUnderKernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderKernels] [CategoryTheory.Limits.HasKernels C],
  CategoryTheory.Limits.HasKernels P.FullSubcategory
-- Mathlib.Order.Hom.BoundedLattice
/-- The type of finitary infimum-preserving homomorphisms from `α` to `β`.  -/
InfTopHom : (α : Type u_6) → (β : Type u_7) → [Min α] → [Min β] → [Top α] → [Top β] → Type (max u_6 u_7)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.inter_eq_inter! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l₁ l₂ : Std.DTreeMap.Internal.Impl α β} {h : l₁.Balanced},
  l₁.inter l₂ h = l₁.inter! l₂
-- Std.Net.Addr
Std.Net.IPAddr.instToString : ToString Std.Net.IPAddr
-- Init.Data.Ord.Array
Array.compare_eq_compare_toList : ∀ {α : Type u_1} [inst : Ord α] {a₁ a₂ : Array α}, compare a₁ a₂ = compare a₁.toList a₂.toList
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.bot_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A], ⊥.toSubalgebra = ⊥
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- The external product bifunctor: given diagrams
`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`.  -/
CategoryTheory.MonoidalCategory.externalProductBifunctor : (J₁ : Type u₁) →
  (J₂ : Type u₂) →
    (C : Type u₃) →
      [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            [CategoryTheory.MonoidalCategory C] →
              CategoryTheory.Functor (CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C)
                (CategoryTheory.Functor (J₁ × J₂) C)
-- Mathlib.RingTheory.Morita.Basic
MoritaEquivalence.mk : {R : Type u₀} →
  [inst : CommSemiring R] →
    {A : Type u₁} →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {B : Type u₂} →
            [inst_3 : Ring B] →
              [inst_4 : Algebra R B] →
                (eqv : ModuleCat A ≌ ModuleCat B) →
                  autoParam (CategoryTheory.Functor.Linear R eqv.functor) MoritaEquivalence.linear._autoParam →
                    MoritaEquivalence R A B
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.le_opNorm_mul_prod_of_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {m : ι → E} (f : E [⋀^ι]→L[𝕜] F) {b : ι → ℝ},
  (∀ (i : ι), ‖m i‖ ≤ b i) → ‖f m‖ ≤ ‖f‖ * ∏ i, b i
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_inl_union_inr_eq_prod : ∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (s : Set A) (t : Set B),
  Algebra.adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) =
    (Algebra.adjoin R s).prod (Algebra.adjoin R t)
-- Mathlib.Order.Types.Defs
OrderType.liftOn₂_type : ∀ {α : Type u} {β : Type v} {δ : Type u_1} [inst : LinearOrder α] [inst_1 : LinearOrder β]
  (f : (α : Type u) → [LinearOrder α] → (β : Type v) → [LinearOrder β] → δ)
  (c :
    ∀ (α₁ : Type u) [inst : LinearOrder α₁] (β₁ : Type v) [inst_2 : LinearOrder β₁] (α₂ : Type u)
      [inst_3 : LinearOrder α₂] (β₂ : Type v) [inst_4 : LinearOrder β₂],
      OrderType.type α₁ = OrderType.type α₂ → OrderType.type β₁ = OrderType.type β₂ → f α₁ β₁ = f α₂ β₂),
  (OrderType.type α).liftOn₂ (OrderType.type β) f c = f α β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List ((a : α) × β a)}, (t.insertMany l).size ≤ t.size + l.length
-- Mathlib.Algebra.Field.Basic
DivisionRing.isDomain : ∀ {K : Type u_1} [inst : DivisionRing K], IsDomain K
-- Mathlib.Data.Fintype.EquivFin
/-- If the cardinality of `α` is `n`, there is computably a bijection between `α` and `Fin n`.

See `Fintype.equivFinOfCardEq` for the noncomputable definition,
and `Fintype.truncEquivFin` and `Fintype.equivFin` for the bijection `α ≃ Fin (card α)`.
 -/
Fintype.truncEquivFinOfCardEq : {α : Type u_1} → [inst : Fintype α] → [DecidableEq α] → {n : ℕ} → Fintype.card α = n → Trunc (α ≃ Fin n)
-- Init.Data.SInt.Lemmas
Int16.toInt_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 15 ≤ n → n < 2 ^ 15 → (Int16.ofInt n).toInt = n
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply : ∀ {J : Type v} (F : J → Type u) [inst : Small.{u, v} J] (j : J) (x : ∏ᶜ F),
  (equivShrink ((j : J) → F j)).symm
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.Small.productIso F).hom) x) j =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
-- Aesop.Forward.State
Aesop.instBEqPatSubstSource : BEq Aesop.PatSubstSource
-- Mathlib.Combinatorics.Colex
Finset.Colex.erase_lt_erase : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} [inst_1 : DecidableEq α],
  a ∈ s → b ∈ s → (toColex (s.erase a) < toColex (s.erase b) ↔ b < a)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.notMem_support_of_degree_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree f) < m.toSyn (m.degree g) → m.degree g ∉ f.support
-- Init.Data.Rat.Lemmas
Rat.den_natCast : ∀ (n : ℕ), (↑n).den = 1
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coeMonoidHom_apply : ∀ {ι : Type u_2} {R : Type u_3} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : CommRing R]
  (g : Matrix.SpecialLinearGroup ι R), Matrix.SpecialLinearGroup.coeMonoidHom g = ↑g
-- Mathlib.Topology.Category.Compactum
_private.Mathlib.Topology.Category.Compactum.0.Compactum.cl_cl : ∀ {X : Compactum} (A : Set X.A), Compactum.cl✝ (Compactum.cl✝ A) ⊆ Compactum.cl✝ A
-- Batteries.Data.RunningStats
/-- Variance of data points times the number of data points.  -/
Batteries.RunningStats.var : Batteries.RunningStats → Float
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.bounded : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β}, IsCauSeq abv f → ∃ r, ∀ (i : ℕ), abv (f i) < r
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.length_digits : ∀ (b n : ℕ), 1 < b → n ≠ 0 → (b.digits n).length = Nat.log b n + 1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S),
  f.mk' x y = f x + ↑(-(IsAddUnit.liftRight (f.toAddMonoidHom.domRestrict S) ⋯) y)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  (F G : CategoryTheory.Functor (↑(Set.Iic x)) C) {k₁ k₂ : K} {h₁₂ : k₁ ≤ k₂} {h₂ : k₂ ≤ x},
  CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G k₁ k₂ h₁₂ h₂ → F.obj ⟨k₁, ⋯⟩ = G.obj ⟨k₁, ⋯⟩
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.exists_isDynCoverOf_of_isCompact_invariant : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} [inst : UniformSpace X],
  IsCompact F → Set.MapsTo T F F → U ∈ uniformity X → ∀ (n : ℕ), ∃ s, Dynamics.IsDynCoverOf T F U n ↑s