mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Sublists
/-- **Alias** of the forward direction of `List.nodup_sublists'`. -/
List.Nodup.of_sublists' : ∀ {α : Type u} {l : List α}, l.sublists'.Nodup → l.Nodup
-- Mathlib.Algebra.WithConv
WithConv.toConv_eq_zero : ∀ {A : Type u_2} [inst : AddMonoid A] {x : A}, WithConv.toConv x = 0 ↔ x = 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_reachable_iff_isEmpty_walk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v ↔ IsEmpty (G.Walk u v)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_add : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : Add R] (A B : Matrix m n R), (A + B).vec = A.vec + B.vec
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → TopologicalSpace (α i)] [∀ (i : ι), MeasureTheory.IsFiniteMeasureOnCompacts (μ i)],
  MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.pi μ)
-- Mathlib.Algebra.Group.Units.Defs
/-- Partial division, denoted `a /ₚ u`. It is defined when the
second argument is invertible, and unlike the division operator
in `DivisionRing` it is not totalized at zero.  -/
divp : {α : Type u} → [inst : Monoid α] → α → αˣ → α
-- Init.Conv
/-- `simp_match` simplifies match expressions. For example,
```
match [a, b] with
| [] => 0
| hd :: tl => hd
```
simplifies to `a`.  -/
Lean.Parser.Tactic.Conv.simpMatch : Lean.ParserDescr
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_ge_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] {f : Filter β} {u v : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f fun a => u a ⊓ v a) ↔
    Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u ∧ Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f v
-- Mathlib.Topology.Sets.Compacts
/-- The image of a positive compact set under a continuous open map.  -/
TopologicalSpace.PositiveCompacts.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : α → β) →
          Continuous f → IsOpenMap f → TopologicalSpace.PositiveCompacts α → TopologicalSpace.PositiveCompacts β
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
inTangentCoordinates.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_5} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [inst_11 : IsManifold I 1 M]
  [inst_12 : IsManifold I' 1 M'] {N : Type u_9} (f : N → M) (g : N → M') (ϕ : N → E →L[𝕜] E') (x₀ x : N),
  inTangentCoordinates I I' f g ϕ x₀ x =
    ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (f x₀) (f x) (g x₀) (g x) (ϕ x)
-- Mathlib.RepresentationTheory.Invariants
/-- The `averageMap` acts as the identity on the subspace of invariants.
 -/
Representation.averageMap_id : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [inst_4 : Fintype G] [inst_5 : Invertible ↑(Fintype.card G)],
  ∀ v ∈ ρ.invariants, ρ.averageMap v = v
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mk_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y), (CategoryTheory.Under.mk f).hom = f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraDualNumber.ι_mul_ι : ∀ {R : Type u_1} [inst : CommRing R] (r₁ r₂ : R), (CliffordAlgebra.ι 0) r₁ * (CliffordAlgebra.ι 0) r₂ = 0
-- Mathlib.Tactic.Linarith.Preprocessing
/-- If `e : ℕ`, returns a proof of `0 ≤ (e : C)`.  -/
Mathlib.Tactic.Linarith.mkNatCastNonnegProof? : Lean.Expr × Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeftIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ≅ Z),
  (CategoryTheory.MonoidalCategory.whiskerLeftIso X f).inv = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.inv
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.largeCategory : CategoryTheory.LargeCategory Pointed
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.instNoZeroDivisors : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Zero α] [inst_2 : Mul α] [NoZeroDivisors α], NoZeroDivisors (Finset α)
-- Init.Data.Array.Lemmas
Array.reverse_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α}, xs.reverse = #[] ↔ xs = #[]
-- Init.Data.ByteArray.Lemmas
ByteArray.fastAppend_eq_copySlice : ∀ {a b : ByteArray}, a.fastAppend b = b.copySlice 0 a a.size b.size false
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `TypeCat.ofHom`.

---

Typecheck a function as a morphism in `Type`.  -/
CategoryTheory.asHom : {X Y : Type u} → (X → Y) → (X ⟶ Y)
-- Mathlib.Order.Filter.Pointwise
Filter.pure_div_pure : ∀ {α : Type u_2} [inst : Div α] {a b : α}, pure a / pure b = pure (a / b)
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Ring homomorphisms preserve addition.  -/
RingHom.map_add : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α),
  f (a + b) = f a + f b
-- Mathlib.Tactic.Tauto
_private.Mathlib.Tactic.Tauto.0.Mathlib.Tactic.Tauto.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.Tauto.Config
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.prev_nil : ∀ {r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor [] r it → String.Legacy.Iterator.ValidFor [] r it.prev
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.instIsStableUnderRetractsMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P₁ P₂ : CategoryTheory.MorphismProperty C)
  [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts], (P₁ ⊓ P₂).IsStableUnderRetracts
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens.mk.injEq : ∀ (resultId? : Option String) (data : Array ℕ) (resultId?_1 : Option String) (data_1 : Array ℕ),
  ({ resultId? := resultId?, data := data } = { resultId? := resultId?_1, data := data_1 }) =
    (resultId? = resultId?_1 ∧ data = data_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldr_eq_foldr_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {f : α → δ → δ}
  {init : δ}, Std.DTreeMap.foldr (fun a x d => f a d) init t = Array.foldr f init t.keysArray
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
Finset.prod_indicator_biUnion_finset_sub_indicator : ∀ {ι : Type u_1} {α : Type u_2} {s : Finset ι} [inst : DecidableEq α],
  s.Nonempty → ∀ (S : ι → Finset α) (a : α), ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.mono_right : ∀ {X : Type u_1} {R : SetRel X X} {s t : Set X}, s ⊆ t → R.IsSeparated t → R.IsSeparated s
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.periodic_derivWeierstrassP : ∀ (L : PeriodPair) (l : ↥L.lattice), Function.Periodic L.derivWeierstrassP ↑l
-- Mathlib.Data.PNat.Factors
/-- Positive integers biject with multisets of primes.  -/
PNat.factorMultisetEquiv : ℕ+ ≃ PrimeMultiset
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_div_cast_nonneg : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (n : ℕ), 0 ≤ 1 / ↑n
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.AddValuation.map_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Padic.addValuationDef 1 = 0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ≌ D)
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- `(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x` when the `f' n` converge
_uniformly_ to their limit on an open set containing `x`.  -/
hasFDerivAt_of_tendstoUniformlyOn : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G}
  {g' : E → E →L[𝕜] G} {x : E} [l.NeBot] {s : Set E},
  IsOpen s →
    TendstoUniformlyOn f' g' l s →
      (∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasFDerivAt g (g' x) x
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- A ring satisfies the strong rank condition if and only if, for all `n : ℕ`, any linear map
`(Fin (n + 1) → R) →ₗ[R] (Fin n → R)` is not injective.  -/
strongRankCondition_iff_succ : ∀ (R : Type u) [inst : Semiring R],
  StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective ⇑f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList.congr_simp : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] (r r_1 : Std.Rio α), r = r_1 → r.toList = r_1.toList
-- Init.Data.Option.Monadic
Option.forIn'_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as bs : Option α}
  (w : as = bs) {b b' : β},
  b = b' →
    ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
      (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- "Base change preserves integral closure" is stable under composition.  -/
TensorProduct.toIntegralClosure_bijective_of_tower : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {T : Type u_4} [inst_5 : CommRing T] [inst_6 : Algebra R T]
  [inst_7 : Algebra S T] [IsScalarTower R S T],
  Function.Bijective ⇑(TensorProduct.toIntegralClosure R S B) →
    Function.Bijective ⇑(TensorProduct.toIntegralClosure S T (TensorProduct R S B)) →
      Function.Bijective ⇑(TensorProduct.toIntegralClosure R T B)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (j : CategoryTheory.Discrete α),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).cocone.ι.app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩)
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) {j})
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_closure : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {s : Set M},
  s.Finite → ((FirstOrder.Language.Substructure.closure L).toFun s).FG
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A left homology data for a short complex `S` in the opposite category
induces a right homology data for `S.unop`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex Cᵒᵖ} → S.LeftHomologyData → S.unop.RightHomologyData
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquashOrUnit.eq_1 : ∀ (α : Type v),
  Std.Internal.USquashOrUnit α = if x : Std.Internal.Small α then Std.Internal.USquash α else PUnit.{u + 1}
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_singleton_iff : ∀ {k n : ℕ}, (*...=n).toList = [k] ↔ n = 0 ∧ 0 = k
-- Mathlib.Algebra.Order.Sub.Defs
/-- Weaker version of `AddLECancellable.eq_tsub_of_add_eq` assuming that `b = a + c` itself is
cancellable rather than `c`.  -/
AddLECancellable.eq_tsub_of_add_eq' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], AddLECancellable b → a + c = b → a = b - c
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.mk.injEq : ∀ (rw : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma)
  (grw : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma)
  (app : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma)
  (appAt : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)
  (rw_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma)
  (grw_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma)
  (app_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma)
  (appAt_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma),
  ({ rw := rw, grw := grw, app := app, appAt := appAt } =
      { rw := rw_1, grw := grw_1, app := app_1, appAt := appAt_1 }) =
    (rw = rw_1 ∧ grw = grw_1 ∧ app = app_1 ∧ appAt = appAt_1)
-- Lean.LocalContext
Lean.LocalDecl.binderInfoEx : Lean.LocalDecl → Lean.BinderInfo
-- Lean.Parser.Syntax
Lean.Parser.Command.syntax.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.neg_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) (v : V), (-f) v = -f v
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_toArray_rco : ∀ {m n : ℤ}, (m...n).toArray.toList = (m...n).toList
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.comap_coclosedCompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Filter.comap (⇑h) (Filter.coclosedCompact Y) = Filter.coclosedCompact X
-- Mathlib.Order.Directed
directedOn_pair : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, r a b → DirectedOn r {a, b}
-- Init.Data.String.Decode
UInt8.isUTF8FirstByte_getElem_utf8EncodeChar : ∀ {c : Char} {i : ℕ} {hi : i < (String.utf8EncodeChar c).length}, (String.utf8EncodeChar c)[i].IsUTF8FirstByte ↔ i = 0
-- Lean.Data.Options
Lean.Option.Decl.descr : {α : Type} → Lean.Option.Decl α → String
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.one_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Preorder α] [inst_1 : DecidableEq α] [inst_2 : Zero 𝕜] [inst_3 : One 𝕜]
  (a b : α), 1 a b = if a = b then 1 else 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcL_integrable : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] (a : A) (f : X → C(↑(spectrum 𝕜 a), 𝕜)),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcL_integrable._auto_1), MeasureTheory.Integrable (fun x => (cfcL ha) (f x)) μ
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.inv_mul_cancel : {R : Type u} →
  [inst : Rack R] → (a : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R (a.inv.mul a) Rack.PreEnvelGroup.unit
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_dep_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {I : Set α} {N : Matroid β},
  (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬Set.InjOn f I
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.mk.sizeOf_spec : ∀ {ι : Type u_1} [inst : SizeOf ι] (toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex ι)
  (singleton_mem : ∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex.faces),
  sizeOf { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, singleton_mem := singleton_mem } =
    1 + sizeOf toPreAbstractSimplicialComplex
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData.mk.injEq : ∀ (errors errors_1 : IO.Ref (Array Lean.Meta.RefinedDiscrTree.ImportFailure✝)),
  ({ errors := errors } = { errors := errors_1 }) = (errors = errors_1)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddCommSemigroup M],
  Filter.Germ.instAddCommSemigroup = { toAddSemigroup := Filter.Germ.instAddSemigroup, add_comm := ⋯ }
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- If `‖ω z‖ ≤ C` at all points of the segment `[a -[ℝ] b]`,
then the curve integral `∫ᶜ x in .segment a b, ω x` has norm at most `C * ‖b - a‖`.  -/
norm_curveIntegral_segment_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  [inst_5 : NormedSpace ℝ E] {C : ℝ},
  (∀ z ∈ segment ℝ a b, ‖ω z‖ ≤ C) → ‖∫ᶜ (x : E) in Path.segment a b, ω x‖ ≤ C * ‖b - a‖
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.differentiableOn_cuspFunction_ball : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f → DifferentiableOn ℂ (UpperHalfPlane.cuspFunction h f) (Metric.ball 0 1)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If we reflect limits of some arbitrary size, then we reflect all finite limits.  -/
CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on a typed expression `e : α`,
returning a typed expression `lit : ℤ`, and a proof of `IsInt e lit` in expression form.  -/
Mathlib.Meta.NormNum.deriveInt : {u : Lean.Level} →
  {α : Q(Type u)} →
    (e : Q(«$α»)) →
      (_inst : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.deriveInt._auto_1) →
        Lean.MetaM ((lit : Q(ℤ)) × Q(Mathlib.Meta.NormNum.IsInt «$e» «$lit»))
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minEntry! : {α : Type u} → {β : α → Type v} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Internal.Impl α β → (a : α) × β a
-- Mathlib.Analysis.Normed.Field.Basic
nnnorm_inv : ∀ {α : Type u_2} [inst : NormedDivisionRing α] (a : α), ‖a⁻¹‖₊ = ‖a‖₊⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.termY_1 : Lean.ParserDescr
-- Mathlib.MeasureTheory.Constructions.Pi
/-- A measure on a finite product space equals the product measure if they are equal on rectangles
with as sides sets that generate the corresponding σ-algebras.  -/
MeasureTheory.Measure.pi_eq_generateFrom : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), MeasurableSpace.generateFrom (C i) = inst_1 i) →
    (∀ (i : ι), IsPiSystem (C i)) →
      ∀ (h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)) {μν : MeasureTheory.Measure ((i : ι) → α i)},
        (∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (Set.univ.pi s) = ∏ i, (μ i) (s i)) →
          MeasureTheory.Measure.pi μ = μν
-- Mathlib.Control.Traversable.Basic
instTraversableSum : {σ : Type u} → Traversable (Sum σ)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.imageι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'),
  CategoryTheory.Sheaf.imageι f =
    { hom := (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range f.hom)).ι }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.maxKey? = some km → (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Lean.Util.Trace
Lean.TraceElem.mk : Lean.Syntax → Lean.MessageData → Lean.TraceElem
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.unionₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Algebra.Prime.Lemmas
DvdNotUnit.ne : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p q : M}, DvdNotUnit p q → p ≠ q
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_eq_ofNat_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} [inst_1 : n.AtLeastTwo] {a : WithBot β},
  WithBot.map f a = OfNat.ofNat n ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.Tactic.Sat.FromLRAT
/-- An LRAT step is either an addition or a deletion step.  -/
Mathlib.Tactic.Sat.LRATStep : Type
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
/-- **Alias** of `EisensteinSeries.eisensteinSeriesSIF_mdifferentiable`.

---

Eisenstein series are MDifferentiable (i.e. holomorphic functions from `ℍ → ℂ`).  -/
EisensteinSeries.eisensteinSeries_SIF_MDifferentiable : ∀ {k : ℤ} {N : ℕ}, 3 ≤ k → ∀ (a : Fin 2 → ZMod N), MDiff ⇑(EisensteinSeries.eisensteinSeriesSIF a k)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
DirectedOn.le_csInf : ∀ {α : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → (∀ b ∈ s, a ≤ b) → a ≤ sInf s
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instLELex : {α : Type u_1} → [LT α] → [inst : LE α] → LE (Lex (NonemptyInterval α))
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
/-- Open ball w.r.t. the Euclidean distance.  -/
Euclidean.ball : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [T2Space E] → [inst_4 : Module ℝ E] → [ContinuousSMul ℝ E] → [FiniteDimensional ℝ E] → E → ℝ → Set E
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_E6 : ADEInequality.Admissible ADEInequality.E6
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_sub_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract (a - 1) = Int.fract a
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePosAssignment.eq_2 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.removePosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
-- Mathlib.Topology.Filter
Continuous.nhds : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Continuous (nhds ∘ f)