mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  (i₁ i₂ i₃ : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₂ i₃) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
-- Lean.Data.KVMap
Lean.KVMap.insertCore : List (Lean.Name × Lean.DataValue) → Lean.Name → Lean.DataValue → List (Lean.Name × Lean.DataValue)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_getElem! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, a ∈ m → m[a]? = some m[a]!
-- Aesop.Rule
Aesop.RegularRule.unsafe.injEq : ∀ (r r_1 : Aesop.UnsafeRule), (Aesop.RegularRule.unsafe r = Aesop.RegularRule.unsafe r_1) = (r = r_1)
-- Mathlib.Logic.Denumerable
/-- Returns the `n`-th element of a set, according to the usual ordering of `ℕ`.  -/
Nat.Subtype.ofNat : (s : Set ℕ) → [DecidablePred fun x => x ∈ s] → [Infinite ↑s] → ℕ → ↑s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableWithinAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => Real.cosh (f x)) s x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Ico : ∀ {a b : ℝ}, MeasureTheory.volume (Set.Ico a b) = ENNReal.ofReal (b - a)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If a simple graph `G` is bipartite, then there exist disjoint sets `s` and `t`
such that all edges in `G` connect a vertex in `s` to a vertex in `t`.  -/
SimpleGraph.IsBipartite.exists_isBipartiteWith : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsBipartite → ∃ s t, G.IsBipartiteWith s t
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `n` and shifting by `-n` forms an equivalence.  -/
CategoryTheory.shiftEquiv : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : AddGroup A] → [CategoryTheory.HasShift C A] → A → (C ≌ C)
-- Mathlib.Order.WithBot
Equiv.withTopSubtypeNe.eq_1 : ∀ {α : Type u_1},
  Equiv.withTopSubtypeNe =
    {
      toFun := fun x =>
        match x with
        | ⟨x, h⟩ => x.untop h,
      invFun := fun x => ⟨↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Init.System.IO
/-- Reads the entire remaining contents of the stream until an end-of-file marker (EOF) is
encountered.

The underlying stream is not automatically closed upon encountering an EOF, and subsequent reads from
the stream may block and/or return data.
 -/
IO.FS.Stream.readBinToEnd : IO.FS.Stream → IO ByteArray
-- Mathlib.GroupTheory.GroupAction.ConjAct
MulAut.conjNormal_apply : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] (g : G) (h : ↥H),
  ↑((MulAut.conjNormal g) h) = g * ↑h * g⁻¹
-- Mathlib.Order.Disjointed
Finset.disjiUnion_Iic_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : DecidableEq α]
  (n : ι) (t : ι → Finset α), (Finset.Iic n).disjiUnion (disjointed t) ⋯ = (partialSups t) n
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  t ∈ nhds x → VectorField.mlieBracketWithin I V W (s ∩ t) x = VectorField.mlieBracketWithin I V W s x
-- Mathlib.CategoryTheory.Limits.Preserves.Ulift
/-- The equivalence between `K.sections` and `(K ⋙ uliftFunctor.{v, u}).sections`. This is used to show
that `uliftFunctor` preserves limits that are potentially too large to exist in the source
category.
 -/
CategoryTheory.Limits.Types.sectionsEquiv : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    (K : CategoryTheory.Functor J (Type u)) → ↑K.sections ≃ ↑(K.comp CategoryTheory.uliftFunctor.{v, u}).sections
-- Mathlib.Algebra.Category.Ring.Limits
/-- Some definitions may be extremely slow to elaborate, when the target type to be constructed
is complicated and when the type of the term given in the definition is also complicated and does
not obviously match the target type. In this case, instead of just giving the term, prefixing it
with `by apply` may speed up things considerably as the types are not elaborated in the same order.
 -/
LibraryNote.«change_elaboration_strategy_with_`by_apply`» : Batteries.Util.LibraryNote
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem : {α : Type u_1} → [inst : Group α] → (s : Subgroup α) → [DecidablePred fun x => x ∈ s] → DecidableEq (α ⧸ s)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The short complex `A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A)`.  -/
groupCohomology.shortComplexH1 : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → Rep.{max u u_1, u, u} k G → CategoryTheory.ShortComplex (ModuleCat k)
-- Lean.Environment
Lean.PersistentEnvExtensionState.state : {α σ : Type} → Lean.PersistentEnvExtensionState α σ → σ
-- Mathlib.Algebra.Group.Basic
zpow_eq_zpow_emod : ∀ {G : Type u_3} [inst : Group G] {x : G} (m : ℤ) {n : ℤ}, x ^ n = 1 → x ^ m = x ^ (m % n)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vge_of_veq`. -/
ValuativeRel.veq.vge : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → y ≤ᵥ x
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.Dual.finrank_ker_add_one_of_ne_zero : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  {f : Module.Dual K V₁},
  f ≠ 0 → ∀ [FiniteDimensional K V₁], Module.finrank K ↥(LinearMap.ker f) + 1 = Module.finrank K V₁
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_sq : ∀ (x : ℝ), Real.cosh x ^ 2 = Real.sinh x ^ 2 + 1
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.gcdCoeffs.match_1.splitter : (motive : Int.Internal.Linear.Poly → ℤ → Sort u_1) →
  (x : Int.Internal.Linear.Poly) →
    (x_1 : ℤ) →
      ((k k_1 : ℤ) → motive (Int.Internal.Linear.Poly.num k) k_1) →
        ((k' : ℤ) →
            (v : Int.Internal.Linear.Var) →
              (p : Int.Internal.Linear.Poly) → (k : ℤ) → motive (Int.Internal.Linear.Poly.add k' v p) k) →
          motive x x_1
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Down.mem_compression_of_insert_mem_compression : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  insert a s ∈ Down.compression a 𝒜 → s ∈ Down.compression a 𝒜
-- Mathlib.Analysis.Convex.Between
sbtw_neg_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V}, Sbtw R (-x) (-y) (-z) ↔ Sbtw R x y z
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.insert.eq_2 : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (k_1 : ℤ) (v_1 : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.insert k v (Int.Internal.Linear.Poly.add k_1 v_1 p_2) =
    bif Nat.blt v_1 v then Int.Internal.Linear.Poly.add k v (Int.Internal.Linear.Poly.add k_1 v_1 p_2)
    else
      bif Nat.beq v v_1 then if (k.add k_1 == 0) = true then p_2 else Int.Internal.Linear.Poly.add (k.add k_1) v_1 p_2
      else Int.Internal.Linear.Poly.add k_1 v_1 (Int.Internal.Linear.Poly.insert k v p_2)
-- Mathlib.Logic.Embedding.Basic
/-- Define an embedding `(Π a : α, β a) ↪ (Π a : α, γ a)` from a family of embeddings
`e : Π a, (β a ↪ γ a)`. This embedding sends `f` to `fun a ↦ e a (f a)`.  -/
Function.Embedding.piCongrRight : {α : Sort u_1} → {β : α → Sort u_2} → {γ : α → Sort u_3} → ((a : α) → β a ↪ γ a) → ((a : α) → β a) ↪ (a : α) → γ a
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubVSubWeights.congr_simp : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] (i i_1 : ι),
  i = i_1 →
    ∀ (j j_1 : ι),
      j = j_1 →
        ∀ (a a_1 : ι), a = a_1 → Finset.weightedVSubVSubWeights k i j a = Finset.weightedVSubVSubWeights k i_1 j_1 a_1
-- Mathlib.Order.Hom.Basic
/-- If the images by an order embedding of two elements are complements,
then they are themselves complements.  -/
IsCompl.of_orderEmbedding : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ↪o β) [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] {a₁ a₂ : α}, IsCompl (f a₁) (f a₂) → IsCompl a₁ a₂
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX_hom_D₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Aesop.Tree.Data
Aesop.GoalState.provenByRuleApplication.sizeOf_spec : sizeOf Aesop.GoalState.provenByRuleApplication = 1
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addCommMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : AddCommMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Injective.addCommMonoid f hf one mul npow =
    { toAddMonoid := Function.Injective.addMonoid f hf one mul npow, add_comm := ⋯ }
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Given functors `F G : C ⥤ D`, and an equation `η = θ` between natural transformations
(possibly after a `∀` binder), produce the equation `∀ (X : C), η.app X = θ.app X`, and simplify
it using basic lemmas about `NatTrans.app`.  -/
Mathlib.Tactic.CategoryTheory.ToApp.toAppExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.subsingletonEquiv_symm_apply' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {M : Type u_8} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Subsingleton ι] (i₀ : ι) (x : M),
  (PiTensorProduct.subsingletonEquiv i₀).symm x = (PiTensorProduct.tprod R) fun x_1 => x
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.additive_of_preserves_binary_products : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasBinaryProducts C]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [F.PreservesZeroMorphisms], F.Additive
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_zsmul : ∀ {X : Type u_1} (k : ℤ), k ≠ 0 → ∀ (a : FreeAbelianGroup X), (k • a).support = a.support
-- Mathlib.Order.Hom.Lattice
InfHom.instOrderTop : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → [OrderTop β] → OrderTop (InfHom α β)
-- Init.Core
/-- If two types are equal and one of them is a subsingleton, then all of their elements are
[heterogeneously equal](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=HEq).
 -/
Subsingleton.helim : ∀ {α β : Sort u} [h₁ : Subsingleton α], α = β → ∀ (a : α) (b : β), a ≍ b
-- Mathlib.CategoryTheory.IsoCat
/-- The identity isomorphism of categories.  -/
CategoryTheory.IsoCat.refl : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.IsoCat C C
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- If `I` is a `ModelWithCorners.Boundaryless` model, then it is a homeomorphism.  -/
ModelWithCorners.toHomeomorph : {𝕜 : 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) → [I.Boundaryless] → H ≃ₜ E
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modifyGetThe_eq : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (f : σ → α × σ),
  modifyGetThe σ f = do
    let z ← f <$> get
    set z.2
    pure z.1
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.regularTopology.instIsDenseSubsite : ∀ {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] (F : CategoryTheory.Functor C D) [inst_2 : F.PreservesEffectiveEpis]
  [inst_3 : F.ReflectsEffectiveEpis] [inst_4 : F.Full] [inst_5 : F.Faithful] [inst_6 : F.EffectivelyEnough]
  [inst_7 : CategoryTheory.Preregular D],
  CategoryTheory.Functor.IsDenseSubsite (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D) F
-- Mathlib.Analysis.RCLike.Basic
RCLike.toDecidableEq : {K : semiOutParam (Type u_1)} → [self : RCLike K] → DecidableEq K
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_const_mul_of_nonneg_of_ne_top : ∀ {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal},
  0 ≤ c → c ≠ ⊤ → Filter.liminf (fun x => c * u x) f = c * Filter.liminf u f
-- Init.Data.SInt.Basic
/-- The smallest number that `Int8` can represent: `-2^7 = -128`.  -/
Int8.minValue : Int8
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The subsemiring `R` of the semiring `R`.  -/
Subsemiring.instTop : {R : Type u} → [inst : NonAssocSemiring R] → Top (Subsemiring R)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (hu : u = u') (hv : v = v'),
  (p.copy hu hv).Nil = p.Nil
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.nnnorm_vadd_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)), ‖c +ᵥ f‖₊ = ‖f‖₊
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_factors_comp_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {W : C} (k : W ⟶ X),
  (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k f)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.toStrongDual_apply : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x : WeakDual 𝕜 E) (y : E), (WeakDual.toStrongDual x) y = x y
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.add_sum_Ioo_eq_sum_Ioc : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → f b + ∑ x ∈ Finset.Ioo a b, f x = ∑ x ∈ Finset.Ioc a b, f x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space,
and compositions of zero morphisms with anything give the zero morphism.  -/
CategoryTheory.Limits.HasZeroMorphisms : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instAddCommGroup : {R : Type u_3} → {c₁ c₂ c₃ : R} → [AddCommGroup R] → AddCommGroup (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) T.hom))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst R.hom S.hom) h)
-- Mathlib.AlgebraicGeometry.ResidueField
/-- If `K` is a field and `f : 𝒪_{X, x} ⟶ K` is a ring map, then this is the induced
map `κ(x) ⟶ K`.  -/
AlgebraicGeometry.Scheme.descResidueField : {K : Type u} →
  [inst : Field K] →
    {X : AlgebraicGeometry.Scheme} →
      {x : ↥X} →
        (f : X.presheaf.stalk x ⟶ CommRingCat.of K) →
          [IsLocalHom (CommRingCat.Hom.hom f)] → X.residueField x ⟶ CommRingCat.of K
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.instIsCommMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.IsCommMonObj X
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app._auto_1)
  {Z : Cᵒᵖ}
  (h :
    (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj X) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
      h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C n).map
            ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X).unop).op
        h)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : Set α) (h : IsClosed s), ↑{ carrier := s, isClosed' := h } = s
-- Mathlib.Algebra.Order.Group.PosPart
posPart_inf_negPart_eq_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α), a⁺ ⊓ a⁻ = 0
-- Lean.Util.CollectMVars
Lean.CollectMVars.Visitor : Type
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.Meta.NormNum.IsInt.nnreal_rpow_eq_inv_nnreal_pow : ∀ {b : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsInt b (Int.negOfNat n) → ∀ (a : NNReal), a ^ b = (a ^ n)⁻¹
-- Lean.Elab.Exception
Lean.Elab.autoBoundImplicitExceptionId : Lean.InternalExceptionId
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_iff_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  a ∈ m ↔ (m.get? a).isSome = true
-- Aesop.Tree.Data
Aesop.GoalId.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Init.Data.Array.Lemmas
Array.getElem?_push_eq : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x)[xs.size]? = some x
-- Mathlib.Topology.Baire.LocallyCompactRegular
/-- **Second Baire theorem**: locally compact R₁ spaces are Baire.  -/
BaireSpace.of_t2Space_locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [LocallyCompactSpace X], BaireSpace X
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalExprAbelMode : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Abel.AbelMode
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_empty : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty.toListModel = []
-- Init.Data.String.Iterator
String.Legacy.Iterator.mk.inj : ∀ {s : String} {i : String.Pos.Raw} {s_1 : String} {i_1 : String.Pos.Raw},
  { s := s, i := i } = { s := s_1, i := i_1 } → s = s_1 ∧ i = i_1
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_inclusion : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t), Measurable (Set.inclusion h)
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- `(c • ·)` is a proper map.  -/
ProperConstSMul.isProperMap_smul : ∀ {M : Type u_1} {X : Type u_2} {inst : SMul M X} {inst_1 : TopologicalSpace X} [self : ProperConstSMul M X] (c : M),
  IsProperMap fun x => c • x
-- Lean.Meta.Iterator
Lean.Meta.Iterator.mk : {α : Type} → Lean.MetaM (Option (α × Lean.Meta.SavedState)) → Lean.Meta.Iterator α
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.mono : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l₁ l₂ : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l₁] g → l₂ ≤ l₁ → f =o[𝕜; l₂] g
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear isometric equivalence, applied with `Basis.map`, preserves the property of being
orthonormal.  -/
Orthonormal.mapLinearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E']
  {v : Module.Basis ι 𝕜 E}, Orthonormal 𝕜 ⇑v → ∀ (f : E ≃ₗᵢ[𝕜] E'), Orthonormal 𝕜 ⇑(v.map f.toLinearEquiv)
-- Lean.Compiler.IR.Basic
Lean.IR.instHashableJoinPointId : Hashable Lean.IR.JoinPointId