mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The bijection of `Cotrident.IsColimit.homIso` is natural in `Z`.  -/
CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {t : CategoryTheory.Limits.Cotrident f} {Z Z' : C} (q : Z ⟶ Z') (ht : CategoryTheory.Limits.IsColimit t)
  (k : t.pt ⟶ Z),
  ↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) =
    CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k)) q
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelSemigroup α],
  Colex.instAddLeftCancelSemigroup = { toAddSemigroup := Colex.instAddSemigroup, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- An absolute value `w` of `L / K` lies over the absolute value `v` of `K` if `v` is the
restriction of `w` to `K`.  -/
AbsoluteValue.LiesOver : {K : Type u_3} →
  {L : Type u_4} →
    {S : Type u_5} →
      [inst : CommRing K] →
        [IsSimpleRing K] →
          [inst_2 : CommRing L] →
            [Algebra K L] →
              [inst_4 : PartialOrder S] →
                [Nontrivial L] → [inst_6 : Semiring S] → AbsoluteValue L S → AbsoluteValue K S → Prop
-- Mathlib.Algebra.Polynomial.RuleOfSigns
Polynomial.signVariations_zero : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : LinearOrder R], Polynomial.signVariations 0 = 0
-- Lean.Data.AssocList
Lean.instInhabitedAssocList : {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Lean.AssocList a a_1)
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function within
this set is bounded by `C`, then the function is `C`-Lipschitz. Version with `derivWithin`  -/
Convex.norm_image_sub_le_of_norm_derivWithin_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜} {x y : 𝕜} {C : ℝ},
  DifferentiableOn 𝕜 f s → (∀ x ∈ s, ‖derivWithin f s x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.selectionRange : Lean.Lsp.CallHierarchyItem → Lean.Lsp.Range
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instMul : {G : Type u_1} → [inst : Add G] → {a : G} → Mul (AddConstMap G G a a)
-- Batteries.Lean.NameMapAttribute
Lean.instInhabitedNameMapAttributeImpl : {a : Type} → Inhabited (Lean.NameMapAttributeImpl a)
-- Lean.Parser.Syntax
Lean.Parser.Command.elabArg.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.lt_def : ∀ {E : Type u_3} [inst : Group E] {p q : GroupNorm E}, p < q ↔ ⇑p < ⇑q
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGTHAddIntOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C), t.IsGE ((t.truncGT n).obj X) (n + 1)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.isEmpty.eq_1 : ∀ (ss : Substring.Raw), ss.isEmpty = (ss.bsize == 0)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instSupSet : {V : Type u} → {G : SimpleGraph V} → SupSet G.Subgraph
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.isIso_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  CategoryTheory.Limits.IsZero (S.X₂.homology i) →
    CategoryTheory.Limits.IsZero (S.X₂.homology j) → CategoryTheory.IsIso (hS.δ i j hij)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.repr_eq_single : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v) (i : ι) (x : ↥(Submodule.span R (Set.range v))),
  ↑x = v i → hv.repr x = fun₀ | i => 1
-- Mathlib.Order.Closure
ClosureOperator.conjBy_refl : ∀ {α : Type u_4} [inst : Preorder α] (c : ClosureOperator α), c.conjBy (OrderIso.refl α) = c
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hasForgetToAddCommMonCat.eq_1 : AddCommGrpCat.hasForgetToAddCommMonCat =
  {
    forget₂ :=
      { obj := fun X => AddCommMonCat.of ↑X, map := fun {X Y} f => AddCommMonCat.ofHom (AddCommGrpCat.Hom.hom f),
        map_id := AddCommGrpCat.hasForgetToAddCommMonCat._proof_1,
        map_comp := @AddCommGrpCat.hasForgetToAddCommMonCat._proof_2 },
    forget_comp := AddCommGrpCat.hasForgetToAddCommMonCat._proof_4 }
-- Init.Meta.Defs
Lean.Name.instRepr : Repr Lean.Name
-- Init.Data.List.Lemmas
List.isEmpty_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β}, (List.map f l).isEmpty = l.isEmpty
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.rightPadAscii : ℕ → Char → String → String
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult.finset : BigOperators.FinsetFilterResult✝ → BigOperators.FinsetResult✝
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.CommGrpCat.Hom.mk : {A B : CommGrpCat} → (↑A →* ↑B) → A.Hom B
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_eq_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {a : α}, t.get? a = t[a]?
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ofClass_symm_apply : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B]
  [inst_4 : EquivLike F A B] [inst_5 : MulEquivClass F A B] [inst_6 : StarHomClass F A B] (f : F) (a : B),
  (StarMulEquiv.ofClass f).symm a = EquivLike.inv f a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- Star algebra homomorphisms commute with the continuous functional calculus.
This version is specialized to `A →⋆ₐ[S] B` to allow for dot notation.  -/
StarAlgHom.map_cfc : ∀ {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [inst : CommSemiring R]
  [inst_1 : StarRing R] [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R]
  [inst_5 : Ring A] [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : Ring B]
  [inst_10 : StarRing B] [inst_11 : TopologicalSpace B] [inst_12 : Algebra R B] [inst_13 : CommSemiring S]
  [inst_14 : Algebra R S] [inst_15 : Algebra S A] [inst_16 : Algebra S B] [IsScalarTower R S A] [IsScalarTower R S B]
  [inst_19 : ContinuousFunctionalCalculus R A p] [inst_20 : ContinuousFunctionalCalculus R B q]
  [ContinuousMap.UniqueHom R B] (φ : A →⋆ₐ[S] B) (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) StarAlgHom.map_cfc._auto_1 →
    autoParam (Continuous ⇑φ) StarAlgHom.map_cfc._auto_3 →
      autoParam (p a) StarAlgHom.map_cfc._auto_5 →
        autoParam (q (φ a)) StarAlgHom.map_cfc._auto_7 → φ (cfc f a) = cfc f (φ a)
-- Lean.Elab.Match
Lean.Elab.Term.Discr.mk.inj : ∀ {expr : Lean.Expr} {h? : Option Lean.Syntax} {expr_1 : Lean.Expr} {h?_1 : Option Lean.Syntax},
  { expr := expr, h? := h? } = { expr := expr_1, h? := h?_1 } → expr = expr_1 ∧ h? = h?_1
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_π_three : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨3, SSet.horn₃₁.desc.multicofork_π_three._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 3).inv f₃
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- If a graph is locally finite at a vertex, then so is a subgraph of that graph.  -/
SimpleGraph.Subgraph.finiteAt : {V : Type u} →
  {G : SimpleGraph V} →
    {G' : G.Subgraph} →
      (v : ↑G'.verts) → [DecidableRel G'.Adj] → [Fintype ↑(G.neighborSet ↑v)] → Fintype ↑(G'.neighborSet ↑v)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The trivial additive monoid object. We later show this is initial in `AddMon C`  -/
CategoryTheory.AddMon.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.AddMon C
-- Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
CategoryTheory.Projective.hasLiftingProperty_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Z P X Y : C} (i : Z ⟶ P) (p : X ⟶ Y) [CategoryTheory.Epi p]
  [CategoryTheory.Projective P], CategoryTheory.Limits.IsZero Z → CategoryTheory.HasLiftingProperty i p
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom.inj : ∀ {α α_1 : Mathlib.Tactic.BicategoryLike.CoherenceHom},
  Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α_1 →
    α = α_1
-- Mathlib.Algebra.Star.LinearMap
Module.End.isUnit_intrinsicStar_iff : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : InvolutiveStar R] [inst_2 : AddCommMonoid E]
  [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E] {f : WithConv (Module.End R E)},
  IsUnit (star f).ofConv ↔ IsUnit f.ofConv
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabSyntheticHole : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- A monoidal functor `F : C ⥤ (D ⥤ D)ᴹᵒᵖ` can be thought of as a left action
of `C` on `D`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) →
            [F.Monoidal] → CategoryTheory.MonoidalCategory.MonoidalLeftAction C D
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_injective : ∀ {M : Type u_1} [inst : AddMonoid M], Function.Injective AddSubgroup.ofAddUnits
-- Mathlib.Algebra.Divisibility.Basic
dvd_of_eq : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ b
-- Aesop.Rule.Basic
Aesop.Rule.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (name : Aesop.RuleName) (indexingMode : Aesop.IndexingMode)
  (pattern? : Option Aesop.RulePattern) (extra : α) (tac : Aesop.RuleTacDescr),
  sizeOf { name := name, indexingMode := indexingMode, pattern? := pattern?, extra := extra, tac := tac } =
    1 + sizeOf name + sizeOf indexingMode + sizeOf pattern? + sizeOf extra + sizeOf tac
-- Init.Data.List.Basic
List.Pairwise.brecOn : ∀ {α : Type u} {R : α → α → Prop} {motive : (a : List α) → List.Pairwise R a → Prop} {a : List α}
  (t : List.Pairwise R a), (∀ (a : List α) (t : List.Pairwise R a), List.Pairwise.below t → motive a t) → motive a t
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- `m ^ (period m a)` fixes `a`.  -/
MulAction.pow_period_smul : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α), m ^ MulAction.period m a • a = a
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃)
  (g : M₁ →ₛₗ[σ₁₂] M₂), ⇑(f ∘ₛₗ g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Order.Round
round_le_add_half : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α),
  ↑(round x) ≤ x + 1 / 2
-- Mathlib.Algebra.Notation.Indicator
Set.comp_mulIndicator_const : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] {s : Set α} (c : M) (f : M → N),
  f 1 = 1 → (fun x => f (s.mulIndicator (fun x => c) x)) = s.mulIndicator fun x => f c
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- `χ` of level `n` factors through a Dirichlet character `χ₀` of level `d` if `d ∣ n` and
`χ₀ = χ ∘ (ZMod n → ZMod d)`.  -/
DirichletCharacter.FactorsThrough : {R : Type u_1} → [inst : CommMonoidWithZero R] → {n : ℕ} → DirichletCharacter R n → ℕ → Prop
-- Mathlib.Data.Real.ConjExponents
/-- useful for introducing all three facts simultaneously within a proof.  -/
Real.HolderTriple.all_pos : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < p ∧ 0 < q ∧ 0 < r
-- Init.Data.ToString.Basic
instToStringId_1 : {α : Type u_1} → [ToString α] → ToString (Id α)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.top_prod_top : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N], ⊤.prod ⊤ = ⊤
-- Lean.Server.Utils
Lean.Server.instInhabitedDocumentMeta : Inhabited Lean.Server.DocumentMeta
-- Mathlib.RingTheory.MatrixAlgebra
matrixEquivTensor_apply_symm : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (a : A) (M : Matrix n n R),
  (matrixEquivTensor n R A).symm (a ⊗ₜ[R] M) = a • M.map ⇑(algebraMap R A)
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.iterate : ∀ {α : Type u_1} {f : α → α} {l : Filter α}, Filter.Tendsto f l l → ∀ (n : ℕ), Filter.Tendsto f^[n] l l
-- Mathlib.Topology.Algebra.Support
exists_compact_iff_hasCompactMulSupport : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} [R1Space α],
  (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
-- Mathlib.Tactic.HaveI
/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term.

(This is the do-notation version of the term-mode `haveI`.)
 -/
Mathlib.Tactic.HaveI.doElemLetI'_ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.mono_ae : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u v : Set α},
  MeasureTheory.AEDisjoint μ s t → u ≤ᵐ[μ] s → v ≤ᵐ[μ] t → MeasureTheory.AEDisjoint μ u v
-- Mathlib.Tactic.Translate.Core
/-- Linter used by translate attributes that checks if the `relevant_arg` is
automatically generated.  -/
Mathlib.Tactic.Translate.linter.translateRelevantArg : Lean.Option Bool
-- Mathlib.Algebra.Group.Action.End
/-- Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of `MulAction.toPerm`.  -/
MulDistribMulAction.toMulEquiv : {G : Type u_1} → (M : Type u_2) → [inst : Group G] → [inst_1 : Monoid M] → [MulDistribMulAction G M] → G → M ≃* M
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.whiskerLeft₂_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u_1} {B : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} A]
  [inst_3 : CategoryTheory.Category.{v_2, u_2} B] (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D)
  (F : CategoryTheory.Functor A C) (G : CategoryTheory.Functor B D) (X : A) (X_1 : Bᵒᵖ),
  ((P.whiskerLeft₂ F G).obj X).obj X_1 = (P.obj (F.obj X)).obj (Opposite.op (G.obj (Opposite.unop X_1)))
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonLeanServerCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.LeanServerCapabilities
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The type of homomorphisms between two pointed Galois objects. This is a homomorphism
of the underlying objects of `C` that maps the distinguished points to each other.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        CategoryTheory.PreGaloisCategory.PointedGaloisObject F →
          CategoryTheory.PreGaloisCategory.PointedGaloisObject F → Type u₂
-- Init.Sym.Lemmas
Lean.Sym.UInt64.le_eq_true : ∀ (a b : UInt64), decide (a ≤ b) = true → (a ≤ b) = True
-- Lean.Data.Json.FromToJson.Basic
Lean.ToJson.toJson : {α : Type u} → [self : Lean.ToJson α] → α → Lean.Json
-- Mathlib.Topology.Category.Sequential
Sequential.mk.injEq : ∀ (toTop : TopCat) [is_sequential : SequentialSpace ↑toTop] (toTop_1 : TopCat)
  (is_sequential_1 : SequentialSpace ↑toTop_1),
  ({ toTop := toTop, is_sequential := is_sequential } = { toTop := toTop_1, is_sequential := is_sequential_1 }) =
    (toTop = toTop_1)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.unopFunctorCompSnd_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op),
  (CategoryTheory.Comma.unopFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_mul_unit_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z)
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurve.isMIntegralCurveAt : ∀ {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] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v → ∀ (t : ℝ), IsMIntegralCurveAt γ v t
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.laplacian_eq_fourierMultiplierCLM : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (f : TemperedDistribution E F),
  Laplacian.laplacian f = -(2 * Real.pi) ^ 2 • (TemperedDistribution.fourierMultiplierCLM F fun x => ↑(‖x‖ ^ 2)) f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : CategoryTheory.MonObj X], CategoryTheory.IsMonHom (CategoryTheory.CategoryStruct.id X)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedKey.default : Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_finset_product₃ : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {γ : Type u_7} (s : Finset (α × β × γ))
  (f : α × β × γ → M),
  ∑ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∑ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sum_fun_sum' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι}
  [MeasureTheory.IsFiniteMeasure μ] {ι' : Type u_3} {Y : ι' → Ω → ℝ} {t : Finset ι'},
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    (∀ i ∈ t, MeasureTheory.MemLp (Y i) 2 μ) →
      ProbabilityTheory.covariance (fun ω => ∑ i ∈ s, X i ω) (fun ω => ∑ j ∈ t, Y j ω) μ =
        ∑ i ∈ s, ∑ j ∈ t, ProbabilityTheory.covariance (X i) (Y j) μ
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.linearIndependent_cols_of_det_ne_zero : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] [IsDomain R]
  {A : Matrix m m R}, A.det ≠ 0 → LinearIndependent R A.col
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.pointCount_le_lineCount : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.HasLines P L] {p : P} {l : L},
  p ∉ l → ∀ [Finite { l // p ∈ l }], Configuration.pointCount P l ≤ Configuration.lineCount L p
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] {A : Type u'}
  [inst_3 : CategoryTheory.Category.{v', u'} A] [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {P P' : CategoryTheory.Functor Cᵒᵖ A} (F : P ⟶ P') {Z : A} (h : P'.obj (Opposite.op (⊤_ C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber.map F)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom
      (CategoryTheory.CategoryStruct.comp (F.app (Opposite.op (⊤_ C))) h)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  (MeasureTheory.Measure.haar.addHaarProduct ↑K₀ ∩ ⋂ V, MeasureTheory.Measure.haar.clAddPrehaar (↑K₀) V).Nonempty
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_add_pi : ∀ (x : ℝ), Real.tan (x + Real.pi) = Real.tan x
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extend the base of a pretrivialization from a set to the whole space.  -/
Bundle.Pretrivialization.codExtend' : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {s : Set B} →
            IsOpen s →
              {proj : Z → ↑s} →
                Bundle.Pretrivialization F proj →
                  [Nonempty (B → F → Z)] → Bundle.Pretrivialization F (Subtype.val ∘ proj)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.mk : Lean.Meta.Sym.Simp.Simproc → Lean.Meta.Sym.Simp.Simproc → Lean.Meta.Sym.Simp.Methods
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.ofSliceFrom_prev : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).startPos},
  String.Slice.Pos.ofSliceFrom (p.prev h) = (String.Slice.Pos.ofSliceFrom p).prev ⋯
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.natTrailingDegree 1 = 0
-- Init.Data.BitVec.Bitblast
BitVec.mul_eq_mulRec : ∀ {w : ℕ} {x y : BitVec w}, x * y = x.mulRec y w
-- Mathlib.Computability.Partrec
Computable.list_getElem? : ∀ {α : Type u_1} [inst : Primcodable α], Computable₂ fun x1 x2 => x1[x2]?
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.instMulRingNormClassReal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], MulRingNormClass (NumberField.FinitePlace K) K ℝ
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.appr.eq_1 : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), x.appr 0 = 0
-- Init.Data.Int.Order
Int.eq_zero_of_sign_eq_zero : ∀ {a : ℤ}, a.sign = 0 → a = 0
-- Mathlib.SetTheory.ZFC.Rank
/-- The ordinal rank of a ZFC set  -/
ZFSet.rank : ZFSet.{u} → Ordinal.{u}
-- Mathlib.GroupTheory.CoprodI
/-- The type of reduced words. A reduced word cannot contain a letter `1`, and no two adjacent
letters can come from the same summand.  -/
Monoid.CoprodI.Word : {ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → Type (max u_1 u_2)