mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.EReal.Basic
EReal.coe_coe_eq_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Lean.Meta.Basic
Lean.Meta.PostponedEntry.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (lhs rhs : Lean.Level) (ctx? : Option Lean.Meta.DefEqContext),
  sizeOf { ref := ref, lhs := lhs, rhs := rhs, ctx? := ctx? } = 1 + sizeOf ref + sizeOf lhs + sizeOf rhs + sizeOf ctx?
-- Mathlib.Algebra.Order.ZeroLEOne
Nat.instZeroLEOneClass : ZeroLEOneClass ℕ
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- Addition in `E` is continuous when `E` is equipped with a `LinearMap.IsWeak` topology.  -/
LinearMap.IsWeak.continuousAdd : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] [ContinuousAdd 𝕜], ContinuousAdd E
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Submodule.cardQuot_bot : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Infinite M],
  ⊥.cardQuot = 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.base : Lean.Environment → Lean.VisibilityMap✝ Lean.Kernel.Environment
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_monotone : ∀ {p q : ℕ} (L : List ℕ), p ≤ q → Nat.ofDigits p L ≤ Nat.ofDigits q L
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (x y : CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n),
  R.extEquivCohomologyClass.symm (x - y) = R.extEquivCohomologyClass.symm x - R.extEquivCohomologyClass.symm y
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The left whiskering of an isomorphism is an isomorphism.  -/
CategoryTheory.MonoidalCategory.whiskerLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        {Y Z : C} →
          (Y ≅ Z) →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
-- Mathlib.RingTheory.RegularLocalRing.Polynomial
MvPolynomial.isRegularRing_of_isRegularRing : ∀ (R : Type u_1) [inst : CommRing R] [IsRegularRing R] {ι : Type u_2} [Finite ι], IsRegularRing (MvPolynomial ι R)
-- Init.Data.List.Nat.Sum
List.sum_reverse_nat : ∀ (xs : List ℕ), xs.reverse.sum = xs.sum
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toListRev_valuesIter : ∀ {α β : Type u} {m : Std.HashMap.Raw α β}, m.valuesIter.toListRev = (List.map Prod.snd m.toList).reverse
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.uIcc i j = Set.uIcc (i.addNat m) (j.addNat m)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_p_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C} (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp P.decompId_p f =
    CategoryTheory.CategoryStruct.comp { f := f.f, comm := ⋯ } Q.decompId_p
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.prod : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter α} {g : Filter β},
  Cauchy f → Cauchy g → Cauchy (f ×ˢ g)
-- Init.Data.UInt.Lemmas
UInt32.lt_or_eq_of_le : ∀ {a b : UInt32}, a ≤ b → a < b ∨ a = b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.support_pow_eq_iff : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.IsCycle → ∀ {n : ℕ}, (f ^ n).support = f.support ↔ ¬orderOf f ∣ n
-- Lean.Meta.Basic
Lean.Meta.instInhabitedExprConfigCacheKey.default : Lean.Meta.ExprConfigCacheKey
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.neg_add_cancel_right_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {b : α}, b ≠ ⊤ → ∀ (a : α), a + -b + b = a
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofEq_symm : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  {p q : Submodule R M} (h : p = q), (LinearEquiv.ofEq p q h).symm = LinearEquiv.ofEq q p ⋯
-- Mathlib.Algebra.Homology.Homotopy
HomologicalComplex.instRespectsIsoHomotopyEquivalences : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι}, (HomologicalComplex.homotopyEquivalences V c).RespectsIso
-- Lean.Meta.Tactic.Simp.Types
/-- Recall that we cannot store `Simproc` into .olean files because it is a closure.
Given `SimprocOLeanEntry.declName`, we convert it into a `Simproc` by using the unsafe function `evalConstCheck`.
 -/
Lean.Meta.Simp.SimprocEntry.proc : Lean.Meta.Simp.SimprocEntry → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc
-- Mathlib.Logic.Function.Basic
Function.uncurry_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ), Function.uncurry f = fun p => f p.1 p.2
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
/-- The shifted Legendre polynomial multiplied by a factorial equals the higher-order derivative of
the combinatorial function `X ^ n * (1 - X) ^ n`. This is the analogue of Rodrigues' formula for
the shifted Legendre polynomials.  -/
Polynomial.factorial_mul_shiftedLegendre_eq : ∀ (n : ℕ),
  ↑n.factorial * Polynomial.shiftedLegendre n = (⇑Polynomial.derivative)^[n] (Polynomial.X ^ n * (1 - Polynomial.X) ^ n)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.map_unique : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β}
  {g : UniformSpace.Completion α → UniformSpace.Completion β},
  UniformContinuous g → (∀ (a : α), ↑(f a) = g ↑a) → UniformSpace.Completion.map f = g
-- Mathlib.Data.Part
Part.instInv.eq_1 : ∀ {α : Type u_1} [inst : Inv α], Part.instInv = { inv := Part.map Inv.inv }
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.prodAssoc_toEquiv : ∀ (X : Type u) (Y : Type v) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z], (Homeomorph.prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z
-- Mathlib.Topology.Algebra.Monoid
continuousAt_pow : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] (x : M) (n : ℕ),
  ContinuousAt (fun x => x ^ n) x
-- Mathlib.Algebra.Jordan.Basic
commute_lmul_rmul_sq : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [IsJordan A] (a : A),
  Commute (AddMonoid.End.mulLeft a) (AddMonoid.End.mulRight (a * a))
-- Init.Data.List.Basic
List.intersperseTR.eq_3 : ∀ {α : Type u} (sep x_1 y : α) (xs : List α),
  List.intersperseTR sep (x_1 :: y :: xs) = x_1 :: sep :: y :: List.foldr (fun a r => sep :: a :: r) [] xs
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_getD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β}, a ∈ m → m[a]? = some (m.getD a fallback)
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroOneClass.mk : {M₀ : Type u} →
  [toMulOneClass : MulOneClass M₀] →
    [toZero : Zero M₀] → (∀ (a : M₀), 0 * a = 0) → (∀ (a : M₀), a * 0 = 0) → MulZeroOneClass M₀
-- Init.Data.List.Erase
List.erase_eq_nil_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α} {a : α}, xs.erase a = [] ↔ xs = [] ∨ xs = [a]
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.localizationAway_relation : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (x : Unit),
  (Algebra.Presentation.localizationAway S r).relation x = MvPolynomial.C r * MvPolynomial.X () - 1
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubmonoid_iUnion : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α] {ι : Sort u_3} {s : ι → Set α},
  fixingAddSubmonoid M (⋃ i, s i) = ⨅ i, fixingAddSubmonoid M (s i)
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.introsClean.isTrivialType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Lie.Prod
/-- The second projection of a product is a Lie algebra map.  -/
LieHom.snd : (R : Type u_1) →
  (L₁ : Type u_2) →
    (L₂ : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → L₁ × L₂ →ₗ⁅R⁆ L₂
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_pow_eq_iterate`. -/
ContinuousLinearMap.coe_pow' : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : Monoid F'] [IsMulApplyEqComp F' α]
  [IsOneApplyEqSelf F' α] (f : F') (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Topology.IsInducing.multipliable_iff_tprod_comp_mem_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ] [T2Space γ] {G : Type u_4}
  [inst_5 : FunLike G α γ] [MonoidHomClass G α γ] {g : G},
  Topology.IsInducing ⇑g →
    ∀ (f : β → α), Multipliable f L ↔ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList_zero : ∀ (R : Type u_1) [inst : Semiring R], Polynomial.coeffList 0 = []
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains a t = false → Std.DTreeMap.Internal.Impl.Const.getD t a fallback = fallback
-- Mathlib.Data.List.Chain
/-- **Alias** of `List.IsChain.rel`. -/
List.IsChain.rel_head : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → R a b
-- Mathlib.Analysis.Convex.Function
ConcaveOn.convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConcaveOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
-- Mathlib.Algebra.Group.EvenFunction
/-- The zero function is odd.  -/
Function.Odd.zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] [inst_1 : NegZeroClass β], Function.Odd fun x => 0
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.degrees 0 = 0
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- `AddMonoidHom.toMultiplicativeRight` as an `AddEquiv`.  -/
AddMonoidHom.toMultiplicativeRightAddEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Monoid M] → [inst_1 : AddCommMonoid N] → (Additive M →+ N) ≃+ Additive (M →* Multiplicative N)
-- Mathlib.CategoryTheory.Action.Basic
Action.mk : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → (V_1 : V) → (G →* CategoryTheory.End V_1) → Action V G
-- Mathlib.Algebra.Group.Shrink
equivShrink_neg : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Neg α] (x : α), (equivShrink α) (-x) = -(equivShrink α) x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.toPresheaf_obj : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules}, (AlgebraicGeometry.Scheme.Modules.toPresheaf X).obj M = M.presheaf
-- Init.Grind.Module.Basic
/-- Subtraction is addition of the negative.  -/
Lean.Grind.AddCommGroup.sub_eq_add_neg : ∀ {M : Type u} [self : Lean.Grind.AddCommGroup M] (a b : M), a - b = a + -b
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (e e_1 : x.fst ≅ y.fst) (e_e : e = e_1) (he : (CategoryTheory.ConcreteCategory.hom (F.map e.hom)) x.snd = y.snd),
  CategoryTheory.CategoryOfElements.isoMk x y e he = CategoryTheory.CategoryOfElements.isoMk x y e_1 ⋯
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.pairwiseDisjoint : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D],
  Set.univ.PairwiseDisjoint fun ni => Topology.RelCWComplex.openCell ni.fst ni.snd
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.throwUnexpected : {α : Type} → Lean.MessageData → Lean.Meta.SizeOfSpecNested.M α
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_13.eq_2 : ∀ (C : Type u_1) (motive : CategoryTheory.WithTerminal Cᵒᵖ → Sort u_2)
  (h_1 : (x : Cᵒᵖ) → motive (CategoryTheory.WithTerminal.of x)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of x => h_1 x
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Sets.Compacts
/-- The set of compacts inside an open subset  -/
TopologicalSpace.Opens.compactsInside : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.Opens α → Set (TopologicalSpace.Compacts α)
-- Lean.Language.Lean.Types
/-- State after command elaborator has returned.  -/
Lean.Language.Lean.CommandElaboratingSnapshot.resultSnap : Lean.Language.Lean.CommandElaboratingSnapshot → Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot
-- Mathlib.Algebra.Group.Basic
additive_of_symm_of_total : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β) [Std.Symm p],
  (∀ {a b : α}, p a b → f a b + f b a = 0) →
    (∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b + f b c) →
      ∀ {a b c : α}, p a b → p b c → p a c → f a c = f a b + f b c
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_5 : ∀ (a b : PosNum), a.bit1.sub' b.bit0 = (a.sub' b).bit1
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instAlgebraQuotient : {α : Type u_1} →
  {R : Type u_3} →
    [inst : CommSemiring α] → [inst_1 : Semiring R] → [Algebra α R] → (c : RingCon R) → Algebra α c.Quotient
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
/-- The morphism `X _⦋n+1⦌ ⟶ Z` associated to `f : MorphComponents X n Z`.  -/
AlgebraicTopology.DoldKan.MorphComponents.φ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        {n : ℕ} → {Z : C} → AlgebraicTopology.DoldKan.MorphComponents X n Z → (X.obj (Opposite.op { len := n + 1 }) ⟶ Z)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    (↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).size = l.length
-- Mathlib.Combinatorics.Quiver.Basic
/-- A quiver `G` on a type `V` of vertices assigns to every pair `a b : V` of vertices
a type `a ⟶ b` of arrows from `a` to `b`. This is hence a form of directed multigraphs.

For graphs with no repeated edges, one can either use `Quiver.IsThin` to demand
that the hom sets are subsingletons, or `Digraph V` (where the hom sets
are Prop-valued).

Because `Category` will later extend this class, we call the field `Hom`.
Except when constructing instances, you should rarely see this, and use the `⟶` notation instead.
 -/
Quiver : Type u → Type (max u (v + 1))
-- Mathlib.Data.Sym.Basic
Sym.append_inj_right : ∀ {α : Type u_1} {n n' : ℕ} (s : Sym α n) {t t' : Sym α n'}, s.append t = s.append t' ↔ t = t'
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x x_1 : NumberField.mixedEmbedding.mixedSpace K),
  x = x_1 → NumberField.mixedEmbedding.convexBodySumFun x = NumberField.mixedEmbedding.convexBodySumFun x_1
-- Init.Data.List.Scan.Lemmas
List.scanl_singleton : ∀ {β : Type u_1} {α : Type u_2} {b : β} {a : α} {f : β → α → β}, List.scanl f b [a] = [b, f b a]
-- Mathlib.Analysis.Seminorm
Seminorm.sup_apply : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] (p q : Seminorm 𝕜 E)
  (x : E), (p ⊔ q) x = max (p x) (q x)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {Y : AlgebraicGeometry.Scheme}
  (g g_1 : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (e_g : g = g_1)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i),
  𝒰.glueMorphismsOfLocallyDirected g h = 𝒰.glueMorphismsOfLocallyDirected g_1 ⋯
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.coe_modularForm : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : FunLike F UpperHalfPlane ℂ]
  [inst_1 : ModularFormClass F Γ k] (f : F), ⇑(ModularFormClass.modularForm f) = ⇑f
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instIsRightAdjointForgetAlgHomCarrier : ∀ (R : Type u) [inst : CommRing R], (CategoryTheory.forget (AlgCat R)).IsRightAdjoint
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.mk.injEq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (hom : C ⟶ D) (inv : D ⟶ C)
  (homotopyHomInvId : Homotopy (CategoryTheory.CategoryStruct.comp hom inv) (CategoryTheory.CategoryStruct.id C))
  (homotopyInvHomId : Homotopy (CategoryTheory.CategoryStruct.comp inv hom) (CategoryTheory.CategoryStruct.id D))
  (hom_1 : C ⟶ D) (inv_1 : D ⟶ C)
  (homotopyHomInvId_1 : Homotopy (CategoryTheory.CategoryStruct.comp hom_1 inv_1) (CategoryTheory.CategoryStruct.id C))
  (homotopyInvHomId_1 : Homotopy (CategoryTheory.CategoryStruct.comp inv_1 hom_1) (CategoryTheory.CategoryStruct.id D)),
  ({ hom := hom, inv := inv, homotopyHomInvId := homotopyHomInvId, homotopyInvHomId := homotopyInvHomId } =
      { hom := hom_1, inv := inv_1, homotopyHomInvId := homotopyHomInvId_1, homotopyInvHomId := homotopyInvHomId_1 }) =
    (hom = hom_1 ∧ inv = inv_1 ∧ homotopyHomInvId ≍ homotopyHomInvId_1 ∧ homotopyInvHomId ≍ homotopyInvHomId_1)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_1.splitter : (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) →
  (p₁ p₂ : Int.Internal.Linear.Poly) →
    ((k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂)) →
      ((k₁ a : ℤ) →
          (x : Int.Internal.Linear.Var) →
            (p : Int.Internal.Linear.Poly) →
              motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p)) →
        ((a : ℤ) →
            (x : Int.Internal.Linear.Var) →
              (p : Int.Internal.Linear.Poly) →
                (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂)) →
          ((a₁ : ℤ) →
              (x₁ : Int.Internal.Linear.Var) →
                (p₁ : Int.Internal.Linear.Poly) →
                  (a₂ : ℤ) →
                    (x₂ : Int.Internal.Linear.Var) →
                      (p₂ : Int.Internal.Linear.Poly) →
                        motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)) →
            motive p₁ p₂
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.of_hasCokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasCokernel f],
  { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.HasLeftHomology
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.mem_boundary_iff_notMem_range : ∀ {n d : ℕ} (s : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })),
  s ∈ (SSet.boundary n).obj (Opposite.op { len := d }) ↔ ∃ j, j ∉ Set.range ⇑s
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_mul_left : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit b → b / (a * b) = 1 / a
-- Init.Data.String.Substring
Substring.Raw.Internal.allImpl : Substring.Raw → (Char → Bool) → Bool
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.objEqToHom_refl : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β),
  X.objEqToHom ⋯ = CategoryTheory.CategoryStruct.id (X.obj i)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- Given a compact set in a proper space, the measure of its `r`-closed thickenings converges to
its measure as `r` tends to `0`.  -/
tendsto_measure_cthickening_of_isCompact : ∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] [ProperSpace α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {s : Set α},
  IsCompact s → Filter.Tendsto (fun r => μ (Metric.cthickening r s)) (nhds 0) (nhds (μ s))
-- Mathlib.Probability.Moments.ComplexMGF
/-- If two random variables have the same moment-generating function then they have
the same `complexMGF` on the vertical strip `{z | z.re ∈ interior (integrableExpSet X μ)}`.  -/
ProbabilityTheory.eqOn_complexMGF_of_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ],
  ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ' →
    Set.EqOn (ProbabilityTheory.complexMGF X μ) (ProbabilityTheory.complexMGF Y μ')
      {z | z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)}
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_ofNat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) [inst_3 : OfNat F n], deriv (OfNat.ofNat n) = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqResolvableCompletionItemData : BEq Lean.Lsp.ResolvableCompletionItemData
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.n : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w → ℕ
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- If the first `n` derivatives within a set of a function are continuous, and its first `n-1`
derivatives are differentiable, then the function is `C^n`. This is not an equivalence in general,
but this is an equivalence when the set has unique derivatives, see
`contDiffOn_iff_continuousOn_differentiableOn_deriv`.  -/
contDiffOn_of_continuousOn_differentiableOn_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞},
  (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s) →
    (∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s) → ContDiffOn 𝕜 (↑n) f s