mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  o.bsup f = o.blsub f ∨ Order.succ (o.bsup f) = o.blsub f
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Homotopy between morphisms of short complexes is compatible with postcomposition.  -/
CategoryTheory.ShortComplex.Homotopy.compRight : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            (ψ : S₂ ⟶ S₃) →
              CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp φ₁ ψ)
                (CategoryTheory.CategoryStruct.comp φ₂ ψ)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.one_le_pi_div_two : 1 ≤ Real.pi / 2
-- Mathlib.RingTheory.RingHom.Locally
/-- **Alias** of the forward direction of `RingHom.locally_iff_span_eq_top`. -/
RingHom.Locally.span_eq_top : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f →
    Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)} = ⊤
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The positive cone is the convex cone formed by the set of nonnegative elements in an ordered
module.  -/
ConvexCone.positive : (R : Type u_2) →
  (M : Type u_4) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : PartialOrder M] →
            [IsOrderedAddMonoid M] → [inst_5 : Module R M] → [PosSMulMono R M] → ConvexCone R M
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearEquiv.ofInjectiveEndo_left_inv : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f),
  ↑(LinearEquiv.ofInjectiveEndo f h_inj).symm * f = 1
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instFinitenessRelation : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] →
      [Std.Rxi.IsAlwaysFinite α] → Std.Iterators.FinitenessRelation (Std.Rxi.Iterator α) Id
-- Mathlib.Tactic.FunProp.Theorems
/-- Get lambda theorems for particular function property `funPropName`.  -/
Mathlib.Meta.FunProp.getLambdaTheorems : Lean.Name → Mathlib.Meta.FunProp.LambdaTheoremType → Lean.CoreM (Array Mathlib.Meta.FunProp.LambdaTheorem)
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.functorialityRightAdjoint.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C),
  adj.functorialityRightAdjoint K =
    (CategoryTheory.Limits.Cocone.functoriality (K.comp F) G).comp
      (CategoryTheory.Limits.Cocone.precompose
        (CategoryTheory.CategoryStruct.comp K.rightUnitor.inv
          (CategoryTheory.CategoryStruct.comp (K.whiskerLeft adj.unit) (K.associator F G).inv)))
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- If `f` is a.e. equal to zero on a rectangular box, then it has McShane integral zero on this
box.  -/
BoxIntegral.HasIntegral.of_aeEq_zero : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)}
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
  f =ᵐ[μ.restrict ↑I] 0 → l.bRiemann = false → BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul 0
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.mk.sizeOf_spec : ∀ (kinds : Array Lean.Json.CompressWorkItemKind✝) (values : Array Lean.Json) (objectFieldKeys : Array String),
  sizeOf { kinds := kinds, values := values, objectFieldKeys := objectFieldKeys } =
    1 + sizeOf kinds + sizeOf values + sizeOf objectFieldKeys
-- Mathlib.CategoryTheory.IsConnected
/-- j₁ and j₂ are related by `Zag` if there is a morphism between them.  -/
CategoryTheory.Zag : {J : Type u₁} → [CategoryTheory.Category.{v₁, u₁} J] → J → J → Prop
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_diff_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.Analysis.Convex.Between
mem_vadd_const_affineSegment : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : V} (p : P),
  z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `IsEffective` descends along faithfully flat algebras.  -/
Algebra.IsEffective.of_isEffective_tensorProduct_of_faithfullyFlat : ∀ (R : Type u_3) [inst : CommRing R] (S : Type u_4) (T : Type u_5) [inst_1 : CommRing T] [inst_2 : Algebra R T]
  [inst_3 : Ring S] [inst_4 : Algebra R S] [Module.FaithfullyFlat R T],
  Algebra.IsEffective T (TensorProduct R T S) → Algebra.IsEffective R S
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
defines a semigroup homomorphism to `Nᵐᵒᵖ`.  -/
MulHom.toOpposite : {M : Type u_3} →
  {N : Type u_4} → [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → (∀ (x y : M), Commute (f x) (f y)) → M →ₙ* Nᵐᵒᵖ
-- Mathlib.Data.Finmap
Finmap.union_comm_of_disjoint : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ : Finmap β}, s₁.Disjoint s₂ → s₁ ∪ s₂ = s₂ ∪ s₁
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.comm_assoc : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (self : M.Hom N) (g : G) {Z : V} (h : N.V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (M.ρ g) (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (N.ρ g) h)
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F ↥A],
      Cardinal.lift.{v, w} (Module.rank F L) * Cardinal.lift.{w, v} (Module.rank (↥(IntermediateField.adjoin L ↑A)) E) =
        Cardinal.lift.{w, v} (Module.rank (↥A) E)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.root_mem_span_int : ∀ {ι : 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} (b : P.Base) (i : ι),
  P.root i ∈ Submodule.span ℤ (⇑P.root '' ↑b.support)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
MeasureTheory.MemLp.aefinStronglyMeasurable : ∀ {α : Type u_1} {G : Type u_2} {p : ENNReal} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup G] {f : α → G},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → MeasureTheory.AEFinStronglyMeasurable f μ
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.getSimprocExtensionCore? : Lean.Name → IO (Option Lean.Meta.Simp.SimprocExtension)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_le_count_of_le : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)]
  {a b p : Associates α}, b ≠ 0 → Irreducible p → a ≤ b → p.count a.factors ≤ p.count b.factors
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.success : {α : Type} → α → Lean.Server.ServerRequestResponse α
-- Mathlib.Order.CompleteLattice.Lemmas
codisjoint_sInf_left : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α},
  Codisjoint (sInf a) b → ∀ {i : α}, i ∈ a → Codisjoint i b
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
/-- If a set has the unique differentiability property at a point x, then the image of this set
under a map with onto derivative has also the unique differentiability property at the image point.
 -/
HasFDerivWithinAt.uniqueDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {f' : E →L[𝕜] F} {x : E},
  HasFDerivWithinAt f f' s x → UniqueDiffWithinAt 𝕜 s x → DenseRange ⇑f' → UniqueDiffWithinAt 𝕜 (f '' s) (f x)
-- Init.Data.Int.DivMod.Lemmas
Int.exists_add_of_le : ∀ {a b : ℤ}, a ≤ b → ∃ c, b = a + ↑c
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The rightmost object of the fork diagram of the Stacks entry, which
contains the data used to check a family of elements for a presieve is compatible.
 -/
CategoryTheory.Presheaf.secondObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {U : C} →
          CategoryTheory.Presieve U →
            CategoryTheory.Functor Cᵒᵖ A →
              [CategoryTheory.Limits.HasProducts A] → [CategoryTheory.Limits.HasPullbacks C] → A
-- Lean.Meta.BinderNameHint
_private.Lean.Meta.BinderNameHint.0.Lean.makeFresh : ℕ → Array Lean.Name → Lean.CoreM (Array Lean.Name)
-- Mathlib.Order.WithBot
WithBot.monotone_map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone (WithBot.map f) ↔ Monotone f
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.eq_one_of_pos_of_logb_eq_zero_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → Real.logb b x = 0 → x = 1
-- Mathlib.Order.KrullDimension
/-- The Krull dimension is the supremum of the elements' heights.

This version of the lemma assumes that `α` is nonempty. In this case, the coercion from `ℕ∞` to
`WithBot ℕ∞` is on the outside of the right-hand side, which is usually more convenient.

If `α` were empty, then `krullDim α = ⊥`. See `krullDim_eq_iSup_height` for the more general
version, with the coercion under the supremum.
 -/
Order.krullDim_eq_iSup_height_of_nonempty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim α = ↑(⨆ a, Order.height a)
-- Mathlib.Order.SupClosed
latticeClosure_mono : ∀ {α : Type u_3} [inst : Lattice α], Monotone ⇑latticeClosure
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_ne_top_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  InformationTheory.klDiv μ ν ≠ ⊤ ↔ μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
-- Mathlib.Topology.Convenient.Category
/-- The equivalence of categories `GeneratedByTopCat X ≌ ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.equivalence : {ι : Type t} →
  {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → GeneratedByTopCat X ≌ ContinuousGeneratedByCat X
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_comp_smul_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} {E : Type u_5} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 E] {X : Ω → 𝓧} {Y : Ω → 𝓨}
  {f : 𝓧 → 𝕜} {g : 𝓨 → E},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ) →
            ∫ (x : Ω), (f ∘ X • g ∘ Y) x ∂μ = (∫ (x : Ω), (f ∘ X) x ∂μ) • ∫ (x : Ω), (g ∘ Y) x ∂μ
-- Mathlib.Topology.Algebra.Module.Basic
continuousSMul_inducedₛₗ : ∀ {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂' : Type u_5} {φ : R → S} [inst : SMul R M₁] [inst_1 : SMul S M₂']
  [u : TopologicalSpace R] [u' : TopologicalSpace S] {t' : TopologicalSpace M₂'} [ContinuousSMul S M₂'] {F' : Type u_7}
  [inst_3 : FunLike F' M₁ M₂'] [MulActionSemiHomClass F' φ M₁ M₂'] (f' : F'), Continuous φ → ContinuousSMul R M₁
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax'_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] (a : B),
  ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapId a).hom = F.mapId a
-- Mathlib.Analysis.Normed.Field.UnitBall
/-- Monoid homomorphism from the unit sphere in a normed division ring to the group of units.  -/
unitSphereToUnits : (𝕜 : Type u_2) → [inst : NormedDivisionRing 𝕜] → ↑(Metric.sphere 0 1) →* 𝕜ˣ
-- Mathlib.Data.EReal.Operations
EReal.le_add_of_forall_gt : ∀ {a b c : EReal}, a ≠ ⊥ ∨ b ≠ ⊤ → a ≠ ⊤ ∨ b ≠ ⊥ → (∀ a' > a, ∀ b' > b, c ≤ a' + b') → c ≤ a + b
-- Mathlib.Algebra.Order.CauSeq.BigOperators
cauchy_product : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f g : ℕ → β},
  (IsCauSeq abs fun m => ∑ n ∈ Finset.range m, abv (f n)) →
    (IsCauSeq abv fun m => ∑ n ∈ Finset.range m, g n) →
      ∀ (ε : α),
        0 < ε →
          ∃ i,
            ∀ j ≥ i,
              abv
                  ((∑ k ∈ Finset.range j, f k) * ∑ k ∈ Finset.range j, g k -
                    ∑ n ∈ Finset.range j, ∑ m ∈ Finset.range (n + 1), f m * g (n - m)) <
                ε
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Hom.inv_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G X : C}
  [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ G), f⁻¹ = CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv
-- Mathlib.Algebra.Group.Basic
inv_div_left : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), a⁻¹ / b = (b * a)⁻¹
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_smulₛₗ : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S) (m : M) (x : R), f (m • x) = φ m • f x
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of an integrable function is greater than its integral,
while avoiding a null set.  -/
MeasureTheory.exists_notMem_null_integral_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → μ N = 0 → ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_X_right : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R) (i : σ),
  (MvPolynomial.bind₁ f) (MvPolynomial.X i) = f i
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.divMod.match_3.eq_3 : ∀ (motive : PosNum → Sort u_1) (h_1 : (n : PosNum) → motive n.bit0) (h_2 : (n : PosNum) → motive n.bit1)
  (h_3 : Unit → motive PosNum.one),
  (match PosNum.one with
    | n.bit0 => h_1 n
    | n.bit1 => h_2 n
    | PosNum.one => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_hom_ne_zero : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Multiset M},
  s ≠ 0 → ∀ {F : Type u_8} [inst_2 : FunLike F M N] [MulHomClass F M N] (f : F), (Multiset.map (⇑f) s).prod = f s.prod
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.mapAux.eq_def : ∀ (f : Char → Char) (i : String.Pos.Raw) (s : String),
  String.Legacy.mapAux f i s =
    if h : String.Pos.Raw.atEnd s i = true then s
    else
      have c := f (String.Pos.Raw.get s i);
      have this := ⋯;
      have s := String.Pos.Raw.set s i c;
      String.Legacy.mapAux f (String.Pos.Raw.next s i) s
-- Mathlib.Order.SymmDiff
bihimp_left_injective : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), Function.Injective fun x => bihimp x a
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J) {Z : C}
  (h : CategoryTheory.Limits.colimit F.leftOp ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).unop
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLeftOpIsoUnopLimit F).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.leftOp (Opposite.op j)) h
-- Mathlib.Analysis.SpecialFunctions.Exponential
Complex.exp_eq_exp_ℂ : Complex.exp = NormedSpace.exp
-- Mathlib.Algebra.Group.Conj
ConjClasses.instDecidableEqOfDecidableRelIsConj.eq_1 : ∀ {α : Type u} [inst : Monoid α] [inst_1 : DecidableRel IsConj],
  ConjClasses.instDecidableEqOfDecidableRelIsConj = ConjClasses.instDecidableEqOfDecidableRelIsConj._aux_1
-- Lean.DocString.Types
Lean.Doc.instInhabitedInline.default : {i : Type u} → Lean.Doc.Inline i
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.instCoeOutIsometryEquiv : {F : Type u_1} →
  {α : Type u} →
    {β : Type v} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : EquivLike F α β] → [IsometryClass F α β] → CoeOut F (α ≃ᵢ β)
-- Mathlib.Data.Int.Basic
Int.natCast_dvd_ofNat : ∀ {x y : ℕ}, ↑x ∣ OfNat.ofNat y ↔ x ∣ OfNat.ofNat y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.rfl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.Equiv t
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_add_right_sub_eq : ∀ {α : Type u_1} {M : Type u_3} [inst : CommMonoid M] {f : α → M} [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [inst_5 : LocallyFiniteOrder α] [inst_6 : Sub α] [OrderedSub α]
  (a b c : α), ∏ x ∈ Finset.Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Finset.Ico a b, f x
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trLList.match_1.eq_2 : ∀ (motive : List (List ℕ) → Sort u_1) (l : List ℕ) (ls : List (List ℕ)) (h_1 : Unit → motive [])
  (h_2 : (l : List ℕ) → (ls : List (List ℕ)) → motive (l :: ls)),
  (match l :: ls with
    | [] => h_1 ()
    | l :: ls => h_2 l ls) =
    h_2 l ls
-- Mathlib.Logic.Function.Defs
/-- A function is called bijective if it is both injective and surjective.  -/
Function.Bijective : {α : Sort u₁} → {β : Sort u₂} → (α → β) → Prop
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_5 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match q.copy with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_5 q
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
bddAbove_neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G},
  BddAbove (-s) ↔ BddBelow s
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingProd.eq_2 : ∀ {G : Type u_4} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G] (g : G), [g].alternatingProd = g
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.instMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.monomorphisms C).IsMultiplicative
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instInhabitedLabel.default : Lean.Meta.NormCast.Label
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- A Lie algebra is simple if it is irreducible as a Lie module over itself via the adjoint
action, and it is non-Abelian.  -/
LieAlgebra.IsSimple : (R : Type u_1) → (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey?.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minKey? = some k
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.mul_inv_toRightFun_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hT : Subgroup.IsComplement (↑H) T) (g : G),
  g * (↑(hT.toRightFun g))⁻¹ ∈ H
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- If `g` maps a second argument of 0 to 1, then multiplying it over the
result of `onFinset` is the same as multiplying it over the original `Finset`.  -/
Finsupp.onFinset_prod : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {s : Finset α} {f : α → M}
  {g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
  (∀ (a : α), g a 0 = 1) → (Finsupp.onFinset s f hf).prod g = ∏ a ∈ s, g a (f a)
-- Init.Data.List.MinMaxIdx
List.ne_nil_of_maxIdxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {k : ℕ} {xs : List α},
  List.maxIdxOn? f xs = some k → xs ≠ []
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.contains.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ],
  s.contains pat =
    Std.Iter.any
      (fun x =>
        match x with
        | String.Slice.Pattern.SearchStep.matched startPos endPos => true
        | x => false)
      (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s)