mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.rightUnitor_naturality : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X Y : CategoryTheory.LocalizedMonoidal L W ε} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.LocalizedMonoidal L W ε)))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f
-- Mathlib.Lean.MessageData.ForExprs
/-- Iterate over all the expressions in a `MessageData`. Used to implement
`for (ppCtx, e) in msg.exprs do` notation, which should be preferred over using this declaration
directly.  -/
Lean.MessageData.forExprsIn : {m : Type → Type u} →
  [Monad m] →
    [MonadLiftT BaseIO m] → {σ : Type} → Lean.MessageData → σ → (Lean.PPContext × Lean.Expr → σ → m (ForInStep σ)) → m σ
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
deriv_cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {x : 𝕜},
  DifferentiableAt 𝕜 f x → deriv (fun x => Complex.exp (f x)) x = Complex.exp (f x) * deriv f x
-- Mathlib.NumberTheory.Modular
ModularGroup.fdo_subset_fd : ModularGroup.fdo ⊆ ModularGroup.fd
-- Batteries.Tactic.Alias
/-- The name underlying an alias target  -/
Batteries.Tactic.Alias.AliasInfo.name : Batteries.Tactic.Alias.AliasInfo → Lean.Name
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_δ' : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j) =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (j.pred ⋯)) (SimplexCategory.δ i.castSucc)
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.add : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMinOn f s a → IsLocalMinOn g s a → IsLocalMinOn (fun x => f x + g x) s a
-- Lean.Meta.Sym.SymM
/-- Information on how to build congruence proofs for function applications.
This enables efficient rewriting of subterms without repeatedly inferring types or instances.
 -/
Lean.Meta.Sym.CongrInfo : Type
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.map_le_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  {f g : α →o β}, f ≤ g → c.map f ≤ c.map g
-- Mathlib.Computability.Reduce
OneOneReducible.disjoin_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  q ≤₁ Sum.elim p q
-- Init.Meta.Defs
Lean.Syntax.decodeCharLit : String → Option Char
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivision.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] (f f_1 : PowerSeries A),
  f = f_1 →
    ∀ (g g_1 : PowerSeries A),
      g = g_1 →
        ∀ (q q_1 : PowerSeries A),
          q = q_1 →
            ∀ (r r_1 : Polynomial A),
              r = r_1 →
                ∀ [inst_1 : IsLocalRing A], f.IsWeierstrassDivision g q r = f_1.IsWeierstrassDivision g_1 q_1 r_1
-- Mathlib.Data.List.MinMax
List.argmax_cons : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] (f : α → β) (a : α) (l : List α),
  List.argmax f (a :: l) = Option.casesOn (List.argmax f l) (some a) fun c => if f a < f c then some c else some a
-- Mathlib.Algebra.Order.Module.Defs
PosSMulMono.toPosSMulStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] [inst_5 : Preorder α] [inst_6 : PartialOrder β] [PosSMulMono α β], PosSMulStrictMono α β
-- Mathlib.Data.List.Basic
List.notMem_of_subset : ∀ {α : Type u} {l l₁ : List α}, l ⊆ l₁ → ∀ {a : α}, a ∉ l₁ → a ∉ l
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  (a : A), 0 ≤ a⁻
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting
finset is in `𝒜`.  -/
Finset.mem_upShadow_iff_erase_mem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.upShadow ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instForInProdOfMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForIn m (Std.TreeMap.Raw α β cmp) (α × β)
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The type of open subgroups of a topological group.  -/
OpenSubgroup : (G : Type u_1) → [Group G] → [TopologicalSpace G] → Type u_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.containsThenInsert_snd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.containsThenInsert k v).2 = m.insert k v
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_apply : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M}
  {g : α → M → β →₀ N} {a₂ : β}, (f.sum g) a₂ = f.sum fun a₁ b => (g a₁ b) a₂
-- Init.Data.Array.Find
Array.findIdx?_eq_some_of_exists : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (∃ x ∈ xs, p x = true) → Array.findIdx? p xs = some (Array.findIdx p xs)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.piBinderNames.hygienic : Lean.Option Bool
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.of_ρ : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (X : Type w) [inst_2 : AddCommGroup X]
  [inst_3 : Module k X] (ρ : Representation k G X), (Rep.of ρ).ρ = ρ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.bot_prod_bot : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N], ⊥.prod ⊥ = ⊥
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.mem_prod : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s : AffineSubspace k P) (t : AffineSubspace k Q) (x : P × Q),
  x ∈ s.prod t ↔ x.1 ∈ s ∧ x.2 ∈ t
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.instCoproductsOfShapeDisjointOfFinitaryExtensiveOfFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι],
  CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_by_cases : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a : α} (P : α → Prop), P a → P a⁻¹ → P |a|ₘ
-- Lean.Parser.Term
Lean.Parser.Term.str.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_neg_of_nonneg : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {a : 𝕜}, 0 ≤ a → RCLike.sqrt (-a) = RCLike.I * RCLike.sqrt a
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.nonempty_algHom_extension : ∀ (k : Type u_1) [inst : Field k] [Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [NeZero n] [inst_5 : Algebra (ZMod p) k], Nonempty (k →ₐ[ZMod p] FiniteField.Extension k p n)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.spine_map_subinterval : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1) (j l : ℕ) (h : j + l ≤ m)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := hₘ })),
  X.spine l ⋯
      ((CategoryTheory.ConcreteCategory.hom
          (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.subinterval j l h) ⋯ hₘ).op))
        Δ) =
    (X.spine m hₘ Δ).interval j l h
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.diff.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₁_1 : Std.ExtTreeSet α cmp),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.ExtTreeSet α cmp), t₂ = t₂_1 → t₁.diff t₂ = t₁_1.diff t₂_1
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.one_comp : ∀ {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : One M] (f : α → β), 1 ∘ f = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keysArray_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → γ},
  (Std.TreeMap.Raw.map f t).keysArray = t.keysArray
-- Init.Data.UInt.Lemmas
UInt8.sub_zero : ∀ (a : UInt8), a - 0 = a
-- Std.Sat.AIG.CNF
/-- Keeps track of AIG nodes that we already turned into CNF.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.marks : {aig : Std.Sat.AIG ℕ} → {cnf : Std.Sat.CNF ℕ} → Std.Sat.AIG.toCNF.Cache✝ aig cnf → Array Bool
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The unit of an adjunction.  -/
CategoryTheory.Bicategory.Adjunction.unit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          CategoryTheory.Bicategory.Adjunction f g →
            (CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Topology.Category.TopCat.Sphere
/-- The inclusion `𝔹 n ⟶ 𝔻 n` of the interior of the `n`-disk.  -/
TopCat.ballInclusion : (n : ℕ) → TopCat.ball n ⟶ TopCat.disk n
-- Mathlib.Control.Random
Random.instBoundedRandomFin : {m : Type → Type u_1} → [Monad m] → {n : ℕ} → BoundedRandom m (Fin n)
-- Lean.Meta.Basic
/-- Enable/disable the unification hints feature.  -/
Lean.Meta.Config.unificationHints : Lean.Meta.Config → Bool
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_eq_addMonoidOf_mk'_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (x : M) (y : ↥S),
  AddLocalization.mk x y = (AddLocalization.addMonoidOf S).mk' x y
-- Lean.Meta.Tactic.Grind.Split
/-- Constructs a major premise for the `cases` tactic used by `grind`.  -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.mkCasesMajor : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Logic.Nonempty
nonempty_ulift : ∀ {α : Type u_1}, Nonempty (ULift.{u_4, u_1} α) ↔ Nonempty α
-- Mathlib.Order.Filter.CountablyGenerated
Filter.iInf.isCountablyGenerated : ∀ {ι : Sort u_6} {α : Type u_7} [Countable ι] (f : ι → Filter α) [∀ (i : ι), (f i).IsCountablyGenerated],
  (⨅ i, f i).IsCountablyGenerated
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.ofReal_cpow : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), ↑(x ^ y) = ↑x ^ ↑y
-- Mathlib.RingTheory.Binomial
BinomialRing.toIsAddTorsionFree : ∀ {R : Type u_1} {inst : AddCommMonoid R} {inst_1 : Pow R ℕ} [self : BinomialRing R], IsAddTorsionFree R
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.dim_le_of_nonDegenerate : ∀ (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) (d : ℕ) [X.HasDimensionLE d], n ≤ d
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The `ℝ`-basis of `ℂ` determined by a pair of periods.  -/
PeriodPair.basis : PeriodPair → Module.Basis (Fin 2) ℝ ℂ
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.paren.sizeOf_spec : ∀ (ref : Lean.Syntax) (a : Lean.Elab.Tactic.RCases.RCasesPatt),
  sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.paren ref a) = 1 + sizeOf ref + sizeOf a
-- Init.Data.Int.Cooper
Int.Cooper.le_mul_resolve_left_inv : ∀ (a p k : ℤ), 0 ≤ k → a ∣ k + p → p ≤ a * Int.Cooper.resolve_left_inv a p k
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.splits : ∀ {k : Type u} {inst : Field k} [self : IsAlgClosed k] (p : Polynomial k), p.Splits
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.innerₛₗ_apply : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [inst_10 : StarModule ℂ A] {x y : E},
  (CStarModule.innerₛₗ x) y = inner A x y
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isEmbedding_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5}
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  Topology.IsEmbedding (ContinuousAlternatingMap.restrictScalars 𝕜')
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier.eq_1 : AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier =
  { hom := fun {X Y} => AddCommMonCat.Hom.hom', ofHom := fun {X Y} => AddCommMonCat.Hom.mk✝,
    hom_ofHom := @AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_1,
    ofHom_hom := @AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_2,
    id_apply := @AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_3,
    comp_apply := @AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier._proof_4 }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_eq_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₁₃ = ⋯.lift h.p₁ h.p₃ ⋯
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
/-- [Stacks Tag 02LS](https://stacks.math.columbia.edu/tag/02LS) ((1) <=> (3)) -/
AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsFinite f ↔ AlgebraicGeometry.IsProper f ∧ AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.p_fromOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] {Z : C}
  (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h) =
    CategoryTheory.CategoryStruct.comp (K.d i j) h
-- Mathlib.Data.Quot
/-- Descends a function `f : α → β → γ` to quotients of `α` and `β` with values in a quotient of
`γ`.  -/
Quot.map₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_4} →
      {r : α → α → Prop} →
        {s : β → β → Prop} →
          {t : γ → γ → Prop} →
            (f : α → β → γ) →
              (∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → t (f a b₁) (f a b₂)) →
                (∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → t (f a₁ b) (f a₂ b)) → Quot r → Quot s → Quot t
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- The iff version of `affineCombination_mem_shift` for affine independent points.  -/
AffineIndependent.affineCombination_mem_shift_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] {ι : Type u_4} [inst_4 : Fintype ι] [Nontrivial ι] {p : ι → P},
  AffineIndependent k p →
    ∀ (i : ι) {w : ι → k},
      ∑ i, w i = 1 →
        ∀ (c : k), (Finset.affineCombination k Finset.univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c ↔ w i = 1 - c
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- The fork induced by a split equalizer is an equalizer, justifying the name. In some cases it
is more convenient to show a given fork is an equalizer by showing it is split.
 -/
CategoryTheory.IsSplitEqualizer.isEqualizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {W : C} → {h : W ⟶ X} → (t : CategoryTheory.IsSplitEqualizer f g h) → CategoryTheory.Limits.IsLimit t.asFork
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), { toCompletion := x.toCompletion } = x
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.mk.injEq : ∀ {X : TopCat} {x y : ↑X} (hom : TopCat.I ⟶ X)
  (hom₀ : autoParam ((CategoryTheory.ConcreteCategory.hom hom) 0 = x) TopCat.Path.hom₀._autoParam)
  (hom₁ : autoParam ((CategoryTheory.ConcreteCategory.hom hom) 1 = y) TopCat.Path.hom₁._autoParam)
  (hom_1 : TopCat.I ⟶ X)
  (hom₀_1 : autoParam ((CategoryTheory.ConcreteCategory.hom hom_1) 0 = x) TopCat.Path.hom₀._autoParam)
  (hom₁_1 : autoParam ((CategoryTheory.ConcreteCategory.hom hom_1) 1 = y) TopCat.Path.hom₁._autoParam),
  ({ hom := hom, hom₀ := hom₀, hom₁ := hom₁ } = { hom := hom_1, hom₀ := hom₀_1, hom₁ := hom₁_1 }) = (hom = hom_1)
-- Mathlib.Combinatorics.Graph.Basic
Graph.bouquet_adj : ∀ {α : Type u_1} {β : Type u_2} {x y : α} (v : α) (edgeSet : Set β),
  (Graph.bouquet v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ x = v ∧ y = v
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `s` is closed under negation  -/
NegMemClass.neg_mem : ∀ {S : Type u_3} {G : outParam (Type u_4)} {inst : Neg G} {inst_1 : SetLike S G} [self : NegMemClass S G] {s : S}
  {x : G}, x ∈ s → -x ∈ s
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonneg_of_ae_restrict : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  0 ≤ᵐ[μ.restrict s] f → 0 ≤ ∫ (x : X) in s, f x ∂μ
-- Mathlib.NumberTheory.NumberField.CMField
_private.Mathlib.NumberTheory.NumberField.CMField.0.NumberField.IsCMField.«termK⁺» : Lean.ParserDescr
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.leftUnitor_def : ∀ (R : Type u) [inst : CommRing R] (X : CoalgCat R),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Coalgebra.TensorProduct.lid R ↑X.toModuleCat).toCoalgIso
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommSemiring.toQFn? : Lean.Meta.Grind.Arith.CommRing.CommSemiring → Option Lean.Expr
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Turn a left exact functor into an object of the category `LeftExactFunctor C D`.  -/
CategoryTheory.LeftExactFunctor.of : {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.PreservesFiniteLimits F] → C ⥤ₗ D
-- Mathlib.Algebra.Group.ULift
ULift.mul_down : ∀ {α : Type u} {x y : ULift.{w, u} α} [inst : Mul α], (x * y).down = x.down * y.down
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.toIsOrderedMonoid : ∀ {α : Type u_2} {inst : CommMonoid α} {inst_1 : Preorder α} [self : IsOrderedCancelMonoid α], IsOrderedMonoid α
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (l : ℕ),
  ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑l)
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.HasInjectiveDimensionLT.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {n : ℕ},
  (∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext Y X i)) →
    CategoryTheory.HasInjectiveDimensionLT X n
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.pack.eq_4 : ∀ (spec : Float.Model.Format) (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ) (mantissa_pos : 0 < m),
  Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.finite s m e mantissa_pos) =
    if 2 ^ spec.exponentBits ≤ (e + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat + 1 then
      Float.Model.UnpackedFloat.packedInfinity spec s
    else
      if m.log2 + 1 = spec.mantissaBits then
        Float.Model.UnpackedFloat.packComponents spec s
          (BitVec.ofNat spec.exponentBits (e + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat)
          (BitVec.ofNat spec.mantissaBitsWithoutImplicit m)
      else
        Float.Model.UnpackedFloat.packComponents spec s (0#spec.exponentBits)
          (BitVec.ofNat spec.mantissaBitsWithoutImplicit m)
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_findSomeRevM? : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m (Option β)) (xs : Array α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.findSomeRevM? (f x) xs
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_nnratCast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℚ≥0), ↑↑n = ↑n
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.inverts_iff_factors : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) D),
  (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C)).IsInvertedBy F ↔
    ∀ ⦃K L : HomotopicalAlgebra.BifibrantObject C⦄ (f g : K ⟶ L),
      HomotopicalAlgebra.BifibrantObject.homRel C f g → F.map f = F.map g
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 z x y)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
            (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))))) =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
      (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated : ∀ {X : AlgebraicGeometry.Scheme} [X.IsSeparated], QuasiSeparatedSpace ↥X
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_eq_span : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A),
  Subalgebra.toSubmodule (StarAlgebra.adjoin R s).toSubalgebra = Submodule.span R ↑(Submonoid.closure (s ∪ star s))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ),
  Turing.TM1.stmts M S = Finset.insertNone (S.biUnion fun q => Turing.TM1.stmts₁ (M q))
-- Lean.Parser.Command
Lean.Parser.Command.genInjectiveTheorems.formatter : Lean.PrettyPrinter.Formatter