mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.toFun_comp_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (S : Type u_7) [inst_7 : CommSemiring S] [inst_8 : Algebra R S]
  (m : TensorProduct R S M), PolynomialLaw.toFun S (g.comp f) m = PolynomialLaw.toFun S g (PolynomialLaw.toFun S f m)
-- Init.Control.Lawful.Basic
Id.run_seq : ∀ {α β : Type u_1} (f : Id (α → β)) (x : Id α), (f <*> x).run = f.run x.run
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α},
  t.contains k = true → t.get? k = some k
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfToPiQuotient_mk' : ∀ {R : Type u} [inst : Ring R] {ι : Type u_1} (I : ι → Ideal R) [inst_1 : ∀ (i : ι), (I i).IsTwoSided] (x : R) (i : ι),
  (Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ i, I i)) x) i = (Ideal.Quotient.mk (I i)) x
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atTop` then `f * g` tends to `atTop`.  -/
Filter.Tendsto.mul_atTop' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.mk.sizeOf_spec : ∀ {T : Type u_1} [inst : SizeOf T] (NT : Type) (initial : NT) (rules : Finset (ContextFreeRule T NT)),
  sizeOf { NT := NT, initial := initial, rules := rules } = 1 + sizeOf NT + sizeOf initial + sizeOf rules
-- Aesop.Tree.State
Aesop.GoalRef.markSubtreeIrrelevant : Aesop.GoalRef → BaseIO Unit
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The diagram `{Dᵢ}`.  -/
CategoryTheory.Limits.ColimitPresentation.diag : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} → CategoryTheory.Limits.ColimitPresentation J X → CategoryTheory.Functor J C
-- Init.Data.Char.Lemmas
Char.leAntisymm : Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_consₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ (a : α) (b : β a), m.containsₘ a = false → Std.DHashMap.Internal.Raw.WFImp ↑(m.consₘ a b)
-- Mathlib.Order.WithBot
WithBot.lt_iff_exists_coe_btwn' : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α}, a < b ↔ ∃ x, ↑x < b ∧ a < ↑x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_sub_pi : ∀ (x : ℂ), Complex.cos (x - ↑Real.pi) = -Complex.cos x
-- Mathlib.Order.Grade
IsMin.grade : ∀ (𝕆 : Type u_1) {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeMinOrder 𝕆 α] {a : α},
  IsMin a → IsMin (grade 𝕆 a)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.act_incl.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] (x y : R),
  sizeOf (Rack.PreEnvelGroupRel'.act_incl x y) = 1 + sizeOf x + sizeOf y
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.bialgEquivOfIso_symm_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (i : A ≅ B) (a : ↑B),
  (CommBialgCat.bialgEquivOfIso i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a
-- Mathlib.Logic.Relation
Relation.ReflGen.instRefl : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Refl (Relation.ReflGen r)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_sum`. -/
ContinuousLinearMap.coe_sum' : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.instIsCommComonObjTensorObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (A B : C) [inst_3 : CategoryTheory.ComonObj A]
  [inst_4 : CategoryTheory.ComonObj B] [CategoryTheory.IsCommComonObj A] [CategoryTheory.IsCommComonObj B],
  CategoryTheory.IsCommComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)
-- Init.Data.String.Subslice
String.Slice.Subslice.ext : ∀ {s : String.Slice} {x y : s.Subslice}, x.startInclusive = y.startInclusive → x.endExclusive = y.endExclusive → x = y
-- Lean.CoreM
/-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`.  -/
Lean.mkArrowN : Array Lean.Expr → Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑X.toTopCat) (x : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (f.c.app (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U))))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U)) x) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- **Alias** of `CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom`. -/
CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  (F : CategoryTheory.Sheaf J A),
  ((G.sheafAdjunctionCocontinuous A J K).counit.app F).hom = (G.op.ranAdjunction A).counit.app F.obj
-- Mathlib.CategoryTheory.Filtered.Final
/-- The functor `StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S)` that `u : e ⟶ S.obj d`
induces via `StructuredArrow.map₂` is final, if `T` and `S` are final and the domain of `T` is
filtered.  -/
CategoryTheory.StructuredArrow.final_map₂_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {T : CategoryTheory.Functor C D} [T.Final] {S : CategoryTheory.Functor D E} [S.Final]
  {T' : CategoryTheory.Functor C E} {d : D} {e : E} (u : e ⟶ S.obj d) (α : T.comp S ⟶ T') [CategoryTheory.IsIso α],
  (CategoryTheory.StructuredArrow.map₂ u α).Final
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.is_quadratic : ∀ {K : Type u_1} {inst : Field K} {inst_1 : CharZero K} [self : NumberField.IsCMField K],
  Algebra.IsQuadraticExtension (↥(NumberField.maximalRealSubfield K)) K
-- Mathlib.RingTheory.Congruence.Hom
/-- The **second isomorphism theorem for semirings**.  -/
RingCon.comapQuotientEquivRangeS : {M : Type u_1} →
  {N : Type u_2} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring N] →
        (c : RingCon M) → (f : N →+* M) → {d : RingCon N} → d = c.comap f → d.Quotient ≃+* ↥(c.mk'.comp f).rangeS
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.equiv_refl : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (P Q : Submodule R M)
  (hf : Submodule.map (↑(LinearEquiv.refl R M)) P = Q),
  Submodule.Quotient.equiv P Q (LinearEquiv.refl R M) hf = P.quotEquivOfEq Q ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instOrderBot : {α : Type u_1} → [inst : LE α] → OrderBot (WithZero α)
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instFaithfulLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism : ∀ {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  (A B : CategoryTheory.ObjectProperty C) [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.HasShift C ℤ] [inst_5 : CategoryTheory.Preadditive C]
  [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_7 : CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C] [inst_9 : A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
  [A.IsVerdierRightLocalizing B] (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂)
  [inst_13 : L₁.IsLocalization (B.inverseImage A.ι).trW] [inst_14 : L₂.IsLocalization B.trW],
  ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful
-- Lean.ReducibilityAttrs
/-- Return `true` if the given declaration has been marked as `[irreducible]`  -/
Lean.isIrreducible : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_iff_add_self_lt : ∀ {a : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a ↔ ∀ b < a, b + b < a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInsertReplaceEdit.fromJson : Lean.Json → Except String Lean.Lsp.InsertReplaceEdit
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.iff_of_unique : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {U : Set S} [inst_1 : Unique ι], IsCompactOpenCovered f U ↔ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.edgeDisjointTriangles_bot : ∀ {α : Type u_1}, ⊥.EdgeDisjointTriangles
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsFixedPt.prodMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {a : α} {b : β},
  Function.IsFixedPt f a → Function.IsFixedPt g b → Function.IsFixedPt (Prod.map f g) (a, b)
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.disjoint_smul_left : ∀ {M : Type u_1} {X : Type u_2} [inst : Monoid M] [inst_1 : MulAction M X] {B : Set X} {s : Set M},
  MulAction.IsBlock M B → ¬B ⊆ s • B → Disjoint (s • B) B
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constAddHom.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : Add β], Pi.constAddHom α β = { toFun := Function.const α, map_add' := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.mem_lrat_of_mem : ∀ {n : ℕ} {l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)}
  {lratClause : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n}
  (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  l ∈ clause →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray (List.toArray clause) = some lratClause →
      l ∈ lratClause.clause
-- Mathlib.RingTheory.SimpleModule.Basic
isSemisimpleModule_of_isSemisimpleModule_submodule' : ∀ {ι : Type u_1} {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : ι → Submodule R M}, (∀ (i : ι), IsSemisimpleModule R ↥(p i)) → ⨆ i, p i = ⊤ → IsSemisimpleModule R M
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesLimitsOfShapeSheafTypeYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K],
  CategoryTheory.Limits.PreservesLimitsOfShape K J.yoneda
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (D : CategoryTheory.ComposableArrows ι 2),
  X.ω₂.obj D ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Data.Rel
SetRel.core_union_subset : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t₁ t₂ : Set β}, R.core t₁ ∪ R.core t₂ ⊆ R.core (t₁ ∪ t₂)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The canonical map from `TensorAlgebra R M` into `TrivSqZeroExt R M` that sends
`TensorAlgebra.ι` to `TrivSqZeroExt.inr`.  -/
TensorAlgebra.toTrivSqZeroExt : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] → [inst_4 : IsCentralScalar R M] → TensorAlgebra R M →ₐ[R] TrivSqZeroExt R M
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquivClass.toAddEquiv_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : AddEquivClass F α β], Function.Injective AddEquivClass.toAddEquiv
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_lt_cons_iff : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, a ::ₘ s < a ::ₘ t ↔ s < t
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'_hom_app_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] {U : Set ↥X},
  IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(X.basicOpen i)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.instDecidableEqPartition : {n : ℕ} → DecidableEq n.Partition
-- Mathlib.Data.List.Sigma
List.dlookup_map₂ : ∀ {α : Type u} [inst : DecidableEq α] {γ : α → Type u_1} {δ : α → Type u_2} {l : List ((a : α) × γ a)}
  {f : (a : α) → γ a → δ a} (a : α), List.dlookup a (List.map (Sigma.map id f) l) = Option.map (f a) (List.dlookup a l)
-- Mathlib.Algebra.Regular.Basic
/-- Two elements `a` and `b` are regular if and only if both products `a * b` and `b * a`
are regular.  -/
isRegular_mul_and_mul_iff : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
-- Mathlib.Data.Finset.NAry
Finset.image₂_nonempty_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (Finset.image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.repFn : ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulCommClassAddMonoidHom : ∀ {A : Type u_5} {B : Type u_6} {M : Type u_7} {M' : Type u_8} [inst : AddMonoid A] [inst_1 : DistribSMul M A]
  [inst_2 : AddZeroClass B] [inst_3 : DistribSMul M' A] [SMulCommClass M M' A], SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+ B)
-- Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Set.mem_list_sum : ∀ {α : Type u_1} [inst : AddMonoid α] {l : List (Set α)} {a : α},
  a ∈ l.sum ↔ ∃ l', (List.map (fun x => ↑x.snd) l').sum = a ∧ List.map Sigma.fst l' = l
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.contDiffWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E} {n : ℕ∞} {s : Set E}, ContDiffWithinAt ℝ (↑n) (↑f) s x
-- Init.GrindInstances.Ring.UInt
UInt32.ofInt.eq_1 : ∀ (x : ℤ), UInt32.ofInt x = UInt32.ofNat (x % 2 ^ 32).toNat
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictAnti.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α}, StrictAnti f → StrictMono fun x => -f x
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The linearization of a type `X` on which `G` acts trivially is the trivial `G`-representation
on `k[X]`.  -/
Rep.linearizationTrivialIso : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (X : Type u) → (Rep.linearization k G).obj (Action.trivial G X) ≅ Rep.trivial k G (MonoidAlgebra k X)
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.prod_ne_zero_iff : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀]
  [NoZeroDivisors M₀], ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
/-- If `T` is a triangle in `CochainComplex C ℤ`, this is the connecting homomorphism
`T.obj₃.homology n₀ ⟶ T.obj₁.homology n₁` in homology when `n₀ + 1 = n₁`.  -/
CochainComplex.homologyδOfTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) →
        (n₀ n₁ : ℤ) →
          autoParam (n₀ + 1 = n₁) CochainComplex.homologyδOfTriangle._auto_1 →
            (HomologicalComplex.homology T.obj₃ n₀ ⟶ HomologicalComplex.homology T.obj₁ n₁)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The identity isomorphism of a graph with itself.  -/
SimpleGraph.Iso.refl : {V : Type u_1} → {G : SimpleGraph V} → G ≃g G
-- Lean.Data.KVMap
Lean.KVMap.instValueName : Lean.KVMap.Value Lean.Name
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A measure on a countable space is sigma-finite iff it gives finite mass to every singleton.

See `measure_singleton_lt_top` for the forward direction without the countability assumption.  -/
MeasureTheory.Measure.sigmaFinite_iff_measure_singleton_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable α],
  MeasureTheory.SigmaFinite μ ↔ ∀ (a : α), μ {a} < ⊤
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.addRight_add : ∀ {X : Type u_6} [inst : AddSemigroup X] [inst_1 : TopologicalSpace X] [inst_2 : SeparatelyContinuousAdd X] (x y : X),
  ContinuousMap.addRight (x + y) = (ContinuousMap.addRight y).comp (ContinuousMap.addRight x)
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that
each `γ a` is defined on `Ioo (-a) a`, the function `γ_ext := fun t ↦ γ (|t| + 1) t` is a global
integral curve.  -/
isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {x : M} (γ : ℝ → ℝ → M),
      (∀ (a : ℝ), γ a 0 = x) →
        (∀ a > 0, IsMIntegralCurveOn (γ a) v (Set.Ioo (-a) a)) → IsMIntegralCurve (fun t => γ (|t| + 1) t) v
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The family of objects `A x.i` parametrized by `x : FunctorObjIndex f πX`.  -/
CategoryTheory.SmallObject.functorObjSrcFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) → {S X : C} → (πX : X ⟶ S) → CategoryTheory.SmallObject.FunctorObjIndex f πX → C
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedBall x)
-- Init.Prelude
Fin.val_eq_of_eq : ∀ {n : ℕ} {i j : Fin n}, i = j → ↑i = ↑j
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverseOpEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q), CliffordAlgebra.reverseOpEquiv a = CliffordAlgebra.reverseOp a
-- Lean.Util.CollectAxioms
/-- Extension state holding imported module entries for efficient lookup of
pre-computed axiom data.

We use `registerPersistentEnvExtension` with manual lookup instead of `MapDeclarationExtension`
because `exportEntriesFnEx` needs to call `collect`, which needs the extension's `find?`, but
`exportEntriesFnEx` is defined inside the `builtin_initialize` that creates the extension and
thus cannot reference it. This state replicates `MapDeclarationExtension.find?`'s per-module
binary search without requiring the extension object.
 -/
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState : Type
-- Mathlib.Topology.Instances.NNReal.Lemmas
ENNReal.iSup_pow_of_ne_zero : ∀ {ι : Sort u_1} {n : ℕ}, n ≠ 0 → ∀ (f : ι → ENNReal), (⨆ i, f i) ^ n = ⨆ i, f i ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_incl_app : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (x : ℕ),
  (SSet.relativeCellComplexOfMono i).incl.app x = (⋯.functor.obj x).ι
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_eq_covariance : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E),
      ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ = ProbabilityTheory.covariance (⇑L₁) (⇑L₂) μ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mk.inj : ∀ {A : Type u_2} {B : Type u_3} {inst : Monoid A} {inst_1 : Monoid B} {inst_2 : TopologicalSpace A}
  {inst_3 : TopologicalSpace B} {toMonoidHom : A →* B}
  {continuous_toFun : autoParam (Continuous (↑toMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam}
  {toMonoidHom_1 : A →* B}
  {continuous_toFun_1 : autoParam (Continuous (↑toMonoidHom_1).toFun) ContinuousMap.continuous_toFun._autoParam},
  { toMonoidHom := toMonoidHom, continuous_toFun := continuous_toFun } =
      { toMonoidHom := toMonoidHom_1, continuous_toFun := continuous_toFun_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.id.eq_1 : Nat.Partrec.Code.id = Nat.Partrec.Code.left.pair Nat.Partrec.Code.right
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_inv`. -/
MonovaryOn.of_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f⁻¹ g⁻¹ s → MonovaryOn f g s