mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Height.NumberField
/-- This statement is equivalent to the fact that the "finite part" of the multiplicative
height of a (non-zero) tuple `x` is the inverse of the absolute norm of the ideal generated
by the values of `x`. We state it in a way that avoids taking an inverse.  -/
NumberField.absNorm_mul_finprod_finitePlace_eq_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} [Finite ι]
  {x : ι → NumberField.RingOfIntegers K},
  x ≠ 0 → ↑(Ideal.absNorm (Ideal.span (Set.range x))) * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ i, v ↑(x i) = 1
-- Mathlib.Algebra.Module.PUnit
PUnit.instVAddCommClass_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : VAdd R S], VAddCommClass PUnit.{u_3 + 1} R S
-- Init.Data.Order.Ord
Std.ReflOrd.compare_self : ∀ {α : Type u} [inst : Ord α] [Std.ReflOrd α] {a : α}, compare a a = Ordering.eq
-- Mathlib.Algebra.Exact.Basic
/-- Two maps `f : M →* N` and `g : N →* P` are exact if and only if the induced maps
`MonoidHom.range f → N → MonoidHom.range g` are exact.  -/
Function.MulExact.iff_monoidHom_rangeRestrict : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, Function.MulExact ⇑f ⇑g ↔ Function.MulExact ⇑f.range.subtype ⇑g.rangeRestrict
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.congr_uIoo : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {g : ℝ → ε},
  IntervalIntegrable f μ a b → Set.EqOn f g (Set.uIoo a b) → IntervalIntegrable g μ a b
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks
for the action of `G`  -/
MulAction.IsBlockSystem : (G : Type u_1) → [inst : Group G] → {X : Type u_2} → [MulAction G X] → Set (Set X) → Prop
-- Mathlib.Analysis.Convex.Segment
Prod.image_mk_openSegment_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (x : E) (y₁ y₂ : F),
  (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.next : Lean.ParseImports.State → String → String.Pos.Raw → Lean.ParseImports.State
-- Mathlib.Computability.Language
Language.add_def : ∀ {α : Type u_1} (l m : Language α), l + m = l ∪ m
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SFinite μ] (n : ℕ),
  (MeasureTheory.sfiniteSeq μ n).AbsolutelyContinuous μ.toFinite
-- Mathlib.Analysis.Complex.Basic
/-- Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`.  -/
Complex.ofRealCLM : ℝ →L[ℝ] ℂ
-- Lean.Parser.Term
Lean.Parser.Term.noindex.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Vector.MapIdx
Vector.mapFinIdxM.map.eq_2 : ∀ {n : ℕ} {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (xs : Vector α n)
  (f : (i : ℕ) → α → i < n → m β) (j i_2 : ℕ) (inv_2 : i_2 + 1 + j = n) (ys : Vector β (n - i_2.succ)),
  Vector.mapFinIdxM.map xs f i_2.succ j inv_2 ys = do
    let __do_lift ← f j xs[j] ⋯
    Vector.mapFinIdxM.map xs f i_2 (j + 1) ⋯ (Vector.cast ⋯ (ys.push __do_lift))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.deriv_sinh : deriv Complex.sinh = Complex.cosh
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_10 : ∀ (motive : Lean.Expr → Sort u_1) (binderName : Lean.Name) (d b : Lean.Expr) (binderInfo : Lean.BinderInfo)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.forallE binderName d b binderInfo with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_10 binderName d b binderInfo
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.insertMany m l) k = Std.DHashMap.Raw.Const.get? m k
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F] {Z : CategoryTheory.Functor A D} (h : F.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (L.pointwiseRightKanExtensionCounit F) G) h)) =
    CategoryTheory.CategoryStruct.comp (L.pointwiseRightKanExtensionCounit (F.comp G)) h
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans'_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z)
  (h : e.target = e'.source) (a : Z), ↑(e.trans' e' h).symm a = ↑e.symm (↑e'.symm a)
-- Batteries.Data.Array.Basic
/-- Check whether a subarray is empty.
 -/
Subarray.isEmpty : {α : Type u_1} → Subarray α → Bool
-- Mathlib.Order.RelSeries
RelSeries.append_toFun : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r)
  (a : Fin (p.length + q.length + 1 + 1)), (p.append q connect).toFun a = (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) a
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.mk.sizeOf_spec : ∀ (nonOverlapping : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (current? : Option Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (surrounding : List Lean.Server.FileWorker.AbsoluteLspSemanticToken),
  sizeOf { nonOverlapping := nonOverlapping, current? := current?, surrounding := surrounding } =
    1 + sizeOf nonOverlapping + sizeOf current? + sizeOf surrounding
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_smul_product : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  Finset.image (fun x => x.1 • x.2) (s ×ˢ t) = s • t
-- Aesop.Search.Queue
Aesop.BestFirstQueue : Type
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.TransversalPair.mk : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      (set : ℤˣ → Set G) →
        (∀ (u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (set u)) →
          HNNExtension.NormalWord.TransversalPair G A B
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.one_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (a : α), 1 a = 1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_lt_iff_le_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, a * b⁻¹ < c ↔ a < b * c
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For a finite subset `s` of `M ⊗[R] N`, there exists a finitely generated
submodule `N'` of `N`, such that `s` is contained in the image
of `M ⊗[R] N'` in `M ⊗[R] N`.  -/
TensorProduct.exists_finite_submodule_right_of_setFinite : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (s : Set (TensorProduct R M N)),
  s.Finite → ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range
-- Init.Data.UInt.Bitwise
UInt32.or_not_self : ∀ {a : UInt32}, a ||| ~~~a = -1
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.instDecidableEqCodiscrete : {α : Type u} → [DecidableEq α] → DecidableEq (CategoryTheory.Codiscrete α)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app : ∀ (X : AlgebraicGeometry.LocallyRingedSpace)
  (r :
    (CategoryTheory.InducedCategory
        (TopologicalSpace.Opens (PrimeSpectrum ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))))
        PrimeSpectrum.basicOpen)ᵒᵖ),
  X.toΓSpecCBasicOpens.app r = X.toΓSpecCApp (Opposite.unop r)
-- Mathlib.GroupTheory.Congruence.Defs
Con.conGen_sup : ∀ {M : Type u_1} [inst : Mul M] (r s : M → M → Prop), conGen (r ⊔ s) = conGen r ⊔ conGen s
-- Mathlib.Order.ScottContinuity
ScottContinuous.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  ScottContinuous f =
    ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_ground : ∀ {α : Type u_1} (M : Matroid α) (C : Set α), (M.contract C).E = M.E \ C
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instMonoid : {α : Type u_1} → [Monoid α] → Monoid αᵃᵒᵖ
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductCompDiagIso_inv_app_app : ∀ (J₁ : Type u₁) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₃, u₃} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₁ C) (X_1 : J₁),
  ((CategoryTheory.MonoidalCategory.externalProductCompDiagIso J₁ C).inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (X.1.obj X_1) (X.2.obj X_1))
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- A variant of `exact_map_δ` that takes in an arbitrary map between generators.  -/
Algebra.Generators.H1Cotangent.exact_map_δ' : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} {τ : Type w₅} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (W : Algebra.Generators R T τ) (f : W.Hom Q),
  Function.Exact ⇑(Algebra.Extension.H1Cotangent.map f.toExtensionHom) ⇑(Algebra.Generators.H1Cotangent.δ Q P)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.ofDual_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β) (f : β → αᵒᵈ),
  OrderDual.ofDual (s.inf f) = s.sup (⇑OrderDual.ofDual ∘ f)
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withBotCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  [inst_2 : PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ),
  (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.ker_self_comp_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (T : E →L[𝕜] F),
  (↑(T ∘SL ContinuousLinearMap.adjoint T)).ker = (↑(ContinuousLinearMap.adjoint T)).ker
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (X : CategoryTheory.Endofunctor.Algebra F),
  (CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.hom.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.ofCommaObject_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)))
  (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.ofCommaObject c).obj X =
    match X with
    | CategoryTheory.WithInitial.of x => c.right.obj x
    | CategoryTheory.WithInitial.star => c.left
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] (n : ℕ) (a : α), (Multiset.replicate n a).toFinset = if n = 0 then ∅ else {a}
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type u_1}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (hι : HasCardinalLT ι κ),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup D hι).W = ⨆ i, (D i).W
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.visitExpr : Lean.Expr → Lean.CollectLevelMVars.Visitor
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.exp_def : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [Algebra ℚ R] [Module ℚ M]
  [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : IsCentralScalar R M] [inst_7 : TopologicalSpace R]
  [inst_8 : TopologicalSpace M] [inst_9 : IsTopologicalRing R] [inst_10 : IsTopologicalAddGroup M]
  [inst_11 : ContinuousSMul R M] [inst_12 : ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M),
  NormedSpace.exp x = TrivSqZeroExt.inl (NormedSpace.exp x.fst) + TrivSqZeroExt.inr (NormedSpace.exp x.fst • x.snd)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.sum_add_distrib : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), Cardinal.sum (f + g) = Cardinal.sum f + Cardinal.sum g
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.natDegree_linear_le : ∀ {R : Type u} {a b : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree ≤ 1
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.isIso_homOfLE : ∀ {X : Type u} [inst : Preorder X] {x y : X} (h : x = y), CategoryTheory.IsIso (CategoryTheory.homOfLE ⋯)
-- Mathlib.Data.Finset.Slice
Set.Sized.univ_mem_iff : ∀ {α : Type u_1} {A : Set (Finset α)} {r : ℕ} [inst : Fintype α], Set.Sized r A → (Finset.univ ∈ A ↔ A = {Finset.univ})
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [h : Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Topology.Constructions.SumProd
continuous_sum_dom : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X ⊕ Y → Z}, Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given a morphism `k : A ⟶ S.opcycles` such that `k ≫ S.fromOpcycles = 0`, this is the
induced morphism `A ⟶ S.homology`.  -/
CategoryTheory.ShortComplex.liftHomology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        {A : C} →
          [inst_2 : S.HasHomology] →
            (k : A ⟶ S.opcycles) → CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0 → (A ⟶ S.homology)
-- Mathlib.Order.Bounded
Set.bounded_le_Icc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≤ x2) (Set.Icc a b)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.mem_center_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (u : α), u ∈ G.center ↔ G.eccent u = G.radius
-- Init.GrindInstances.ToInt
Lean.Grind.instLEInt64SintOfNatNat : Lean.Grind.ToInt.LE Int64 (Lean.Grind.IntInterval.sint 64)
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The norm of an element of `ℤ[√d]`.  -/
Zsqrtd.norm : {d : ℤ} → ℤ√d → ℤ
-- Mathlib.RingTheory.Adjoin.Field
/-- If `p` is the minimal polynomial of `a` over `F` then `F[a] ≃ₐ[F] F[x]/(p)`  -/
AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly : (F : Type u_1) →
  [inst : Field F] →
    {R : Type u_2} → [inst_1 : CommRing R] → [inst_2 : Algebra F R] → (x : R) → ↥F[x] ≃ₐ[F] AdjoinRoot (minpoly F x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (↑(t.insertMany! l)).get? k = t.get? k
-- Mathlib.Analysis.Normed.Group.Quotient
Ideal.Quotient.norm_mk_le : ∀ {R : Type u_3} [inst : SeminormedCommRing R] (I : Ideal R) (r : R), ‖(Ideal.Quotient.mk I) r‖ ≤ ‖r‖
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.fst_decompLinearEquiv : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : IsTopologicalAddGroup W]
  (f : V →ᴬ[R] W), ((ContinuousAffineMap.decompLinearEquiv R S V W) f).1 = f 0
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instRingOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → Ring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → Ring (DirectLimit G f)
-- Mathlib.Analysis.Normed.Module.Basic
/-- If `E` is a normed space over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
`RestrictScalars.module` is additionally a `NormedSpace`.  -/
RestrictScalars.normedSpace : (𝕜 : Type u_1) →
  (𝕜' : Type u_2) →
    (E : Type u_3) →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedField 𝕜'] →
          [NormedAlgebra 𝕜 𝕜'] →
            [inst_3 : SeminormedAddCommGroup E] → [NormedSpace 𝕜' E] → NormedSpace 𝕜 (RestrictScalars 𝕜 𝕜' E)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.diff.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t₁ t₂ : Std.DTreeMap.Internal.Impl α β) (h₁ : t₁.Balanced),
  t₁.diff t₂ h₁ =
    if t₁.size ≤ t₂.size then
      (Std.DTreeMap.Internal.Impl.filter (fun p x => !Std.DTreeMap.Internal.Impl.contains p t₂) t₁ h₁).impl
    else ↑(t₁.eraseManyEntries t₂ h₁)
-- Init.Control.Option
OptionT.instAlternative : {m : Type u → Type v} → [Monad m] → Alternative (OptionT m)
-- Mathlib.Data.Finset.Sups
Finset.image_infs : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : SemilatticeInf α] [inst_3 : SemilatticeInf β] [inst_4 : FunLike F α β] [InfHomClass F α β] (f : F)
  (s t : Finset α), Finset.image (⇑f) (s ⊼ t) = Finset.image (⇑f) s ⊼ Finset.image (⇑f) t
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.pairwise_toList_le : ∀ {α : Type u} {r : Std.Roi α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => a ≤ b) r.toList
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequence.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data],
  X.spectralSequence data =
    { page := CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data,
      iso := fun r r' pq hrr' hr =>
        CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso X data r r' hrr' hr pq }
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_inv_iff_mul_le_one_right : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, a ≤ b⁻¹ ↔ a * b ≤ 1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom_id : ∀ {R : Type u} [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ModuleCat.ofHom LinearMap.id = CategoryTheory.CategoryStruct.id (ModuleCat.of R M)
-- Mathlib.Analysis.Normed.Operator.Basic
sphere_subset_range_iff_surjective : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {F' : Type u_9} {𝓕' : Type u_10} [inst_3 : NormedAddCommGroup F']
  [inst_4 : NormedSpace ℝ F'] [Nontrivial F'] {τ : 𝕜 →+* ℝ} [inst_6 : FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F']
  [RingHomSurjective τ] {f : 𝓕'} {x : F'} {r : ℝ}, 0 < r → (Metric.sphere x r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f)
-- Mathlib.Data.ENNReal.Action
ENNReal.instPosSMulStrictMonoNNReal : PosSMulStrictMono NNReal ENNReal
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Finite.equivFin.congr_simp : ∀ (α : Type u_4) [inst : Finite α], Finite.equivFin α = Finite.equivFin α
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.match_1.eq_2 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.done d))
  (h_2 : (d : δ) → motive (ForInStep.yield d)),
  (match ForInStep.yield d with
    | ForInStep.done d => h_1 d
    | ForInStep.yield d => h_2 d) =
    h_2 d