mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Extension
Lean.VersoDocString.mk.inj : ∀ {text : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {subsections : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)}
  {text_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {subsections_1 : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)},
  { text := text, subsections := subsections } = { text := text_1, subsections := subsections_1 } →
    text = text_1 ∧ subsections = subsections_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a b : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates K a =
      NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates K b ↔
    ∃ ζ, ζ • a = b
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomSurjective.invPair : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁}
  [RingHomInvPair σ₁ σ₂], RingHomSurjective σ₁
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- Given a family of morphisms `g a : A a ⟶ B a` and a morphism `f : X₁ ⟶ X₂`,
this structure contains the data and properties which expresses that `X₂`
is obtained from `X₁` by attaching cells of the form `g a`.  -/
HomotopicalAlgebra.AttachCells : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} → ((a : α) → A a ⟶ B a) → {X₁ X₂ : C} → (X₁ ⟶ X₂) → Type (max (max (max t u) v) (w + 1))
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.trans_sOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WOppSide x y → s.SOppSide y z → s.WSameSide x z
-- Mathlib.Data.Matrix.Basis
Matrix.single_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (c : α) (i' : m) (j' : n), Matrix.single i j c i' j' = if i = i' ∧ j = j' then c else 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.toOuterMeasure_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α},
  μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ₁ ≤ μ₂
-- Lean.Meta.Tactic.Simp.Main
/-- Try to unfold `e`.
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.unfold? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
/-- An alias of `MeasureTheory.MeasurePreserving.comp` with a convenient defeq and argument order
for `MeasurableEquiv`  -/
MeasureTheory.MeasurePreserving.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {e : α ≃ᵐ β} {e' : β ≃ᵐ γ} {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β}
  {μc : MeasureTheory.Measure γ},
  MeasureTheory.MeasurePreserving (⇑e) μa μb →
    MeasureTheory.MeasurePreserving (⇑e') μb μc → MeasureTheory.MeasurePreserving (⇑(e.trans e')) μa μc
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `P` is stable under composition, cobase change and satisfies pre-cancellation,
`P.Under ⊤ X` has pushouts.  -/
CategoryTheory.MorphismProperty.Under.instHasPushoutsTopOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange]
  [P.HasOfPrecompProperty P], CategoryTheory.Limits.HasPushouts (P.Under ⊤ X)
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.absolutelyContinuous_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → μ.AbsolutelyContinuous (μ.tilted f)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.log_sub_self_isBigO : (fun z => Complex.log (1 + z) - z) =O[nhds 0] fun z => z ^ 2
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.noncommCoprod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)),
  f.noncommCoprod g comm = { toFun := fun mn => f mn.1 + g mn.2, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.get?_empty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] {k : α},
  Std.DTreeMap.Internal.Cell.empty.get? = none
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `MonoOver.map` preserves the identity (up to a natural isomorphism).  -/
CategoryTheory.MonoOver.mapId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) →
      CategoryTheory.MonoOver.map (CategoryTheory.CategoryStruct.id X) ≅
        CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is associative  -/
NonUnitalSemiring.mul_assoc : ∀ {α : Type u} [self : NonUnitalSemiring α] (a b c : α), a * b * c = a * (b * c)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofNatMultiset.eq_1 : ∀ (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p), PrimeMultiset.ofNatMultiset v h = Multiset.pmap (fun p hp => ⟨p, hp⟩) v h
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- **Alias** of `Stirling.log_stirlingSeq_sdiff_le`.

---

**Robbins' sharp stepwise bound** for the Stirling sequence:
`log (stirlingSeq n) - log (stirlingSeq (n+1)) ≤ 1 / (12 n (n + 1))`.  -/
Stirling.log_stirlingSeq_diff_le : ∀ (n : ℕ), Real.log (Stirling.stirlingSeq n) - Real.log (Stirling.stirlingSeq (n + 1)) ≤ 1 / (12 * ↑n * (↑n + 1))
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor preserving larger colimits also preserves smaller colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.Order.Bounds.Basic
IsGreatest.insert : ∀ {γ : Type u_3} [inst : LinearOrder γ] (a : γ) {b : γ} {s : Set γ}, IsGreatest s b → IsGreatest (insert a s) (max a b)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.iInf_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_4} (s : ι → Set α) (h : ∀ (i : ι), IsClosed (s i)),
  ⨅ i, { carrier := s i, isClosed' := ⋯ } = { carrier := ⋂ i, s i, isClosed' := ⋯ }
-- Mathlib.Data.Stream.Init
Stream'.concat_take_get : ∀ {α : Type u} {n : ℕ} {s : Stream' α}, Stream'.take n s ++ [s.get n] = Stream'.take (n + 1) s
-- Mathlib.Algebra.Ring.ULift
RingHom.down_ulift_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x : ULift.{u₁, u_1} R),
  ((RingHom.ulift.{u₁, u_3, u_1, u_2} f) x).down = f x.down
-- Mathlib.Combinatorics.Additive.Convolution
Finset.smul_convolution_eq_convolution_inv_mul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (s x : G),
  (s • A).convolution B x = A.convolution B (s⁻¹ * x)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- A group object internal to a cartesian monoidal category. Also see the bundled `Grp`.  -/
CategoryTheory.GrpObj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.CartesianMonoidalCategory C] → C → Type v₁
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Cardinal.mk_biUnion_le_of_le_lift`.

---

Bounds the cardinal of an ordinal-indexed union of sets.  -/
Cardinal.mk_iUnion_Ordinal_lift_le_of_le : ∀ {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}},
  Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c →
    Cardinal.aleph0 ≤ c →
      ∀ (A : Ordinal.{u} → Set β), (∀ j < o, Cardinal.mk ↑(A j) ≤ c) → Cardinal.mk ↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.pathsHomRel.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (x x_1 : CategoryTheory.Paths C) (p q : x ⟶ x_1),
  CategoryTheory.pathsHomRel C p q =
    ((CategoryTheory.pathComposition C).map p = (CategoryTheory.pathComposition C).map q)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_sum : ∀ {ι : Type u_2} {m : Type u_3} {n : Type u_4} {R : Type u_1} [inst : AddCommMonoid R] (s : Finset ι)
  (A : ι → Matrix m n R), (∑ i ∈ s, A i).vec = ∑ i ∈ s, (A i).vec
-- Lean.Parser.Term
Lean.Parser.Term.ellipsis.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.FunProp.Types
/-- Structure holding transition or morphism theorems for `fun_prop` tactic.  -/
Mathlib.Meta.FunProp.GeneralTheorems : Type
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.instInhabitedContext.default : Aesop.RuleTac.ForwardM.Context
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.toLinearPreorderOfLEArgs : {α : Type u} → Std.Packages.LinearOrderOfLEArgs α → Std.Packages.LinearPreorderOfLEArgs α
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.leftUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.LaxTrans.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.module : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] →
        {R : Type u_5} →
          [inst_2 : Semiring R] →
            [inst_3 : Module R V₂] →
              [inst_4 : PseudoMetricSpace R] → [IsBoundedSMul R V₂] → Module R (NormedAddGroupHom V₁ V₂)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toLinearEquiv_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ↑e.symm = (↑e).symm
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Expr.updateMDataS! : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.liftAlgHom_of : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T)
  (h : Polynomial.eval₂ (↑i) x p = 0) (r : R), (AdjoinRoot.liftAlgHom p i x h) ((AdjoinRoot.of p) r) = i r
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.mul_self : ∀ {α : Type u_1} [inst : Semigroup α] (a b : α), a ∣ᵣ b * a
-- Mathlib.Analysis.Calculus.LocalExtr.Polynomial
/-- The number of roots of a real polynomial is at most the number of roots of its derivative plus
one.  -/
Polynomial.card_roots_toFinset_le_derivative : ∀ (p : Polynomial ℝ), p.roots.toFinset.card ≤ (Polynomial.derivative p).roots.toFinset.card + 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedLeanImportMetaKind.default : Lean.Lsp.LeanImportMetaKind
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.continuous_coe' : ∀ (K : Type u_2) [inst : Field K],
  Continuous (⇑(algebraMap (RatFunc K) (LaurentSeries K)) ∘ ⇑(WithVal.equiv (RatFunc.polynomialValuationX K)))
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.rename_comp_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R)
  (g : τ → υ),
  (MvPolynomial.rename g).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun i => (MvPolynomial.rename g) (f i)
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.le_mul_norm_sub : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] {E : Type u_5} [inst_1 : SeminormedAddCommGroup E] {K : NNReal}
  {f : E → F}, AntilipschitzWith K f → ∀ (x y : E), ‖-x + y‖ ≤ ↑K * ‖-f x + f y‖
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_comp_val_Ioi_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] [NoMaxOrder α] {a : α} {f : α → β}
  {l : Filter β}, Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_0_comp_cochainsIso₀ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 0) (groupCohomology.cochainsIso₀ B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom (Rep.Hom.toModuleCatHom φ)
-- Mathlib.Condensed.Functors
/-- Dot notation for the value of `profiniteToCondensed`.  -/
Profinite.toCondensed : Profinite → CondensedSet
-- Mathlib.Data.Real.Basic
Real.instCommSemigroup : CommSemigroup ℝ
-- Init.Data.UInt.BasicAux
/-- Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.toUInt16 : UInt64 → UInt16
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_leftUnitor_inv_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.leftUnitor f).inv.1 = (CategoryTheory.Bicategory.leftUnitor f.1).inv
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_comp_le : ∀ {u : ℕ → EReal} {v : ℕ → ℕ},
  (∃ᶠ (n : ℕ) in Filter.atTop, 0 ≤ u n) →
    (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ 0 →
      (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ ⊤ →
        Filter.Tendsto v Filter.atTop Filter.atTop →
          LinearGrowth.linearGrowthSup (u ∘ v) ≤
            (LinearGrowth.linearGrowthSup fun n => ↑(v n)) * LinearGrowth.linearGrowthSup u
-- Lean.Util.Diff
/-- Insert the item into the source  -/
Lean.Diff.Action.insert : Lean.Diff.Action
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
  DifferentiableAt 𝕜 Prod.snd p
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.instDecidablePredMemSetFixedByOfDecidableEq.eq_1 : ∀ {M : Type u} [inst : Monoid M] {β : Type u_1} [inst_1 : MulAction M β] (m : M) [inst_2 : DecidableEq β] (b : β),
  MulAction.instDecidablePredMemSetFixedByOfDecidableEq m b = ⋯.mpr inferInstance
-- Mathlib.Order.CompleteLattice.Basic
sSup_apply : ∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α},
  sSup s a = ⨆ f, ↑f a
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDeriv_const_mul` without differentiability assumption when
the multiplication is in a division ring.  -/
iteratedDeriv_const_mul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {n : ℕ} (c : 𝕜') (f : 𝕜 → 𝕜'),
  iteratedDeriv n (fun x => c * f x) x = c * iteratedDeriv n f x
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.coe_mulRight : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : SeparatelyContinuousMul X] (x : X),
  ⇑(ContinuousMap.mulRight x) = fun y => y * x
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.ext : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} ⦃f g : Q₁ →qᵢ Q₂⦄,
  (∀ (x : M₁), f x = g x) → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The n-coskeleton as a functor `SSet.Truncated n ⥤ SSet`.  -/
SSet.Truncated.cosk : (n : ℕ) → CategoryTheory.Functor (SSet.Truncated n) SSet
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isomorphisms.iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.isomorphisms C f ↔ CategoryTheory.IsIso f
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_eq_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (r : R), (algebraMap R S) r = 0 ↔ ∃ m, ↑m * r = 0
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- Given a point `Φ` on a site `(C, J)`, and an object `M` of a category `A`,
this is the skyscraper sheaf with value `M`: it sends `X : C` to the
product of copies of `M` indexed by `Φ.fiber.obj X`.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      J.Point →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] → A → CategoryTheory.Sheaf J A
-- Init.Data.SInt.Lemmas
Int16.toISize_neg_of_ne : ∀ {x : Int16}, x ≠ -32768 → (-x).toISize = -x.toISize
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add β] (f g : UniformFun α β),
  UniformFun.toFun (f + g) = UniformFun.toFun f + UniformFun.toFun g
-- Mathlib.Order.Basic
lt_iff_lt_of_le_iff_le : ∀ {α : Type u_2} {β : Type u_5} [inst : LinearOrder α] [inst_1 : LinearOrder β] {a b : α} {c d : β},
  (a ≤ b ↔ c ≤ d) → (b < a ↔ d < c)
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.norm.eq_1 : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : SlashInvariantFormClass F 𝒢 k] [inst_2 : 𝒢.IsFiniteRelIndex ℋ] [inst_3 : ℋ.HasDetPlusMinusOne],
  SlashInvariantForm.norm ℋ f =
    {
      toFun :=
        have this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
        ∏ q, SlashInvariantForm.quotientFunc f q,
      slash_action_eq' := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co.inj : ∀ {lo hi lo_1 hi_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound},
  Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo hi =
      Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo_1 hi_1 →
    lo = lo_1 ∧ hi = hi_1
-- Mathlib.Analysis.Normed.Ring.Basic
norm_mul : ∀ {α : Type u_2} [inst : Norm α] [inst_1 : Mul α] [NormMulClass α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
-- Mathlib.Data.Int.Log
Int.log_of_right_le_one : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) {r : R}, r ≤ 1 → Int.log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
-- Init.Data.Array.Find
Array.findIdx_lt_size_of_exists : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (∃ x ∈ xs, p x = true) → Array.findIdx p xs < xs.size
-- Mathlib.Data.Sum.Order
OrderIso.sumAssoc_symm_apply_inr_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (b : β),
  (OrderIso.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
isUniformGroup_iff_left_right : ∀ {γ : Type u_3} [inst : Group γ] [inst_1 : UniformSpace γ],
  IsUniformGroup γ ↔ IsLeftUniformGroup γ ∧ IsRightUniformGroup γ
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toQuotient.eq_1 : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M}, AddCon.toQuotient = Quotient.mk''
-- Mathlib.CategoryTheory.Discrete.Basic
/-- For functors out of a discrete category,
a natural transformation is just a collection of maps,
as the naturality squares are trivial.
 -/
CategoryTheory.Discrete.natTrans : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} →
        ((i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i) → (F ⟶ G)
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options) (annotationId? : Option String),
  sizeOf { uri := uri, options? := options?, annotationId? := annotationId? } =
    1 + sizeOf uri + sizeOf options? + sizeOf annotationId?
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g c : Equiv.Perm α},
  c ∈ g.cycleFactorsFinset → g.IsCycleOn ↑c.support
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instUnique.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Subsingleton R],
  MonoidAlgebra.instUnique = { default := MonoidAlgebra.coeffEquiv.symm default, uniq := ⋯ }
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The type of morphisms in `CommAlgCat R`.  -/
CommAlgCat.Hom : {R : Type u} → [inst : CommRing R] → CommAlgCat R → CommAlgCat R → Type v
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.alphaEq : Lean.Expr → Lean.Expr → Bool
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Cache.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {sα : Q(CommSemiring «$α»)} →
      Option Q(CommRing «$α») → Option Q(Semifield «$α») → Option Q(CharZero «$α») → Mathlib.Tactic.Ring.Common.Cache sα
-- Init.Data.Nat.Sqrt.Basic
Nat.sqrt.iter.eq_def : ∀ (n guess : ℕ),
  Nat.sqrt.iter n guess =
    have next := (guess + n / guess) / 2;
    if _h : next < guess then Nat.sqrt.iter n next else guess
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.exists_superset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, 𝒜.Shatters s → ∃ t ∈ 𝒜, s ⊆ t
-- Aesop.Check
_private.Aesop.Check.0.Aesop.commandRegister_aesop_check_option__ : Lean.ParserDescr
-- Batteries.Data.List.Perm
List.Perm.diff_left : ∀ {α : Type u_1} {t₁ t₂ : List α} [inst : BEq α] [LawfulBEq α] (l : List α), t₁.Perm t₂ → l.diff t₁ = l.diff t₂
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffOn.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 F₁) n f s →
      ContMDiffOn I (modelWithCornersSelf 𝕜 F₂) n (fun x => (g x) (f x)) s
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1}
  {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y},
  x.IsCompatible →
    ∀ {X Z : C} (f : Z ⟶ X) (i : I) (φ : Z ⟶ Y i),
      x.familyOfElements X f ⋯ = (CategoryTheory.ConcreteCategory.hom (F.map φ.op)) (x i)