mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Get coloring of `H` from coloring of `G ⊕g H`  -/
SimpleGraph.Coloring.sumRight : {V : Type u_3} →
  {W : Type u_5} → {γ : Type u_7} → {G : SimpleGraph V} → {H : SimpleGraph W} → (G ⊕g H).Coloring γ → H.Coloring γ
-- Init.Tactics
/-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names.  -/
Lean.Parser.Tactic.renameI : Lean.ParserDescr
-- Mathlib.Topology.Irreducible
isClosed_irreducibleComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsClosed (irreducibleComponent x)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.trivializationAt_eq_localTriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M),
  trivializationAt E (TangentSpace I) x = (tangentBundleCore I M).toFiberBundleCore.localTriv (achart H x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).maxKey?.isSome = !t.isEmpty
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- One line is contained in another differing in the first point if the first point of the first
line is contained in the second line.  -/
affineSpan_pair_le_of_left_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, p₁ ∈ line[k, p₂, p₃] → line[k, p₁, p₃] ≤ line[k, p₂, p₃]
-- Mathlib.Dynamics.Flow
/-- If `τ` is a `CanonicallyOrderedAdd` monoid (e.g., `ℕ` or `ℝ≥0`), then the notions
`IsForwardInvariant` and `IsInvariant` are equivalent.  -/
isForwardInvariant_iff_isInvariant : ∀ {τ : Type u_1} {α : Type u_2} [inst : AddMonoid τ] [inst_1 : PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α}
  {s : Set α}, IsForwardInvariant ϕ s ↔ IsInvariant ϕ s
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.id_comp : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b),
  AddConstMap.id.comp f = f
-- Lean.Level
Lean.Level.param : Lean.Name → Lean.Level
-- Init.Data.Order.Lemmas
Std.not_gt_of_lt : ∀ {α : Type u} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {a b : α}, a < b → ¬b < a
-- Aesop.Tree.Data
Aesop.Goal.setIsIrrelevant : Bool → Aesop.Goal → Aesop.Goal
-- Init.Data.Nat.Basic
Nat.zero_lt_of_ne_zero : ∀ {a : ℕ}, a ≠ 0 → 0 < a
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_descCochain_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n)
  (p q : ℤ) (hpq : p + m = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      ((CochainComplex.mappingCocone.descCochain φ α β h).v p q hpq) =
    α.v p q hpq
-- Mathlib.Order.RelIso.Basic
/-- Two irreflexive relations on a unique type are isomorphic.  -/
RelIso.ofUniqueOfIrrefl : {α : Type u_1} →
  {β : Type u_2} →
    (r : α → α → Prop) → (s : β → β → Prop) → [Std.Irrefl r] → [Std.Irrefl s] → [Unique α] → [Unique β] → r ≃r s
-- Init.Omega.Constraint
Lean.Omega.instBEqConstraint.beq : Lean.Omega.Constraint → Lean.Omega.Constraint → Bool
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_ne_zero_iff : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, ‖a‖₊ ≠ 0 ↔ a ≠ 0
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f: M → N` and `g: M' → N'` are submersions at `x` and `x'` (w.r.t. `F` and `F'`),
respectively, then `f × g: M × M' → N × N'` is a submersion at `(x, x')` w.r.t. `F × F'`.  -/
Manifold.IsSubmersionOfComplement.prodMap : ∀ {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {F : Type u_5} {F' : Type u_6} {H : Type u_7}
  {H' : Type u_8} {G : Type u_9} {G' : Type u_10} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E']
  [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedAddCommGroup E''] [inst_6 : NormedSpace 𝕜 E'']
  [inst_7 : NormedAddCommGroup E'''] [inst_8 : NormedSpace 𝕜 E'''] [inst_9 : NormedAddCommGroup F]
  [inst_10 : NormedSpace 𝕜 F] [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F']
  [inst_13 : TopologicalSpace H] [inst_14 : TopologicalSpace H'] [inst_15 : TopologicalSpace G]
  [inst_16 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} {M' : Type u_12} {N : Type u_13}
  {N' : Type u_14} [inst_17 : TopologicalSpace M] [inst_18 : ChartedSpace H M] [inst_19 : TopologicalSpace M']
  [inst_20 : ChartedSpace H' M'] [inst_21 : TopologicalSpace N] [inst_22 : ChartedSpace G N]
  [inst_23 : TopologicalSpace N'] [inst_24 : ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'}
  [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [⋯], ⋯
-- Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
NumberField.LiesOver.instIsScalarTowerCompletion : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  IsScalarTower K v.Completion w.Completion
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) (x : B),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.mk' S).mapId x = CategoryTheory.eqToHom ⋯
-- Init.Data.List.Perm
List.decidablePerm : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁.Perm l₂)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_add_add_eq_append : ∀ {m n k : ℕ}, (m...m + n + k).toArray = (m...m + n).toArray ++ ((m + n)...m + n + k).toArray
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.instFinCategoryOfLOfDecidableEqR.match_7.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape}
  (motive :
    (b : J.R) →
      (a : J.L) →
        (CategoryTheory.Limits.WalkingMulticospan.left a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b) →
          J.fst b = a → J.snd b = a → Sort u_3)
  (a : J.R) (h₁ : J.fst a = J.snd a) (h₂ : J.snd a = J.snd a)
  (h_1 :
    (a : J.R) →
      (h₁ : J.fst a = J.fst a) →
        (h₂ : J.snd a = J.fst a) → motive a (J.fst a) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst a) h₁ h₂)
  (h_2 :
    (a : J.R) →
      (h₁ : J.fst a = J.snd a) →
        (h₂ : J.snd a = J.snd a) → motive a (J.snd a) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd a) h₁ h₂),
  (match a, J.snd a, CategoryTheory.Limits.WalkingMulticospan.Hom.snd a, h₁, h₂ with
    | a, .(J.fst a), CategoryTheory.Limits.WalkingMulticospan.Hom.fst .(a), h₁, h₂ => h_1 a h₁ h₂
    | a, .(J.snd a), CategoryTheory.Limits.WalkingMulticospan.Hom.snd .(a), h₁, h₂ => h_2 a h₁ h₂) =
    h_2 a h₁ h₂
-- Mathlib.Order.FixedPoints
/-- Least fixed point of a monotone function  -/
OrderHom.lfp : {α : Type u} → [inst : CompleteLattice α] → (α →o α) →o α
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rii.length_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {r : Std.Rii α},
  r.iter.length = r.size
-- Mathlib.Algebra.Group.Defs
RightCancelSemigroup.ext_iff : ∀ {G : Type u} {x y : RightCancelSemigroup G}, x = y ↔ Mul.mul = Mul.mul
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.congr_arg : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {e : A ≃ₐc[R] B} {x x' : A}, x = x' → e x = e x'
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.reflection_weightEquiv : ∀ {ι : 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) (i : ι),
  RootPairing.Equiv.weightEquiv P P (RootPairing.Equiv.reflection P i) = P.reflection i
-- Mathlib.GroupTheory.Goursat
Subgroup.normal_goursatSnd : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)},
  Function.Surjective (Prod.snd ∘ ⇑I.subtype) → I.goursatSnd.Normal
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Init.Prelude
/-- All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. -/
Subtype : {α : Sort u} → (α → Prop) → Sort (max 1 u)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful] {Z : C} (h : b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.snd f') h) =
    CategoryTheory.CategoryStruct.comp (hf'.fst' g) h
-- Mathlib.ModelTheory.Encoding
/-- Applies the `forall` quantifier to an element of `(Σ n, L.BoundedFormula α n)`,
or returns `default` if not possible.  -/
FirstOrder.Language.BoundedFormula.sigmaAll : {L : FirstOrder.Language} → {α : Type u'} → (n : ℕ) × L.BoundedFormula α n → (n : ℕ) × L.BoundedFormula α n
-- Mathlib.Algebra.Opposites
/-- Additive opposite of a type.  -/
«term_ᵃᵒᵖ» : Lean.TrailingParserDescr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instModule' : {α : Type u_1} →
  {l : Filter α} →
    {M : Type u_5} →
      {R : Type u_7} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Module (l.Germ R) (l.Germ M)
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- Construct a term of `limit F : Type u` from a family of terms `x : Π j, F.obj j`
which are "coherent": `∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j'`.
 -/
CategoryTheory.Limits.Types.Limit.mk : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      [inst_1 : CategoryTheory.Limits.HasLimit F] →
        (x : (j : J) → F.obj j) →
          (∀ (j j' : J) (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (x j) = x j') →
            CategoryTheory.Limits.limit F
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- The `DPMorphism` induced by a ring morphism, given that divided powers are compatible on a
generating set.
See [N. Roby, *Les algèbres à puissances dividées* (Proposition 3)][Roby-1965].  -/
DividedPowers.DPMorphism.fromGens : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} →
          {J : Ideal B} →
            (hI : DividedPowers I) →
              (hJ : DividedPowers J) →
                {f : A →+* B} →
                  {S : Set A} →
                    I = Ideal.span S →
                      Ideal.map f I ≤ J → (∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)) → hI.DPMorphism hJ
-- Mathlib.Tactic.ReduceModChar
/-- If `e` is of the form `a ^ b`, reduce it using fast modular exponentiation, otherwise
reduce it using `norm_num`.  -/
Tactic.ReduceModChar.normIntNumeral' : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n n' : Q(ℕ)) →
      Q(Mathlib.Meta.NormNum.IsNat «$n» «$n'») →
        (e : Q(«$α»)) → (x : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mapAlgHom_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (f : PowerSeries A),
  (PowerSeries.mapAlgHom φ) f = (PowerSeries.map ↑φ) f
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_lift_ExceptT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε ε' α : Type u} {x : ExceptT ε' m α} {h : ε → ExceptT ε' m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' sh)} [inst : Std.Do.WP m sh] [Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q =
    (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsNonloop.of_isMinor : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, N.IsNonloop e → N ≤m M → M.IsNonloop e
-- Mathlib.Topology.Algebra.IsOpenUnits
IsOpenUnits.isOpenEmbedding_unitsVal : ∀ {M : Type u_1} {inst : Monoid M} {inst_1 : TopologicalSpace M} [self : IsOpenUnits M],
  Topology.IsOpenEmbedding Units.val
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_d : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι),
  CategoryTheory.CategoryStruct.comp (C.d i j) (C.d j k) = 0
-- Mathlib.Data.Sign.Basic
/-- `SignType.sign` as a `MonoidWithZeroHom` for a nontrivial ordered semiring. Note that linearity
is required; consider ℂ with the order `z ≤ w` iff they have the same imaginary part and
`z - w ≤ 0` in the reals; then `1 + I` and `1 - I` are incomparable to zero, and thus we have:
`0 * 0 = SignType.sign (1 + I) * SignType.sign (1 - I) ≠ SignType.sign 2 = 1`.
(`Complex.orderedCommRing`)  -/
signHom : {α : Type u} → [inst : Ring α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → α →*₀ SignType
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.nontrivial : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsRegular M rs → Nontrivial M
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulRight_apply : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ), ⇑u.mulRight = fun x => x * ↑u
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_diff!_eq_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₁ = true → Std.DTreeMap.Internal.Impl.contains a m₂ = false) →
        (m₁.diff! m₂).size = m₁.size
-- Mathlib.Dynamics.Flow
/-- The time-reversal of a flow `ϕ` by a (commutative, additive) group
is defined `ϕ.reverse t x = ϕ (-t) x`.  -/
Flow.reverse : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] → [inst_2 : SubtractionCommMonoid τ] → [ContinuousNeg τ] → Flow τ α → Flow τ α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.mk.inj : ∀ {toGoalState : Lean.Meta.Grind.GoalState} {mvarId : Lean.MVarId} {toGoalState_1 : Lean.Meta.Grind.GoalState}
  {mvarId_1 : Lean.MVarId},
  { toGoalState := toGoalState, mvarId := mvarId } = { toGoalState := toGoalState_1, mvarId := mvarId_1 } →
    toGoalState = toGoalState_1 ∧ mvarId = mvarId_1
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `MeasureTheory.VectorMeasure.restrict_inter_add_sdiff`. -/
MeasureTheory.VectorMeasure.restrict_inter_add_diff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [T2Space M] [inst_3 : ContinuousAdd M] {v : MeasureTheory.VectorMeasure α M} {s t : Set α},
  MeasurableSet s → MeasurableSet t → v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.zero_le_self_sub_floor : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] {a : R},
  0 ≤ a → 0 ≤ a - ↑⌊a⌋₊
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.finitenessRelation : {ρ : Type} →
  (pat : ρ) →
    (s : String.Slice) →
      [inst : String.Slice.Pattern.BackwardPattern pat] →
        [String.Slice.Pattern.StrictBackwardPattern pat] →
          Std.Iterators.FinitenessRelation (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s) Id
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs
/-- This simproc reduces `Ord.compare _ _` when both arguments are constructor applications and the
`Ord` instance in question has been annotated with `@[method_specs]`.
 -/
reduceOrd : Lean.Meta.Simp.Simproc
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `- ⊗ M` is an exact functor. See
`Module.Flat.iff_rTensor_exact` to specialize the universe of `N, N', N''` to `Type (max u v)`.  -/
Module.Flat.iff_rTensor_exact' : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v', u} R],
  Module.Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.instLinearAddOrderOfIsOrderedAddCancelMonoid : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : LinearOrder α] → [IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → LinearOrder (AddLocalization s)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.of_discrete : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {f : α → β} [inst : TopologicalSpace β]
  [MeasurableSingletonClass α] [Countable α], MeasureTheory.StronglyMeasurable f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_univ_of_one_mem : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} [inst_2 : Fintype α],
  1 ∈ s → s * Finset.univ = Finset.univ
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_add : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f₁ f₂ : M) (g₁ g₂ : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁)
  (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂),
  AlgebraicGeometry.StructureSheaf.const f₁ g₁ U hu₁ + AlgebraicGeometry.StructureSheaf.const f₂ g₂ U hu₂ =
    AlgebraicGeometry.StructureSheaf.const (g₂ • f₁ + g₁ • f₂) (g₁ * g₂) U ⋯
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_pos_of_eval₂_root : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R},
  p ≠ 0 → ∀ (f : R →+* S) {z : S}, Polynomial.eval₂ f z p = 0 → (∀ (x : R), f x = 0 → x = 0) → 0 < p.degree
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasFDerivWithinAt_iff_hasGradientWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : StrongDual 𝕜 F} {s : Set F},
  HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) s x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.lift_comp_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : StarRing P] (g : (i : ι) → G i →⋆ₙ+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι},
  (DirectLimit.NonUnitalStarRing.lift G f P g Hg).comp (DirectLimit.NonUnitalStarRing.of G f i) = g i
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_trans : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] (f : α ≃+o β) (g : β ≃+o γ), ⇑(f.trans g) = ⇑g ∘ ⇑f
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain.addMonoidHom_comp_mapRange : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  (f : α → β) (g : M →+ N),
  (Finsupp.mapDomain.addMonoidHom f).comp (Finsupp.mapRange.addMonoidHom g) =
    (Finsupp.mapRange.addMonoidHom g).comp (Finsupp.mapDomain.addMonoidHom f)
-- Std.Data.ExtDTreeMap.Basic
/-- Updates the values of the map by applying the given function to all mappings.  -/
Std.ExtDTreeMap.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {cmp : α → α → Ordering} → ((a : α) → β a → γ a) → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α γ cmp
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_finite' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} (s_fin : s.Finite),
  MeasurableSet s → MeasureTheory.Measure.count s = ↑s_fin.toFinset.card
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.instSetLike : {R : Type u_2} →
  {E : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] → [inst_5 : Module R E] → SetLike (ProperCone R E) E
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D =
    CategoryTheory.ObjectProperty.lift (fun F => W.IsInvertedBy F)
      ((CategoryTheory.Functor.whiskeringLeft C W.Localization D).obj W.Q) ⋯
-- Init.Notation
/-- The `run_meta doSeq` command executes code in `MetaM Unit`.
This is the same as `#eval show MetaM Unit from discard do doSeq`.

(This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.)
 -/
Lean.runMeta : Lean.ParserDescr