mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Basic
NNReal.isEmbedding_coe : Topology.IsEmbedding NNReal.toReal
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_inj : ∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, hs.toFinset = ht.toFinset ↔ s = t
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_ofNat : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : NatCast M] (n : ℕ) [inst_1 : n.AtLeastTwo],
  ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.factor.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p p' : Submodule R M}
  (H : p ≤ p'), Submodule.factor H = Submodule.factor H
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.commonSection.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f f_1 : A ⟶ B) (e_f : f = f_1) (g g_1 : A ⟶ B)
  (e_g : g = g_1) [inst_1 : CategoryTheory.IsReflexivePair f g],
  CategoryTheory.commonSection f g = CategoryTheory.commonSection f_1 g_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.proj_apply : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12}
  [inst_1 : (i : ι) → AddCommGroup (V i)] [inst_2 : (i : ι) → Module k (V i)] [inst_3 : (i : ι) → AddTorsor (V i) (P i)]
  (i : ι) (f : (i : ι) → P i), (AffineMap.proj i) f = f i
-- Mathlib.Order.Irreducible
IsMax.not_infPrime : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, IsMax a → ¬InfPrime a
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Hom.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.OplaxTrans.Hom η θ},
  x.as = y.as → x = y
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Consider two angles `∡ p₁ p₂ p₃` and `∡ p₄ p₅ p₆` defined by triples of points. Each is the
angle between two lines; if the pair `p₁ p₂` and `p₄ p₅` of corresponding lines is parallel, and
also the pair `p₃ p₂` and `p₆ p₅` of corresponding lines is parallel, and also (roughly) the third
pair of lines `p₁ p₃` and `p₄ p₆` are the same line, then the two angles are equal.  This is a
stronger version of `two_zsmul_oangle_of_parallel`, which shows that the two angles are equal mod
`π` in the absence of the condition on the third pair of lines.  -/
EuclideanGeometry.oangle_eq_of_parallel : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  p₂ ∉ line[ℝ, p₁, p₃] →
    p₄ ∈ line[ℝ, p₁, p₃] →
      p₆ ∈ line[ℝ, p₁, p₃] →
        line[ℝ, p₁, p₂].Parallel line[ℝ, p₄, p₅] →
          line[ℝ, p₃, p₂].Parallel line[ℝ, p₆, p₅] →
            EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.of_small_tripling : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} [inst_1 : DecidableEq G] {A : Finset G},
  1 ∈ A → A⁻¹ = A → ↑(A ^ 3).card ≤ K * ↑A.card → IsApproximateSubgroup (K ^ 3) (↑A ^ 2)
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = CategoryTheory.Limits.coprod.inr
-- Mathlib.RingTheory.WittVector.Identities
WittVector.coeff_p_pow_eq_zero : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] {i j : ℕ},
  j ≠ i → (↑p ^ i).coeff j = 0
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
Lean.Meta.Grind.Arith.normFieldExpr? : Lean.Expr → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Lean.DocString.Types
/-- Block-level content in a document.
 -/
Lean.Doc.Block : Type u → Type v → Type (max u v)
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.tacticWf_trivial : Lean.ParserDescr
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- If `P : ProjectiveResolution X` and `F` is an additive functor, this is
the canonical morphism from the opcycles in degree `0` of
`(F.mapHomologicalComplex _).obj P.complex` to `F.obj X`.  -/
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Abelian D] →
            {X : C} →
              (P : CategoryTheory.ProjectiveResolution X) →
                (F : CategoryTheory.Functor C D) →
                  [inst_4 : F.Additive] →
                    ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).opcycles 0 ⟶ F.obj X
-- Mathlib.RingTheory.Grassmannian
/-- The Grassmannian functor sends an `R`-algebra `A` to `G(k, A ⊗[R] M; A)`.  -/
Module.Grassmannian.functor : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} → [inst_1 : AddCommGroup M] → [Module R M] → ℕ → CategoryTheory.Functor (CommAlgCat R) (Type (max v w))
-- Mathlib.Algebra.Module.Equiv.Basic
/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives an
additive isomorphism between the two function spaces.

See also `LinearEquiv.arrowCongr` for the linear version of this isomorphism.  -/
LinearEquiv.arrowCongrAddEquiv : {R₁ : Type u_9} →
  {R₂ : Type u_10} →
    {R₁' : Type u_11} →
      {R₂' : Type u_12} →
        {M₁ : Type u_13} →
          {M₂ : Type u_14} →
            {M₁' : Type u_15} →
              {M₂' : Type u_16} →
                [inst : Semiring R₁] →
                  [inst_1 : Semiring R₂] →
                    [inst_2 : Semiring R₁'] →
                      [inst_3 : Semiring R₂'] →
                        [inst_4 : AddCommMonoid M₁] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : AddCommMonoid M₁'] →
                              [inst_7 : AddCommMonoid M₂'] →
                                [inst_8 : Module R₁ M₁] →
                                  [inst_9 : Module R₂ M₂] →
                                    [inst_10 : Module R₁' M₁'] →
                                      [inst_11 : Module R₂' M₂'] →
                                        {σ₁₂ : R₁ →+* R₂} →
                                          {σ₂₁ : R₂ →+* R₁} →
                                            {σ₁'₂' : R₁' →+* R₂'} →
                                              {σ₂'₁' : R₂' →+* R₁'} →
                                                {σ₁₁' : R₁ →+* R₁'} →
                                                  {σ₂₂' : R₂ →+* R₂'} →
                                                    {σ₂₁' : R₂ →+* R₁'} →
                                                      {σ₁₂' : R₁ →+* R₂'} →
                                                        [inst_12 : RingHomInvPair σ₁₂ σ₂₁] →
                                                          [inst_13 : RingHomInvPair σ₂₁ σ₁₂] →
                                                            [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                                                              [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                                                                [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] →
                                                                  [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] →
                                                                    [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] →
                                                                      [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] →
                                                                        (M₁ ≃ₛₗ[σ₁₂] M₂) →
                                                                          (M₁' ≃ₛₗ[σ₁'₂'] M₂') →
                                                                            (M₁ →ₛₗ[σ₁₁'] M₁') ≃+ (M₂ →ₛₗ[σ₂₂'] M₂')
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
IsCovariantDerivativeOn.torsion.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 2 M] [inst_7 : CompleteSpace E]
  {cov cov_1 : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} (e_cov : cov = cov_1)
  [inst_8 : CompleteSpace 𝕜] [inst_9 : FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) (x : M),
  hcov.torsion x = ⋯.torsion x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_inl_inr_codiag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
      (CategoryTheory.Limits.codiag (X ⨿ Y)) =
    CategoryTheory.CategoryStruct.id (X ⨿ Y)
-- Lean.Meta.MkIffOfInductiveProp
/-- Converts an inductive constructor `c` into a `Shape` that will be used later in
while proving the iff theorem, and a proposition representing the constructor.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.constrToProp : List Lean.Level → List Lean.Expr → List Lean.Expr → Lean.Name → Lean.MetaM (Lean.Meta.Shape✝ × Lean.Expr)
-- Init.Data.Format.Basic
Std.Format.text.injEq : ∀ (a a_1 : String), (Std.Format.text a = Std.Format.text a_1) = (a = a_1)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpecIso_obj_hom : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map U.topIso.inv))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (↑U).toSpecΓ) U.topIso.hom)
-- Mathlib.Analysis.Calculus.Rademacher
LipschitzWith.ae_lineDifferentiableAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f → ∀ (v : E), ∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i))
  [CategoryTheory.Presheaf.IsLocallySurjective AlgebraicGeometry.Scheme.zariskiTopology
      (CategoryTheory.Limits.Sigma.desc f)],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf)
-- Mathlib.Order.Lattice
Prod.instSemilatticeSup : (α : Type u) → (β : Type v) → [SemilatticeSup α] → [SemilatticeSup β] → SemilatticeSup (α × β)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (n₁ n₂ : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₁)
      ((CochainComplex.mappingCone φ).d n₁ n₂) =
    CategoryTheory.CategoryStruct.comp (G.d n₁ n₂) ((CochainComplex.mappingCone.inr φ).f n₂)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.antidiagonal.snd_le : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedAdd A]
  [inst_3 : Finset.HasAntidiagonal A] {n : A} {kl : A × A}, kl ∈ Finset.HasAntidiagonal.antidiagonal n → kl.2 ≤ n
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impTo.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Category.TopCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
TopCat.Hom.Simps.hom : (X Y : TopCat) → X.Hom Y → C(↑X, ↑Y)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, a ∉ t → Std.DTreeMap.Const.getD t a fallback = fallback
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.mk.inj : ∀ {α : Type u_2} {measureOf : Set α → ENNReal} {empty : measureOf ∅ = 0}
  {mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂}
  {iUnion_nat :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i)}
  {measureOf_1 : Set α → ENNReal} {empty_1 : measureOf_1 ∅ = 0}
  {mono_1 : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf_1 s₁ ≤ measureOf_1 s₂}
  {iUnion_nat_1 :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf_1 (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf_1 (s i)},
  { measureOf := measureOf, empty := empty, mono := mono, iUnion_nat := iUnion_nat } =
      { measureOf := measureOf_1, empty := empty_1, mono := mono_1, iUnion_nat := iUnion_nat_1 } →
    measureOf = measureOf_1
-- Init.Data.Array.Erase
Array.eraseIdx_eq_eraseIdxIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs.eraseIdx i h = xs.eraseIdxIfInBounds i
-- Init.Data.Array.Nat
Array.mul_length_le_sum_of_min?_eq_some_nat : ∀ {x : ℕ} {xs : Array ℕ}, xs.min? = some x → x * xs.size ≤ xs.sum
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π_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.HasColimit F] (j : J) {Z : Cᵒᵖ}
  (h : F.rightOp.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.rightOp j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.op j)).op h
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring.sizeOf_spec : ∀ (id : ℕ), sizeOf (Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring id) = 1 + sizeOf id
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_add`. -/
ContinuousLinearMap.coe_add : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : ContinuousAdd M₂]
  (f g : M₁ →SL[σ₁₂] M₂), ↑(f + g) = ↑f + ↑g
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.comp_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) (a : A), (f.comp g) a = f (g a)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {V W : QuadraticModuleCat R} {x y : V.Hom W}, x = y ↔ x.toIsometry' = y.toIsometry'
-- Mathlib.Order.Closure
/-- The set of closed elements for `c` is exactly its range.  -/
ClosureOperator.setOfPred_isClosed_eq_range_closure : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α}, {x | c.IsClosed x} = Set.range ⇑c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.DTreeMap.Raw.ofList l cmp).getKey! k' = k
-- Mathlib.Order.SupClosed
InfClosed.finsetInf_mem : ∀ {α : Type u_3} [inst : SemilatticeInf α] {ι : Type u_5} {f : ι → α} {s : Set α} {t : Finset ι} [inst_1 : OrderTop α],
  InfClosed s → t.Nonempty → (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pi_rpow_one : ∀ {α : Type u_1} (f : α → ℝ), f ^ 1 = f
-- Lean.Elab.InfoTree.Main
Lean.Elab.InfoTree.format : Lean.Elab.InfoTree → optParam (Option Lean.Elab.ContextInfo) none → IO Std.Format
-- Mathlib.RingTheory.Localization.BaseChange
Localization.tensorRightAlgEquiv_apply_one_tmul : ∀ {R : Type u_10} [inst : CommRing R] (M : Submonoid R) {S : Type u_12} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (x : S),
  (Localization.tensorRightAlgEquiv M S) (1 ⊗ₜ[R] x) = (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) x
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.forget_additive : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive], T.forget.Additive
-- Mathlib.Order.CountableSupClosed
/-- If a set is closed under binary suprema, then its countable infimum closure is also closed under
binary suprema.  -/
SupClosed.countableInfClosure : ∀ {α : Type u_2} {s : Set α} [inst : Order.Coframe α], SupClosed s → SupClosed (countableInfClosure s)
-- Init.Data.List.TakeDrop
List.takeWhile.eq_1 : ∀ {α : Type u} (p : α → Bool), List.takeWhile p [] = []
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜},
  HasFPowerSeriesAt f p x → deriv f x = (p 1) fun x => 1
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.infinitePlace_complexConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (w : NumberField.InfinitePlace K) (x : K),
  w ((NumberField.IsCMField.complexConj K) x) = w x
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool true → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `MeromorphicNFOn.zpow`

---

Integer powers of meromorphic functions in normal form are in normal form.
 -/
MeromorphicNFOn.fun_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {n : ℤ} {U : Set 𝕜},
  MeromorphicNFOn f U → MeromorphicNFOn (fun i => f i ^ n) U
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q),
  (CochainComplex.HomComplex.Cochain.toSingleEquiv h) (CochainComplex.HomComplex.Cochain.toSingleMk f h) = f
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Two equivalent open partial homeomorphisms are equal when the source and target are `univ`.  -/
OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, Set.EqOn (↑e) (↑e') (e.source ∩ e'.source) → e.restr e'.source ≈ e'.restr e.source
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.mk : (toGlueData : CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace) →
  (∀ (i j : toGlueData.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (toGlueData.f i j)) →
    AlgebraicGeometry.LocallyRingedSpace.GlueData
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.swap.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Mathlib.Analysis.CStarAlgebra.Basic
IsSelfAdjoint.norm_mul_self : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E},
  IsSelfAdjoint x → ‖x * x‖ = ‖x‖ ^ 2
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_add_nonpos : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atBot → (∀ (x : α), g x ≤ 0) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Std.Time.Format.Modifier
/-- IANA time zone ID (2 letters, `VV`, e.g., "America/Los_Angeles").
 -/
Std.Time.ZoneId.short : Std.Time.ZoneId
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- The unitary group in a C⋆-algebra is locally path connected.  -/
Unitary.instLocallyPathConnectedSpace : ∀ {A : Type u_1} [inst : CStarAlgebra A], LocallyPathConnectedSpace ↥(unitary A)
-- Mathlib.Order.SymmDiff
symmDiff_eq_bot : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, symmDiff a b = ⊥ ↔ a = b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaMon.Faithful
-- Batteries.Data.AssocList
Batteries.AssocList.foldl_eq : ∀ {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (l : Batteries.AssocList α β),
  Batteries.AssocList.foldl f init l =
    List.foldl
      (fun d x =>
        match x with
        | (a, b) => f d a b)
      init l.toList
-- Lean.Attributes
Lean.AttributeImpl.mk.sizeOf_spec : ∀ (toAttributeImplCore : Lean.AttributeImplCore) (add : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit)
  (erase : Lean.Name → Lean.AttrM Unit),
  sizeOf { toAttributeImplCore := toAttributeImplCore, add := add, erase := erase } = 1 + sizeOf toAttributeImplCore
-- Mathlib.Topology.Bases
TopologicalSpace.empty_notMem_countableBasis : ∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α], ∅ ∉ TopologicalSpace.countableBasis α
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_neg : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℤ), preNormEDS b c d (-n) = -preNormEDS b c d n
-- Lean.Meta.Match.NamedPatterns
Lean.Meta.Match.unfoldNamedPattern : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.inverse.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f), f.inverse g h₁ = { toFun := g, map_one' := ⋯ }
-- Mathlib.Topology.Order.Basic
pi_Icc_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' b' x' : ι → α}, (∀ (i : ι), a' i < x' i) → (∀ (i : ι), x' i < b' i) → Set.Icc a' b' ∈ nhds x'
-- Init.Data.Vector.Zip
Vector.zip_eq_zipWith : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n}, as.zip bs = Vector.zipWith Prod.mk as bs
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_natCast : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), ↑↑n = ↑n
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.EvalExpr.mk : {α : Type} → (Lean.Expr → Lean.MetaM α) → Option Lean.Expr → Lean.Elab.ConfigEval.EvalExpr α