mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight : ∀ {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.OplaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insert_le : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insert k v).size ≤ m.size + 1
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instHomIsOverOfIsOverTower_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (S S' : C)
  [inst_1 : CategoryTheory.OverClass X S] [inst_2 : CategoryTheory.OverClass X S']
  [inst_3 : CategoryTheory.CanonicallyOverClass Y S] [inst_4 : CategoryTheory.OverClass Y S']
  [inst_5 : CategoryTheory.OverClass S S'] [CategoryTheory.IsOverTower X S S'] [CategoryTheory.IsOverTower Y S S']
  [CategoryTheory.HomIsOver f S], CategoryTheory.HomIsOver f S'
-- Aesop.Rule.Name
Aesop.instBEqScopeName : BEq Aesop.ScopeName
-- Init.Data.UInt.Lemmas
UInt32.toNat_mod_lt : ∀ {m : ℕ} (u : UInt32), 0 < m → (u % UInt32.ofNat m).toNat < m
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_zero_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F), μ.transpose 0 = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_add : ∀ {α : Type u} [inst : Add α] (a b : α), ↑(a + b) = ↑a + ↑b
-- Mathlib.Analysis.Convex.Strong
/-- **Alias** of the reverse direction of `uniformConvexOn_zero`. -/
ConvexOn.uniformConvexOn_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
  ConvexOn ℝ s f → UniformConvexOn s 0 f
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul'_ulift : ∀ (R : Type u_4) (S : Type u_5) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.TensorProduct.lmul' (ULift.{u₁, u_4} R) =
    (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (Algebra.TensorProduct.lmul' R)).comp
      ↑(Algebra.TensorProduct.uliftEquiv R (ULift.{u₁, u_4} R) S S).symm
-- Mathlib.Algebra.Group.Basic
mul_zsmul' : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m n : ℤ), (m * n) • a = n • m • a
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- **Alias** of `Real.finsetProd_rpow`.

---

`rpow` version of `Finset.prod_pow`.  -/
Real.finset_prod_rpow : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℝ), (∀ i ∈ s, 0 ≤ f i) → ∀ (r : ℝ), ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- A pretransitive action on a set of prime order is preprimitive  -/
AddAction.IsPreprimitive.of_prime_card : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [hGX : AddAction.IsPretransitive G X],
  Nat.Prime (Nat.card X) → AddAction.IsPreprimitive G X
-- Mathlib.Algebra.Star.CHSH
/-- Given a CHSH tuple (A₀, A₁, B₀, B₁) in a *commutative* ordered \*-algebra over ℝ,
`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2`.

(We could work over ℤ[⅟2] if we wanted to!)
 -/
CHSH_inequality_of_comm : ∀ {R : Type u} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : Algebra ℝ R] [IsOrderedModule ℝ R] (A₀ A₁ B₀ B₁ : R),
  IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIleanInfoParams.mk.injEq : ∀ (version : ℕ) (references : Lean.Lsp.ModuleRefs) (decls : Lean.Lsp.Decls) (version_1 : ℕ)
  (references_1 : Lean.Lsp.ModuleRefs) (decls_1 : Lean.Lsp.Decls),
  ({ version := version, references := references, decls := decls } =
      { version := version_1, references := references_1, decls := decls_1 }) =
    (version = version_1 ∧ references = references_1 ∧ decls = decls_1)
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.of_restrictScalars : ∀ (R : Type u) (A : Type v) (B : Type u_1) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.Etale R A]
  [Algebra.Etale R B], Algebra.Etale A B
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The orbit of a periodic point `x` of `f` is the cycle `[x, f x, f (f x), ...]`. Its length is
the minimal period of `x`.

If `x` is not a periodic point, then this is the empty (aka nil) cycle.  -/
Function.periodicOrbit : {α : Type u_1} → (α → α) → α → Cycle α
-- Mathlib.Topology.Instances.Int
Int.dist_eq : ∀ (x y : ℤ), dist x y = |↑x - ↑y|
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.WF.below.erase : ∀ {α : Type u_1} {cmp : α → α → Ordering} {motive : (a : RBTree.RBNode α) → RBTree.RBNode.WF cmp a → Prop}
  {t : RBTree.RBNode α} {cut : α → Ordering} (a : RBTree.RBNode.WF cmp t),
  RBTree.RBNode.WF.below a → motive t a → RBTree.RBNode.WF.below ⋯
-- Std.Time.Zoned.RecurringRule
/-- DST details, if this zone observes DST.
 -/
Std.Time.TimeZone.RecurringRule.dst : Std.Time.TimeZone.RecurringRule → Option Std.Time.TimeZone.DaylightSavingRule
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.leftFun_implicitFunctionDataOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  (dfu.implicitFunctionDataOfProdDomain if₂u).leftFun = f
-- Init.Data.Slice.Array.Iterator
instCoeSubarrayArray : {α : Type u} → Coe (Subarray α) (Array α)
-- Mathlib.Algebra.IsPrimePow
IsUnit.not_isPrimePow : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsUnit n → ¬IsPrimePow n
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product with values in `𝕜`.  -/
InnerProductSpace.«term⟪_,_⟫__» : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instIntCast : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → IntCast (DoubleCentralizer 𝕜 A)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.spine_map_vertex : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := hₘ })) (a : ℕ) (hₐ : a ≤ n + 1)
  (φ : { obj := { len := a }, property := hₐ } ⟶ { obj := { len := m }, property := hₘ }) (i : Fin (a + 1)),
  (X.spine a hₐ ((CategoryTheory.ConcreteCategory.hom (X.map φ.op)) Δ)).vertex i =
    (X.spine m hₘ Δ).vertex ((SimplexCategory.Hom.toOrderHom φ.hom) i)
-- Mathlib.RingTheory.HopkinsLevitzki
/-- [Stacks Tag 00KH](https://stacks.math.columbia.edu/tag/00KH) -/
isArtinianRing_iff_isNoetherianRing_krullDimLE_zero : ∀ {R : Type u_3} [inst : CommRing R], IsArtinianRing R ↔ IsNoetherianRing R ∧ Ring.KrullDimLE 0 R
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.isStarProjection_toContinuousLinearMap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E},
  have this := ⋯;
  IsStarProjection (LinearMap.toContinuousLinearMap T) ↔ IsStarProjection T
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflecting twice in the same subspace.  -/
Submodule.reflection_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (p : E), K.reflection (K.reflection p) = p
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every isomorphism is a regular epimorphism.  -/
CategoryTheory.RegularEpi.ofIso : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (e : X ≅ Y) → CategoryTheory.RegularEpi e.hom
-- Mathlib.Data.Finset.Update
Function.update_eq_updateFinset : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {i : ι} {y : π i},
  Function.update x i y = Function.updateFinset x {i} (uniqueElim y)
-- Lean.MetavarContext
Lean.MetavarDecl.mk : Lean.Name → Lean.LocalContext → Lean.Expr → ℕ → Lean.LocalInstances → Lean.MetavarKind → ℕ → ℕ → Lean.MetavarDecl
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_sum : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) {s : Set α},
  MeasurableSet s → (MeasureTheory.Measure.sum μ).restrict s = MeasureTheory.Measure.sum fun i => (μ i).restrict s
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [FaithfulSMul R S],
  Module.IsTorsionFree S (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Mathlib.Topology.Order.MonotoneConvergence
OrderDual.supConvergenceClass : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [InfConvergenceClass α], SupConvergenceClass αᵒᵈ
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.ne : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_strict_mono : ∀ {a b : ENNReal}, b ≠ ⊤ → a < b → a.toReal < b.toReal
-- Batteries.Tactic.Alias
/-- Add a docstring to the alias `declName` if it doesn't already have one.
This needs to run after elaboration of attributes, because e.g. `inherit_doc` could a add docstring.
This is also used in `to_additive`/`to_dual`.
 -/
Batteries.Tactic.Alias.addAliasDocstring : Lean.Name → Batteries.Tactic.Alias.AliasInfo → Lean.CoreM Unit
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.norm_rpow : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → MeasureTheory.MemLp (fun x => ‖f x‖ ^ p.toReal) 1 μ
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.isometry_embed : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [inst : Encodable ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (Y i)], Isometry (Metric.PiNatEmbed.embed X Y f)
-- Batteries.Data.UnionFind.Basic
/-- Link a union-find node to a root node.  -/
Batteries.UnionFind.linkN : {n : ℕ} → (self : Batteries.UnionFind) → Fin n → (y : Fin n) → self.parent ↑y = ↑y → n = self.size → Batteries.UnionFind
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.ensureAtomicBinderName : Lean.Elab.Term.BinderView → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Sites.Coverage
/-- Any pretopology is a coverage.  -/
CategoryTheory.Pretopology.toCoverage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Pretopology C → CategoryTheory.Coverage C
-- Lean.Parser.Do
Lean.Parser.Term.doIfLetBind.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.one_lt_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, 1 < ↑n ↔ 1 < n
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.meas_inter : ∀ {Ω : Type u_1} {β : Type u_3} {γ : Type u_4} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ},
  ProbabilityTheory.IndepFun f g μ → ∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → μ (s ∩ t) = μ s * μ t
-- Mathlib.Combinatorics.Additive.Corner.Roth
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.triangleIndices.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G] (A : Finset (G × G)),
  Corners.triangleIndices✝ A =
    Finset.map
      {
        toFun := fun x =>
          match x with
          | (a, b) => (a, b, a + b),
        inj' := ⋯ }
      A
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_of_beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [LawfulBEq α] [inst_3 : BEq β] [LawfulBEq β],
  (↑m₁).WF → (↑m₂).WF → Std.DHashMap.Internal.Raw₀.Const.beq m₁ m₂ = true → (↑m₁).Equiv ↑m₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_ofMon : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.ofMon m) = Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational.  -/
AlgebraicGeometry.Scheme.BirationalOver.isRationalOver : ∀ {S X Y : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.Scheme.IsRationalOver sY],
  AlgebraicGeometry.Scheme.BirationalOver sX sY → AlgebraicGeometry.Scheme.IsRationalOver sX
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power. Variant of
`ExteriorAlgebra.ιMulti_span_fixedDegree`, useful in rewrites.  -/
exteriorPower.ιMulti_span_fixedDegree : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Submodule.span R (Set.range ⇑(ExteriorAlgebra.ιMulti R n)) = ⋀[R]^n M
-- Mathlib.Topology.Algebra.Field
Nonneg.unitsHomeomorphPos_apply_coe : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R] [inst_4 : TopologicalSpace R] [inst_5 : ContinuousInv₀ R] (r : { r // 0 ≤ r }ˣ),
  ↑((Nonneg.unitsHomeomorphPos R) r) = ↑↑r
-- Mathlib.Analysis.Convex.Extreme
Set.extremePoints.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (A : Set E),
  Set.extremePoints 𝕜 A = {x | x ∈ A ∧ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x}
-- Lean.ToLevel
Lean.instToLevel : Lean.ToLevel
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.balance2_toList : ∀ {α : Type u_1} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  (l.balance2 v r).toList = l.toList ++ v :: r.toList
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.mk : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  S.IsWide →
    (∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c},
        γ ∈ S.arrows c c →
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p) ∈
            S.arrows d d) →
      S.IsNormal
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_iSup_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Sort u_4} {U : ι → Submodule 𝕜 E} {V : Submodule 𝕜 E}, iSup U ⟂ V ↔ ∀ (i : ι), U i ⟂ V
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsComplete.not_isTrivial : ∀ {α : Type u_1} {H : Hypergraph α}, H.IsComplete → ¬H.IsTrivial
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.mk : Lean.Meta.Simp.Cache →
  Lean.Meta.Simp.CongrCache →
    Lean.ExprStructMap Lean.Expr → Lean.Meta.Simp.UsedSimps → ℕ → Lean.Meta.Simp.Diagnostics → Lean.Meta.Simp.State
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.ParseResult.error.sizeOf_spec : ∀ {α ι : Type} [inst : SizeOf α] [inst_1 : SizeOf ι] (pos : ι) (err : Std.Internal.Parsec.Error),
  sizeOf (Std.Internal.Parsec.ParseResult.error pos err) = 1 + sizeOf pos + sizeOf err
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supportedEquivMvPolynomial_symm_X : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] (s : Set σ) (i : ↑s),
  ↑((MvPolynomial.supportedEquivMvPolynomial s).symm (MvPolynomial.X i)) = MvPolynomial.X ↑i
-- Init.Data.Array.InsertionSort
/-- Sorts an array using insertion sort.

The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be
decidable to be used for sorting.
 -/
Array.insertionSort : {α : Type u_1} → Array α → autoParam (α → α → Bool) Array.insertionSort._auto_1 → Array α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A morphism `k : W ⟶ X` satisfying `k ≫ f = k ≫ g` induces a morphism `l : W ⟶ equalizer f g`
satisfying `l ≫ equalizer.ι f g = k`.  -/
CategoryTheory.Limits.equalizer.lift' : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasEqualizer f g] →
          {W : C} →
            (k : W ⟶ X) →
              CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
                { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k }
-- Init.Data.Fin.Lemmas
Fin.last_pos : ∀ {n : ℕ}, 0 < Fin.last (n + 1)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsLittleO.isEquivalent : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  (u - v) =o[l] v → Asymptotics.IsEquivalent l u v
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `AddMonoidHomClass.isometry_iff_norm`. -/
AddMonoidHomClass.isometry_of_norm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕), (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_apply : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  Polynomial.derivative p = p.sum fun n a => Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.congrLeft` as a linear equivalence.  -/
LocallyConstant.congrLeftₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} →
          (R : Type u_7) →
            [inst_2 : Semiring R] →
              [inst_3 : AddCommMonoid Z] →
                [inst_4 : Module R Z] → X ≃ₜ Y → LocallyConstant X Z ≃ₗ[R] LocallyConstant Y Z
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimit_zero_eq : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (j : J),
  0 = ModuleCat.FilteredColimits.M.mk F ⟨j, 0⟩
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.lt_coeff : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly) (k : ℕ),
  Lean.Grind.Linarith.coeff_cert p₁ p₂ k = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ < 0 → Lean.Grind.Linarith.Poly.denote' ctx p₂ < 0
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.left_unitor_hom_inv : ∀ {B : Type u} [inst : Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.left_unitor f).vcomp (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f))
    (CategoryTheory.FreeBicategory.Hom₂.id ((CategoryTheory.FreeBicategory.Hom.id a).comp f))
-- Mathlib.Analysis.Normed.Field.UnitBall
Subsemigroup.mem_unitBall : ∀ (𝕜 : Type u_2) [inst : NonUnitalSeminormedRing 𝕜] {x : 𝕜}, x ∈ Subsemigroup.unitBall 𝕜 ↔ ‖x‖ < 1
-- Std.Data.ExtDHashMap.Lemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`.  -/
Std.ExtDHashMap.contains_of_contains_insertIfNew' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k},
  (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Lean.Data.DeclarationRange
/-- A declaration location is a declaration range along with the name of the module the declaration resides in.
 -/
Lean.DeclarationLocation : Type
-- Mathlib.FieldTheory.SplittingField.Construction
/-- Auxiliary construction to a splitting field of a polynomial, which removes
`n` (arbitrarily-chosen) factors.

It constructs the type, proves that is a field and algebra over the base field.

Uses recursion on the degree.
 -/
Polynomial.SplittingFieldAuxAux : ℕ → {K : Type u} → [inst : Field K] → Polynomial K → (L : Type u) × (x : Field L) × Algebra K L
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Hour.Offset
-- Mathlib.Order.Defs.LinearOrder
le_total : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqSymbolKind : BEq Lean.Lsp.SymbolKind
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_ext : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] {A B : TopRep k G}
  {f g : A ⟶ B}, TopRep.Hom.hom f = TopRep.Hom.hom g → f = g
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.throwNonSupported : Lean.Meta.Match.Problem → Lean.MetaM Unit
-- Mathlib.Data.Fin.VecNotation
/-- We don't want to always simplify `Fin.cons` to `vecCons`.
But in cases that we are already mixing the declarations for dependent tuples and non-dependent
tuples, we can simplify to the non-dependent tuples.
This allows us to simplify `Fin.cons 5 ![1, 3, 7]` to `![5, 1, 3, 7]`.  -/
Matrix.Fin.cons_vecCons : ∀ {n : ℕ} {α : Type u_1} (x y : α) (p : Fin n → α),
  Fin.cons x (Matrix.vecCons y p) = Matrix.vecCons x (Matrix.vecCons y p)
-- Mathlib.Topology.Sober
/-- In a T₀ space, each set has at most one generic point.  -/
IsGenericPoint.eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α} {S : Set α} [T0Space α],
  IsGenericPoint x S → IsGenericPoint y S → x = y
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isoMk_inv_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left)
  (r : f.right ≅ g.right)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
      CategoryTheory.Arrow.isoMk._auto_1),
  (CategoryTheory.Arrow.isoMk l r h).inv.left = l.inv
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor α).hom.τr = (CategoryTheory.Bicategory.leftUnitor α.r).inv