mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.BifibrantObject.ιFibrantObject.obj X).obj
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.val_apply_equiv : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (r : WithVal v), v ((WithVal.equiv v) r) = Valued.v r
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.toAddSubmonoid_toNatSubmodule : ∀ {M : Type u_3} [inst : AddCommMonoid M] (S : Submodule ℕ M), AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S
-- Mathlib.Topology.Separation.Regular
closed_nhds_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsClosed s) id
-- Mathlib.Order.Hom.CompleteLattice
/-- Reinterpret an order isomorphism as a morphism of complete lattices.  -/
CompleteLatticeHom.OrderIso.toCompleteLatticeHom : {α : Type u_2} →
  {β : Type u_3} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → α ≃o β → CompleteLatticeHom α β
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_pos : ∀ {f : ℝ → ℝ} {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      (∀ x ∈ Set.Ioc a b, 0 ≤ f x) → (∃ c ∈ Set.Icc a b, 0 < f c) → 0 < ∫ (x : ℝ) in a..b, f x
-- Mathlib.Data.FP.Basic
FP.ofRat : [C : FP.FloatCfg] → FP.RMode → ℚ → FP.Float
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.filter_apply_ne_zero_iff : ∀ {α : Type u_1} {p : PMF α} {s : Set α} (h : ∃ a ∈ s, a ∈ p.support) (a : α),
  (p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_le_cardinalMk : ∀ {α : Type u} (M : Matroid α) (X : Set α), M.cRk X ≤ Cardinal.mk ↑X
-- Mathlib.Algebra.Category.BoolRing
BoolRing.instCoeSortType : CoeSort BoolRing (Type u_1)
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
/-- For cofans on maps `f₁ : ι₁ → C`, `f₂ : ι₂ → C` and a binary cofan on their
cocone points, construct one family of morphisms indexed by `ι₁ ⊕ ι₂`  -/
CategoryTheory.Limits.Cofan.combPairHoms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {ι₁ : Type u_1} →
      {ι₂ : Type u_2} →
        {f₁ : ι₁ → C} →
          {f₂ : ι₂ → C} →
            (c₁ : CategoryTheory.Limits.Cofan f₁) →
              (c₂ : CategoryTheory.Limits.Cofan f₂) →
                (bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt) → (i : ι₁ ⊕ ι₂) → Sum.elim f₁ f₂ i ⟶ bc.pt
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_coord_zero : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) {m : (i : ι) → M₁ i} (i : ι), m i = 0 → f m = 0
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `f □ g` lifts against `h` if and only if `g` lifts against `f ⋔ h`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] {A B K L X Y : C} {f : A ⟶ B} {g : K ⟶ L} {h : X ⟶ Y},
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk g).hom h ↔
    CategoryTheory.HasLiftingProperty g (Opposite.op (CategoryTheory.Arrow.mk f) ⋔ CategoryTheory.Arrow.mk h).hom
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
(weak) convergence of `FiniteMeasure`s on `X` implies (weak) convergence of the push-forwards
of these measures by `f`.  -/
MeasureTheory.FiniteMeasure.tendsto_map_of_tendsto_of_continuous : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] [inst_2 : TopologicalSpace Ω]
  [inst_3 : OpensMeasurableSpace Ω] [inst_4 : TopologicalSpace Ω'] [inst_5 : BorelSpace Ω'] {ι : Type u_3}
  {L : Filter ι} (νs : ι → MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω),
  Filter.Tendsto νs L (nhds ν) →
    ∀ {f : Ω → Ω'}, Continuous f → Filter.Tendsto (fun i => (νs i).map f) L (nhds (ν.map f))
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.continuous_CC'₀ : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2), Continuous (Profinite.NobelingProof.CC'₀ C ho)
-- Init.Data.UInt.Lemmas
UInt16.ofNat_le_iff_le : ∀ {a b : ℕ}, a < UInt16.size → b < UInt16.size → (UInt16.ofNat a ≤ UInt16.ofNat b ↔ a ≤ b)
-- Mathlib.Tactic.TacticAnalysis
/-- Type returned by the `.trigger` function.  -/
Mathlib.TacticAnalysis.ComplexConfig.ctx : Mathlib.TacticAnalysis.ComplexConfig → Type
-- Aesop.Forward.State
/-- The rule pattern substitution.  -/
Aesop.RawHyp.patSubst : Aesop.Substitution → Aesop.RawHyp
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.delta.eq_1 : Std.DTreeMap.Internal.delta = 3
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  [inst_4 : CategoryTheory.ExponentiableMorphism f] [inst_5 : CategoryTheory.ExponentiableMorphism g]
  [inst_6 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ExponentiableMorphism.pushforwardComp f g).hom
        (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.comp f g)))
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).counit =
    (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).counit
-- Mathlib.Data.ENNReal.Operations
/-- An element `a` is `AddLECancellable` if `a + b ≤ a + c` implies `b ≤ c` for all `b` and `c`.
This is true in `ℝ≥0∞` for all elements except `∞`.  -/
ENNReal.addLECancellable_iff_ne : ∀ {a : ENNReal}, AddLECancellable a ↔ a ≠ ⊤
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.symm_apply_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) (a_1 : G),
  e.symm (e a_1) = a_1
-- Mathlib.Data.List.Sym
List.sym2.eq_def : ∀ {α : Type u_1} (x : List α),
  x.sym2 =
    match x with
    | [] => []
    | x :: xs => List.map (fun y => s(x, y)) (x :: xs) ++ xs.sym2
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termHatγ : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderRetractsFunctorFunctorCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderRetracts] (J : Type u'') [inst_2 : CategoryTheory.Category.{v'', u''} J],
  (W.functorCategory J).IsStableUnderRetracts
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.unop_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.Precylinder A),
  P.unop.p₁ = P.i₁.unop
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.glue_condition_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F] (x : carrier (D.V (i, j))),
  (CategoryTheory.ConcreteCategory.hom (D.ι j))
      ((CategoryTheory.ConcreteCategory.hom (D.f j i)) ((CategoryTheory.ConcreteCategory.hom (D.t i j)) x)) =
    (CategoryTheory.ConcreteCategory.hom (D.ι i)) ((CategoryTheory.ConcreteCategory.hom (D.f i j)) x)
-- Mathlib.Topology.NhdsWithin
nhdsWithin_eq_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, nhdsWithin a s = nhds a ↔ s ∈ nhds a
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.left_act_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp M.actLeft (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.hom)
      (CategoryTheory.CategoryStruct.comp N.actLeft h)
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- The counit isomorphism upgrades to a monoidal isomorphism.  -/
CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Monoidal.equivalenceTransported e).counit
-- Mathlib.Analysis.Normed.Ring.Basic
SubringClass.toNormOneClass : ∀ {S : Type u_5} {R : Type u_6} [inst : SetLike S R] [inst_1 : SeminormedRing R] [NormOneClass R]
  [inst_3 : SubringClass S R] (s : S), NormOneClass ↥s
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State.mk : Aesop.Script.UScript → Bool → Aesop.ExtractScriptM.State
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Helper function for throwing exceptions.  -/
Mathlib.Tactic.Coherence.exception : {α : Type} → Lean.MVarId → Lean.MessageData → Lean.MetaM α
-- Mathlib.Data.Nat.Count
Nat.count.eq_1 : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p n = List.countP (fun b => decide (p b)) (List.range n)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Kan lifts on `g` along `f` are unique up to isomorphism.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} → {g : c ⟶ a} → {s t : CategoryTheory.Bicategory.LeftLift f g} → s.IsKan → t.IsKan → (s ≅ t)
-- Init.Data.List.Perm
List.isPerm.eq_1 : ∀ {α : Type u} [inst : BEq α] (x : List α), [].isPerm x = x.isEmpty
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.ULiftYoneda.instFullFunctorOppositeTypeUliftYoneda : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.uliftYoneda.{w, v₁, u₁}.Full
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] (X : B),
  P.fullsubcategory.obj X = CategoryTheory.Cat.of (P.Obj X)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.functorialityCompPrecompose.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H'),
  CategoryTheory.Functor.functorialityCompPrecompose α =
    CategoryTheory.NatIso.ofComponents' (fun c => CategoryTheory.Limits.Cocone.extInv (α.app c.pt) ⋯) ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_mem_smul_iff_of_isUnit : ∀ {M : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : Monoid M] [inst_4 : DistribMulAction M V] [inst_5 : SMulCommClass M k V] {a : M} {s : AffineSubspace k V}
  {p : V}, IsUnit a → (a • p ∈ a • s ↔ p ∈ s)
-- Init.Data.Int.LemmasAux
Int.mul_le_mul_of_le_of_le_of_nonpos_of_nonpos : ∀ {a b c d : ℤ}, c ≤ a → d ≤ b → b ≤ 0 → c ≤ 0 → a * b ≤ c * d
-- Init.Grind.Ring.Field
Lean.Grind.Field.zpow_sub_one : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : α}, a ≠ 0 → ∀ (n : ℤ), a ^ (n - 1) = a ^ n * a⁻¹
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β γ : Type t}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C]
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape γ C] (f : α → β) (g : β → γ),
  U.mapPower (g ∘ f) = CategoryTheory.CategoryStruct.comp (U.mapPower g) (U.mapPower f)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.mconv_smul_left : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite ν] (s : ENNReal), (s • μ).mconv ν = s • μ.mconv ν
-- Mathlib.Computability.TuringMachine.Computable
/-- The forgetful map, forgetting the upper bound on the number of steps.  -/
Turing.TM2OutputsInTime.toTM2Outputs : {tm : Turing.FinTM2} →
  {l : List (tm.Γ tm.k₀)} →
    {l' : Option (List (tm.Γ tm.k₁))} → {m : ℕ} → Turing.TM2OutputsInTime tm l l' m → Turing.TM2Outputs tm l l'
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatTrans_id : ∀ {C D : CategoryTheory.Cat} (F : C ⟶ D),
  (CategoryTheory.CategoryStruct.id F).toNatTrans = CategoryTheory.CategoryStruct.id F.toFunctor
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMax.match_1.eq_3 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α) (sz : ℕ) (l' : Ordnode α) (y : α)
  (r' : Ordnode α) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → motive (Ordnode.node size l x Ordnode.nil))
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) →
          (sz : ℕ) →
            (l' : Ordnode α) → (y : α) → (r' : Ordnode α) → motive (Ordnode.node size l x (Ordnode.node sz l' y r'))),
  (match Ordnode.node size l x (Ordnode.node sz l' y r') with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size l x Ordnode.nil => h_2 size l x
    | Ordnode.node size l x (Ordnode.node sz l' y r') => h_3 size l x sz l' y r') =
    h_3 size l x sz l' y r'
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.comp_assoc : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {L3 : FirstOrder.Language}
  (F : L'' →ᴸ L3) (G : L' →ᴸ L'') (H : L →ᴸ L'), (F.comp G).comp H = F.comp (G.comp H)
-- Lean.Elab.PreDefinition.TerminationHint
/-- Remembers `extraParams` for later use. Needs to happen early enough where we still know
how many parameters came from the function header (`headerParams`).
 -/
Lean.Elab.TerminationHints.rememberExtraParams : ℕ → Lean.Elab.TerminationHints → Lean.Expr → Lean.Elab.TerminationHints
-- Mathlib.Algebra.Group.Torsion
nsmul_eq_zero_iff_left : ∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M}, a ≠ 0 → (n • a = 0 ↔ n = 0)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The division in the Ore localization `X[S⁻¹]`, as a fraction of an element of `X` and `S`.  -/
OreLocalization.oreDiv : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] → {X : Type u_2} → [inst_2 : MulAction R X] → X → ↥S → OreLocalization S X
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_succ_succ : ∀ {m n : ℕ}, ((m + 1)...=n + 1).toArray = Array.map (fun x => x + 1) (m...=n).toArray
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumCompl_symm_apply_of_notMem : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {x : α} (hx : x ∉ s),
  (Equiv.Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  2 < s.ncard → ∃ g ∈ MulAction.stabilizer (Equiv.Perm α) s, g.IsThreeCycle
-- Mathlib.Algebra.Category.FGModuleCat.Limits
FGModuleCat.instFiniteCarrierPiObjModuleCatOfFinite : ∀ {k : Type u} [inst : Ring k] {J : Type} [Finite J] (Z : J → ModuleCat k) [∀ (j : J), Module.Finite k ↑(Z j)],
  Module.Finite k ↑(∏ᶜ fun j => Z j)
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.Splits.of_degree_le_zero`. -/
Polynomial.splits_of_degree_le_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.degree ≤ 0 → f.Splits
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.b.eq_1 : ∀ (x : ℝ) (n : ℕ), Chebyshev.b✝ x n = Chebyshev.theta (x ^ (↑n)⁻¹)
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.mk.injEq : ∀ (cache : Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr) (varTypes lhss rhss : Array Lean.Expr)
  (cache_1 : Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr) (varTypes_1 lhss_1 rhss_1 : Array Lean.Expr),
  ({ cache := cache, varTypes := varTypes, lhss := lhss, rhss := rhss } =
      { cache := cache_1, varTypes := varTypes_1, lhss := lhss_1, rhss := rhss_1 }) =
    (cache = cache_1 ∧ varTypes = varTypes_1 ∧ lhss = lhss_1 ∧ rhss = rhss_1)
-- Mathlib.Order.Preorder.Chain
Monotone.isChain_range : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → IsChain (fun x1 x2 => x1 ≤ x2) (Set.range f)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_iSup : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A] {ι : Sort u_4}
  (T : AddSubmonoid R) (S : ι → AddSubmonoid A), T • ⨆ i, S i = ⨆ i, T • S i
-- Mathlib.Order.Filter.IsBounded
isCoboundedUnder_le_max : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : Filter α} {u v : α → β},
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u ∨ Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => max (u a) (v a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.nfp_lt_ord_of_isRegular : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}} {c : Cardinal.{u_1}},
  c.IsRegular →
    c ≠ Cardinal.aleph0 → (∀ i < c.ord, f i < c.ord) → ∀ {a : Ordinal.{u_1}}, a < c.ord → Ordinal.nfp f a < c.ord
-- Batteries.Data.Array.Merge
/-- `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`. If the arrays are sorted according to `lt`, then the
result is sorted as well. If two (or more) elements are equal according to `lt`, they are preserved.
 -/
Array.merge : {α : Type u_1} → (α → α → Bool) → Array α → Array α → Array α
-- Mathlib.Algebra.GroupWithZero.Associated
dvd_prime_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p q : M},
  Prime p → ∀ (n : ℕ), q ∣ p ^ n ↔ ∃ i ≤ n, Associated q (p ^ i)
-- Mathlib.Data.Finsupp.Single
Finsupp.support_eq_singleton : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, f.support = {a} ↔ f a ≠ 0 ∧ f = fun₀ | a => f a
-- Init.Omega.Logic
Lean.Omega.Decidable.and_not_or_not_and_of_not_iff : ∀ {a b : Prop} [Decidable a] [Decidable b], ¬(a ↔ b) → a ∧ ¬b ∨ ¬a ∧ b
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_apply_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α γ}
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α},
  ((κ.prod η) a) (s ×ˢ t) = (κ a) s * (η a) t
-- Mathlib.SetTheory.Cardinal.Basic
/-- To prove that the lift of a supremum is bounded by some cardinal `t`,
it suffices to show that the lift of each cardinal is bounded by `t`.  -/
Cardinal.lift_iSup_le : ∀ {ι : Type v} {f : ι → Cardinal.{w}} {t : Cardinal.{max u w}},
  BddAbove (Set.range f) → (∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t) → Cardinal.lift.{u, w} (iSup f) ≤ t
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.nth_map : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (l : Turing.ListBlank Γ) (n : ℕ), (Turing.ListBlank.map f l).nth n = f.f (l.nth n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGT_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, compare a k = Ordering.gt},
  Std.DTreeMap.Internal.Impl.Const.getEntryGT k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.Const.getEntryGT k t₂ ⋯ ⋯
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.tensorμ_apply : ∀ {R : Type u} [inst : CommSemiring R] {A B C D : SemimoduleCat R} (x : ↑A) (y : ↑B) (z : ↑C) (w : ↑D),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.tensorμ A B C D))
      (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) =
    x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_rightOp_iff_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  {F : CategoryTheory.Functor Jᵒᵖ C}, CategoryTheory.Limits.HasColimit F.rightOp ↔ CategoryTheory.Limits.HasLimit F
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.ici_isAdmissible : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → ChainCompletePartialOrder.IsAdmissible x f (Set.Ici x)
-- Mathlib.Algebra.Order.Archimedean.Basic
eq_of_forall_rat_lt_iff_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  (∀ (q : ℚ), ↑q < x ↔ ↑q < y) → x = y
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Universal property of `IsAdicComplete`.
The lift linear map `lift I f h : M →ₗ[R] N` of a sequence of compatible
linear maps `f n : M →ₗ[R] N ⧸ (I ^ n • ⊤)`.
 -/
IsAdicComplete.lift : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_5} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  [IsAdicComplete I N] →
                    (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) →
                      (∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) → M →ₗ[R] N
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.range_eq_ofSimplex : ∀ {X : SSet} {n : ℕ} (f : SSet.stdSimplex.obj { len := n } ⟶ X),
  SSet.Subcomplex.range f = SSet.Subcomplex.ofSimplex (SSet.yonedaEquiv f)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.domExtend_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Bundle.Trivialization F fun z => proj ↑z)
  [inst_3 : Nonempty (Z → F)], (Bundle.Trivialization.domExtend hps e).target = e.toPretrivialization.target
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprULift_mathlib.toExpr : {α : Type s} → [Lean.ToExpr α] → Lean.ToLevel → Lean.ToLevel → ULift.{r, s} α → Lean.Expr