mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- If `D` is a reflective subcategory, the property of being an exponential ideal is equivalent to
the presence of a natural isomorphism `i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A`, that is:
`(A ⟹ iB) ≅ i L (A ⟹ iB)`, naturally in `B`.
The converse is given in `ExponentialIdeal.mk_of_iso`.
 -/
CategoryTheory.exponentialIdealReflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (i : CategoryTheory.Functor D C) →
          [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
            [inst_3 : CategoryTheory.MonoidalClosed C] →
              (A : C) →
                [inst_4 : CategoryTheory.Reflective i] →
                  [CategoryTheory.ExponentialIdeal i] →
                    i.comp ((CategoryTheory.ihom A).comp ((CategoryTheory.reflector i).comp i)) ≅
                      i.comp (CategoryTheory.ihom A)
-- Mathlib.Combinatorics.Quiver.Basic
/-- The opposite of an arrow in `V`.  -/
Quiver.Hom.op : {V : Type u_1} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) → (Opposite.op Y ⟶ Opposite.op X)
-- Aesop.Rule.Name
Aesop.PhaseName : Type
-- Mathlib.Data.Multiset.AddSub
Multiset.cons_sub_of_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {s t : Multiset α}, t ≤ s → a ::ₘ s - t = a ::ₘ (s - t)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
the size of `t` divides the size of `s * t`.  -/
Finset.card_dvd_card_mul_right : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
  ((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s * t).card
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mkActionCore.go.eq_def : ∀ (exts : Array (Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.SolverExtensionState)) (i : ℕ)
  (acc : Lean.Meta.Grind.Action),
  Lean.Meta.Grind.Solvers.mkActionCore.go✝ exts i acc =
    if h : i < exts.size then Lean.Meta.Grind.Solvers.mkActionCore.go✝ exts (i + 1) (acc.andAlso exts[i].action)
    else acc
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- If the pre-`0`-hypercover `E` has pairwise pullbacks, then the multifork associated to the
full saturated pre-`1`-hypercover is exact if and only if the minimal one given by taking
the pairwise pullbacks is exact.  -/
CategoryTheory.PreZeroHypercover.isLimitSaturateEquivOfHasPullbacks : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
        {S : C} →
          (E : CategoryTheory.PreZeroHypercover S) →
            [inst_2 : E.HasPullbacks] →
              (F : CategoryTheory.Functor Cᵒᵖ A) →
                CategoryTheory.Limits.IsLimit (E.saturate.multifork F) ≃
                  CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)
-- Mathlib.Analysis.SpecificLimits.Basic
summable_geometric_two_encode : ∀ {ι : Type u_4} [inst : Encodable ι], Summable fun i => (1 / 2) ^ Encodable.encode i
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.mem_normalizedFactors_iff : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDedekindDomain A] {p I : Ideal A},
  I ≠ ⊥ → (p ∈ UniqueFactorizationMonoid.normalizedFactors I ↔ p.IsPrime ∧ I ≤ p)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.instTop : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → Top (I.Filtration M)
-- Mathlib.Analysis.Fourier.AddCircle
/-- Under the isometric isomorphism `fourierBasis` from `Lp ℂ 2 haarAddCircle` to `ℓ²(ℤ, ℂ)`, the
`i`-th coefficient is `fourierCoeff f i`, i.e., the integral over `AddCircle T` of
`fun t => fourier (-i) t * f t` with respect to the Haar measure of total mass 1.  -/
fourierBasis_repr : ∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (i : ℤ),
  ↑(fourierBasis.repr f) i = fourierCoeff (↑↑f) i
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expCoeff.eq_1 : ∀ (n : ℕ), WeierstrassCurve.expCoeff✝ n = if Even n then ↑n / 2 else ↑n
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.upper : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), IsUpperSet ↑s
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_fun_zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜},
  DifferentiableAt 𝕜 f x → ∀ (n : ℤ), logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) {Z : CochainComplex C ℤ}
  (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.cm5b.i f)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.cm5b.p K L) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Data.Complex.Basic
Complex.mem_reProdIm : ∀ {z : ℂ} {s t : Set ℝ}, z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t
-- Mathlib.Topology.Order.Basic
dense_of_exists_between : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α},
  (∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Set.Ioo a b) → Dense s
-- Mathlib.Order.Filter.Map
Filter.map_le_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β},
  Function.Injective m → (Filter.map m f ≤ Filter.map m g ↔ f ≤ g)
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Trivialization.continuousLinearMap.congr_simp : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ e₁_1 : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) (e_e₂ : e₂ = e₂_1)
  [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜₁ F₁ E₁]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜₂ F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)]
  [inst_21 : RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂],
  Bundle.Trivialization.continuousLinearMap σ e₁ e₂ = Bundle.Trivialization.continuousLinearMap σ e₁_1 e₂_1
-- Mathlib.NumberTheory.MahlerMeasure
RingHom.IsIntegralElem.eq_1 : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] (f : R →+* A) (x : A),
  f.IsIntegralElem x = ∃ p, p.Monic ∧ Polynomial.eval₂ f x p = 0
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
associatedPrimes.eq_singleton_of_isPrimary : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [IsNoetherianRing R],
  I.IsPrimary → associatedPrimes R (R ⧸ I) = {I.radical}
-- Mathlib.Topology.Algebra.Group.Basic
topologicalAddGroup_induced : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {F : Type u_1}
  [inst_3 : AddGroup H] [inst_4 : FunLike F H G] [AddMonoidHomClass F H G] (f : F), IsTopologicalAddGroup H
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- Given a family of kernels `κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))`, and the
trajectory up to time `a` we can construct an additive content over cylinders. It corresponds
to composing the kernels, starting at time `a + 1`.  -/
ProbabilityTheory.Kernel.trajContent : {X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] →
    (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] →
        {a : ℕ} →
          ((i : ↥(Finset.Iic a)) → X ↑i) → MeasureTheory.AddContent ENNReal (MeasureTheory.measurableCylinders X)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leSubmodule_monotone : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Monotone v.leSubmodule
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.neg_mem_iff : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x : M}, -x ∈ p ↔ x ∈ p
-- Batteries.Util.LibraryNote
/-- Environment extension supporting `library_note`.  -/
Batteries.Util.LibraryNote.libraryNoteExt : Lean.SimplePersistentEnvExtension Batteries.Util.LibraryNote.LibraryNoteEntry
  (Array Batteries.Util.LibraryNote.LibraryNoteEntry)
-- Mathlib.Order.Completion
DedekindCut.principal_lt_principal : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, DedekindCut.principal a < DedekindCut.principal b ↔ a < b
-- Init.Data.SInt.Lemmas
Int32.toInt_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toInt = b.toInt
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (x : CategoryTheory.LocallyDiscrete Cᵒᵖ)
  (X : CategoryTheory.Sheaf (J.over (Opposite.unop x.as)) A) (X_1 : (CategoryTheory.Over (Opposite.unop x.as))ᵒᵖ),
  (((J.pseudofunctorOver A).mapId x).inv.toNatTrans.app X).hom.app X_1 =
    X.obj.map ((CategoryTheory.Over.mapId (Opposite.unop x.as)).hom.app (Opposite.unop X_1)).op
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.toSubmodule : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  {𝒜 : ιA → σA} →
                    {ℳ : ιM → σM} →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [inst_7 : GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [inst_11 : DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] →
                                          [inst_13 : SetLike.GradedSMul 𝒜 ℳ] → HomogeneousSubmodule 𝒜 ℳ → Submodule A M
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorSet.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], addCommutatorSet G = {g | ∃ g₁ g₂, ⁅g₁, g₂⁆ = g}
-- Mathlib.Order.Basic
instDenselyOrderedProd : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [DenselyOrdered α] [DenselyOrdered β],
  DenselyOrdered (α × β)
-- Mathlib.CategoryTheory.Sites.Sheaf
_private.Mathlib.CategoryTheory.Sites.Sheaf.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.R) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.right i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_2 i
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_add : ∀ {R : Type u} {a b : R} [inst : Semiring R], Polynomial.C (a + b) = Polynomial.C a + Polynomial.C b
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ioo_right : ∀ {α : Type v} [inst : Preorder α] [NoMaxOrder α] (a : α), ⋃ b, Set.Ioo a b = Set.Ioi a
-- Lean.Meta.ForEachExpr
/-- Similar to `Expr.forEach`, but creates free variables whenever going inside of a binder.  -/
Lean.Meta.forEachExpr : {m : Type → Type} →
  [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadControlT Lean.MetaM m] → Lean.Expr → (Lean.Expr → m Unit) → m Unit
-- Mathlib.Order.SetNotation
/-- Indexed supremum  -/
iSup : {α : Type u} → {ι : Sort v} → [SupSet α] → (ι → α) → α
-- Mathlib.NumberTheory.Rayleigh
/-- Let `0 < r ∈ ℝ` and `j ∈ ℤ`. Then either `j ∈ B'_r` or `B'_r` jumps over `j`.  -/
_private.Mathlib.NumberTheory.Rayleigh.0.Beatty.hit_or_miss' : ∀ {r : ℝ} {j : ℤ}, r > 0 → j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {m : ℕ},
  ContDiffWithinAt 𝕜 n f s x →
    ↑m < n → UniqueDiffOn 𝕜 (insert x s) → DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical equivalence between `Unitization R A` and `R × A`.  -/
Unitization.equiv : {R : Type u_1} → {A : Type u_2} → Unitization R A ≃ R × A
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.smulOfNeZero_symm_apply : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [inst_3 : ContinuousConstSMul G₀ α] {c : G₀} (hc : c ≠ 0), ⇑(Homeomorph.smulOfNeZero c hc).symm = fun x => c⁻¹ • x
-- Mathlib.Analysis.Analytic.Constructions
analyticOnNhd_inverse : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_7} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A], AnalyticOnNhd 𝕜 Ring.inverse {x | IsUnit x}
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- A finsupp `x : G × G →₀ A` satisfies the 2-boundary condition if there's a finsupp
`∑ aᵢ·(gᵢ, hᵢ, jᵢ) : G × G × G →₀ A` such that
`∑ (gᵢ⁻¹ • aᵢ)·(hᵢ, jᵢ) - aᵢ·(gᵢhᵢ, jᵢ) + aᵢ·(gᵢ, hᵢjᵢ) - aᵢ·(gᵢ, hᵢ) = x.`  -/
groupHomology.IsBoundary₂ : {G : Type u_1} → {A : Type u_2} → [Mul G] → [Inv G] → [inst : AddCommGroup A] → [SMul G A] → (G × G →₀ A) → Prop
-- Mathlib.Util.FormatTable
instInhabitedAlignment.default : Alignment
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgHom.liftEquiv_tmul : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [inst : DecidableEq ι]
  [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Semiring A] [inst_5 : Semiring B]
  [inst_6 : Algebra R A] [inst_7 : Algebra S B] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule S B}
  [inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] [inst_10 : Algebra R S] [inst_11 : Algebra R B]
  [inst_12 : IsScalarTower R S B] (f : 𝒜 →ₐᵍ[R] fun x => Submodule.restrictScalars R (ℬ x)) (r : S) (x : A),
  ((GradedAlgHom.liftEquiv 𝒜 ℬ) f) (r ⊗ₜ[R] x) = r • f x
-- Mathlib.Data.Nat.Factorial.NatCast
IsUnit.natCast_factorial_of_le : ∀ {A : Type u_1} [inst : Semiring A] {n : ℕ}, IsUnit ↑n.factorial → ∀ {m : ℕ}, m ≤ n → IsUnit ↑m.factorial
-- Lean.Environment
Lean.Kernel.Exception.funExpected.inj : ∀ {env : Lean.Kernel.Environment} {lctx : Lean.LocalContext} {expr : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {lctx_1 : Lean.LocalContext} {expr_1 : Lean.Expr},
  Lean.Kernel.Exception.funExpected env lctx expr = Lean.Kernel.Exception.funExpected env_1 lctx_1 expr_1 →
    env = env_1 ∧ lctx = lctx_1 ∧ expr = expr_1
-- Mathlib.Analysis.Real.Sqrt
Real.tendsto_sqrt_atTop : Filter.Tendsto (fun x => √x) Filter.atTop Filter.atTop
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_neg : ∀ {α : Type u_1} {M : Type u_8} {G : Type u_12} [inst : Zero M] [inst_1 : AddCommGroup G] {f : α →₀ M} {h : α → M → G},
  (f.sum fun a b => -h a b) = -f.sum h
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : Y.Opens)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.preimageIso f U).hom
      (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι
      (CategoryTheory.CategoryStruct.comp f h)
-- Lean.Data.Options
Lean.Option.Decl.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (defValue : α) (descr : String) (deprecation? : Option Lean.OptionDeprecation),
  sizeOf { defValue := defValue, descr := descr, deprecation? := deprecation? } =
    1 + sizeOf defValue + sizeOf descr + sizeOf deprecation?
-- Std.Time.Format.Modifier
/-- `E`: Day of week as text (e.g., Tue, Tuesday, T).
 -/
Std.Time.Modifier.E : Std.Time.Text → Std.Time.Modifier
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.punitCoprod.eq_1 : ∀ (M : Type u_1) [inst : AddMonoid M], AddEquiv.punitCoprod M = AddMonoid.Coprod.snd.toAddEquiv AddMonoid.Coprod.inr ⋯ ⋯
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.of.inj : ∀ {carrier : Type u} {str : SeminormedAddCommGroup carrier} {carrier_1 : Type u}
  {str_1 : SeminormedAddCommGroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.Raw.keys_inner : ∀ {α β : Type u} {m : Std.HashMap.Raw α β}, m.inner.keys = m.keys
-- Mathlib.Data.Seq.Computation
/-- `tail c` is the remainder of computation, either `c` if `c = pure a`
or `c'` if `c = think c'`.  -/
Computation.tail : {α : Type u} → Computation α → Computation α
-- Init.Control.Lawful.Instances
StateT.run_mk : ∀ {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] (x : σ → m (α × σ)) (s : σ), (StateT.mk x).run s = x s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.hom_ext_iff : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : CategoryTheory.SimplicialThickening J} {x y : i ⟶ j},
  x = y ↔ ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The chain rule.  -/
HasDerivAt.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F},
  HasDerivAt g₁ g₁' (h x) → HasDerivAt h h' x → HasDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_lt_ofNat : ∀ {m : ℕ∞} {n : ℕ} [inst : n.AtLeastTwo], ↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The chain rule.  -/
HasDerivAt.scomp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'},
  HasDerivAt g₁ g₁' y → HasDerivAt h h' x → y = h x → HasDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.smul.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  (I' : ModelWithCorners 𝕜 E' H') {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : Group G]
  [inst_12 : MulAction G M] (n : WithTop ℕ∞) [inst_13 : ContMDiffSMul I I' n G M] (g : G),
  Diffeomorph.smul I I' n g = { toEquiv := MulAction.toPerm g, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The limits of `F : J ⥤ C` and `G : J ⥤ C` are isomorphic,
if the functors are naturally isomorphic.
 -/
CategoryTheory.Limits.HasLimit.isoOfNatIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F G : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            [inst_3 : CategoryTheory.Limits.HasLimit G] →
              (F ≅ G) → (CategoryTheory.Limits.limit F ≅ CategoryTheory.Limits.limit G)
-- Batteries.Data.Float.Lemmas
Float.beq_self_eq_false_iff : ∀ {f : Float}, (f == f) = false ↔ f = Float.nan
-- Mathlib.Topology.Algebra.Module.Determinant
/-- The determinant of a continuous linear map, mainly as a convenience device to be able to
write `A.det` instead of `(A : M →ₗ[R] M).det`.  -/
ContinuousLinearMap.det : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → (M →L[R] M) → R
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAdd.continuous_add : ∀ {M : Type u_1} {inst : TopologicalSpace M} {inst_1 : Add M} [self : ContinuousAdd M], Continuous fun p => p.1 + p.2
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_map_ofDual`. -/
List.SortedGT.map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedGT → l.SortedLT
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_coeMonoidHom : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α], ⇑Finset.coeMonoidHom = SetLike.coe
-- Lean.SubExpr
/-- Which goal the location is in.  -/
Lean.SubExpr.GoalsLocation.mvarId : Lean.SubExpr.GoalsLocation → Lean.MVarId
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.sSup_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasCoproducts C]
  [inst_4 : CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A))
  (f : CategoryTheory.Subobject A), (∀ g ∈ s, g ≤ f) → CategoryTheory.Subobject.sSup s ≤ f
-- Mathlib.Order.Interval.Finset.Basic
/-- In a locally finite partial order, `≤` is the reflexive transitive closure of `⋖`.  -/
le_iff_reflTransGen_covBy : ∀ {α : Type u_2} [inst : PartialOrder α] [LocallyFiniteOrder α] {x y : α},
  x ≤ y ↔ Relation.ReflTransGen (fun x1 x2 => x1 ⋖ x2) x y
-- Mathlib.Data.List.Sublists
List.revzip_sublists' : ∀ {α : Type u} (l l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.revzip → (l₁ ++ l₂).Perm l
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- (Implementation detail) The relation that `℘'` and `℘` satisfies.
We will show that this is constant zero. See `PeriodPair.relation_eq_zero`  -/
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation : PeriodPair → ℂ → ℂ
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquivLast_castSucc : ∀ {n : ℕ} (i : Fin n), finSuccEquivLast i.castSucc = some i
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The global function which has a partial inverse. Its value outside of the `source` subset is
irrelevant.  -/
PartialEquiv.toFun : {α : Type u_5} → {β : Type u_6} → PartialEquiv α β → α → β
-- Mathlib.Order.CompleteLattice.Basic
iInf_subtype' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α},
  ⨅ i, ⨅ (h : p i), f i h = ⨅ x, f ↑x ⋯