mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.MonoidalCategory.inducingFunctorData_μIso : ∀ (R : Type u) [inst : CommRing R] (x x_1 : BialgCat R),
  (BialgCat.MonoidalCategory.inducingFunctorData R).μIso x x_1 =
    CategoryTheory.Iso.refl
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj x)
        ((CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj x_1))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.maxKey! ∈ t
-- Mathlib.Topology.Compactness.Lindelof
countable_cover_nhds_interior : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X] {U : X → Set X},
  (∀ (x : X), U x ∈ nhds x) → ∃ t, t.Countable ∧ ⋃ x ∈ t, interior (U x) = Set.univ
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of `LinearMap.toMatrix` does not depend on the choice of basis.  -/
LinearMap.det_toMatrix_eq_det_toMatrix : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] {κ : Type u_6} [inst_5 : Fintype κ] [inst_6 : DecidableEq κ]
  (b : Module.Basis ι A M) (c : Module.Basis κ A M) (f : M →ₗ[A] M),
  ((LinearMap.toMatrix b b) f).det = ((LinearMap.toMatrix c c) f).det
-- Mathlib.Topology.Bornology.Hom
/-- Construct a `LocallyBoundedMap` from the fact that the function maps bounded sets to bounded
sets.  -/
LocallyBoundedMap.ofMapBounded : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Bornology α] →
      [inst_1 : Bornology β] →
        (f : α → β) → (∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)) → LocallyBoundedMap α β
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_4.eq : ∀ {motive_1 : Lean.Widget.MsgEmbed → Sort u} {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u}
  {motive_3 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
      Sort u}
  {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) (F_1 : (t : Lean.Widget.MsgEmbed) → t.below → motive_1 t)
  (F_2 : (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t)
  (F_3 :
    (t :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
          (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
      Lean.Widget.MsgEmbed.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_4 t → motive_5 t),
  Lean.Widget.MsgEmbed.brecOn_4 t F_1 F_2 F_3 F_4 F_5 = F_5 t (Lean.Widget.MsgEmbed.brecOn_4.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map_id_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C],
  CategoryTheory.ThinSkeleton.map (CategoryTheory.Functor.id C) =
    CategoryTheory.Functor.id (CategoryTheory.ThinSkeleton C)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- A shorthand to bundle the μᵣ as an isomorphism  -/
CategoryTheory.Functor.RightLinear.μᵣIso : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        (F : CategoryTheory.Functor D D') →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] →
                    [F.RightLinear C] →
                      (d : D) →
                        (c : C) →
                          CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ≅
                            F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Icc_eq_insert_of_Icc_succ_eq : ∀ {m n : ℕ} {s : Finset ℕ}, m.ble n = true → Finset.Icc (m + 1) n = s → Finset.Icc m n = insert m s
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functorToPresheaves_map_app : ∀ {P : TopCat → Prop} {X Y : Type (max u w)} (f : X ⟶ Y) (x : (CompHausLike P)ᵒᵖ),
  (CompHausLike.LocallyConstant.functorToPresheaves.map f).app x =
    TypeCat.ofHom fun t => LocallyConstant.map (⇑(CategoryTheory.ConcreteCategory.hom f)) t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM f init t =
    Array.foldlM (fun a b => f a b.1 b.2) init (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Equivalence between Dyck words and rooted binary trees.  -/
DyckWord.equivTree : DyckWord ≃ BinaryTree Unit
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The map between formal power series induced by a map on the coefficients.  -/
PowerSeries.map : {R : Type u_1} →
  [inst : Semiring R] → {S : Type u_2} → [inst_1 : Semiring S] → (R →+* S) → PowerSeries R →+* PowerSeries S
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorRight_apply_tmul : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) {α : Type w'} [inst_6 : DecidableEq α] (v : V) (f : α →₀ W),
  (σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f) = f.sum fun i w => fun₀ | i => v ⊗ₜ[k] w
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mulVec_surjective_iff_exists_right_inverse : ∀ {m : Type u} {n : Type u'} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq m] [Finite m] [inst_3 : Fintype n]
  {A : Matrix m n R}, Function.Surjective A.mulVec ↔ ∃ B, A * B = 1
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.leftFun_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (p : F × G) in nhds (φ.prodFun φ.pt), φ.leftFun (φ.implicitFunction p.1 p.2) = p.1
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Expr.instantiateBetaRevRange.visit : ℕ → ℕ → Array Lean.Expr → Lean.Expr → ℕ → Lean.MonadStateCacheT (Lean.ExprStructEq × ℕ) Lean.Expr Id Lean.Expr
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_add_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R}, (p + Polynomial.C a).natDegree = p.natDegree
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mulEquivToUnitHom_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'),
  MulChar.mulEquivToUnitHom χ = MulChar.equivToUnitHom χ
-- Aesop.Builder.Forward
Aesop.RuleBuilderOptions.forwardIndexTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_prev_right : ∀ {s : String.Slice} (p : s.Pos) (hp : p ≠ s.startPos),
  p.Splits ((s.sliceTo (p.prev hp)).copy ++ String.singleton ((p.prev hp).get ⋯)) (s.sliceFrom p).copy
-- Mathlib.Combinatorics.Graph.Simple
/-- Construct a graph from a simple graph. It has every element of the vertex type as a vertex.  -/
Graph.ofSimpleGraph : {α : Type u_1} → SimpleGraph α → Graph α (Sym2 α)
-- Init.Data.SInt.Bitwise
Int64.or_eq_zero_iff : ∀ {a b : Int64}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.disjoint_hull_left_of_convex : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {C : ConvexCone 𝕜 M} {s : Set M},
  Convex 𝕜 s → (Disjoint (ConvexCone.hull 𝕜 s) C ↔ Disjoint s ↑C)
-- Mathlib.Computability.Primrec.Basic
/-- `Primrec f` means `f` is primitive recursive (after
encoding its input and output as natural numbers).  -/
Primrec : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → β) → Prop
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (i num : ℕ) (source : Lean.Meta.Grind.SplitSource),
  sizeOf { expr := expr, i := i, num := num, source := source } =
    1 + sizeOf expr + sizeOf i + sizeOf num + sizeOf source
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.s.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i : ℕ) (h_1 : Unit → motive 0) (h_2 : (i : ℕ) → motive i.succ),
  (match i.succ with
    | 0 => h_1 ()
    | i.succ => h_2 i) =
    h_2 i
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_eq_of_bound_le : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  a < b → N ≤ n → MeasureTheory.upperCrossingTime a b f N n ω = N
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C}
  [inst_1 : SizeOf C] (a : X.obj (Opposite.op { len := n + 1 }) ⟶ Z)
  (b : Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z)), sizeOf { a := a, b := b } = 1 + sizeOf a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)], a ∈ t → t.get? a = some (t.get! a)
-- Mathlib.Combinatorics.Graph.Simple
Graph.toSimpleGraph_mono : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤s H), G.toSimpleGraph ≤ ⋯ ▸ H.toSimpleGraph
-- Plausible.Sampleable
Plausible.List.sampleableExt : {α : Type u_1} → [Plausible.SampleableExt α] → Plausible.SampleableExt (List α)
-- Mathlib.Data.Set.Function
Set.InjOn.image_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t u : Set α},
  Set.InjOn f u → s ⊆ u → t ⊆ u → f '' (s ∩ t) = f '' s ∩ f '' t
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_ofNat_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℕ) [inst_4 : c.AtLeastTwo] (M : Matrix m n α),
  (OfNat.ofNat c • M).conjTranspose = OfNat.ofNat c • M.conjTranspose
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.erase_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m
-- Mathlib.CategoryTheory.EpiMono
/-- This is a theorem saying if five faces of a cube commute and one edge is a monomorphism,
then the sixth face must also commute.  -/
CategoryTheory.cube_lemma_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M000 M001 M010 M011 M100 M101 M110 M111 : C}
  (f00x : M000 ⟶ M001) (f01x : M010 ⟶ M011) (f10x : M100 ⟶ M101) (f11x : M110 ⟶ M111) (f0x0 : M000 ⟶ M010)
  (f0x1 : M001 ⟶ M011) (f1x0 : M100 ⟶ M110) (f1x1 : M101 ⟶ M111) (fx00 : M000 ⟶ M100) (fx01 : M001 ⟶ M101)
  (fx10 : M010 ⟶ M110) (fx11 : M011 ⟶ M111),
  CategoryTheory.CategoryStruct.comp f0x0 f01x = CategoryTheory.CategoryStruct.comp f00x f0x1 →
    CategoryTheory.CategoryStruct.comp f1x0 f11x = CategoryTheory.CategoryStruct.comp f10x f1x1 →
      CategoryTheory.CategoryStruct.comp fx00 f10x = CategoryTheory.CategoryStruct.comp f00x fx01 →
        CategoryTheory.CategoryStruct.comp fx10 f11x = CategoryTheory.CategoryStruct.comp f01x fx11 →
          CategoryTheory.CategoryStruct.comp f0x1 fx11 = CategoryTheory.CategoryStruct.comp fx01 f1x1 →
            ∀ [CategoryTheory.Mono f11x],
              CategoryTheory.CategoryStruct.comp f0x0 fx10 = CategoryTheory.CategoryStruct.comp fx00 f1x0
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProd_adj : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x y : α × β},
  (G □ H).Adj x y ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1
-- Mathlib.Order.SuccPred.Archimedean
Succ.rec_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] [IsSuccArchimedean α] (p : α → Prop),
  p ⊥ → (∀ (a : α), p a → p (Order.succ a)) → ∀ (a : α), p a
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNeg_addPos_eq_both : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  assignment.addPosAssignment.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.eq_add_coeff_insert : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (x : Int.Internal.Linear.Var),
  Int.Internal.Linear.Poly.denote ctx p =
    p.coeff x * Int.Internal.Linear.Var.denote ctx x +
      Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.insert (-p.coeff x) x p)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.refl_partialEquiv : ∀ {X : Type u_1} [inst : TopologicalSpace X], (OpenPartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.instIsDenseCompOfIsEquivalence : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor C' C) [F.IsDense] [G.IsEquivalence], (G.comp F).IsDense
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.mk : {R : Type u} → R → R → R → R → R → WeierstrassCurve R
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.beq : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivisionMonoid : {α : Type u_1} → [DivisionMonoid α] → DivisionMonoid αᵒᵈ
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `LeftDistribClass` instance along a surjective function.  -/
Function.Surjective.leftDistribClass : ∀ {R : Type u_1} {S : Type u_2} (f : R → S),
  Function.Surjective f →
    ∀ [inst : Add S] [inst_1 : Mul S] [inst_2 : Mul R] [inst_3 : Add R] [LeftDistribClass R],
      (∀ (x y : R), f (x + y) = f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → LeftDistribClass S
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.sInf : ∀ {𝕜 : Type u_2} {E : Type u_6} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {ts : Set (TopologicalSpace E)}, (∀ t ∈ ts, PolynormableSpace 𝕜 E) → PolynormableSpace 𝕜 E
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
/-- The two-sided ideal of compactly supported functions.  -/
compactlySupported : (α : Type u_1) →
  (γ : Type u_2) →
    [inst : TopologicalSpace α] → [inst_1 : NonUnitalNormedRing γ] → TwoSidedIdeal (BoundedContinuousFunction α γ)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.coe_continuousLinearEquiv : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)]
  [inst_3 : (i : ι) → TopologicalSpace (β i)], ⇑(PiLp.continuousLinearEquiv p 𝕜 β) = WithLp.ofLp
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.both : Lean.Meta.SplitKind
-- Mathlib.Algebra.Group.End
/-- `Additive G` and `G` have isomorphic automorphism groups.  -/
AddAutAdditive : (G : Type u_3) → [inst : Group G] → AddAut (Additive G) ≃+ Additive (MulAut G)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.neg_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommGroup R]
  {s : HahnSeries.SummableFamily Γ R α} {a : α}, (-s) a = -s a
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).natDegree = 0
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Bundled left-exact functors.  -/
CategoryTheory.LeftExactFunctor : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of a monotone function and a strictly monotone function is strictly monotone.  -/
Monotone.mul_strictMono' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] [MulLeftStrictMono α]
  [MulRightMono α] {f g : β → α}, Monotone f → StrictMono g → StrictMono fun x => f x * g x
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesColimitsOfShape_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sSupHomClass F α β] {J : Type w} [inst_4 : CategoryTheory.Category.{w', w} J],
  CategoryTheory.Limits.PreservesColimitsOfShape J (↑f).toFunctor
-- Mathlib.Algebra.Order.Floor.Div
zero_floorDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] (a : α), 0 ⌊/⌋ a = 0
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_injective : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate),
  B.IsSymm → Function.Injective (B.dualBasis hB)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_replicate : ∀ {α : Type u_1} {β : Type v} (f : α → β) (k : ℕ) (a : α),
  Multiset.map f (Multiset.replicate k a) = Multiset.replicate k (f a)
-- Mathlib.Analysis.Convex.Between
wbtw_total_of_sameRay_vsub_left : ∀ {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] {x y z : P},
  SameRay R (y -ᵥ x) (z -ᵥ x) → Wbtw R x y z ∨ Wbtw R x z y
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset_1 : HSub Std.Time.Timestamp Std.Time.Week.Offset Std.Time.Timestamp
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching -∞, `deriv` version  -/
deriv.lhopital_zero_atBot : ∀ {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in Filter.atBot, DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in Filter.atBot, deriv g x ≠ 0) →
      Filter.Tendsto f Filter.atBot (nhds 0) →
        Filter.Tendsto g Filter.atBot (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atBot l →
            Filter.Tendsto (fun x => f x / g x) Filter.atBot l
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.coe_symm_toCLMEquiv : ∀ {X : Type u_1} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : CommRing R] [inst_5 : TopologicalSpace R]
  [inst_6 : IsTopologicalRing R] [inst_7 : Module R E] [inst_8 : ContinuousSMul R E] (L : C(X, R) →L[R] E)
  (f : C(X, R)), (AbstractMeasure.toCLMEquiv.symm L) f = L f
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.instCompleteLattice : {X : Type u_1} → CompleteLattice (DiffeologicalSpace X)
-- Mathlib.Analysis.InnerProductSpace.Basic
ext_iff_inner_left : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, x = y ↔ ∀ (v : E), inner 𝕜 v x = inner 𝕜 v y
-- Mathlib.Topology.Algebra.MulAction
/-- An `AddTorsor` for a connected space is a connected space. This is not an instance because
it loops for a group as a torsor over itself.  -/
AddTorsor.connectedSpace : ∀ (G : Type u_1) (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P] [inst_2 : TopologicalSpace G]
  [PreconnectedSpace G] [inst_4 : TopologicalSpace P] [ContinuousVAdd G P], ConnectedSpace P
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_matches_empty : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat], ¬String.Slice.Pattern.Model.PatternModel.Matches pat ""
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_natural_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁)
  (g₂ : U₂ ⟶ V₂) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ V₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ V₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ V₁ V₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ U₁ U₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ g₁)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ g₂))
        h)
-- Mathlib.Algebra.Group.Basic
div_eq_div_iff_div_eq_div : ∀ {G : Type u_3} [inst : CommGroup G] {a b c d : G}, a / b = c / d ↔ a / c = b / d
-- Init.Data.List.Lemmas
List.filter_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Bool},
  List.filter p (x :: xs) = if p x = true then x :: List.filter p xs else List.filter p xs
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_fin_zero : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : Fin 0 → M),
  Finsupp.linearCombination R f = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `neg_lt`. -/
neg_lt_of_neg_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α],
  -a < b → -b < a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew!_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} {l : List ((a : α) × β a)},
  (↑(t₁.insertManyIfNew! l)).Equiv
    (List.foldl (fun acc p => Std.DTreeMap.Internal.Impl.insertIfNew! p.fst p.snd acc) t₁ l)