mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The cardinality of the edge set of a bipartite graph is upper bounded by the product
of the cardinality of the two partitions.  -/
SimpleGraph.IsBipartiteWith.encard_edgeSet_le : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → G.edgeSet.encard ≤ s.encard * t.encard
-- Mathlib.Order.Filter.Lift
Filter.lift_lift'_same_eq_lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Set α → Set β},
  (∀ (s : Set α), Monotone fun t => g s t) →
    (∀ (t : Set α), Monotone fun s => g s t) → (f.lift fun s => f.lift' (g s)) = f.lift' fun s => g s s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a k : α}
  {v : β}, (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Additive closure of an additive submonoid `S` equals `S`  -/
AddSubmonoid.closure_eq : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.closure ↑S = S
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_two_mul : ∀ (x : ℝ), Real.sinh (2 * x) = 2 * Real.sinh x * Real.cosh x
-- Lean.Parser.Types
Lean.Parser.InputContext.mk : (input : String) →
  String →
    (endPos : optParam String.Pos.Raw input.rawEndPos) →
      autoParam (endPos ≤ input.rawEndPos) Lean.Parser.InputContext.mk._auto_1 →
        optParam Lean.FileMap (Lean.FileMap.ofString input) → Lean.Parser.InputContext
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_obj_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).inverse.obj X).right = X.right
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.const_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : Group γ]
  [inst_2 : DistribMulAction γ α], Function.Periodic f c → ∀ (a : γ), Function.Periodic (fun x => f (a • x)) (a⁻¹ • c)
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).f x =
    (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)
        (AlgebraicGeometry.Scheme.Hom.asOverProp f S)).left
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.isMaximal_comap_of_isIntegral_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] (I : Ideal S) [hI : I.IsMaximal], (Ideal.comap (algebraMap R S) I).IsMaximal
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The component 1-morphisms of an oplax transformation.  -/
CategoryTheory.Oplax.OplaxTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → CategoryTheory.Oplax.OplaxTrans F G → (a : B) → F.obj a ⟶ G.obj a
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff : ∀ {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] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide
          ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔
        0 ≤ w i
-- Lean.Meta.LazyDiscrTree
/-- Initial capacity for key and todo vector.  -/
Lean.Meta.LazyDiscrTree.initCapacity : ℕ
-- Mathlib.Topology.Path
Path.image_extend_of_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y) {s : Set ℝ},
  unitInterval ⊆ s → ⇑γ.extend '' s = Set.range ⇑γ
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
IntermediateField.isTranscendenceBasis_adjoin_iff : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [inst : Field F] [inst_1 : Field E]
  [inst_2 : Algebra F E] [inst_3 : CommRing S] [inst_4 : Algebra E S] {x : ι → S},
  IsTranscendenceBasis (↥(IntermediateField.adjoin F s)) x ↔ IsTranscendenceBasis (↥(Algebra.adjoin F s)) x
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.equiv : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Module.Finite R M] (e : M ≃ₗ[R] N), Module.Finite R N
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit : {α : Type u} → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.contains a = false → m.getKey! a = default
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `x ↦ a / x` as an order-reversing equivalence.  -/
OrderIso.divLeft : {α : Type u} → [inst : Group α] → [inst_1 : LE α] → [MulLeftMono α] → [MulRightMono α] → α → α ≃o αᵒᵈ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ftaylorSeriesWithin.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (s : Set E) (x : E) (n : ℕ), ftaylorSeriesWithin 𝕜 f s x n = iteratedFDerivWithin 𝕜 n f s x
-- Lean.Elab.Parallel
/-- Internal state for an iterator over tasks.
Maintains the list of tasks that haven't completed yet.
 -/
Std.Iterators.Types.Internal.TaskIterator : Type w → Type w
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_hom_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] [inst_1 : AlgebraicGeometry.IsAffine Y]
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp X.isoSpec.hom
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) =
    CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComonObj_mon_one_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.MonObj.one.hom = CategoryTheory.MonObj.one
-- Batteries.Data.Fin.Basic
/-- Compute the element of `Fin (m * n)` with quotient `i : Fin m` and remainder `j : Fin n`
when divided by `n`.
 -/
Fin.mkDivMod : {m n : ℕ} → Fin m → Fin n → Fin (m * n)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] {f g : BoundedOrderHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.instIsIsoMapS_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {X Y : C} (z : W.LeftFraction₃ X Y),
  CategoryTheory.IsIso (L.map z.s)
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.equivBEq : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [inst_1 : Std.LawfulBEqCmp cmp] [Std.TransCmp cmp], EquivBEq α
-- Mathlib.Algebra.Group.Conj
AddConjClasses.map_surjective : ∀ {α : Type u} {β : Type v} [inst : AddMonoid α] [inst_1 : AddMonoid β] {f : α →+ β},
  Function.Surjective ⇑f → Function.Surjective (AddConjClasses.map f)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] (G : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)]
  (f f_1 : (i j : ι) → i ≤ j → G i →ₗ[R] G j),
  f = f_1 → ∀ {inst_4 : DecidableEq ι} [inst_5 : DecidableEq ι], Module.DirectLimit G f = Module.DirectLimit G f_1
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.unmopEquiv C).unitIso.inv.app X).unmop = CategoryTheory.CategoryStruct.id X.unmop
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.instIteratorLoop : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {n : Type u_1 → Type u_2} →
        {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
          [inst : Monad m] →
            [Monad n] →
              [inst_2 : Std.Iterator α m β] →
                [Std.IteratorLoop α m n] → Std.IteratorLoop (Std.Iterators.Types.TakeWhile α m β P) m n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- For `X : Truncated C n` and `m ≤ n`, `X _⦋m⦌ₙ` is the `m`-th term of X. The
proof `p : m ≤ n` can also be provided using the syntax `X _⦋m, p⦌ₙ`.  -/
CategoryTheory.SimplicialObject.Truncated.mkNotation : Lean.TrailingParserDescr
-- Mathlib.Topology.Order.LiminfLimsup
/-- If a function has a limit, then its liminf coincides with its limit.  -/
Filter.Tendsto.liminf_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {f : Filter β} {u : β → α} {a : α} [f.NeBot], Filter.Tendsto u f (nhds a) → Filter.liminf u f = a
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.comm_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (self : F.Hom G) (n a a' : A)
  (ha' : n + a = a') {Z : CategoryTheory.Functor C D} (h : G.functor a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (CategoryTheory.CategoryStruct.comp (self.hom a) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (self.hom a') (CategoryTheory.shiftFunctor D n))
      (CategoryTheory.CategoryStruct.comp (G.shiftIso n a a' ha').hom h)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorObj_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {S T : CategoryTheory.Over X} {f₁ f₂ : R ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).left},
  f₁ = f₂ ↔
    CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Limits.pullback.fst S.hom T.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.Limits.pullback.fst S.hom T.hom) ∧
      CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Limits.pullback.snd S.hom T.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.Limits.pullback.snd S.hom T.hom)
-- Mathlib.Algebra.CharP.Frobenius
MonoidHom.iterate_map_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (f : R →* R) (p : ℕ) [inst_1 : ExpChar R p] (n : ℕ),
  (⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.corootSpan_dualAnnihilator_map_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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),
  Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator =
    (Submodule.span R (Set.range P.coroot')).dualCoannihilator
-- Mathlib.Analysis.Matrix.Order
/-- **Alias** of the reverse direction of `Matrix.isStrictlyPositive_iff_posDef`. -/
Matrix.PosDef.isStrictlyPositive : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {x : Matrix n n 𝕜},
  x.PosDef → IsStrictlyPositive x
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
toDegLex_injective : ∀ {α : Type u_1}, Function.Injective ⇑toDegLex
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.smallHomMap.eq_1 : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {X Y : C₁}
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)]
  (f : CategoryTheory.Localization.SmallHom W₁ X Y),
  Φ.smallHomMap f =
    (CategoryTheory.Localization.SmallHom.equiv W₂ W₂.Q).symm
      ((((CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr
          ((CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y))
        ((Φ.localizedFunctor W₁.Q W₂.Q).map ((CategoryTheory.Localization.SmallHom.equiv W₁ W₁.Q) f)))
-- Mathlib.Data.Sym.Sym2
Sym2.rel_iff : ∀ {α : Type u_1} {x y z w : α}, Sym2.Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
-- Init.System.IOError
IO.Error.permissionDenied.injEq : ∀ (filename : Option String) (osCode : UInt32) (details : String) (filename_1 : Option String) (osCode_1 : UInt32)
  (details_1 : String),
  (IO.Error.permissionDenied filename osCode details = IO.Error.permissionDenied filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of colimits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesColimits_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_mono : ∀ {V : Type u_1} {G H : SimpleGraph V} {s : Set (Sym2 V)}, G ≤ H → G.deleteEdges s ≤ H.deleteEdges s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k fallback : α}, (Std.HashMap.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.inv : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {s : Set α},
  IsLowerSet s → IsUpperSet s⁻¹
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.inhabited : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) → [inst_4 : DecidableEq ι] → Inhabited (Module.DirectLimit G f)
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.ext_iff : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {S T : StarSubsemiring R},
  S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Structure witnessing that a bicone is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.Bicone.IsBilimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Limits.Bicone F → Type (max (max uC uC') w)
-- Mathlib.Order.Defs.PartialOrder
instLawfulOrderLT_mathlib : ∀ {α : Type u_1} [inst : Preorder α], Std.LawfulOrderLT α
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects finite products, then `F.rightOp : C ⥤ Dᵒᵖ` reflects finite
coproducts.  -/
CategoryTheory.Limits.reflectsFiniteCoproducts_rightOp : ∀ {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.ReflectsFiniteProducts F],
  CategoryTheory.Limits.ReflectsFiniteCoproducts F.rightOp
-- Init.Data.Array.Lemmas
/-- Simplifies a normal form from `get!`  -/
Array.getD_getElem?_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {v d : α}, (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d
-- Std.Http.Data.Status
/-- 411 Length Required
 -/
Std.Http.Status.lengthRequired : Std.Http.Status
-- Init.Core
Std.Identity.mk : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [toLeftIdentity : Std.LeftIdentity op o], Std.Identity op o
-- Lean.Elab.Do.Basic
/-- The cached `PUnit` expression.  -/
Lean.Elab.Do.MonadInfo.cachedPUnit : Lean.Elab.Do.MonadInfo → Lean.Expr
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceCastLT : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)],
  Monotone DFunLike.coe
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_compLinearMap : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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] {n : ℕ} (g : M₂ →ₗ[R] M) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M₂),
  (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g
-- Mathlib.Data.Complex.Basic
Complex.inv_re : ∀ (z : ℂ), z⁻¹.re = z.re / Complex.normSq z
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul' : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (s : S) (a : A),
  (KaehlerDifferential.tensorKaehlerEquiv R S A (TensorProduct R A S)).symm
      ((KaehlerDifferential.D S (TensorProduct R A S)) (a ⊗ₜ[R] s)) =
    (algebraMap S (TensorProduct R A S)) s ⊗ₜ[A] (KaehlerDifferential.D R A) a
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_char_of_commute : ∀ {R : Type u_1} [inst : Ring R] {x y : R} (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  Commute x y → (x - y) ^ p = x ^ p - y ^ p
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_log_iff_exp_lt : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  x ≠ 0 → (a < x.log ↔ WithZero.exp a < x)
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.instMeasurableConstVAdd : ∀ {M : Type u_2} {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → VAdd M (α i)]
  [inst_1 : (i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableConstVAdd M (α i)],
  MeasurableConstVAdd M ((i : ι) → α i)
-- Mathlib.Order.Hom.Bounded
TopHom.mk : {α : Type u_6} → {β : Type u_7} → [inst : Top α] → [inst_1 : Top β] → (toFun : α → β) → toFun ⊤ = ⊤ → TopHom α β
-- Mathlib.Data.Finsupp.Option
Finsupp.prod_option_index : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : CommMonoid N] (f : Option α →₀ M)
  (b : Option α → M → N),
  (∀ (o : Option α), b o 0 = 1) →
    (∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) →
      f.prod b = b none (f none) * f.some.prod fun a => b (some a)
-- Mathlib.Order.Monotone.Odd
/-- An odd function on a linear ordered additive commutative group is antitone on the whole group
provided that it is monotone on `Set.Ici 0`.  -/
antitone_of_odd_of_monotoneOn_nonneg : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup H] [inst_4 : PartialOrder H] [IsOrderedAddMonoid H] {f : G → H},
  (∀ (x : G), f (-x) = -f x) → AntitoneOn f (Set.Ici 0) → Antitone f
-- Mathlib.Algebra.Order.Star.Basic
star_pos_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 < star x ↔ 0 < x
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.support_subset : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : AddCommMonoid M] [inst_1 : SetLike S M]
  [inst_2 : AddSubmonoidClass S M] [inst_3 : DecidableEq ι] [inst_4 : DecidableEq M] (A : ι → S)
  (x : DirectSum ι fun i => ↥(A i)), (Function.support fun i => ↑(x i)) ⊆ ↑(DFinsupp.support x)
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.mem_ball_dynEntourage : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {x y : X},
  y ∈ UniformSpace.ball x (Dynamics.dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ UniformSpace.ball (T^[k] x) U
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_of_not_bddBelow : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, ¬BddBelow s → sInf s = sInf ∅
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict derivative in right endpoint for a locally finite
measure.

Let `f` be a measurable function integrable on `a..b`. Let `(lb, lb')` be a pair of
`intervalIntegral.FTCFilter`s around `b`. Suppose that `f` has a finite limit `c` at `lb' ⊓ ae μ`.

Then `∫ x in a..v, f x ∂μ - ∫ x in a..u, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)` as
`u` and `v` tend to `lb`.
 -/
intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {c : E}
  {lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter b lb lb'],
  IntervalIntegrable f μ a b →
    StronglyMeasurableAtFilter f lb' μ →
      Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (nhds c) →
        Filter.Tendsto u lt lb →
          Filter.Tendsto v lt lb →
            (fun t => ∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt]
              fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Matrix.iSup_eigenspace_toLin'_diagonal_eq_top : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] (d : n → R),
  ⨆ μ, Module.End.eigenspace (Matrix.toLin' (Matrix.diagonal d)) μ = ⊤
-- Mathlib.Algebra.Module.Equiv.Opposite
LinearMap.ext_ring_op : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module S M] {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M}, f 1 = g 1 → f = g
-- Mathlib.Data.Nat.Log
Nat.log_mono_right : ∀ {b n m : ℕ}, n ≤ m → Nat.log b n ≤ Nat.log b m