mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The isomorphism `f₊ (h ≫ g) ≅ h ≫ f₊ g` at the level of structured arrows.  -/
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            {x : B} →
              (h : x ⟶ c) →
                [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h] →
                  CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g) ≅
                    (CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeHomEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type u},
  M.freeHomEquiv =
    { toFun := fun f i => M.unitHomEquiv (CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) f),
      invFun := fun s =>
        CategoryTheory.Limits.Cofan.IsColimit.desc (SheafOfModules.isColimitFreeCofan I) fun i =>
          M.unitHomEquiv.symm (s i),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (v : ι' → M) (e : ι ≃ ι'),
  (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm) id
-- Mathlib.Topology.Sheaves.Limits
TopCat.instHasColimitsOfSizePresheafOfHasColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] (X : TopCat),
  CategoryTheory.Limits.HasColimitsOfSize.{v, v, max t v, max (max u v) t} (TopCat.Presheaf C X)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticWithinAt.zpow`

---

ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticWithinAt.fun_zpow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {s : Set E} {n : ℤ}, AnalyticWithinAt 𝕜 f s z → f z ≠ 0 → AnalyticWithinAt 𝕜 (fun i => f i ^ n) s z
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestFirstParTac : Lean.Elab.Tactic.Try.TryTactic
-- Lean.Meta.Sym.InstantiateS
/-- Caches the result `r` for `key` and returns `r`.  -/
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.save : Lean.Meta.Sym.ExprPtr × ℕ → Lean.Expr → Lean.Meta.Sym.M✝ Lean.Expr
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sub_one_left_of_dvd : ∀ {R : Type u} [inst : CommRing R] {x y : R}, y ∣ x → IsCoprime (x - 1) y
-- Mathlib.Data.Multiset.Bind
Multiset.filter_eq_bind : ∀ {α : Type u_1} (m : Multiset α) (p : α → Prop) [inst : DecidablePred p],
  Multiset.filter p m = m.bind fun a => if p a then {a} else 0
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_div : ∀ (x y : NNReal), NNReal.sqrt (x / y) = NNReal.sqrt x / NNReal.sqrt y
-- Mathlib.LinearAlgebra.TensorProduct.Matrix
/-- The linear map built from `TensorProduct.map` corresponds to the matrix built from
`Matrix.kronecker`.  -/
TensorProduct.toMatrix_map : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8}
  {ι' : Type u_10} {κ' : Type u_11} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι]
  [inst_3 : Fintype κ] [inst_4 : Finite ι'] [inst_5 : Finite κ'] [inst_6 : CommRing R] [inst_7 : AddCommGroup M]
  [inst_8 : AddCommGroup N] [inst_9 : AddCommGroup M'] [inst_10 : AddCommGroup N'] [inst_11 : Module R M]
  [inst_12 : Module R N] [inst_13 : Module R M'] [inst_14 : Module R N'] (bM : Module.Basis ι R M)
  (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (f : M →ₗ[R] M') (g : N →ₗ[R] N'),
  (LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (TensorProduct.map f g) =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) ((LinearMap.toMatrix bM bM') f) ((LinearMap.toMatrix bN bN') g)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is right distributive over addition  -/
RightDistribClass.right_distrib : ∀ {R : Type u_1} {inst : Mul R} {inst_1 : Add R} [self : RightDistribClass R] (a b c : R), (a + b) * c = a * c + b * c
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {s : ι → Set Ω}, ProbabilityTheory.Kernel.iIndepSet s κ 0
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.tuple.injEq : ∀ (args args_1 : List Lean.Parser.Tactic.MRefinePat),
  (Lean.Parser.Tactic.MRefinePat.tuple args = Lean.Parser.Tactic.MRefinePat.tuple args_1) = (args = args_1)
-- Mathlib.Algebra.Order.Monoid.PNat
/-- `ℕ+` is equivalent to `nonZeroDivisors ℕ` in terms of order and multiplication.  -/
PNat.equivNonZeroDivisorsNat : ℕ+ ≃*o ↥(nonZeroDivisors ℕ)
-- Lean.Environment
Lean.Environment.isConstructor : Lean.Environment → Lean.Name → Bool
-- Lean.PrettyPrinter.Delaborator.Basic
/-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
its semantics. While the elaborator emits `InfoTree`s, here we have no real text location tree
to traverse, so we use a flattened map.  -/
Lean.PrettyPrinter.Delaborator.State.infos : Lean.PrettyPrinter.Delaborator.State → Lean.SubExpr.PosMap Lean.Elab.Info
-- Mathlib.FieldTheory.SplittingField.Construction
/-- Non-computably choose an irreducible factor from a polynomial.  -/
Polynomial.factor : {K : Type v} → [inst : Field K] → Polynomial K → Polynomial K
-- Mathlib.Control.Functor.Multivariate
/-- Any type function that is (extensionally) equivalent to a functor, is itself a functor  -/
MvFunctor.ofEquiv : {n : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {F' : TypeVec.{u} n → Type u_2} → [MvFunctor F'] → ((α : TypeVec.{u} n) → F α ≃ F' α) → MvFunctor F
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedLeanDiagnosticTag.default : Lean.Lsp.LeanDiagnosticTag
-- Mathlib.Analysis.SumIntegralComparisons
MonotoneOn.sum_le_integral_Ico : ∀ {a b : ℕ} {f : ℝ → ℝ}, a ≤ b → MonotoneOn f (Set.Icc ↑a ↑b) → ∑ x ∈ Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x
-- Lean.CoreM
Lean.Core.Context.currNamespace : Lean.Core.Context → Lean.Name
-- Lean.Meta.Closure
Lean.Meta.Closure.pushFVarArg : Lean.Expr → Lean.Meta.Closure.ClosureM Unit
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.nndist_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P),
  nndist (f x) (f y) = nndist x y
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking for unused arguments. We skip all declarations that contain `sorry` in
their value, and allow arguments starting with `_` to be unused.  -/
Batteries.Tactic.Lint.unusedArguments : Batteries.Tactic.Lint.Linter
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.isOrderedAdd : Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Init.Data.Int.DivMod.Lemmas
Int.neg_fdiv : ∀ {a b : ℤ}, (-a).fdiv b = -a.fdiv b - if b = 0 ∨ b ∣ a then 0 else 1
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- `gramSchmidt` preserves span of vectors.  -/
InnerProductSpace.span_gramSchmidt : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E),
  Submodule.span 𝕜 (Set.range (InnerProductSpace.gramSchmidt 𝕜 f)) = Submodule.span 𝕜 (Set.range f)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_fin_bijective : ∀ (R : Type u_3) [inst : CommRing R] (n : ℕ), Function.Bijective ⇑(MvPolynomial.esymmAlgHom (Fin n) R n)
-- Std.Data.Internal.List.Associative
Std.Internal.List.alterKey_append_of_containsKey_right_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
  {l l' : List ((a : α) × β a)},
  Std.Internal.List.containsKey a l' = false →
    Std.Internal.List.alterKey a f (l ++ l') = Std.Internal.List.alterKey a f l ++ l'
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
/-- The converse of `type_equalizer_of_unique`.  -/
CategoryTheory.Limits.Types.unique_of_type_equalizer : ∀ {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h)
  (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) (y : Y),
  (CategoryTheory.ConcreteCategory.hom g) y = (CategoryTheory.ConcreteCategory.hom h) y →
    ∃! x, (CategoryTheory.ConcreteCategory.hom f) x = y
-- Mathlib.RepresentationTheory.Coinvariants
/-- The adjunction between the functor sending a representation to its coinvariants and the functor
equipping a module with the trivial representation.  -/
Rep.coinvariantsAdjunction : (k : Type u) →
  (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → Rep.coinvariantsFunctor k G ⊣ Rep.trivialFunctor k G
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomainLinearMap_comp : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N) (g : N → O),
  MonoidAlgebra.mapDomainLinearMap R S (g ∘ f) =
    MonoidAlgebra.mapDomainLinearMap R S g ∘ₗ MonoidAlgebra.mapDomainLinearMap R S f
-- Init.Data.Int.Lemmas
Int.negSucc_add_negSucc : ∀ (m n : ℕ), Int.negSucc m + Int.negSucc n = Int.negSucc (m + n).succ
-- Batteries.CodeAction.Attr
Batteries.CodeAction.mkTacticCodeAction.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Batteries.CodeAction.TacticCodeAction
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.lt_iff : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β},
  RightOrdContinuous f → Function.Injective f → ∀ {x y : α}, f y < f x ↔ y < x
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.coe_neg : ∀ {G : Type u_1} [inst : AddCommGroup G] (a : G), ↑(-a) = -↑a
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBot_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (β : LieModule.Weight R L M),
  LieModule.chainBot 0 β = β
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.subtype_injective : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), Function.Injective ⇑s.subtype
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousConstSMul.toMeasurableConstSMul : ∀ {M : Type u_7} {α : Type u_8} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α]
  [inst_3 : SMul M α] [ContinuousConstSMul M α], MeasurableConstSMul M α
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_lt_zero : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0}, ↑q < 0 ↔ q < 0
-- Mathlib.Topology.Constructions
/-- **Alias** of `Pi.continuous_domRestrict₂`. -/
Pi.continuous_restrict₂ : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {s t : Set ι} (hst : s ⊆ t),
  Continuous (Set.domRestrict₂ hst)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_id : ∀ {G : Type u_1} [inst : Add G] {a : G}, ⇑AddConstMap.id = id
-- Mathlib.Algebra.Ring.Opposite
/-- A non-unital ring hom `R →ₙ+* S` can equivalently be viewed as a non-unital ring hom
`Rᵐᵒᵖ →+* Sᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
NonUnitalRingHom.op : {R : Type u_2} →
  {S : Type u_3} →
    [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadMap_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {f : {β : Type u} → m β → m β} {x : m α}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps], (Std.Do.wp (monadMap f x)).apply Q = (Std.Do.wp (f x)).apply Q
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (T : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj T (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.η F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.ε F)) h) =
    h
-- Mathlib.Algebra.Group.Basic
zsmul_zero_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), n • (0 - a) = 0 - n • a
-- Mathlib.Analysis.Complex.IsIntegral
Complex.isIntegral_int_I : IsIntegral ℤ Complex.I
-- Mathlib.Order.Hom.Basic
OrderIso.arrowCongr_symm_apply : ∀ {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : γ →o δ),
  (RelIso.symm (f.arrowCongr g)) p = (↑g.symm).comp (p.comp ↑f)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.mk.sizeOf_spec : ∀ (paramNamePrefix : Lean.Name) (alreadyUsedPred : Lean.Name → Bool) (except : Lean.LMVarId → Bool),
  sizeOf { paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred, except := except } =
    1 + sizeOf paramNamePrefix
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_ne_top : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I ≠ ⊤ → ∀ [I.FiniteHeight], I.height ≠ ⊤
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R), Polynomial.dickson k a 0 = 3 - ↑k
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_lt : ∀ {a b : UInt8}, a.toUInt16 < b.toUInt16 ↔ a < b
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.mem_vonNeumann_of_subset : ∀ {o : Ordinal.{u}} {x y : ZFSet.{u}}, x ⊆ y → y ∈ ZFSet.vonNeumann o → x ∈ ZFSet.vonNeumann o
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.containsThenInsert.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → t.containsThenInsert a b = t_1.containsThenInsert a_1 b_1
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_inv_toFunctor_map_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y)
  (X_1 : C) (Y_1 : D), ((CategoryTheory.curryingIso.inv.toFunctor.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of an integrable function is greater than its mean.  -/
MeasureTheory.exists_average_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  μ ≠ 0 → MeasureTheory.Integrable f μ → ∃ x, ⨍ (a : α), f a ∂μ ≤ f x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X : ∀ {R : Type u} [inst : Semiring R] {k : ℕ}, 1 < k → (⇑Polynomial.derivative)^[k] Polynomial.X = 0
-- Mathlib.Algebra.Group.NatPowAssoc
/-- Exponent one is identity.  -/
NatPowAssoc.npow_one : ∀ {M : Type u_2} {inst : MulOneClass M} {inst_1 : Pow M ℕ} [self : NatPowAssoc M] (x : M), x ^ 1 = x
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.finprod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {F : ι → 𝕜 → 𝕜'},
  (∀ (σ : ι), Meromorphic (F σ)) → Meromorphic (∏ᶠ (σ : ι), F σ)
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of `sup_sdiff_self`. -/
sup_sdiff_self_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊔ b \ a = a ⊔ b
-- Mathlib.Topology.Instances.ENat
ENat.mem_nhds_iff : ∀ {x : ℕ∞} {s : Set ℕ∞}, x ≠ ⊤ → (s ∈ nhds x ↔ x ∈ s)
-- Mathlib.Topology.ContinuousOn
ContinuousOn.iterate : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → α} {s : Set α},
  ContinuousOn f s → Set.MapsTo f s s → ∀ (n : ℕ), ContinuousOn f^[n] s
-- Mathlib.Order.Partition.Basic
Partition.sSupIndep : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P : Partition s), sSupIndep ↑P
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_sub_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α}, (s - t).card ≤ s.card * t.card
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `HasMFDerivWithinAt` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabHasMFDerivAt : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Parser.Types
Lean.Parser.TokenTable : Type
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `R` is of characteristic `p` and `p ∣ n`, then
`cyclotomic (n * p) R = (cyclotomic n R) ^ p`.  -/
Polynomial.cyclotomic_mul_prime_dvd_eq_pow : ∀ (R : Type u_1) {p n : ℕ} [hp : Fact (Nat.Prime p)] [inst : Ring R] [CharP R p],
  p ∣ n → Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ p
-- Mathlib.Order.Category.DistLat
/-- Typecheck a `LatticeHom` as a morphism in `DistLat`.  -/
DistLat.ofHom : {X Y : Type u} →
  [inst : DistribLattice X] → [inst_1 : DistribLattice Y] → LatticeHom X Y → (DistLat.of X ⟶ DistLat.of Y)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.PseudoCore.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.OplaxFunctor B C}
  (mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_hom :
    autoParam (∀ {a : B}, (mapIdIso a).hom = F.mapId a) CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom._autoParam)
  (mapCompIso_hom :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).hom = F.mapComp f g)
      CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom._autoParam)
  (mapIdIso_1 : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso_1 :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_hom_1 :
    autoParam (∀ {a : B}, (mapIdIso_1 a).hom = F.mapId a)
      CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom._autoParam)
  (mapCompIso_hom_1 :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso_1 f g).hom = F.mapComp f g)
      CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom._autoParam),
  ({ mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_hom := mapIdIso_hom, mapCompIso_hom := mapCompIso_hom } =
      { mapIdIso := mapIdIso_1, mapCompIso := mapCompIso_1, mapIdIso_hom := mapIdIso_hom_1,
        mapCompIso_hom := mapCompIso_hom_1 }) =
    (mapIdIso = mapIdIso_1 ∧ mapCompIso = mapCompIso_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensor_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The predicate on products which we prove picks out a basis of `LocallyConstant C ℤ`. We call such a
product "good".
 -/
Profinite.NobelingProof.Products.isGood : {I : Type u} → Set (I → Bool) → [inst : LinearOrder I] → Profinite.NobelingProof.Products I → Prop
-- Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty : ∀ (X : AlgebraicGeometry.Scheme) (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)] [IsEmpty ↥X],
  CategoryTheory.Limits.IsZero (X.ellAdicSheaf ℓ)
-- Lean.Util.NumApps
Lean.Expr.NumApps.State : Type
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_range_map_lift : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A)
  (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)),
  Submodule.map ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap (CliffordAlgebra.ι Q).range = f.range
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toGlobalRuleFilters : Aesop.Frontend.RuleExpr → Lean.Elab.TermElabM (Array (Aesop.RuleSetNameFilter × Aesop.RuleFilter))
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_withDensity_eq_integral_smul : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → NNReal},
  Measurable f → ∀ (g : X → E), (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ
-- Lean.Compiler.IR.Basic
Lean.IR.Param.mk.sizeOf_spec : ∀ (x : Lean.IR.VarId) (borrow : Bool) (ty : Lean.IR.IRType),
  sizeOf { x := x, borrow := borrow, ty := ty } = 1 + sizeOf x + sizeOf borrow + sizeOf ty
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀ : (α : Type u) → (α → Type v) → Type (max 0 u v)
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3) →
        (r : Std.DTreeMap.Internal.Impl α β) →
          (h : r.size > Std.DTreeMap.Internal.delta * l.size) →
            ((h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
                motive Std.DTreeMap.Internal.Impl.leaf h) →
              ((size : ℕ) →
                  (rk : α) →
                    (rv : β rk) →
                      (rl rr : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size >
                              Std.DTreeMap.Internal.delta * l.size) →
                          motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h) →
                motive r h