mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mk_toAddMonoidHom : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ → V₂)
  (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ C, ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖),
  { toFun := f, map_add' := h₁, bound' := h₂ }.toAddMonoidHom = AddMonoidHom.mk' f h₁
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsFlat.closure : ∀ {α : Type u_2} {M : Matroid α} {F : Set α}, M.IsFlat F → M.closure F = F
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_dirac : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} [MeasurableSingletonClass Ω] (x : Ω),
  ProbabilityTheory.variance X (MeasureTheory.Measure.dirac x) = 0
-- Mathlib.Logic.Equiv.Prod
/-- The type `∀ (i : α), β i` can be split as a product by separating the indices in `α`
depending on whether they satisfy a predicate `p` or not.  -/
Equiv.piEquivPiSubtypeProd : {α : Type u_9} →
  (p : α → Prop) →
    (β : α → Type u_10) →
      [DecidablePred p] → ((i : α) → β i) ≃ ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv) =
    CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  {data : (X : C) → F.OneHypercoverDenseData J₀ J X} [inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A]
  {G₀ : CategoryTheory.Sheaf J₀ A} {X : C} {Z : A}
  {f g : Z ⟶ CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X},
  (∀ (i : (data X).I₀),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i) =
        CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)) →
    f = g
-- Mathlib.Algebra.Ring.Prod
/-- Product of two semirings is a semiring.  -/
Prod.instSemiring : {R : Type u_1} → {S : Type u_3} → [Semiring R] → [Semiring S] → Semiring (R × S)
-- Lean.MetavarContext
Lean.MetavarContext.findLevelDecl? : Lean.MetavarContext → Lean.LMVarId → Option Lean.LevelMetavarDecl
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.eval_continuous : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (y : E), Continuous fun x => x y
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable;
a version for the region together with the graph of the upper function.  -/
nullMeasurableSet_region_between_oc : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {s : Set α},
        MeasureTheory.NullMeasurableSet s μ →
          MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
-- Mathlib.LinearAlgebra.Dual.Basis
/-- The coefficients of `v` on the basis `e`  -/
Module.DualBases.coeffs : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → {e : ι → M} → {ε : ι → Module.Dual R M} → Module.DualBases e ε → M → ι →₀ R
-- Mathlib.Algebra.Group.Subgroup.Defs
mul_mem_cancel_left : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [SubgroupClass S G] {x y : G},
  x ∈ H → (x * y ∈ H ↔ y ∈ H)
-- Mathlib.Topology.Irreducible
IsPreirreducible.of_subtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [PreirreducibleSpace ↑s], IsPreirreducible s
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasInjectiveDimensionLT S.X₂ n →
        CategoryTheory.HasInjectiveDimensionLT S.X₁ (n + 1) → CategoryTheory.HasInjectiveDimensionLT S.X₃ n
-- Init.Grind.Order
Lean.Grind.Order.lt_of_not_le_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsLinearPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k k' : ℤ},
  k'.beq' (-k) = true → ¬a ≤ b + ↑k → b < a + ↑k'
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The identity natural transformation is a `BasedNatTrans`.  -/
CategoryTheory.BasedNatTrans.id : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} → (F : CategoryTheory.BasedFunctor 𝒳 𝒴) → CategoryTheory.BasedNatTrans F F
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.monoLift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) [inst_2 : CategoryTheory.Mono f] {T : C} (g g_1 : T ⟶ Y) (e_g : g = g_1)
  (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0),
  CategoryTheory.Abelian.monoLift f g hg = CategoryTheory.Abelian.monoLift f_1 g_1 ⋯
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.runMatch : {α β : Type} →
  Lean.Meta.LazyDiscrTree α → Lean.Meta.LazyDiscrTree.MatchM α β → Lean.MetaM (β × Lean.Meta.LazyDiscrTree α)
-- Mathlib.CategoryTheory.Products.Basic
/-- The Cartesian product of two natural transformations.  -/
CategoryTheory.NatTrans.prod : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F G : CategoryTheory.Functor A B} →
                  {H I : CategoryTheory.Functor C D} → (F ⟶ G) → (H ⟶ I) → (F.prod H ⟶ G.prod I)
-- Mathlib.Probability.Moments.SubGaussian
/-- A random variable `X` has a sub-Gaussian moment-generating function with parameter `c`
with respect to a measure `μ` if for all `t : ℝ`, `exp (t * X)` is `μ`-integrable and
the moment-generating function of `X` is bounded by `exp (c * t ^ 2 / 2)` for all `t : ℝ`.
This implies in particular that `X` has expectation 0.

This is equivalent to `Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())`,
as proved in `HasSubgaussianMGF_iff_kernel`.
Properties about sub-Gaussian moment-generating functions should be proved first for
`Kernel.HasSubgaussianMGF` when possible.  -/
ProbabilityTheory.HasSubgaussianMGF : {Ω : Type u_1} →
  {mΩ : MeasurableSpace Ω} →
    (Ω → ℝ) → NNReal → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasSubgaussianMGF._auto_1 → Prop
-- Lean.Parser.Command
Lean.Parser.Command.structExplicitBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_mul_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R}, (p * q).degrees ≤ p.degrees + q.degrees
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- Semilinear sets in a finitely generated monoid are closed under complement.  -/
IsSemilinearSet.compl : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} [AddMonoid.FG M], IsSemilinearSet s → IsSemilinearSet sᶜ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.monObjObj.eq_1 : ∀ {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 D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.MonObj X],
  CategoryTheory.Functor.monObjObj X =
    {
      one :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one),
      mul :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X)
          (F.map CategoryTheory.MonObj.mul),
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' fallback : α},
      cmp k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
            k ∈ l → (t.insertManyIfNewUnit l).getKeyD k' fallback = k
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- `MvPowerSeries` on a `T2Space` form a `T2Space`  -/
MvPowerSeries.WithPiTopology.instT2Space : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [T2Space R], T2Space (MvPowerSeries σ R)
-- Mathlib.FieldTheory.Separable
/-- If `E / L / F` is a scalar tower and `x : E` is separable over `F`, then it's also separable
over `L`.  -/
IsSeparable.tower_top : ∀ {F : Type u_1} (L : Type u_2) [inst : CommRing F] {E : Type u_4} [inst_1 : Field L] [inst_2 : Ring E]
  [inst_3 : Algebra F L] [inst_4 : Algebra F E] [inst_5 : Algebra L E] [IsScalarTower F L E] {x : E},
  IsSeparable F x → IsSeparable L x
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `F` is an empty diagram, then a cone over `F` is limiting iff the cone point is terminal.  -/
CategoryTheory.Limits.isLimitEquivIsTerminalOfIsEmpty : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        [IsEmpty J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cone F) → CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsTerminal c.pt
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgEquiv.toAlgebraIso_inv : ∀ {R : Type u} [inst : CommRing R] {X₁ X₂ : Type v} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁}
  {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂), e.toAlgebraIso.inv = AlgCat.ofHom ↑e.symm
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If a vector space has a basis indexed by elements of a finite set, then it is
finite-dimensional.  -/
FiniteDimensional.of_finite_basis : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type w}
  {s : Set ι} (h : Module.Basis (↑s) K V), s.Finite → FiniteDimensional K V
-- Mathlib.Order.Category.DistLat
DistLat.id_apply : ∀ (X : DistLat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.mk : {G : Type u_6} →
  [inst : Group G] →
    (toGroupSeminorm : GroupSeminorm G) → (∀ (x : G), toGroupSeminorm.toFun x = 0 → x = 1) → GroupNorm G
-- Mathlib.Order.Cofinal
IsCofinal.mono : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, s ⊆ t → IsCofinal s → IsCofinal t
-- Mathlib.Data.Finset.Image
Finset.filterMap_val : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (s' : Finset α) {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'},
  (Finset.filterMap f s' f_inj).val = Multiset.filterMap f s'.val
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.conj : ∀ {α : Type u_2} {f g : Equiv.Perm α} {x y : α}, f.SameCycle x y → (g * f * g⁻¹).SameCycle (g x) (g y)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isTangentAt_orthRadius_iff_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P}, s.IsTangentAt p (s.orthRadius p) ↔ p ∈ s
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_ciSup : ∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] {f : α → β},
  LeftOrdContinuous f → ∀ {g : ι → α}, BddAbove (Set.range g) → f (⨆ i, g i) = ⨆ i, f (g i)
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.AddConjClasses.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G), S.AddConjClasses = Quotient (AddGroupExtension.IsAddConj.setoid S)
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.nhds_zero_hasBasis : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M},
  (nhds 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
-- Mathlib.Order.UpperLower.Closure
LowerSet.erase_le : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {a : α}, s.erase a ≤ s
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprGlobalBranchingPreprocessor.unsafe_1 : Lean.Expr → Lean.MetaM Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Init.Internal.Order.Basic
Lean.Order.Example.find_spec : ∀ {P : ℕ → Bool} (n m : ℕ), Lean.Order.Example.find P n = some m → n ≤ m ∧ P m = true
-- Mathlib.Order.Quotient
Quotient.instReflLe_mathlib : ∀ {α : Type u_1} {s : Setoid α} [inst : LE α], Std.Refl fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.prop_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero]
  [P.IsClosedUnderIsomorphisms] [inst_3 : CategoryTheory.Limits.HasZeroObject C], P 0
-- Mathlib.GroupTheory.OrderOfElement
orderOf_map_dvd : ∀ {G : Type u_1} [inst : Monoid G] {H : Type u_6} [inst_1 : Monoid H] (ψ : G →* H) (x : G), orderOf (ψ x) ∣ orderOf x
-- Mathlib.Data.Ordmap.Ordset
/-- The validity predicate for an `Ordnode` subtree. This asserts that the `size` fields are
correct, the tree is balanced, and the elements of the tree are organized according to the
ordering.  -/
Ordnode.Valid : {α : Type u_1} → [Preorder α] → Ordnode α → Prop
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.Context.mk : Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step) → Aesop.Script.StaticStructureM.Context
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_mul_le_of_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ}, ‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ * a₂‖ ≤ r₁ + r₂
-- Mathlib.Order.Interval.Finset.Defs
instFiniteSubtypeLtOfLocallyFiniteOrderTop : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [LocallyFiniteOrderTop α], Finite { x // y < x }
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The distinguished basis carried by an `EmbeddedG2`.

In fact this is a `RootPairing.Base`. TODO Upgrade to this stronger statement.  -/
RootPairing.EmbeddedG2.basis : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    [P.EmbeddedG2] →
                      [Finite ι] → [CharZero R] → [IsDomain R] → [P.IsIrreducible] → Module.Basis (Fin 2) R M
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {E : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} E] (φ : CategoryTheory.Functor C D)
  (φ' : CategoryTheory.Functor D E),
  CategoryTheory.FreeGroupoid.map (φ.comp φ') =
    (CategoryTheory.FreeGroupoid.map φ).comp (CategoryTheory.FreeGroupoid.map φ')
-- Init.Data.List.Monadic
List.filterMapM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : List α}
  {f : α → m (Option β)}, List.filterMapM f (wfParam xs) = List.filterMapM f xs.attach.unattach
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.mk : Lean.MVarId → List Lean.Expr → List Lean.Meta.Match.Alt → List Lean.Meta.Match.Example → Lean.Meta.Match.Problem
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.one_lt_goldenRatio : 1 < Real.goldenRatio
-- Mathlib.Order.Nucleus
Nucleus.range_subset_range : ∀ {X : Type u_1} [inst : Order.Frame X] {n m : Nucleus X}, Set.range ⇑m ⊆ Set.range ⇑n ↔ n ≤ m
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.instIsRegularEpiFst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C] {X Y B : C} (f : X ⟶ B) (g : Y ⟶ B)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [CategoryTheory.IsRegularEpi g],
  CategoryTheory.IsRegularEpi (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
/-- The natural transformation `F ⊠ G ⟶ (tensor C) ⋙ (G ⊛ F)` that corepresents
the braiding morphism `F ⊛ G ⟶ G ⊛ F`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.braidingInvCorepresenting : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.BraidedCategory C] →
            [inst_4 : CategoryTheory.MonoidalCategory V] →
              [CategoryTheory.BraidedCategory V] →
                (F G : CategoryTheory.Functor C V) →
                  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                    CategoryTheory.MonoidalCategory.externalProduct G F ⟶
                      (CategoryTheory.MonoidalCategory.tensor C).comp
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.prop_X₂_of_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {S : CategoryTheory.ShortComplex C},
  S.Exact → P S.X₁ → P S.X₃ → P S.X₂
-- Init.Util
/-- Display the given message if `a` is shared, that is, RC(a) > 1  -/
dbgTraceIfShared : {α : Type u} → String → α → α
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (obj : (U : C) → Submonoid ↑(M.obj U))
  (map :
    autoParam (∀ {U V : C} (i : U ⟶ V), obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj V))
      CategoryTheory.SubmonoidFunctor.map._autoParam)
  (obj_1 : (U : C) → Submonoid ↑(M.obj U))
  (map_1 :
    autoParam (∀ {U V : C} (i : U ⟶ V), obj_1 U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj_1 V))
      CategoryTheory.SubmonoidFunctor.map._autoParam),
  ({ obj := obj, map := map } = { obj := obj_1, map := map_1 }) = (obj = obj_1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Lean.Data.SMap
Lean.SMap.toList : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → List (α × β)
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.right_mem_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P}, p₂ ∈ AffineSubspace.perpBisector p₁ p₂ ↔ p₁ = p₂
-- Std.Time.Duration
/-- Converts a `Duration` to a `Day.Offset`
 -/
Std.Time.Duration.toDays : Std.Time.Duration → Std.Time.Day.Offset
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.map_edgeFinset_induce : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableEq V],
  Finset.map (Function.Embedding.subtype fun x => x ∈ s).sym2Map (SimpleGraph.induce s G).edgeFinset =
    G.edgeFinset ∩ s.toFinset.sym2
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddMonCat
-- Mathlib.MeasureTheory.Integral.CircleIntegral
deriv_circleMap_ne_zero : ∀ {c : ℂ} {R θ : ℝ}, R ≠ 0 → deriv (circleMap c R) θ ≠ 0
-- Mathlib.RingTheory.Valuation.Integral
Valuation.Integers.isIntegrallyClosed : ∀ {K : Type u} {Γ₀ : Type v} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation K Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O K], v.Integers O → IsIntegrallyClosed O
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instDiscreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α],
  DiscreteTopology (TopologicalSpace.NonemptyCompacts α)
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instLawfulOrderOrdOfDecidableLE : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [Std.Total fun x1 x2 => x1 ≤ x2], Std.LawfulOrderOrd α
-- Init.Control.Lawful.Basic
/-- The `map` implementation preserves identity.
 -/
LawfulFunctor.id_map : ∀ {f : Type u → Type v} {inst : Functor f} [self : LawfulFunctor f] {α : Type u} (x : f α), id <$> x = x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} [inst : Inhabited β] {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k' =
    if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
    else Std.DTreeMap.Internal.Impl.Const.get! t k'
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- [Stacks Tag 01KM](https://stacks.math.columbia.edu/tag/01KM) -/
AlgebraicGeometry.isClosedImmersion_equalizer_ι_left : ∀ {S : AlgebraicGeometry.Scheme} {X Y : CategoryTheory.Over S} [AlgebraicGeometry.IsSeparated Y.hom] (f g : X ⟶ Y),
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι f g))
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ → p ≠ 0 → (Function.swap dslope z₀)^[p.order] f z₀ ≠ 0
-- Mathlib.RingTheory.Nilpotent.Defs
eq_zero_of_nilpotencyClass_eq_one : ∀ {R : Type u_1} {x : R} [inst : MonoidWithZero R], nilpotencyClass x = 1 → x = 0
-- Mathlib.Topology.Algebra.Monoid
Submonoid.separatelyContinuousMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [SeparatelyContinuousMul M] (S : Submonoid M),
  SeparatelyContinuousMul ↥S
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `HasImages` asserts that every morphism has an image.  -/
CategoryTheory.Limits.HasImages : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop