mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (a : B × C),
  (CategoryTheory.Bicategory.Prod.swap B C).obj a = (a.2, a.1)
-- Mathlib.Algebra.Ring.Parity
Odd.natCast : ∀ {R : Type u_4} [inst : Semiring R] {n : ℕ}, Odd n → Odd ↑n
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0)
  (h₂ : ∀ (x_2 y : α), (↑f).toFun (x_2 + y) = (↑f).toFun x_2 + (↑f).toFun y),
  ⇑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = ⇑f
-- Mathlib.Order.Defs.Unbundled
/-- A lower set relative to a predicate `P` is a set such that all elements satisfy `P`
and any element less than one of its members and satisfying `P` is also a member.  -/
RelLowerSet : {α : Type u_1} → [LE α] → (α → Prop) → Type u_1
-- Init.Data.UInt.Lemmas
USize.toUInt32_eq : ∀ (a b : USize), a.toUInt32 = b.toUInt32 ↔ a % 4294967296 = b % 4294967296
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only
finitely many members of the union whose measure exceeds any given positive number.  -/
MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ : ∀ {α : Type u_1} {ι : Type u_4} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal},
  0 < ε →
    ∀ {As : ι → Set α},
      (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
        Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) As) → μ (⋃ i, As i) ≠ ⊤ → {i | ε ≤ μ (As i)}.Finite
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg.instIsAddRightInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant], μ.neg.IsAddRightInvariant
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.support_eq_univ_iff : ∀ {β : Type u_2} {L : SummationFilter β}, L.support = Set.univ ↔ L.filter ≤ Filter.atTop
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_3.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_4 size k v l r lrs lrk lrv lrl lrr) =
    h_3 size k v l r
-- Mathlib.Probability.Moments.Variance
/-- **The Bhatia-Davis inequality on variance**

The variance of a random variable `X` satisfying `a ≤ X ≤ b` almost everywhere is at most
`(b - 𝔼 X) * (𝔼 X - a)`.  -/
ProbabilityTheory.variance_le_sub_mul_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ}
  {X : Ω → ℝ},
  (∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) →
    AEMeasurable X μ → ProbabilityTheory.variance X μ ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.nontrivialTopology_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  NontrivialTopology X ↔ NontrivialTopology Y
-- Mathlib.Analysis.Normed.Group.Defs
ContinuousENorm.mk : {E : Type u_8} → [inst : TopologicalSpace E] → [toENorm : ENorm E] → Continuous enorm → ContinuousENorm E
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_norm_left`. -/
Asymptotics.IsBigO.norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, f' =O[l] g → (fun x => ‖f' x‖) =O[l] g
-- Mathlib.Algebra.Group.Action.Defs
VAddCommClass.mk : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} [inst : VAdd M α] [inst_1 : VAdd N α],
  (∀ (m : M) (n : N) (a : α), m +ᵥ n +ᵥ a = n +ᵥ m +ᵥ a) → VAddCommClass M N α
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquivClass.instAddHomClass : ∀ {M : Type u_4} {N : Type u_5} (F : Type u_9) [inst : Add M] [inst_1 : Add N] [inst_2 : EquivLike F M N]
  [h : AddEquivClass F M N], AddHomClass F M N
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_I : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I⁻¹ = -RCLike.I
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.insidePart_zero : DyckWord.insidePart 0 = 0
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.isEmpty.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  (it : Std.IterM m β),
  it.isEmpty =
    Std.IteratorLoop.forIn (fun x x_1 => flip bind) (ULift.{w, 0} Bool)
      (fun x x_1 s => s = ForInStep.done { down := false }) it { down := true } fun x x_1 x_2 =>
      pure ⟨ForInStep.done { down := false }, Std.IterM.isEmpty._proof_1✝⟩
-- Mathlib.Tactic.Variable
/-- Find a synthetic typeclass metavariable with no expr metavariables in its type.  -/
Mathlib.Command.Variable.pendingActionableSynthMVar : Lean.TSyntax `Lean.Parser.Term.bracketedBinder → Lean.Elab.TermElabM (Option Lean.MVarId)
-- Mathlib.Topology.Order.Monotone
sInf_mem_closure : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {s : Set α},
  s.Nonempty → sInf s ∈ closure s
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_sub : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G] (x y : G),
  SeparationQuotient.mk (x - y) = SeparationQuotient.mk x - SeparationQuotient.mk y
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
toDegLex_symm_eq : ∀ {α : Type u_1}, toDegLex.symm = ofDegLex
-- Init.MetaTypes
Lean.Module.mk.inj : ∀ {header : Lean.Syntax} {commands : Array Lean.Syntax} {header_1 : Lean.Syntax} {commands_1 : Array Lean.Syntax},
  { header := header, commands := commands } = { header := header_1, commands := commands_1 } →
    header = header_1 ∧ commands = commands_1
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instOne : One ℕ
-- Mathlib.CategoryTheory.Sites.Over
/-- The pullback functor `Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A` induced
by a morphism `f : X ⟶ Y`.  -/
CategoryTheory.GrothendieckTopology.overMapPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {X Y : C} →
            (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Sheaf (J.over Y) A) (CategoryTheory.Sheaf (J.over X) A)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The negation polynomial `-Y - a₁X - a₃` associated to the negation of a nonsingular affine point
on a Weierstrass curve.  -/
WeierstrassCurve.Affine.negPolynomial : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Affine R → Polynomial (Polynomial R)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- Standard formula for the discriminant of a quadratic polynomial.  -/
Polynomial.discr_of_degree_eq_two : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  f.degree = 2 → f.discr = f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_monotone : Monotone unitInterval.sigmoid
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.instIsScalarTowerRingT : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  IsScalarTower P.Ring (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
-- Init.Data.List.Lemmas
List.tail_eq_tail? : ∀ {α : Type u_1} {l : List α}, l.tail = l.tail?.getD []
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {i j k l : ι} → Monoid.CoprodI.NeWord M i j → j ≠ k → Monoid.CoprodI.NeWord M k l → Monoid.CoprodI.NeWord M i l
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- If the monad `m` is liftable to `n`, lifts `HetT m α` to `HetT n α`.
 -/
Std.Iterators.HetT.liftInner : {α : Type u_1} →
  {m : Type w → Type w'} → (n : Type w → Type w'') → [MonadLiftT m n] → Std.Iterators.HetT m α → Std.Iterators.HetT n α
-- Mathlib.Data.Finset.NAry
Finset.coe_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
  ↑(Finset.image₂ f s t) = Set.image2 f ↑s ↑t
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_inv : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (f : F) (s : Set α), ⇑f '' s⁻¹ = (⇑f '' s)⁻¹
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.empty_toList : ∀ (G : Type u_1) [inst : Group G] (A B : Subgroup G), (HNNExtension.NormalWord.ReducedWord.empty G A B).toList = []
-- Init.Data.UInt.BasicAux
/-- Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.toUInt8 : UInt16 → UInt8
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A morphism in `FreeSimplexQuiver` is either a face map (`δ`) or a degeneracy map (`σ`).  -/
FreeSimplexQuiver.Hom : FreeSimplexQuiver → FreeSimplexQuiver → Type
-- Init.Data.Array.Count
Array.countP_pos_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, 0 < Array.countP p xs ↔ ∃ a ∈ xs, p a = true
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.toSet_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (φ : R →+* S)
  (C : PrimeSpectrum.BasicConstructibleSetData R),
  (PrimeSpectrum.BasicConstructibleSetData.map φ C).toSet = PrimeSpectrum.comap φ ⁻¹' C.toSet
-- Mathlib.Data.Part
Part.bind_some : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → Part β), (Part.some a).bind f = f a
-- Mathlib.Data.Set.Subsingleton
Set.univ_set_of_isEmpty : ∀ {α : Type u} [IsEmpty α], Set.univ = {∅}
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.dim_toN_le : ∀ {X : SSet} (x : X.S), x.toN.dim ≤ x.dim
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.leftUnitor_hom_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f'),
  (CategoryTheory.Bicategory.leftUnitor f).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id x) (CategoryTheory.eqToHom h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f').hom (CategoryTheory.eqToHom ⋯))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termG₁ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorδ_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ W X Y Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.snd W Y)
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X Z))
      h
-- Mathlib.Data.Set.Piecewise
Set.apply_piecewise₂ : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  {δ' : α → Sort u_8} {δ'' : α → Sort u_9} (f' g' : (i : α) → δ' i) (h : (i : α) → δ i → δ' i → δ'' i) {x : α},
  h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.limsup_eq_iInf_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β}
  {u : β → α}, f.HasBasis p s → Filter.limsup u f = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with the Integral form of the remainder. This is an auxiliary theorem
which is used to prove the two useful versions `taylor_integral_remainder_of_absolutelyContinuous`
and `taylor_integral_remainder`.

We assume that for any `k ≤ n`, the following equation on integration by parts hold:
$$\int_{x_0}^x \frac{f^{(k+1)}(t) (x - t)^k}{k!} =
\frac{f^{(k)}(t) (x - t)^k}{k!} |_{x_0}^x -\int_{x_0}^x \frac{f^{(k)}(t) (x - t)^{k-1}}{(k-1)!}.$$
Then
$$f(x) - (P_n f)(x₀, x) = \int_{x_0}^x \frac{f^{(n+1)}(t) (x - t)^n}{n!} dt,$$
where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
derivative.  -/
taylor_integral_remainder_aux : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {x x₀ : ℝ} {n : ℕ},
  (∀ k ≤ n,
      have u := fun t => (x - t) ^ k / ↑k.factorial;
      have v := fun t => iteratedDerivWithin k f (Set.uIcc x₀ x) t;
      ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t) →
    f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n.factorial) • iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) t
-- Mathlib.Data.Finset.Max
Finset.min_eq_inf_withTop : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.min = s.inf WithTop.some
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comap_obj_mod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] (M : CategoryTheory.Mod D B),
  ((CategoryTheory.Mod.comap f).obj M).mod = CategoryTheory.Mod.scalarRestriction f M.X
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.normLeOne K =
    NumberField.mixedEmbedding.normAtAllPlaces ⁻¹'
      ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' NumberField.mixedEmbedding.fundamentalCone.paramSet K
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A presheaf is separated for a presieve if there is at most one amalgamation.  -/
CategoryTheory.Presieve.IsSeparatedFor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor Cᵒᵖ (Type w) → CategoryTheory.Presieve X → Prop
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_real_iff : ∀ {r : ℝ}, (↑r).Infinitesimal ↔ r = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The complex cosine function is everywhere strictly differentiable, with the derivative
`-sin x`.  -/
Complex.hasStrictDerivAt_cos : ∀ (x : ℂ), HasStrictDerivAt Complex.cos (-Complex.sin x) x
-- Mathlib.SetTheory.Cardinal.Defs
/-- The cardinal number of a type  -/
Cardinal.mk : Type u → Cardinal.{u}
-- Mathlib.Computability.Language
Language.mul_iSup : ∀ {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α), m * ⨆ i, l i = ⨆ i, m * l i
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Hour.Offset n
-- Mathlib.Order.Monotone.Extension
/-- If a function is monotone and is bounded on a set `s`, then it admits a monotone extension to
the whole space.  -/
MonotoneOn.exists_monotone_extension : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, MonotoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Monotone g ∧ Set.EqOn f g s
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instCommGrpObjSpecAsOverSpec : {R A : CommRingCat} →
  [inst : HopfAlgebra ↑R ↑A] →
    [Coalgebra.IsCocomm ↑R ↑A] →
      CategoryTheory.CommGrpObj ((AlgebraicGeometry.Spec A).asOver (AlgebraicGeometry.Spec R))
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_ssubset_coe : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : NonemptyInterval α}, ↑s ⊂ ↑t ↔ s < t
-- Mathlib.Data.Finset.Max
Finset.max'_eq_sup' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.max' H = s.sup' H id
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G × G →₀ A` satisfying the 2-cycle condition, produces a 2-cycle for the representation on
`A` induced by the `DistribMulAction`.  -/
groupHomology.cyclesOfIsCycle₂ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              (x : G × G →₀ A) → groupHomology.IsCycle₂ x → ↥(groupHomology.cycles₂ (Rep.ofDistribMulAction k G A))
-- Mathlib.Topology.Order.Filter
Filter.Tendsto.nhds_atBot : ∀ {α : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : PartialOrder X] [OrderTopology X] [NoMinOrder X]
  {f : α → X} {l : Filter α}, Filter.Tendsto f l Filter.atBot → Filter.Tendsto (nhds ∘ f) l (nhds Filter.atBot)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.coeff_domCongrBialgEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_3) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (a : MonoidAlgebra A N),
  ((MonoidAlgebra.domCongrBialgEquiv R A e).symm a).coeff = Finsupp.mapDomain (⇑e.symm) a.coeff
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone G} {t : CategoryTheory.Limits.Cone F}
  (P : CategoryTheory.Limits.IsLimit t) (Q : CategoryTheory.Limits.IsLimit s) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointsIsoOfNatIso Q w).inv =
    CategoryTheory.Limits.IsLimit.map r P w.inv
-- Mathlib.Topology.Constructions.SumProd
map_mem_closure₂ : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z},
  Continuous (Function.uncurry f) → x ∈ closure s → y ∈ closure t → (∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) → f x y ∈ closure u
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.mk.injEq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (functor : CategoryTheory.Functor C₁ C₂)
  (map : W₁ ≤ W₂.inverseImage functor) (functor_1 : CategoryTheory.Functor C₁ C₂)
  (map_1 : W₁ ≤ W₂.inverseImage functor_1),
  ({ functor := functor, map := map } = { functor := functor_1, map := map_1 }) = (functor = functor_1)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The projective subspace corresponding to a submodule `s`, consisting of the one-dimensional
subspaces of `s`. This is the inverse of `Projectivization.Subspace.submodule`.  -/
Submodule.projectivization : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Submodule K V ≃o Projectivization.Subspace K V
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2)
  (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instPow.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Monoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G], ContMDiffMap.instPow = { pow := fun f n_1 => ⟨⇑f ^ n_1, ⋯⟩ }
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.eval_eq : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (l : Profinite.NobelingProof.Products I) (x : ↑C),
  (Profinite.NobelingProof.Products.eval C l) x = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.fintypeDiv.eq_1 : ∀ {α : Type u_2} [inst : Div α] [inst_1 : DecidableEq α] (s t : Set α) [inst_2 : Fintype ↑s] [inst_3 : Fintype ↑t],
  s.fintypeDiv t = Set.fintypeImage2 (fun x1 x2 => x1 / x2) s t
-- Lean.Widget.UserWidget
Lean.Widget.erasePanelWidget : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → UInt64 → m Unit
-- Init.Data.Option.Lemmas
Option.any_max : ∀ {α : Type u_1} [inst : Max α] {o o' : Option α} {p : α → Bool},
  (∀ (a b : α), p (a ⊔ b) = (p a || p b)) → Option.any p (o ⊔ o') = (Option.any p o || Option.any p o')