mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.instAbelianOpposite : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Abelian C] → CategoryTheory.Abelian Cᵒᵖ
-- Mathlib.Algebra.Order.Hom.Basic
MulLEAddHomClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Mul α] [inst_1 : Add β] [inst_2 : LE β]
  [inst_3 : FunLike F α β], (∀ (f : F) (a b : α), f (a * b) ≤ f a + f b) → MulLEAddHomClass F α β
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.size.eq_2 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.size = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_insertRatUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  ∀ c ∈ (f.insertRatUnits units).1.toList,
    c ∈ List.map Std.Tactic.BVDecide.LRAT.Internal.Clause.unit units ∨ c ∈ f.toList
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inl_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Function.Injective ⇑Monoid.Coprod.inl
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.le_succFn : ∀ {ι : Type u_1} [inst : LinearOrder ι] (i : ι), i ≤ LinearLocallyFiniteOrder.succFn i
-- Mathlib.RingTheory.Ideal.Basic
Ideal.instFinite : ∀ {K : Type u_5} [inst : DivisionSemiring K], Finite (Ideal K)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `norm_zero`.  -/
hammingNorm_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)], hammingNorm 0 = 0
-- Lean.Meta.Sym.Arith.MonadCanon
Lean.Meta.Sym.Arith.instMonadCanonOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Meta.Sym.Arith.MonadCanon n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_union_of_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Mathlib.Order.RelSeries
RelSeries.last_eraseLast : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.eraseLast.last = p.toFun ⟨p.length.pred, ⋯⟩
-- Lean.Elab.Command.Scope
/-- The current list of binders to use for new declarations.
This is managed by the `variable` command.
Each binder is represented in `Syntax` form, and it is re-elaborated
within each command that uses this information.

This is also used by commands, such as `#check`, to create an initial local context,
even if they do not work with binders per se.
 -/
Lean.Elab.Command.Scope.varDecls : Lean.Elab.Command.Scope → Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.instMonoidalCategoryStruct : {R : Type u} → [inst : CommSemiring R] → CategoryTheory.MonoidalCategoryStruct (SemimoduleCat R)
-- Lean.SubExpr
Lean.instInhabitedSubExpr : Inhabited Lean.SubExpr
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- `FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  -/
FiniteDimensional : (K : Type u_1) → (V : Type u_2) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Prop
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.inv_bind : ∀ {α β : Type u} (f : α → FreeGroup β) (x : FreeGroup α), x⁻¹ >>= f = (x >>= f)⁻¹
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mem_support_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.degree f ∈ f.support ↔ f ≠ 0
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative groups is faithful.  -/
CommGrpCat.instFaithfulUliftFunctor : CommGrpCat.uliftFunctor.Faithful
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ}
  (h : Opposite.op (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j).op h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.rightOp (Opposite.unop j)) h
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_apply_prime_pow : ∀ {p k : ℕ}, Nat.Prime p → k ≠ 0 → ArithmeticFunction.moebius (p ^ k) = if k = 1 then -1 else 0
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  ((CategoryTheory.Idempotents.toKaroubi C).obj X).decompId_i =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi C).obj X)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- A family of inner product space structures on the fibers of a fiber bundle, defining the same
topology as the already existing one, and varying continuously with the base point. See also
`ContinuousRiemannianMetric` for a continuous version.

This structure is used through `RiemannianBundle` for typeclass inference, to register the inner
product space structure on the fibers without creating diamonds.  -/
Bundle.ContMDiffRiemannianMetric : {EB : Type u_1} →
  [inst : NormedAddCommGroup EB] →
    [inst_1 : NormedSpace ℝ EB] →
      {HB : Type u_2} →
        [inst_2 : TopologicalSpace HB] →
          ModelWithCorners ℝ EB HB →
            WithTop ℕ∞ →
              {B : Type u_3} →
                [inst : TopologicalSpace B] →
                  [ChartedSpace HB B] →
                    (F : Type u_4) →
                      [inst_4 : NormedAddCommGroup F] →
                        [inst_5 : NormedSpace ℝ F] →
                          (E : B → Type u_5) →
                            [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                              [inst_7 : (b : B) → TopologicalSpace (E b)] →
                                [inst_8 : (b : B) → AddCommGroup (E b)] →
                                  [inst_9 : (b : B) → Module ℝ (E b)] →
                                    [inst_10 : FiberBundle F E] → [VectorBundle ℝ F E] → Type (max u_3 u_5)
-- Init.Data.Nat.Div.Basic
Nat.mod_le : ∀ (x y : ℕ), x % y ≤ x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The induced subgraph of a subgraph. The expectation is that `s ⊆ G'.verts` for the usual
notion of an induced subgraph, but, in general, `s` is taken to be the new vertex set and edges
are induced from the subgraph `G'`.  -/
SimpleGraph.Subgraph.induce : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set V → G.Subgraph
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inl_comp_pushoutObjIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D)
  {Z : C} (h : (CategoryTheory.Limits.pushout f g).obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (f.app d) (g.app d))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutObjIso f g d).inv h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pushout.inl f g).app d) h
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂RingHom_comp_C : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x : S),
  (Polynomial.eval₂RingHom f x).comp Polynomial.C = f
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitz.sub : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => f x - g x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.coe_toHomeomorph_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ+ N), (↑f).symm = ↑f.symm
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_of_forall_one_lt_lt_mul' : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α]
  {a b : α}, (∀ (ε : α), 1 < ε → a < b * ε) → a ≤ b
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars_le_iff : ∀ {L : Type u_2} [inst : Field L] {F E : Subfield L} (h : F ≤ E) (E' : IntermediateField (↥F) L),
  Subfield.extendScalars h ≤ E' ↔ E ≤ E'.toSubfield
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_arccos : ∀ {x : ℝ}, 0 ≤ x → Real.arcsin x = Real.arccos √(1 - x ^ 2)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {km : α}, t.min? = some km → t.get! km = km
-- Mathlib.Algebra.Prime.Lemmas
MulEquiv.prime_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : CommMonoidWithZero N] {p : M} {E : Type u_5}
  [inst_2 : EquivLike E M N] [MulEquivClass E M N] (e : E), Prime (e p) ↔ Prime p
-- Mathlib.Algebra.Ring.Parity
Function.Involutive.iterate_odd : ∀ {α : Type u_4} {f : α → α} {n : ℕ}, Function.Involutive f → Odd n → f^[n] = f
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.ringCon.eq_1 : ∀ (R : Type u_2) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  DividedPowerAlgebra.ringCon R M = ringConGen (DividedPowerAlgebra.Rel R M)
-- Mathlib.Computability.Language
/-- A "proxy type" equivalent to `Symbol` that is constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. See `Symbol.proxyTypeEquiv` for the equivalence. (Generated by the `proxy_equiv%` elaborator.) -/
Symbol.proxyType : Type u_4 → Type u_5 → Type (max u_4 u_5)
-- Lean.Exception
/-- Error messages that are displayed to users. `ref` is used to provide position information.  -/
Lean.Exception.error : Lean.Syntax → Lean.MessageData → Lean.Exception
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- Let `J` be a precoverage for which isomorphisms are local at the target. Let
`f, g : X ⟶ Y` be two morphisms over `S` and `𝒰` a `J`-cover of `S`.
If for all `i`, the maps `X ×[S] Uᵢ ⟶ Y ×[S] Uᵢ` are equal, then
`f` and `g` are equal.  -/
CategoryTheory.eq_of_zeroHypercover_target : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s)
  {J : CategoryTheory.Precoverage C} (𝒰 : J.ZeroHypercover S) [J.IsStableUnderBaseChange]
  [(CategoryTheory.MorphismProperty.isomorphisms C).IsLocalAtTarget J],
  (∀ (i : 𝒰.I₀),
      CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) f (CategoryTheory.CategoryStruct.id (𝒰.X i))
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ =
        CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) g (CategoryTheory.CategoryStruct.id (𝒰.X i))
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) →
    f = g
-- Mathlib.Order.Filter.Extr
IsMaxOn.add : ∀ {α : Type u} {β : Type v} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {s : Set α}, IsMaxOn f s a → IsMaxOn g s a → IsMaxOn (fun x => f x + g x) s a
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfLEZero.eq_1 : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i)
  (hi₂ : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i),
  s.toMeasureOfLEZero i hi₁ hi₂ = (-s).toMeasureOfZeroLE i hi₁ ⋯
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_b : ∀ {u : PNat.XgcdType}, u.r ≠ 0 → u.reduce = u.step.reduce.flip
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `addAfterImports fname s` returns the content of the file `fname`, with the string `s` added
after the imports of `fname`.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.addAfterImports : String → String → Lean.Elab.Command.CommandElabM String
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wDest'_wMk : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f' : (P.drop.B a).Arrow α)
  (f : P.last.B a → P.W α), P.wDest' (P.wMk a f' f) = ⟨a, TypeVec.splitFun f' f⟩
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.degBound.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} (e : ChevalleyThm.PolynomialC.InductionObj✝ R n),
  ChevalleyThm.PolynomialC.InductionObj.degBound✝ e = ∑ i, (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).degree.succ
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.instIsCardinalAccessibleId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  (CategoryTheory.Functor.id C).IsCardinalAccessible κ
-- Mathlib.Topology.Filter
Filter.instT0Space : ∀ {α : Type u_2}, T0Space (Filter α)
-- Batteries.Lean.AttributeExtra
Lean.instInhabitedTagAttributeExtra.default : Lean.TagAttributeExtra
-- Init.Tactics
/-- The `⊢` location refers to the current goal.  -/
Lean.Parser.Tactic.locationType : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.Closeds
union_mem_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α) {s₁ s₂ t₁ t₂ : Set α},
  (s₁, t₁) ∈ hausdorffEntourage U → (s₂, t₂) ∈ hausdorffEntourage U → (s₁ ∪ s₂, t₁ ∪ t₂) ∈ hausdorffEntourage U
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms in an
abelian category, this is the long exact sequence
`0 ⟶ ker f ⟶ ker (f ≫ g) ⟶ ker g ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0`.  -/
CategoryTheory.kernelCokernelCompSequence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → {X Y Z : C} → (X ⟶ Y) → (Y ⟶ Z) → CategoryTheory.ComposableArrows C 5
-- Mathlib.Data.Set.Countable
/-- If a family of disjoint sets is included in a countable set, then only countably many of
them are nonempty.  -/
Set.countable_ofPred_nonempty_of_disjoint : ∀ {α : Type u} {β : Type v} {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) →
    ∀ {s : Set α}, (∀ (t : β), f t ⊆ s) → s.Countable → {t | (f t).Nonempty}.Countable
-- Mathlib.Data.ZMod.QuotientGroup
/-- `ℤ` modulo multiples of `n : ℕ` is `ZMod n`.  -/
Int.quotientZMultiplesNatEquivZMod : (n : ℕ) → ℤ ⧸ AddSubgroup.zmultiples ↑n ≃+ ZMod n
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso_hom : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 = 0),
  (CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).hom =
    CategoryTheory.CategoryStruct.comp
      ((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).hom) (e.hom.app (X a.1))
-- Mathlib.Topology.Sober
/-- The generic point of an irreducible component.  -/
genericPoints.ofComponent : {α : Type u_1} → [inst : TopologicalSpace α] → [QuasiSober α] → ↑(irreducibleComponents α) → ↑(genericPoints α)
-- Mathlib.Data.Fin.SuccPred
Fin.sub_castLT_eq_castLT_sub_of_le : ∀ {n m : ℕ} {a b : Fin m} (ha : ↑a < n) (h : b ≤ a), a.castLT ha - b.castLT ⋯ = (a - b).castLT ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.p : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Int.Internal.Linear.Poly
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.mul.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst_1 : CommMonoid N],
  MonoidHom.mul = { mul := fun f g => { toFun := fun m => f m * g m, map_one' := ⋯, map_mul' := ⋯ } }
-- Lean.Level
_private.Lean.Level.0.Lean.Level.find?.visit : (Lean.Level → Bool) → Lean.Level → Option Lean.Level
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.map_f' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).f' = F.map h.f'
-- Lean.Level
Lean.Level.ofNat : ℕ → Lean.Level
-- Mathlib.Data.Set.Prod
Set.mapsTo_fst_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, Set.MapsTo Prod.fst (s ×ˢ t) s
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableAt.coordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
  [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} {g : M → F} {x : M},
  MDiffAt f x → MDiffAt g x → f x ∈ e.baseSet → f x ∈ e'.baseSet → (MDiffAt fun y => e.coordChange e' (f y) (g y)) x
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.add.injEq : ∀ (a b a_1 b_1 : Nat.Internal.SOM.Expr), (a.add b = a_1.add b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.Data.Complex.Basic
/-- Complex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  -/
termℂ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.alternatingMapLinearEquiv_comp_ιMulti : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M [⋀^Fin n]→ₗ[R] N),
  (exteriorPower.alternatingMapLinearEquiv f).compAlternatingMap (exteriorPower.ιMulti R n) = f
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- This holds for `0 < x, y ≤ 1` due to junk values.  -/
Real.arcosh_le_arcosh : ∀ {x y : ℝ}, 0 < x → 0 < y → (Real.arcosh x ≤ Real.arcosh y ↔ x ≤ y)
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instNoZeroDivisors : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [NoZeroDivisors α], NoZeroDivisors (WithBot α)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.localization_comap_range : ∀ {R : Type u} (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Submonoid R)
  [IsLocalization M S], Set.range (PrimeSpectrum.comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}
-- Mathlib.Data.Sigma.Lex
Sigma.Lex.mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop},
  (∀ (a b : ι), r₁ a b → r₂ a b) →
    (∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) → ∀ {a b : (i : ι) × α i}, Sigma.Lex r₁ s₁ a b → Sigma.Lex r₂ s₂ a b
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by subtracting a constant value to both the lower and upper bounds.
 -/
Std.Time.Internal.Bounded.LE.sub : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → Std.Time.Internal.Bounded.LE (n - num) (m - num)
-- Mathlib.Util.Superscript
/-- Applies the alignment mapping to a `SourceInfo`.  -/
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignInfo : Lean.Parser.ParserContext → Array (String.Pos.Raw × String.Pos.Raw) → Lean.SourceInfo → Lean.SourceInfo
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_head?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.min? = t.toList.head?
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
UniqueMDiffWithinAt.preimage_openPartialHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M},
  UniqueMDiffAt[s] x →
    ∀ {e : OpenPartialHomeomorph M M'},
      OpenPartialHomeomorph.MDifferentiable I I' e → x ∈ e.source → UniqueMDiffAt[e.target ∩ ↑e.symm ⁻¹' s] (↑e x)
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the day of the month to the given `days` value, with any
out-of-range days rolled over to the next month or year as needed.
 -/
Std.Time.PlainDateTime.withDaysRollOver : Std.Time.PlainDateTime → Std.Time.Day.Ordinal → Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_inverseImage_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D), (P.inverseImage F).strictMap F ≤ P
-- Lean.ReservedNameAction
/-- Similar to `realizeGlobalConstNoOverload`, but also executes reserved name actions.

Consider using `realizeGlobalConstNoOverloadWithInfo` if you want the syntax to show the resulting
name's info on hover.
 -/
Lean.realizeGlobalConstNoOverload : Lean.Syntax → Lean.CoreM Lean.Name
-- Lean.Meta.Tactic.Grind.CheckResult
/-- Result type for satisfiability checking procedures.
 -/
Lean.Meta.Grind.CheckResult : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k k' : α}, compare k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {fallback : α}
  {hc : t.maxD fallback ∈ t}, t.get (t.maxD fallback) hc = t.maxD fallback
-- Init.Data.SInt.Basic
/-- Subtracts one 8-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.sub : Int8 → Int8 → Int8
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (self : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) {i j : J} {f : i ⟶ j},
  self.W f → self.P i
-- Lean.Parser.Attr
Lean.Parser.Attr.extern.formatter : Lean.PrettyPrinter.Formatter