mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.OfComp.map_iso_inv_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H)
  [inst_3 : G.Full] [inst_4 : G.Faithful] {A : Type u_5} [inst_5 : AddMonoid A] [inst_6 : CategoryTheory.HasShift C A]
  [inst_7 : CategoryTheory.HasShift D A] [inst_8 : CategoryTheory.HasShift E A] [inst_9 : G.CommShift A]
  [inst_10 : H.CommShift A] (a : A) (X : C),
  G.map ((CategoryTheory.Functor.CommShift.OfComp.iso e a).inv.app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G a).hom.app (F.obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E a).map (e.hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso H a).inv.app X)
          (e.inv.app ((CategoryTheory.shiftFunctor C a).obj X))))
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} (hk : k < n) (hk' : k' < n) (a : (X k hk).fst) (a_1 : (X k' hk').fst) (k_1 k'_1 : ℕ) (hk_1 : k_1 < n)
  (hk'_1 : k'_1 < n) (a_2 : (X k_1 hk_1).fst) (a_3 : (X k'_1 hk'_1).fst),
  (CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max✝ hk hk' a a_1 =
      CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max✝ hk_1 hk'_1 a_2 a_3) =
    (k = k_1 ∧ k' = k'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_mul_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (a b : α), {a} * {b} = {a * b}
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_X_mul : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R], (Polynomial.X * f).Splits ↔ f.Splits
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_ratCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (q : ℚ), (↑q).ofVal = ↑q
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_ofHom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f : ρ.IntertwiningMap σ), Rep.Hom.hom (Rep.ofHom f) = f
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.prev_eq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) {i j : ι} (w : c.Rel i j),
  f.prev j =
    CategoryTheory.CategoryStruct.comp (C₁.xPrevIso w).hom
      (CategoryTheory.CategoryStruct.comp (f.f i) (C₂.xPrevIso w).inv)
-- Mathlib.Data.Finset.Sups
Finset.forall_sups_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α} {p : α → Prop},
  (∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_mapComp_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Prod.swap B C).mapComp f g).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.2 g.2))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1))
-- Lean.Message
Lean.MessageData.instCoeExpr : Coe Lean.Expr Lean.MessageData
-- Mathlib.Topology.Sheaves.Skyscraper
/-- A skyscraper presheaf is a presheaf supported at a single point: if `p₀ ∈ X` is a specified
point, then the skyscraper presheaf `𝓕` with value `A` is defined by `U ↦ A` if `p₀ ∈ U` and
`U ↦ *` if `p₀ ∉ A` where `*` is some terminal object.
 -/
skyscraperPresheaf : {X : TopCat} →
  (p₀ : ↑X) →
    [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst : CategoryTheory.Category.{w, v} C] → [CategoryTheory.Limits.HasTerminal C] → C → TopCat.Presheaf C X
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.append.eq_1 : ∀ {α : Type u}, Stream'.WSeq.append = Stream'.Seq.append
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.SurjectiveOnStalks f ↔
    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ⊤)).SurjectiveOnStalks
-- Mathlib.Tactic.FunProp.Mor
/-- An abbreviation of `∀ x, p x`. It is used by `fun_prop` to represent Pi types as function
applications and should not occur in any place other than the implementation of `fun_prop`.  -/
Mathlib.Meta.FunProp.Forall : {α : Sort u_1} → (α → Sort u_2) → Sort (imax u_1 u_2)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- Given a sheaf `Q` and a morphism `P ⟶ Q`, construct a morphism from `J.sheafify P` to `Q`.  -/
CategoryTheory.GrothendieckTopology.sheafifyLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {P Q : CategoryTheory.Functor Cᵒᵖ D} → (P ⟶ Q) → CategoryTheory.Presheaf.IsSheaf J Q → (J.sheafify P ⟶ Q)
-- Mathlib.Order.InitialSeg
PrincipalSeg.transRelIso_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f : PrincipalSeg r s) (g : s ≃r t) (a : α), (f.transRelIso g).toRelEmbedding a = g (f.toRelEmbedding a)
-- Mathlib.Order.CompleteLattice.Basic
unary_relation_sSup_iff : ∀ {α : Type u_8} (s : Set (α → Prop)) {a : α}, sSup s a ↔ ∃ r ∈ s, r a
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.visitedExpr : Lean.CollectLevelMVars.State → Lean.ExprSet
-- Mathlib.Topology.Bornology.Basic
/-- A **bornology** on a type `α` is a filter of cobounded sets which contains the cofinite filter.
Such spaces are equivalently specified by their bounded sets, see `Bornology.ofBounded`
and `Bornology.ext_iff_isBounded`  -/
Bornology : Type u_4 → Type u_4
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGEMap_id : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C],
  HomologicalComplex.truncGEMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.truncGE e)
-- Init.Data.Float.Model.Float32
/-- Converts an `Int32` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofInt32 : Int32 → Float32.Model
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldr_eq_foldr_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_m : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).m = SSet.relativeCellComplexOfMono.l i d
-- Mathlib.Order.Filter.CountableInter
countableInterFilter_top : ∀ {α : Type u_2}, CountableInterFilter ⊤
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.GeneralLinearGroup.fin_two_smul : ∀ {R : Type u_3} [inst : CommRing R] (g : GL (Fin 2) R) (v : Fin 2 → R),
  g • v = ![↑g 0 0 * v 0 + ↑g 0 1 * v 1, ↑g 1 0 * v 0 + ↑g 1 1 * v 1]
-- Mathlib.Analysis.Normed.Lp.SmoothApprox
/-- Every `Lp` function can be approximated by a smooth compactly supported function provided that
`p < ∞`.  -/
MeasureTheory.MemLp.exist_eLpNorm_sub_le : ∀ {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  [inst_6 : NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal},
  p ≠ ⊤ →
    1 ≤ p →
      ∀ {f : E → F},
        MeasureTheory.MemLp f p μ →
          ∀ {ε : ℝ},
            0 < ε → ∃ g, HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.isInfinitePlace_iff : ∀ {K : Type u_1} [inst : Field K] (v : AbsoluteValue K ℝ), NumberField.IsInfinitePlace v ↔ ∃ w, ↑w = v
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder.eq_2 : Nat.smallSchroder 1 = 1
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_injective : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι), Function.Injective fun f => Finsupp.indicator s f
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.isGLB_infDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
  s.Nonempty → IsGLB ((fun x_1 => dist x x_1) '' s) (Metric.infDist x s)
-- Mathlib.RepresentationTheory.Tannaka
/-- Definition of `equivHom g : Aut (forget k G)` by its components.  -/
TannakaDuality.FiniteGroup.equivApp : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → G → (X : FDRep k G) → X.V ≅ X.V
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_mul_left : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α},
  interior s * t ⊆ interior (s * t)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.measurable_apply : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : MeasurableSpace F] [BorelSpace F] (x : E), Measurable fun f => f x
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instReprEMatchTheoremKind : Repr Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- The `AddMonoidHom` from `S.leftNeg` to `S` sending an element to
its right additive inverse in  `S`.  -/
AddSubmonoid.fromCommLeftNeg : {M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → ↥S.leftNeg →+ ↥S
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Constructs a continued fraction without fractional part.  -/
ContFract.ofInteger : {α : Type u_1} → [inst : One α] → [inst_1 : Zero α] → [inst_2 : LT α] → α → ContFract α
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.trivialCofibrations Cᵒᵖ).HasFactorization (HomotopicalAlgebra.fibrations Cᵒᵖ)
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_sup'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (fun a => s.sup' hne fun x => f x a) t x
-- Mathlib.Combinatorics.SimpleGraph.Tutte
SimpleGraph.IsTutteViolator.mono : ∀ {V : Type u_1} {G G' : SimpleGraph V} [Finite V] {u : Set V}, G ≤ G' → G'.IsTutteViolator u → G.IsTutteViolator u
-- Mathlib.Order.Disjoint
disjoint_sup_left : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
  Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.ofSubtype_injective : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Finset α},
  Function.Injective ⇑(alternatingGroup.ofSubtype s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertList_of_mem_of_not_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k l = true →
    Std.Internal.List.containsKey k toInsert = false →
      Std.Internal.List.getKey? k (Std.Internal.List.insertList l toInsert) = some k
-- Mathlib.Topology.MetricSpace.Bounded
/-- If the distance between any two points in a set is bounded by some constant `C`,
then `ENNReal.ofReal C` bounds the emetric diameter of this set.  -/
Metric.ediam_le_of_forall_dist_le : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] {C : ℝ},
  (∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) → Metric.ediam s ≤ ENNReal.ofReal C
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.IsStableUnderBaseChange
-- Init.Data.Float.Model.Float32
/-- Compute the sum of two `Float32.Model`.
 -/
Float32.Model.add : Float32.Model → Float32.Model → Float32.Model
-- Lean.Meta.Tactic.Grind.Extension
/-- A constraint of the form `lhs =?= rhs`.
The `lhs` is one of the bound variables, and the `rhs` an abstract term that must be definitionally
equal to a term `t` assigned to `lhs`.  -/
Lean.Meta.Grind.EMatchTheoremConstraint.defEq : ℕ → Lean.Meta.Grind.CnstrRHS → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Algebra.Order.Group.Lattice
add_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] (a b c : α), c + a ⊔ b = (c + a) ⊔ (c + b)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
/-- A map `f : α → β` is said to be *quasi-measure-preserving* (a.k.a. non-singular) w.r.t. measures
`μa` and `μb` if it is measurable and `μb s = 0` implies `μa (f ⁻¹' s) = 0`.  -/
MeasureTheory.Measure.QuasiMeasurePreserving : {α : Type u_1} →
  {β : Type u_2} →
    {mβ : MeasurableSpace β} →
      {m0 : MeasurableSpace α} →
        (α → β) →
          autoParam (MeasureTheory.Measure α) MeasureTheory.Measure.QuasiMeasurePreserving._auto_1 →
            autoParam (MeasureTheory.Measure β) MeasureTheory.Measure.QuasiMeasurePreserving._auto_3 → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.id_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.CategoryStruct.id S).τ₂ = CategoryTheory.CategoryStruct.id S.X₂
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.coe_toLinear_eq_zero_iff : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M},
  LieModule.Weight.toLinear R L M χ = 0 ↔ χ.IsZero
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Monotone.mul_strictMono : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] [inst_2 : Preorder α]
  {f g : α → M₀} [PosMulStrictMono M₀] [MulPosMono M₀],
  Monotone f → StrictMono g → (∀ (x : α), 0 < f x) → (∀ (x : α), 0 ≤ g x) → StrictMono (f * g)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.instIsMonoidal_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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : G.LaxMonoidal],
  adj.IsMonoidal
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] →
              [inst_5 : StarModule R A] →
                (toSubalgebra : Subalgebra R A) →
                  (∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier) → StarSubalgebra R A
-- Mathlib.Analysis.Normed.Group.Basic
coe_normAddGroupSeminorm : ∀ (E : Type u_5) [inst : SeminormedAddGroup E], ⇑(normAddGroupSeminorm E) = norm
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.rnDeriv_gaussianReal : ∀ (μ : ℝ) (v : NNReal),
  (ProbabilityTheory.gaussianReal μ v).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume]
    ProbabilityTheory.gaussianPDF μ v
-- Lean.Expr
Lean.Nat.mkInstHAdd : Lean.Expr
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instT3Space : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [T3Space R], T3Space (ContinuousMapZero X R)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionResult.stuck.injEq : ∀ (gs gs_1 : List Lean.Meta.Grind.Goal),
  (Lean.Meta.Grind.ActionResult.stuck gs = Lean.Meta.Grind.ActionResult.stuck gs_1) = (gs = gs_1)
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonFloat : Lean.FromJson Float
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_zero : Complex.sqrt 0 = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given a presheaf of modules `M`, this is a morphism between coproducts
of free presheaves of modules on Yoneda presheaves which gives a presentation
of the module `M`, see `isColimitFreeYonedaCoproductsCokernelCofork`.  -/
PresheafOfModules.toFreeYonedaCoproduct : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) →
        (CategoryTheory.Limits.kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct ⟶ M.freeYonedaCoproduct
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.compare_get_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (h' : k ∈ t),
  cmp (t.get k h') k = Ordering.eq
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn_3.go : {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u} →
    {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
      {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u} →
        (t : Task Lean.Language.Lean.CommandParsedSnapshot) →
          ((t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t) →
            ((t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
                Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t) →
              ((t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
                  Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t) →
                ((t : Task Lean.Language.Lean.CommandParsedSnapshot) →
                    Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t) →
                  motive_4 t ×' Lean.Language.Lean.CommandParsedSnapshot.below_3 t
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.isThreeCycle_isConj : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → ∀ {σ τ : ↥(alternatingGroup α)}, (↑σ).IsThreeCycle → (↑τ).IsThreeCycle → IsConj σ τ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_pos_of_nonneg_of_pos`.  -/
Left.add_pos_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  0 ≤ a → 0 < b → 0 < a + b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.zero_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M₁ M₂ : PresheafOfModules R) (X : Cᵒᵖ), PresheafOfModules.Hom.app 0 X = 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_mono_isRestriction : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → N.removeLoops.IsRestriction M.removeLoops
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.submonoid_map_le_is_unit : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.splits_iff : ∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
  [Polynomial.IsSplittingField K L f], f.Splits ↔ ⊤ = ⊥
-- Mathlib.Algebra.Group.Action.Hom
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.

See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
 -/
Function.Surjective.mulActionLeft : {R : Type u_4} →
  {S : Type u_5} →
    {M : Type u_6} →
      [inst : Monoid R] →
        [inst_1 : MulAction R M] →
          [inst_2 : Monoid S] →
            [inst_3 : SMul S M] →
              (f : R →* S) → Function.Surjective ⇑f → (∀ (c : R) (x : M), f c • x = c • x) → MulAction S M
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEMatchTheoremKind : Inhabited Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.length_eq_zero_iff : ∀ {V : Type u_1} [inst : Quiver V] {a : V} (p : Quiver.Path a a), p.length = 0 ↔ p = Quiver.Path.nil
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureRat_vars : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] [inst : Fintype idx] (Φ : MvPolynomial idx ℚ) (n : ℕ),
  (wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoShortComplexH1_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.isoShortComplexH1 A).hom =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 2 1 0 groupHomology.isoShortComplexH1._proof_1
              groupHomology.isoShortComplexH1._proof_2).hom.app
        (groupHomology.inhomogeneousChains A))
      (CategoryTheory.ShortComplex.isoMk (groupHomology.chainsIso₂ A) (groupHomology.chainsIso₁ A)
          (groupHomology.chainsIso₀ A) ⋯ ⋯).hom
-- Mathlib.Order.KrullDimension
/-- Typeclass for orders with krull dimension at most `n`.  -/
Order.KrullDimLE : ℕ → (α : Type u_1) → [Preorder α] → Prop
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.ncs_tendsto_lim : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {ncs : CauSeq ℤ_[p] norm} {F : Polynomial R},
  Filter.Tendsto (fun i => ‖(Polynomial.aeval (↑ncs i)) (Polynomial.derivative F)‖) Filter.atTop
    (nhds ‖(Polynomial.aeval ncs.lim) (Polynomial.derivative F)‖)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transpose_eq_iff_eq_transpose : ∀ {μ ν : YoungDiagram}, μ.transpose = ν ↔ μ = ν.transpose
-- Mathlib.Order.Filter.Pointwise
Filter.bot_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {g : Filter β}, ⊥ +ᵥ g = ⊥
-- Lean.Server.References
/-- No definition, no usages.  -/
Lean.Server.RefInfo.empty : Lean.Server.RefInfo