mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Environment
Lean.registerPersistentEnvExtension : {α β σ : Type} → [Inhabited σ] → Lean.PersistentEnvExtensionDescr α β σ → IO (Lean.PersistentEnvExtension α β σ)
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Starting with `A : MonoOver X`, we can take its equivalence class in `Subobject X`
then pick an arbitrary representative using `representative.obj`.
This is isomorphic (in `MonoOver X`) to the original `A`.
 -/
CategoryTheory.Subobject.representativeIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (A : CategoryTheory.MonoOver X) →
        CategoryTheory.Subobject.representative.obj
            ((CategoryTheory.toThinSkeleton (CategoryTheory.MonoOver X)).obj A) ≅
          A
-- Init.Data.String.Legacy
/-- Splits a string `s` on occurrences of the separator string `sep`. The default separator is `" "`.

When `sep` is empty, the result is `[s]`. When `sep` occurs in overlapping patterns, the first match
is taken. There will always be exactly `n+1` elements in the returned list if there were `n`
non-overlapping matches of `sep` in the string. The separators are not included in the returned
substrings.

This is a legacy function. Use `String.split` instead.

Examples:
* `"here is some text ".splitOn = ["here", "is", "some", "text", ""]`
* `"here is some text ".splitOn "some" = ["here is ", " text "]`
* `"here is some text ".splitOn "" = ["here is some text "]`
* `"ababacabac".splitOn "aba" = ["", "bac", "c"]`
 -/
String.splitOn : String → optParam String " " → List String
-- Batteries.Data.String.Basic
/-- Convert a string of assumed-ASCII characters into a byte array.
(If any characters are non-ASCII they will be reduced modulo 256.)

Note: if you just need the underlying `ByteArray` of a non-ASCII string,
use `String.toUTF8`.
 -/
String.toAsciiByteArray : String → ByteArray
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_4 t (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Lean.LocalContext
Lean.LocalContext.findFromUserName? : Lean.LocalContext → Lean.Name → Option Lean.LocalDecl
-- Mathlib.Algebra.Group.Basic
AddSemigroup.to_isAssociative : ∀ {α : Type u_1} [inst : AddSemigroup α], Std.Associative fun x1 x2 => x1 + x2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toList t).isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Preadditive C] → CategoryTheory.Limits.HasZeroMorphisms C
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommAlgCat.grpObjOpOf : {R : Type u} →
  [inst : CommRing R] →
    {A : Type u} →
      [inst_1 : CommRing A] → [inst_2 : HopfAlgebra R A] → CategoryTheory.GrpObj (Opposite.op (CommAlgCat.of R A))
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_lt_comap_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K L : Subgroup N},
  Function.Surjective ⇑f → (Subgroup.comap f K < Subgroup.comap f L ↔ K < L)
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.Ω_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Sheaf.Ω J).obj = (CategoryTheory.Functor.closedSieves J).toFunctor
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramState : Type
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.biInter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} {t : Set ι},
  t.Countable → (∀ i ∈ t, BaireMeasurableSet (s i)) → BaireMeasurableSet (⋂ i ∈ t, s i)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.integral_llr_add_mul_log_nonneg : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      0 ≤ ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + μ.real Set.univ * Real.log (ν.real Set.univ) + 1 - μ.real Set.univ
-- Mathlib.Order.CompleteLattice.Defs
/-- Every set has a least upper bound.  -/
CompleteSemilatticeSup.isLUB_sSup : ∀ {α : Type u_8} [self : CompleteSemilatticeSup α] (s : Set α), IsLUB s (sSup s)
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofFin : ∀ (n : Fin UInt64.size), (UInt64.ofFin n).toUInt16 = UInt16.ofNat ↑n
-- Mathlib.Logic.Small.Basic
small_subsingleton : ∀ (α : Type v) [Subsingleton α], Small.{w, v} α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
OrthonormalBasis.tensorProduct_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁) (j : ι₂), (b₁.tensorProduct b₂) (i, j) = b₁ i ⊗ₜ[𝕜] b₂ j
-- Mathlib.Algebra.Ring.BooleanRing
instMulBool_mathlib : Mul Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → Std.DHashMap.Raw.Const.getD (m₁.diff m₂) k fallback = fallback
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_inv : ∀ {α : Type u_2} [inst : Inv α] {s t : Set α}, (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectCompIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [inst_3 : CategoryTheory.IsIso h],
  CategoryTheory.Limits.imageSubobjectCompIso f h =
    CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.CategoryStruct.comp f h) ≪≫
      (CategoryTheory.Limits.image.compIso f h).symm ≪≫ (CategoryTheory.Limits.imageSubobjectIso f).symm
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Display `fmt` with a docstring as if it is the constant `n`.  -/
Mathlib.Tactic.ClickSuggestions.formatToHtmlWithDoc : Std.Format → Lean.Name → Lean.MetaM ProofWidgets.Html
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.offset_eq_decreaseBy : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos}, p.Splits t₁ t₂ → p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart_add : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E],
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    (∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) →
      ∀ (n : ℕ),
        MeasureTheory.predictablePart (f + g) ℱ μ n =ᵐ[μ]
          MeasureTheory.predictablePart f ℱ μ n + MeasureTheory.predictablePart g ℱ μ n
-- Mathlib.CategoryTheory.Iso
/-- An isomorphism (a.k.a. an invertible morphism) between two objects of a category.
The inverse morphism is bundled.

See also `CategoryTheory.Core` for the category with the same objects and isomorphisms playing
the role of morphisms.  -/
CategoryTheory.Iso : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type v
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The `ArchimedeanClass.subsemigroup` associated to an upper set in
`FiniteArchimedeanClass M` is a subgroup.  -/
FiniteArchimedeanClass.addSubgroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → UpperSet (FiniteArchimedeanClass M) → AddSubgroup M
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMVarsWithType : Lean.Options → Bool
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DHashMap.Raw.Internal.foldRev f init ↑m = List.foldr (fun a b => f b a.fst a.snd) init (↑m).toList
-- Init.Data.SInt.Bitwise
Int32.zero_or : ∀ {a : Int32}, 0 ||| a = a
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- The composition of Lie-Rinehart algebra morphisms is again a morphism.  -/
LieRinehartAlgebra.Hom.comp : {R : Type u_1} →
  {A₁ : Type u_2} →
    {L₁ : Type u_3} →
      {A₂ : Type u_4} →
        {L₂ : Type u_5} →
          {A₃ : Type u_6} →
            {L₃ : Type u_7} →
              [inst : CommRing R] →
                [inst_1 : CommRing A₁] →
                  [inst_2 : LieRing L₁] →
                    [inst_3 : Module A₁ L₁] →
                      [inst_4 : LieRingModule L₁ A₁] →
                        [inst_5 : CommRing A₂] →
                          [inst_6 : LieRing L₂] →
                            [inst_7 : Module A₂ L₂] →
                              [inst_8 : LieRingModule L₂ A₂] →
                                [inst_9 : CommRing A₃] →
                                  [inst_10 : LieRing L₃] →
                                    [inst_11 : Module A₃ L₃] →
                                      [inst_12 : LieRingModule L₃ A₃] →
                                        [inst_13 : Algebra R A₁] →
                                          [inst_14 : LieAlgebra R L₁] →
                                            [inst_15 : Algebra R A₂] →
                                              [inst_16 : LieAlgebra R L₂] →
                                                [inst_17 : Algebra R A₃] →
                                                  [inst_18 : LieAlgebra R L₃] →
                                                    {σ₁₂ : A₁ →ₐ[R] A₂} →
                                                      {σ₂₃ : A₂ →ₐ[R] A₃} →
                                                        LieRinehartAlgebra.Hom σ₁₂ L₁ L₂ →
                                                          LieRinehartAlgebra.Hom σ₂₃ L₂ L₃ →
                                                            LieRinehartAlgebra.Hom (σ₂₃.comp σ₁₂) L₁ L₃
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- An abbreviation for `IsLocalRing.maximalIdeal 𝒪[K]` of a valued field `K`, enabling the notation
`𝓂[K]` for the maximal ideal in `𝒪[K]` of a valued field `K`.  -/
Valued.maximalIdeal : (K : Type u_1) →
  [inst : Field K] →
    {Γ₀ : outParam (Type u_2)} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [vK : Valued K Γ₀] → Ideal ↥(Valued.integer K)
-- Std.Async.Signal
Std.Async.instDecidableEqSignal : DecidableEq Std.Async.Signal
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.charFn_eq_zero : ∀ {X : Type u_1} (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : MulZeroOneClass Y] {U : Set X} [Nontrivial Y]
  (x : X) (hU : IsClopen U), (LocallyConstant.charFn Y hU) x = 0 ↔ x ∉ U
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_neg : ∀ (a : UInt32), (-a).toUInt8 = -a.toUInt8
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.instFaithfulInclusion : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.Core.inclusion C).Faithful
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.SearchState.mk : List Lean.Meta.Grind.EMatch.Choice → Lean.Meta.Grind.EMatch.InstanceMap → Lean.Meta.Grind.EMatch.SearchState
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.primitiveTriangle_coe : ∀ {n : ℕ} (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ℕ) (h : k < n + 2),
  ↑(SSet.horn.primitiveTriangle i h₀ hₙ k h) = SSet.stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯
-- Mathlib.NumberTheory.Divisors
Int.map_neg_divisorsAntidiag : ∀ {z : ℤ}, Finset.map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I)
  (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (a : Y.I),
  (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).inv.f a = e.symm a
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  Set.range ⇑(CategoryTheory.Limits.pullback.snd f g) =
    ↑((TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f))
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a b : α →₀ M) (i j : M),
  Finsupp.optionElim (i + j) (a + b) = Finsupp.optionElim i a + Finsupp.optionElim j b
-- Mathlib.Topology.Order.IntermediateValue
/-- If a function `f : α → β` is continuous on a nonempty interval `s`, its restriction to `s`
tends to `Filter.atTop : Filter β` along `Filter.atBot : Filter ↥s` and tends to
`Filter.atBot : Filter β` along `Filter.atTop : Filter ↥s`, then the restriction of `f` to `s` is
surjective. We formulate the conclusion as `Function.surjOn f s Set.univ`.  -/
ContinuousOn.surjOn_of_tendsto' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ} {s : Set α} [s.OrdConnected],
  s.Nonempty →
    ContinuousOn f s →
      Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atTop →
        Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atBot → Set.SurjOn f s Set.univ
-- Batteries.Data.String.Lemmas
String.utf8Len_append : ∀ (cs₁ cs₂ : List Char), String.utf8Len (cs₁ ++ cs₂) = String.utf8Len cs₁ + String.utf8Len cs₂
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_snd_dvd : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β},
  Function.minimalPeriod g x.2 ∣ Function.minimalPeriod (Prod.map f g) x
-- Init.Omega.IntList
Lean.Omega.IntList.set_nil_succ : ∀ {i : ℕ} {y : ℤ}, Lean.Omega.IntList.set [] (i + 1) y = 0 :: Lean.Omega.IntList.set [] i y
-- Mathlib.Order.Ideal
Order.Ideal.IsMaximal.toIsProper : ∀ {P : Type u_1} {inst : LE P} {I : Order.Ideal P} [self : I.IsMaximal], I.IsProper
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.fun.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {decl : Lean.Compiler.LCNF.FunDecl pu} {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_5}
  {decl_1 : Lean.Compiler.LCNF.FunDecl pu} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_5},
  Lean.Compiler.LCNF.Code.fun decl k h = Lean.Compiler.LCNF.Code.fun decl_1 k_1 h_1 → decl = decl_1 ∧ k = k_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.rotate_edges : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support),
  (c.rotate u h).edges ~r c.edges
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (n : ℕ),
  hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩ = ⟨σ ^ n, ⋯⟩
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_comp_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p] (x : K), (PerfectRing.lift i j p) (i x) = j x
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mrefinePats : Lean.ParserDescr
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.shiftMap_homologyFunctor_map_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ)
  (h : autoParam (n + a = a') DerivedCategory.shiftMap_homologyFunctor_map_Q._auto_1),
  (DerivedCategory.homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f DerivedCategory.Q) a a' h =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C a).hom.app K)
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
        ((DerivedCategory.homologyFunctorFactors C a').inv.app L))
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Entry.mk : Lean.Name → Lean.Name → Mathlib.TacticAnalysis.Entry
-- Mathlib.Algebra.Group.Ext
AddGroup.ext : ∀ {G : Type u_1} ⦃g₁ g₂ : AddGroup G⦄, HAdd.hAdd = HAdd.hAdd → g₁ = g₂
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a subspace is the subspace.  -/
Projectivization.Subspace.span_coe : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (W : Projectivization.Subspace K V), Projectivization.Subspace.span ↑W = W
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_subtype_and_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α}
  [CompleteSpace α] {s : Set β}, ((Multipliable fun x => f ↑x) ∧ Multipliable fun x => f ↑x) ↔ Multipliable f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.toList_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, (↑(m.erase k)).isEmpty = ((↑m).isEmpty || (↑m).size == 1 && m.contains k)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.cyclesOpIso_hom_naturality : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
      (K.cyclesOpIso i).hom =
    CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).hom (HomologicalComplex.opcyclesMap φ i).op
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal.congr_simp : ∀ {n : Type u_3} {α : Type v} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Zero α] (d d_1 : n → α),
  d = d_1 → ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → Matrix.diagonal d a a_2 = Matrix.diagonal d_1 a_1 a_3
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An injective presentation of an object `X` consists of a monomorphism `f : X ⟶ J`
to some injective object `J`.
 -/
CategoryTheory.InjectivePresentation : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max u₁ v₁)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).maxKey? = some (t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k')
-- Mathlib.Algebra.Order.UpperLower
upperClosure_one : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], upperClosure 1 = 1
-- Mathlib.Topology.Sheaves.Stalks
/-- The isomorphism `ℱ_{f(x)} ≅ (f⁻¹ℱ)ₓ`.  -/
TopCat.Presheaf.stalkPullbackIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        (f : X ⟶ Y) →
          (F : TopCat.Presheaf C Y) →
            (x : ↑X) →
              F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ≅ ((TopCat.Presheaf.pullback C f).obj F).stalk x
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_sub_distrib : ∀ {ι : Type u_1} {G : Type u_5} {s : Finset ι} [inst : SubtractionCommMonoid G] (f g : ι → G),
  ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Given a family of topological spaces `X i`, the `X`-generated topology on
a topological space `Y` is the topology that is coinduced
by all continuous maps `X i → Y`.  -/
TopologicalSpace.generatedBy : {ι : Type t} →
  (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → {Y : Type v} → [tY : TopologicalSpace Y] → TopologicalSpace Y
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measurableSet_sigmaFiniteSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasurableSet μ.sigmaFiniteSet
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.ofList_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α], Std.DHashMap.Raw.ofList [] = ∅
-- Mathlib.LinearAlgebra.Multilinear.Basis
Basis.multilinearMap_apply : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6}
  {N : Type u_7} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b' : Module.Basis ι' R N) [inst_5 : Fintype ι]
  [inst_6 : ∀ (i : ι), Finite (κ i)] (i : ((i : ι) → κ i) × ι'),
  (Basis.multilinearMap b b') i =
    (LinearMap.id.smulRight (b' i.2)).compMultilinearMap
      ((MultilinearMap.mkPiRing R ι 1).compLinearMap fun i' => (b i').coord (i.1 i'))
-- Mathlib.Analysis.Real.Sqrt
/-- The floor of the real square root is the same as the natural square root.  -/
Real.floor_real_sqrt_eq_nat_sqrt : ∀ {a : ℕ}, ⌊√↑a⌋ = ↑a.sqrt
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H)
  (x : TensorProduct 𝕜 E F), (TensorProduct.mapIsometry f g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x
-- Mathlib.Algebra.GCDMonoid.Basic
StrongNormalizationMonoid.toNormalizationMonoid : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : StrongNormalizationMonoid α] → NormalizationMonoid α