mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ},
  n ≠ 1 → ∀ (G : SimpleGraph α) (f : α ↪ β), (SimpleGraph.map (⇑f) G).cliqueSet n = Finset.map f '' G.cliqueSet n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).isEmpty = false →
    ∀ {fallback : α},
      (t.modify k f).maxKeyD fallback = if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Iio_ae_eq_Iic' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a : α},
  μ {a} = 0 → Set.Iio a =ᵐ[μ] Set.Iic a
-- Mathlib.Data.List.Sublists
/-- The list of all sublists of a list `l` that are of length `n`. For instance, for
`l = [0, 1, 2, 3]` and `n = 2`, one gets
`[[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]]`.  -/
List.sublistsLen : {α : Type u} → ℕ → List α → List (List α)
-- Mathlib.Data.Finset.Card
/-- If `a ∈ s` is known, see also `Finset.card_erase_of_mem` and `Finset.erase_eq_of_notMem`.  -/
Finset.card_erase_eq_ite : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], (s.erase a).card = if a ∈ s then s.card - 1 else s.card
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instBraidedMonMapAddMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [inst_4 : CategoryTheory.SymmetricCategory C] →
                [inst_5 : CategoryTheory.SymmetricCategory D] → [inst_6 : F.Braided] → F.mapAddMon.Braided
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f` is a Hölder continuous map with exponent `r > 0`, then the Hausdorff dimension of its
range is at most the Hausdorff dimension of its domain divided by `r`.  -/
HolderWith.dimH_range_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → 0 < r → dimH (Set.range f) ≤ dimH Set.univ / ↑r
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofEq.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂),
  CategoryTheory.ShortComplex.Homotopy.ofEq h = CategoryTheory.ShortComplex.Homotopy.ofEq h
-- Init.Core
/-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop  -/
DoResultBC.continue : {σ : Type u} → σ → DoResultBC σ
-- Batteries.CodeAction.Misc
/-- `findTermInfoWithCtx?` finds the `TermInfo` for an elaborated term `stx`
and also updates the inputted `ContextInfo` using all the
`PartialContextInfo` on the path to the returned `TermInfo`.  -/
Batteries.CodeAction.findTermInfoWithCtx? : Lean.Elab.InfoTree → Lean.Term → Lean.Elab.ContextInfo → Option (Lean.Elab.TermInfo × Lean.Elab.ContextInfo)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.exists_pow_eq'' : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [Finite α], f.SameCycle x y → ∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Sat : {α : Type u_1} → (α → Bool) → Std.Sat.CNF α → Prop
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the condition that the denominator belongs to the given morphism property  -/
CategoryTheory.MorphismProperty.RightFraction₂.hs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (self : W.RightFraction₂ X Y), W self.s
-- Init.Data.List.Sublist
List.instTransSublistSubset : {α : Type u_1} → Trans List.Sublist Subset Subset
-- Mathlib.Data.Sym.NatCard
Sym2.instInfinite : ∀ (α : Type u_1) [Infinite α], Infinite (Sym2 α)
-- Mathlib.Order.RelIso.Basic
RelIso.sumLexEmpty_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsEmpty β] (val : α),
  (RelIso.sumLexEmpty r s).symm val = Sum.inl val
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  (dropping : Bool) (inner : Std.IterM m β) (dropping_1 : Bool) (inner_1 : Std.IterM m β),
  ({ dropping := dropping, inner := inner } = { dropping := dropping_1, inner := inner_1 }) =
    (dropping = dropping_1 ∧ inner = inner_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCone_π_app_mk : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  B.toCone.π.app { as := j } = B.π j
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
/-- If `X ⟶ Y` is a morphism of locally ringed spaces and `x` a point of `X`, we obtain
a morphism of residue fields in the other direction.  -/
AlgebraicGeometry.LocallyRingedSpace.residueFieldMap : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Y) → (x : ↑X.toTopCat) → Y.residueField ((CategoryTheory.ConcreteCategory.hom f.base) x) ⟶ X.residueField x
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.toSigned : ℤ → String
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {W : CategoryTheory.MorphismProperty T}
  [W.RespectsIso], (CategoryTheory.MorphismProperty.commaObj L R W).IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- Given a cocontinuous functor `F : C ⥤ D` between sites `(C, J)` and `(D, K)`,
`P` a presheaf on `D`, `X : C`, `x : Φ.fiber.obj X`, this is the canonical morphism
`P.obj (op (F.obj X)) ⟶ (Φ.map F K).presheafFiber.obj P`, which is part
of the colimit cocone `presheafFiberMapCocone`.  -/
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (Φ : J.Point) →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [inst_2 : F.IsCocontinuous J K] →
                  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] →
                    {A : Type u''} →
                      [inst_4 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (P : CategoryTheory.Functor Dᵒᵖ A) →
                            (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op (F.obj X)) ⟶ (Φ.map F K).presheafFiber.obj P)
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillZero.go : {α : Type} → Std.Internal.Parsec.ByteArray.Parser α → Array α → Std.Internal.Parsec.ByteArray.Parser (Array α)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_getThe_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {post : σ → σ → Pred} {epost : EPred},
  Std.Internal.Do.wp (getThe σ) post epost = Std.Internal.Do.wp MonadStateOf.get post epost
-- Mathlib.CategoryTheory.Functor.Functorial
/-- An unbundled functor.  -/
CategoryTheory.Functorial : {C : Type u₁} →
  [CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [CategoryTheory.Category.{v₂, u₂} D] → (C → D) → Type (max v₁ v₂ u₁ u₂)
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_rcc : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) xs.length - lo
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.map_baseChange : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W.baseChange A).map ↑f = W.baseChange B
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  stereographic hv =
    { toFun := stereoToFun v ∘ Subtype.val, invFun := stereoInvFun hv, source := {⟨v, ⋯⟩}ᶜ, target := Set.univ,
      map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, continuousOn_toFun := ⋯,
      continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A topological space `X` is compactly coherent if a set `s` is open when `f ⁻¹' s?` is open for
every continuous map `f : K → X`, where `K` is compact.  -/
CompactlyCoherentSpace.of_isOpen_forall_compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (s : Set X),
      (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) →
        IsOpen s) →
    CompactlyCoherentSpace X
-- Mathlib.Logic.Function.Defs
Function.swap_def : ∀ {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y), Function.swap f = fun y x => f x y
-- Qq.MetaM
Qq.withLocalDeclQ : {n : Type → Type u_1} →
  {u : Lean.Level} →
    {α : Type} →
      [Monad n] → [MonadControlT Lean.MetaM n] → Lean.Name → Lean.BinderInfo → (β : Q(Sort u)) → (Q(«$β») → n α) → n α
-- Mathlib.Data.List.Map2
List.map₂Left_eq_zipWith : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) (bs : List β),
  as.length ≤ bs.length → List.map₂Left f as bs = List.zipWith (fun a b => f a (some b)) as bs
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.truncTotal_sub_truncTotal_mem_pow_idealOfVars : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ] {l m n : ℕ},
  l ≤ m →
    l ≤ n →
      ∀ (p : MvPowerSeries σ R),
        (MvPowerSeries.truncTotal m) p - (MvPowerSeries.truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ l
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_eq_signedDist_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] {p q : P},
  q ∈ s → s.signedInfDist p = (signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) q
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_apply_inl : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₁)
  (j : n), A₁.fromRows A₂ (Sum.inl i) j = A₁ i j
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instStarAddMonoid : {α : Type u_3} →
  {E : α → Type u_4} →
    {p : ENNReal} →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : (i : α) → StarAddMonoid (E i)] → [∀ (i : α), NormedStarGroup (E i)] → StarAddMonoid ↥(lp E p)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_sum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {ι : Type u_3}
  (f : ι → R → R) (a : A) (s : Finset ι),
  autoParam (∀ i ∈ s, ContinuousOn (f i) (quasispectrum R a)) cfcₙ_sum._auto_1 →
    autoParam (∀ i ∈ s, f i 0 = 0) cfcₙ_sum._auto_3 → cfcₙ (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (f i) a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData.treeMap : {α : Type u} → Std.DTreeMap.Internal.Unit.RiiSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- ...and as such, unique.  -/
CategoryTheory.EffectiveEpiStruct.uniq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X}
  (self : CategoryTheory.EffectiveEpiStruct f) {W : C} (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
  (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = self.desc e ⋯
-- Mathlib.Algebra.CharP.Lemmas
CharP.ringChar_ne_zero_of_finite : ∀ (R : Type u_1) [inst : NonAssocRing R] [Finite R], ringChar R ≠ 0
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.liftCover.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {ι : Type u_5} (S : ι → Set α)
  (φ φ_1 : (i : ι) → C(↑(S i), β)) (e_φ : φ = φ_1)
  (hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩)
  (hS : ∀ (x : α), ∃ i, S i ∈ nhds x), ContinuousMap.liftCover S φ hφ hS = ContinuousMap.liftCover S φ_1 ⋯ hS
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The type of linear maps is an additive monoid.  -/
LinearMap.addCommMonoid : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → AddCommMonoid (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- Suppose `f` and `g` are two morphisms with a common domain and `s` is a colimit cocone over the
diagram formed by `f` and `g`. Suppose `f` and `g` both factor through an epimorphism `h` via
`x` and `y`, respectively. Then `s` is also a colimit cocone over the diagram formed by `x` and
`y`.  -/
CategoryTheory.Limits.PushoutCocone.isColimitOfFactors : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (h : X ⟶ W) →
            [inst_1 : CategoryTheory.Epi h] →
              (x : W ⟶ Y) →
                (y : W ⟶ Z) →
                  (hhx : CategoryTheory.CategoryStruct.comp h x = f) →
                    (hhy : CategoryTheory.CategoryStruct.comp h y = g) →
                      (s : CategoryTheory.Limits.PushoutCocone f g) →
                        CategoryTheory.Limits.IsColimit s →
                          have reassoc₁ := ⋯;
                          have reassoc₂ := ⋯;
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk s.inl s.inr ⋯)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.freeLocus_congr : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_1}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (e : M ≃ₗ[R] M'), Module.freeLocus R M = Module.freeLocus R M'
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A map between convex spaces is affine if it preserves convex combinations.

TODO: Show that this generalises affine maps between affine spaces, see `AffineMap`.  -/
Convexity.IsAffineMap : (R : Type u_1) →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : PartialOrder R] →
        [inst_1 : Semiring R] →
          [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R M] → [Convexity.ConvexSpace R N] → (M → N) → Prop
-- Lean.Language.Basic
/-- Range that is marked as being processed by the server while a task is running.  -/
Lean.Language.SnapshotTask.ReportingRange : Type
-- Std.Time.DateTime
_private.Std.Time.DateTime.0.Std.Time.DateTime.mk : Thunk Std.Time.PlainDateTime → Std.Time.Timestamp → Std.Time.TimeZone.ZoneRules → Std.Time.TimeZone → Std.Time.DateTime
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.IsPath.map`.

---

**Alias** of the reverse direction of `SimpleGraph.Walk.isPath_map_iff_of_injective`. -/
SimpleGraph.Walk.map_isPath_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → p.IsPath → (SimpleGraph.Walk.map f p).IsPath
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- `Π i, A i` is homeomorphic to an open subset of the restricted product.  -/
RestrictedProduct.isOpenEmbedding_structureMap : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) → Topology.IsOpenEmbedding (RestrictedProduct.structureMap R A Filter.cofinite)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Copy of `limit.hom_ext`, specialized to `piInters` for use by the `ext` tactic.  -/
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {X_1 : C}
  {f f' : X_1 ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U},
  (∀ (j : CategoryTheory.Discrete (ι × ι)),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2)))
            j) =
        CategoryTheory.CategoryStruct.comp f'
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2)))
            j)) →
    f = f'
-- Mathlib.CategoryTheory.Category.Pointed
/-- `Option` as a functor from types to pointed types. This is the free functor.  -/
typeToPointed : CategoryTheory.Functor (Type u) Pointed
-- Mathlib.Order.OrderDual
OrderDual.denselyOrdered : ∀ (α : Type u_2) [inst : LT α] [h : DenselyOrdered α], DenselyOrdered αᵒᵈ
-- Std.Http.Data.Headers.Name
/-- Standard Accept header name
 -/
Std.Http.Header.Name.accept : Std.Http.Header.Name
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_idx : ∀ {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (x : ↥(AlgebraicGeometry.Spec R)),
  (AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop s hs).idx x =
    have this := ⋯;
    this.choose
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the sum of two formal power series is at least the minimum of their orders.  -/
MvPowerSeries.min_weightedOrder_le_add : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
  min (MvPowerSeries.weightedOrder w f) (MvPowerSeries.weightedOrder w g) ≤ MvPowerSeries.weightedOrder w (f + g)
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_mod_card_parts_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), s.card % P.parts.card ≤ P.parts.card
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
/-- Left unitor for the vertical composition of strong natural transformations
between pseudofunctors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id F) η ≅ η
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- `m₁` is the morphism `b` of (TR 4) as presented in Stacks.  -/
CategoryTheory.Triangulated.Octahedron'.m₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃ → (Z₁₃ ⟶ Z₂₃)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.lift_comp_mk' : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M) (HN : N ≤ φ.ker), (QuotientAddGroup.lift N φ HN).comp (QuotientAddGroup.mk' N) = φ
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_toDual_symm_eq_charFunDual : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : CompleteSpace E] [inst_2 : InnerProductSpace ℝ E]
  {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} (L : StrongDual ℝ E),
  MeasureTheory.charFun μ ((InnerProductSpace.toDual ℝ E).symm L) = MeasureTheory.charFunDual μ L
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.instIsSplitEpiMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f] (F : CategoryTheory.Functor C D),
  CategoryTheory.IsSplitEpi (F.map f)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
Module.End.ker_pow_constant : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Module.End K V}
  {k : ℕ},
  LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) → ∀ (m : ℕ), LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))
-- Init.Data.Nat.Coprime
Nat.coprime_zero_right : ∀ (n : ℕ), n.Coprime 0 ↔ n = 1
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toArray_take_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.take n it).toArray = it.toArray.take n
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.of_obj_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Function.Bijective (CategoryTheory.FreeGroupoid.of C).obj