mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_pageD_assoc : ∀ {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₀)
  (r : ℤ) (hr : r₀ ≤ r) (pq pq' pq'' : κ) {Z : C}
  (h : CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq'' hr ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq pq' hr)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq' pq'' hr) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_sub : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x y : R), min (v x) (v y) ≤ v (x - y)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Opens.iSupOpenCover.eq_1 : ∀ {J : Type u_1} {X : AlgebraicGeometry.Scheme} (U : J → X.Opens),
  AlgebraicGeometry.Scheme.Opens.iSupOpenCover U =
    { I₀ := J, X := fun i => ↑(U i), f := fun j => X.homOfLE ⋯, mem₀ := ⋯ }
-- Mathlib.Data.Seq.Basic
Stream'.Seq.nats_get? : ∀ (n : ℕ), Stream'.Seq.nats.get? n = some n
-- Lean.Parser.Types
/-- Returns `true` if a specified byte position is greater than or equal to the position which points to
the end of the input string. Otherwise, returns `false`.
 -/
Lean.Parser.InputContext.atEnd : Lean.Parser.InputContext → String.Pos.Raw → Bool
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isVonNBounded_image2_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {R : Type u_6} [inst_7 : SeminormedRing R]
  [inst_8 : TopologicalSpace F] [inst_9 : IsTopologicalAddGroup F] [inst_10 : DistribMulAction R F]
  [inst_11 : ContinuousConstSMul R F] [inst_12 : SMulCommClass 𝕜₂ R F] {𝔖 : Set (Set E)}
  {S : Set (UniformConvergenceCLM σ F 𝔖)},
  Bornology.IsVonNBounded R S → ∀ {s : Set E}, s ∈ 𝔖 → Bornology.IsVonNBounded R (Set.image2 (fun f x => f x) S s)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous iff the function `swap 𝓕 : X → ι → α` is
continuous *when `ι → α` is equipped with the topology of uniform convergence*. This is
very useful for developing the equicontinuity API, but it should not be used directly for other
purposes.  -/
equicontinuous_iff_continuous : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
  Equicontinuous F ↔ Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_rightUnitor_inv_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X
        (CategoryTheory.CategoryStruct.id
                (Opposite.op
                  (CategoryTheory.Comon.MonOpOpToComonObj
                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                        (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The orthogonal projection is self-adjoint.  -/
isSelfAdjoint_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (U : Submodule 𝕜 E) [inst_4 : U.HasOrthogonalProjection], IsSelfAdjoint U.starProjection
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.getAllTheorems : Lean.Meta.Grind.EMatch.InstanceMap → Array Lean.Meta.Grind.EMatchTheorem × Lean.Meta.Grind.Action.EMatchTheoremIds✝
-- Mathlib.Condensed.Light.InternallyProjective
/-- The `S`-valued points of the internal hom `A ⟶[LightCondMod R] B` are in bijection with
morphisms `A ⊗ R[S] ⟶ B`.
 -/
LightCondensed.ihomPoints : (R : Type u) →
  [inst : CommRing R] →
    (A B : LightCondMod R) →
      (S : LightProfinite) →
        ↑((A ⟹ B).obj.obj (Opposite.op S)) ≃
          (CategoryTheory.MonoidalCategoryStruct.tensorObj A ((LightCondensed.free R).obj S.toCondensed) ⟶ B)
-- Mathlib.Combinatorics.Pigeonhole
/-- If `s` is an infinite set of natural numbers and `k > 0`, then `s` contains two elements `m < n`
that are equal mod `k`.  -/
Nat.exists_lt_modEq_of_infinite : ∀ {s : Set ℕ}, s.Infinite → ∀ {k : ℕ}, 0 < k → ∃ m ∈ s, ∃ n ∈ s, m < n ∧ m ≡ n [MOD k]
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableMul : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Mul α] [DiscreteMeasurableSpace α], MeasurableMul α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_iso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).iso.inv = CategoryTheory.CategoryStruct.id S.homology
-- Init.Data.String.Defs
String.Slice.mk : (str : String) → (startInclusive endExclusive : str.Pos) → startInclusive ≤ endExclusive → String.Slice
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.pre_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) (X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)),
  ((CategoryTheory.CostructuredArrow.pre F G S).obj X).hom = X.hom
-- Mathlib.CategoryTheory.Limits.Unit
/-- Any cone over a functor into `PUnit` is a limit cone.
 -/
CategoryTheory.Limits.punitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{v', v} J] →
    {F : CategoryTheory.Functor J (CategoryTheory.Discrete PUnit.{u_1 + 1})} →
      {c : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit c
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The first theorem that characterises the function `reduce`: a word reduces to its maximal
reduction.  -/
FreeGroup.reduce.red : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.Red L (FreeGroup.reduce L)
-- Init.Data.Vector.Basic
/-- Make an empty vector with pre-allocated capacity.  -/
Vector.emptyWithCapacity : {α : Type u_1} → ℕ → Vector α 0
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_inf : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K K' : LieSubalgebra R L) (x : L), x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
-- Mathlib.Data.Fintype.WithTopBot
instFintypeWithTop.eq_1 : ∀ {α : Type u_1} [inst : Fintype α], instFintypeWithTop = { elems := instFintypeWithTop._aux_1, complete := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.
 -/
CategoryTheory.Limits.PreservesFiniteProducts.of_exponentialIdeal : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.ExponentialIdeal i] [CategoryTheory.BraidedCategory C],
  CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.reflector i)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs)
      ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y)
-- Lean.Data.Position
Lean.Position.mk : ℕ → ℕ → Lean.Position
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.toOption.match_1.eq_2 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : String.Slice.SplitInclusiveIterator pat s → Sort u_1)
  (h_1 :
    (currPos : s.Pos) →
      (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.SplitInclusiveIterator.operating currPos s_1))
  (h_2 : Unit → motive String.Slice.SplitInclusiveIterator.atEnd),
  (match String.Slice.SplitInclusiveIterator.atEnd with
    | String.Slice.SplitInclusiveIterator.operating currPos s => h_1 currPos s
    | String.Slice.SplitInclusiveIterator.atEnd => h_2 ()) =
    h_2 ()
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens),
  let this := (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U)).toAlgebra;
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.toNormalization f)
      ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj ↑U) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationObjIso f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          ↑(integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U))
                ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val)
        (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))
-- Init.System.ST
instMonadLiftSTEST : {ε σ : Type} → MonadLift (ST σ) (EST ε σ)
-- Mathlib.LinearAlgebra.Prod
LinearMap.coe_fst : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], ⇑(LinearMap.fst R M M₂) = Prod.fst
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.subsingletonEquiv.congr_simp : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Subsingleton ι] (i₀ : ι),
  PiTensorProduct.subsingletonEquiv i₀ = PiTensorProduct.subsingletonEquiv i₀
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslationInfo.mk.injEq : ∀ (translation : Lean.Name) (reorder : Mathlib.Tactic.Translate.Reorder)
  (relevantArg : Mathlib.Tactic.Translate.RelevantArg) (translation_1 : Lean.Name)
  (reorder_1 : Mathlib.Tactic.Translate.Reorder) (relevantArg_1 : Mathlib.Tactic.Translate.RelevantArg),
  ({ translation := translation, reorder := reorder, relevantArg := relevantArg } =
      { translation := translation_1, reorder := reorder_1, relevantArg := relevantArg_1 }) =
    (translation = translation_1 ∧ reorder = reorder_1 ∧ relevantArg = relevantArg_1)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.tensor : {C : Type u} →
  CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C →
    C → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousOn.rpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℝ} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, f x ≠ 0 ∨ 0 < g x) → ContinuousOn (fun t => f t ^ g t) s
-- Init.Data.Range.Polymorphic.Basic
Std.Rxi.size_pos : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {lo : α},
  Std.Rxi.HasSize.size lo > 0
-- Mathlib.Topology.Order.ScottTopology
/-- The upper topology on a complete linear order is the Scott topology  -/
Topology.IsScott.instUnivSetOfIsUpper : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α],
  Topology.IsScott α Set.univ
-- Lean.Elab.Match
/-- We convert the collected `PatternVar`s intro `PatternVarDecl`  -/
Lean.Elab.Term.PatternVarDecl : Type
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.copy_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.RespectsIso] {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i))
  (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))), (𝒰.copy J obj map e₁ e₂ h).I₀ = J
-- Qq.Match
Qq.Impl.doElemComefrom_Do_ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index_empty : ∀ {G : Type u_1} [inst : Group G] {V : Set G}, MeasureTheory.Measure.haar.index ∅ V = 0
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.instIsRightDerivabilityStructureIdOfContainsIdentities : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁}
  [W₁.ContainsIdentities], (CategoryTheory.LocalizerMorphism.id W₁).IsRightDerivabilityStructure
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.min?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Min α] [inst_2 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.min? = t.minKey?
-- Mathlib.Algebra.Group.Action.Hom
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`.  -/
Function.Surjective.addActionLeft : {R : Type u_4} →
  {S : Type u_5} →
    {M : Type u_6} →
      [inst : AddMonoid R] →
        [inst_1 : AddAction R M] →
          [inst_2 : AddMonoid S] →
            [inst_3 : VAdd S M] →
              (f : R →+ S) → Function.Surjective ⇑f → (∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) → AddAction S M
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instHasLimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject C)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))} (f : X ⟶ Y) (n : α),
  (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.map f).f n).f = f.f.f n
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.mk' : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  (∀ (s : Set (α × α)), s ∈ uniformity α ↔ ∃ t ∈ uniformity β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s) →
    IsUniformInducing f
-- Mathlib.Analysis.Real.Sqrt
MonoidWithZeroHom.mk.congr_simp : ∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  (toZeroHom toZeroHom_1 : ZeroHom α β) (e_toZeroHom : toZeroHom = toZeroHom_1) (map_one' : toZeroHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y),
  { toZeroHom := toZeroHom, map_one' := map_one', map_mul' := map_mul' } =
    { toZeroHom := toZeroHom_1, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Basic
instSeminormedCommRingRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} → {E : Type u_3} → [I : SeminormedCommRing E] → SeminormedCommRing (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S : CategoryTheory.ShortComplex C} {Q H : C} {p : S.X₂ ⟶ Q} {ι : H ⟶ Q}
  {wp : CategoryTheory.CategoryStruct.comp S.f p = 0}
  {hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p wp)}
  {wι : CategoryTheory.CategoryStruct.comp ι (hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0}
  {hι : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι wι)} {Q_1 H_1 : C} {p_1 : S.X₂ ⟶ Q_1}
  {ι_1 : H_1 ⟶ Q_1} {wp_1 : CategoryTheory.CategoryStruct.comp S.f p_1 = 0}
  {hp_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p_1 wp_1)}
  {wι_1 : CategoryTheory.CategoryStruct.comp ι_1 (hp_1.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0}
  {hι_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι_1 wι_1)},
  { Q := Q, H := H, p := p, ι := ι, wp := wp, hp := hp, wι := wι, hι := hι } =
      { Q := Q_1, H := H_1, p := p_1, ι := ι_1, wp := wp_1, hp := hp_1, wι := wι_1, hι := hι_1 } →
    Q = Q_1 ∧ H = H_1 ∧ p ≍ p_1 ∧ ι ≍ ι_1 ∧ hp ≍ hp_1 ∧ hι ≍ hι_1
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.PreservesPullbacksOfInclusions.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D}
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [preservesPullbackInl :
    ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y),
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inl f) F],
  CategoryTheory.PreservesPullbacksOfInclusions F
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.tokens : Lean.Parser.ParserContextCore → Lean.Parser.TokenTable
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.usePartial : Lean.Elab.Deriving.Context → Bool
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.forall_uIoc_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {P : α → Prop},
  (∀ x ∈ Set.uIoc a b, P x) ↔ (∀ x ∈ Set.Ioc a b, P x) ∧ ∀ x ∈ Set.Ioc b a, P x
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis) (x : α),
  a.ofPermHomFun 1 x = x
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.mul_congr.wl : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Mul α] [Lean.Grind.ToInt.Mul α i],
  i.isFinite = true → ∀ {a b : α} {a' b' : ℤ}, ↑a = i.wrap a' → ↑b = b' → ↑(a * b) = i.wrap (a' * b')
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.Hom.ext_iff : ∀ {X Y : TopCat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKey! k = m.getKey! k
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso : ∀ {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) {ι : Type u_3} (c : ComplexShape ι)
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.CategoryWithHomology C] [inst_5 : CategoryTheory.CategoryWithHomology D]
  [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] [inst_7 : F.Additive] [F.PreservesHomology],
  (HomologicalComplex.quasiIso C c).IsInvertedBy ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.congr : ∀ {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α}
  {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o'),
  (∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) →
    (∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) →
      (∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) →
        (match h : o with
          | Ordering.lt => lt h
          | Ordering.eq => eq h
          | Ordering.gt => gt h) =
          match h : o' with
          | Ordering.lt => lt' h
          | Ordering.eq => eq' h
          | Ordering.gt => gt' h
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.IsVeryGood.toIsGood : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : C}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.PathObject A}
  {inst_2 : CategoryTheory.Limits.HasBinaryProduct A A} {inst_3 : HomotopicalAlgebra.CategoryWithFibrations C}
  {inst_4 : HomotopicalAlgebra.CategoryWithCofibrations C} [self : P.IsVeryGood], P.IsGood
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.inv_symm_left_iff₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a x y : G₀}, SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x
-- Mathlib.LinearAlgebra.Trace
/-- The trace of a linear map corresponds to the contraction pairing under the isomorphism
`End(M) ≃ M* ⊗ M`.  -/
LinearMap.trace_eq_contract_of_basis' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M),
  LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorComm_toLinearEquiv : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Invertible 2]
  (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂), (Q₁.tensorComm Q₂).toLinearEquiv = TensorProduct.comm R M₁ M₂
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.mem_hyperfilter_of_finite_compl : ∀ {α : Type u} [inst : Infinite α] {s : Set α}, sᶜ.Finite → s ∈ Filter.hyperfilter α
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted.add : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) {f g : PowerSeries R},
  PowerSeries.IsRestricted c f → PowerSeries.IsRestricted c g → PowerSeries.IsRestricted c (f + g)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instIsMulCommutative_closure : ∀ {R' : Type u_1} [inst : Semiring R'] {S : Type u_5} [inst_1 : SetLike S R'] [inst_2 : MulMemClass S R'] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(Subsemiring.closure ↑s)
-- Lean.CoreM
/-- Creates the expression `d → b`  -/
Lean.mkArrow : Lean.Expr → Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
/-- A Borel-measurable group hom from a locally compact normed group to a real normed space is
continuous.  -/
MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable : ∀ {G : Type u_1} {H : Type u_2} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [LocallyCompactSpace G] [inst_4 : SeminormedAddCommGroup H] [inst_5 : MeasurableSpace H] [OpensMeasurableSpace H]
  [NormedSpace ℝ H] (f : G →+ H), Measurable ⇑f → Continuous ⇑f