mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
/-- The free presheaf of modules functor `(Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R`.  -/
PresheafOfModules.free : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) →
      CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type u)) (PresheafOfModules R)
-- Lean.Environment
Lean.OLeanEntries.private : {α : Type} → Lean.OLeanEntries α → α
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift.congr_simp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI hI_1 : DividedPowers I),
  hI = hI_1 →
    ∀ (g g_1 : M →ₗ[R] A) (e_g : g = g_1) (hg : ∀ (m : M), g m ∈ I),
      DividedPowerAlgebra.lift hI g hg = DividedPowerAlgebra.lift hI_1 g_1 ⋯
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Every object in `Rep k G` naturally correspond to an object in `Action`.  -/
Rep.RepToAction : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] → [inst_1 : Monoid G] → CategoryTheory.Functor (Rep.{w, u, v} k G) (Action (ModuleCat k) G)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then `f` is an antitone
function.  -/
antitone_of_hasDerivAt_nonpos : ∀ {f f' : ℝ → ℝ}, (∀ (x : ℝ), HasDerivAt f (f' x) x) → f' ≤ 0 → Antitone f
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.copy_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.RespectsIso] {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i))
  (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) (i : J),
  (𝒰.copy J obj map e₁ e₂ h).f i = map i
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHom_whisker_exchange : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' Y Y' : C}
  (f : X ⟶ X') (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X' g) (CategoryTheory.eHomWhiskerRight V f Y') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f Y) (CategoryTheory.eHomWhiskerLeft V X g)
-- Mathlib.LinearAlgebra.DFinsupp
/-- The canonical map out of a direct sum of a family of additive subgroups is injective when the
additive subgroups are `iSupIndep`.  -/
iSupIndep.dfinsuppSumAddHom_injective : ∀ {ι : Type u_1} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : AddCommGroup N] {p : ι → AddSubgroup N},
  iSupIndep p → Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- If a partial homeomorphism has source and target equal to univ, then it induces a
homeomorphism between the whole spaces, expressed in this definition.  -/
PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (e : PartialHomeomorph X Y) → e.source = Set.univ → e.target = Set.univ → X ≃ₜ Y
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_5 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (ids : Array ℕ)
  (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.del ids) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_5 ids
-- Init.SimpLemmas
and_true : ∀ (p : Prop), (p ∧ True) = p
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_one : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)], P⁻[1 | mΩ] = 1
-- Mathlib.Algebra.Order.Group.Bounds
IsLUB.exists_between_sub_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α},
  IsLUB s a → 0 < ε → ∃ b ∈ s, a - ε < b ∧ b ≤ a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.getThenInsertIfNew? k v).1 = t.get? k
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_add : ∀ {K : Type u} [inst : Field K] {x y : RatFunc K},
  x + y ≠ 0 → (x + y).intDegree = ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_17.eq_2 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithInitial Cᵒᵖ) → (x ⟶ y) → Sort u_3) (unop : C)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of (Opposite.op unop))
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithInitial.of (Opposite.op x) ⟶ CategoryTheory.WithInitial.of (Opposite.op y)) →
        motive (CategoryTheory.WithInitial.of (Opposite.op x)) (CategoryTheory.WithInitial.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of (Opposite.op unop)) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of (Opposite.op unop)) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x with
    | CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x => h_2 unop x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_2 unop x
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasSum_comap_iff_of_hasSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {f : β → α} {a : α} [L.HasSupport] {g : γ → β} (hg : Function.Injective g),
  (∀ x ∈ L.support, x ∉ Set.range g → f x = 0) → (HasSum (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasSum f a L)
-- Init.Data.UInt.Lemmas
USize.toFin_add : ∀ (a b : USize), (a + b).toFin = a.toFin + b.toFin
-- Mathlib.MeasureTheory.Group.Prod
MeasurableEquiv.shearMulRight.eq_1 : ∀ (G : Type u_1) [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G] [inst_3 : MeasurableInv G],
  MeasurableEquiv.shearMulRight G =
    { toEquiv := (Equiv.refl G).prodShear Equiv.mulLeft, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.length_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_mul_prod : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, (fun x => x.1 * x.2) '' s ×ˢ t = s * t
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalAlgebra.hom_ext : ∀ {R : Type u_1} {ι : 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 : CommSemiring R]
  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] [inst_6 : (i : ι) → DistribMulAction R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : DistribMulAction R P] {g₁ g₂ : DirectLimit G f →ₙₐ[R] P},
  (∀ (i : ι), g₁.comp (DirectLimit.NonUnitalAlgebra.of G f i) = g₂.comp (DirectLimit.NonUnitalAlgebra.of G f i)) →
    g₁ = g₂
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.homToEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (g : Z ⟶ Y),
  α.homToEquiv.symm g = CategoryTheory.CategoryStruct.comp g α.inv
-- Mathlib.Computability.ContextFreeGrammar
/-- Given a context-free grammar `g` and strings `u` and `v`
`g.Produces u v` means that one step of a context-free transformation by a rule from `g` sends
`u` to `v`.  -/
ContextFreeGrammar.Produces : {T : Type u_1} → (g : ContextFreeGrammar T) → List (Symbol T g.NT) → List (Symbol T g.NT) → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → γ} {k : α} {h' : k ∈ Std.DHashMap.map f m},
  Std.DHashMap.Const.get (Std.DHashMap.map f m) k h' = f k (Std.DHashMap.Const.get m k ⋯)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The space of constant maps is equivalent to the space of maps that are multilinear with respect
to an empty family.  -/
MultilinearMap.constLinearEquivOfIsEmpty : (R : Type uR) →
  (S : Type uS) →
    {ι : Type uι} →
      (M₁ : ι → Type v₁) →
        (M₂ : Type v₂) →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : (i : ι) → Module R (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : Semiring S] →
                      [inst_6 : Module S M₂] →
                        [inst_7 : SMulCommClass R S M₂] → [IsEmpty ι] → M₂ ≃ₗ[S] MultilinearMap R M₁ M₂
-- Mathlib.Order.KrullDimension
/-- Alternative definition of height, with the supremum ranging only over those series that end at `a`.
 -/
Order.height_eq_iSup_last_eq : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.height a = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNat : ∀ {n : ℕ}, n < 256 → (OfNat.ofNat n).toUInt32 = OfNat.ofNat n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- Since we have `sum_[]_adjacent_intervals` theorems for both exact and trapezoidal integration,
it's natural to combine them into a similar formula for the error.  This theorem is in particular
used in the proof of the general error bound.  -/
sum_trapezoidal_error_adjacent_intervals : ∀ {f : ℝ → ℝ} {N : ℕ} {a h : ℝ},
  0 < N →
    IntervalIntegrable f MeasureTheory.volume a (a + ↑N * h) →
      ∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + ↑i * h) (a + (↑i + 1) * h) = trapezoidal_error f N a (a + ↑N * h)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
commAlgCatEquivUnder_counitIso : ∀ (R : CommRingCat),
  (commAlgCatEquivUnder R).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun A => CommAlgCat.of ↑R ↑A.right, map := fun {A B} f => CommAlgCat.ofHom (CommRingCat.toAlgHom f),
            map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun A => R.mkUnder ↑A, map := fun {A B} f => (CommAlgCat.Hom.hom f).toUnder, map_id := ⋯,
          map_comp := ⋯ })
-- Init.Prelude
instDecidableEqList : {α : Type u} → [DecidableEq α] → DecidableEq (List α)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- The versal morphism from any other cone to a weak limit cone.  -/
CategoryTheory.Limits.IsWeakLimit.liftConeMorphism : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsWeakLimit t → (s : CategoryTheory.Limits.Cone F) → s ⟶ t
-- Mathlib.Data.Int.Cast.Lemmas
Even.intCast : ∀ {α : Type u_3} [inst : AddGroupWithOne α] {n : ℤ}, Even n → Even ↑n
-- Mathlib.Order.Defs.Unbundled
UpperSet.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SizeOf α] (carrier : Set α) (upper' : IsUpperSet carrier),
  sizeOf { carrier := carrier, upper' := upper' } = 1
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_shiftRight : ∀ (a b : ISize) (h : System.Platform.numBits = 32),
  (a >>> b).toBitVec32 h = (a.toBitVec32 h).sshiftRight' ((b.toBitVec32 h).smod 32)
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.map_log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] {A' : Type u_2} [inst_2 : CommRing A']
  [inst_3 : Algebra ℚ A'] (f : A →+* A'), (PowerSeries.map f) (PowerSeries.log A) = PowerSeries.log A'
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.representative_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.representative.obj Y).arrow = Y.arrow
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.smul_tprodCoeff_aux : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (r : R),
  PiTensorProduct.tprodCoeff R z (Function.update f i (r • f i)) = PiTensorProduct.tprodCoeff R (r * z) f
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_sq : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivative (Polynomial.X ^ 2) = Polynomial.C 2 * Polynomial.X
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instAdd : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] → [ContinuousAdd M] → Add (MeasureTheory.VectorMeasure α M)
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.eq_5 : ∀ (motive : PosNum → ℕ → Sort u_1) (a : PosNum) (h_1 : Unit → motive PosNum.one 0) (h_2 : (x : ℕ) → motive PosNum.one x)
  (h_3 : (a : PosNum) → motive a.bit0 0) (h_4 : (p : PosNum) → (n : ℕ) → motive p.bit0 n.succ)
  (h_5 : (a : PosNum) → motive a.bit1 0) (h_6 : (p : PosNum) → (n : ℕ) → motive p.bit1 n.succ),
  (match a.bit1, 0 with
    | PosNum.one, 0 => h_1 ()
    | PosNum.one, x => h_2 x
    | a.bit0, 0 => h_3 a
    | p.bit0, n.succ => h_4 p n
    | a.bit1, 0 => h_5 a
    | p.bit1, n.succ => h_6 p n) =
    h_5 a
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The proposed colimit cocone is a colimit in `CommRingCat`.  -/
CommRingCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommRingCat) →
        CategoryTheory.Limits.IsColimit (CommRingCat.FilteredColimits.colimitCocone F)
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addCommMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : AddCommMonoid M₁]
  (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Surjective.addCommMonoid f hf one mul npow =
    { toAddMonoid := Function.Surjective.addMonoid f hf one mul npow, add_comm := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inl.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], OrderAddMonoidHom.inl α β = { toAddMonoidHom := AddMonoidHom.inl α β, monotone' := ⋯ }
-- Mathlib.AlgebraicGeometry.EffectiveEpi
/-- The underlying continuous map of a flat, surjective and quasi-compact morphism of schemes is an
effective epimorphism in the category of topological spaces.  -/
AlgebraicGeometry.effectiveEpi_base_of_flat : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.Flat f] [AlgebraicGeometry.Surjective f]
  [AlgebraicGeometry.QuasiCompact f], CategoryTheory.EffectiveEpi f.base
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropWhile_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → (s.dropWhile pat).copy = (t.dropWhile pat).copy
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy_hom_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X)
  (X_1 : Cᵒᵖ) (a : Opposite.unop X_1 ⟶ X),
  (AddMonCat.Hom.hom ((CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy X F α).hom.app X_1)) a = α.homEquiv' a
-- Init.Data.List.TakeDrop
List.rotateRight.eq_1 : ∀ {α : Type u} (xs : List α) (i : ℕ),
  xs.rotateRight i =
    if xs.length ≤ 1 then xs
    else
      have i := xs.length - i % xs.length;
      have ys := List.take i xs;
      have zs := List.drop i xs;
      zs ++ ys
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mulAntidiagonal_mono_right : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO},
  u ⊆ t → Finset.mulAntidiagonal hs hu a ⊆ Finset.mulAntidiagonal hs ht a
-- Mathlib.Data.Rat.Floor
Rat.isNNRat_intFract_of_isNNRat : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (r : α)
  (n d : ℕ), Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNNRat (Int.fract r) (n % d) d
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.termS_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- Given an abelian sheaf `F` on `(C, J)`, `n : ℕ` and `X : C`, this is
the degree-`n` sheaf cohomology of `X` with values in `F`.  -/
CategoryTheory.Sheaf.H' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          CategoryTheory.Sheaf J AddCommGrpCat → ℕ → C → AddCommGrpCat
-- Mathlib.Algebra.GCDMonoid.Nat
instStrongNormalizedGCDMonoidNat : StrongNormalizedGCDMonoid ℕ
-- Mathlib.Data.List.Infix
List.instIsPartialOrderIsPrefix : ∀ {α : Type u_1}, IsPartialOrder (List α) fun x1 x2 => x1 <+: x2
-- Std.Async.Basic
/-- Runs all computations concurrently and returns the result of the first one to finish.
All other results are lost, and the tasks are not cancelled, so they'll continue their execution
until the end.
 -/
Std.Async.EAsync.raceAll : {α ε : Type} →
  {c : Type u_1} →
    [Inhabited α] →
      [ForM (Std.Async.EAsync ε) c (Std.Async.EAsync ε α)] →
        c → optParam Task.Priority Task.Priority.default → Std.Async.EAsync ε α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_of_contains_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = true → Std.Internal.List.getValue? k (List.filter (fun p => !l₂.contains p.fst) l₁) = none
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
OrthonormalBasis.tensorProduct_apply' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁ × ι₂), (b₁.tensorProduct b₂) i = b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Rii α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.comul_natCast : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (n : ℕ),
  CoalgebraStruct.comul ↑n = ↑n
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- If `S` is a simple `R`-module, the `S`-isotypic component in an `R`-module `M` is the sum of
all submodules of `M` isomorphic to `S`.  -/
isotypicComponent : (R : Type u_2) →
  (M : Type u) →
    (S : Type u_4) →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] → [inst_2 : AddCommGroup S] → [inst_3 : Module R M] → [Module R S] → Submodule R M
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.EMatchTheoremKind.explainFailure : Lean.Meta.Grind.EMatchTheoremKind → String
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Given a wide pullback in `C`, construct a product in `C/B`.  -/
CategoryTheory.Over.ConstructProducts.over_product_of_widePullback : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C] {B : C},
  CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Over B)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- The cohomology of an abelian sheaf in degree `n`.  -/
CategoryTheory.Sheaf.H : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      CategoryTheory.Sheaf J AddCommGrpCat →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] → ℕ → Type w'
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.instInhabitedNormNums.default : Mathlib.Meta.NormNum.NormNums
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.tendsto_of_forall_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  (∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)) → Filter.Tendsto f (Filter.cocompact α) (Filter.cocompact β)