mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod_comp_inr : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M), f₁.coprod f₂ ∘SL ContinuousLinearMap.inr R M₁ M₂ = f₂
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.action.sizeOf_spec : ∀ (action : Lean.Syntax), sizeOf (Lean.Elab.Term.Do.Code.action action) = 1 + sizeOf action
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.coneAt_pt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D),
  (E.coneAt Y).pt = (CategoryTheory.CostructuredArrow.left E).obj Y
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
exteriorPower.instCoreRealSubtypeExteriorAlgebraMemSubmoduleExteriorPowerOfFiniteDimensional : {n : ℕ} →
  {E : Type u_1} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : InnerProductSpace ℝ E] → [FiniteDimensional ℝ E] → InnerProductSpace.Core ℝ ↥(⋀[ℝ]^n E)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.le_card_smul_iff_subset : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ s.card • t ↔ s ⊆ t
-- Mathlib.RingTheory.Teichmuller
/-- If `R` is `I`-adically complete and `R ⧸ I` has characteristic `p`, then
`Perfection R p` and `Perfection (R ⧸ I) p` are isomorphic as monoids.

Note that `Perfection R p` is generally not a ring, and the forward map is induced by
the quotient map, and the backwards map is constructed using the Teichmüller map.  -/
Perfection.quotientMulEquiv : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        (I : Ideal R) → [inst_2 : CharP (R ⧸ I) p] → [IsAdicComplete I R] → Perfection R p ≃* Perfection (R ⧸ I) p
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.regular : Lean.Elab.Visibility
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.one_le_prob_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ], 1 ≤ μ s ↔ μ s = 1
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.apply_mem_fixedPoints_iff_mem_of_mem_centralizer : ∀ {α : Type u} {g p : Equiv.Perm α},
  p ∈ Subgroup.centralizer {g} → ∀ {x : α}, p x ∈ Function.fixedPoints ⇑g ↔ x ∈ Function.fixedPoints ⇑g
-- Init.Data.SInt.Lemmas
Int32.toISize_div_of_ne_right : ∀ (a b : Int32), b ≠ -1 → (a / b).toISize = a.toISize / b.toISize
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBy_coe : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : Type v) [inst_1 : TopologicalSpace Y],
  ⇑(Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBy X Y) = ⇑Topology.WithGeneratedByTopology.equiv
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves limits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X),
  Monotone fun n => Urysohns.CU.approx n c x
-- Mathlib.Order.RelClasses
WellFounded.prod_lex : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop},
  WellFounded ra → WellFounded rb → WellFounded (Prod.Lex ra rb)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Return the expression `(stepEntry n A)^[t] (get n A)`.  -/
Mathlib.Tactic.Determinant.Ctx.iterStepEntry : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Ctx rα → ℕ → Q(ℕ → ℕ → «$α»)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (r : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β k_1) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size k v
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
              motive x
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] (toFun toFun_1 : X → Y)
  (e_toFun : toFun = toFun_1) (supportWithinDomain' : Function.support toFun ⊆ U)
  (supportLocallyFiniteWithinDomain' : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun).Finite),
  { toFun := toFun, supportWithinDomain' := supportWithinDomain',
      supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain' } =
    { toFun := toFun_1, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.isLocalization_algebraMapSubmonoid_map_algHom : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Bₚ : Type u_10)
  [inst_5 : CommSemiring Bₚ] [inst_6 : Algebra B Bₚ] [IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
  (f : A →ₐ[R] B), IsLocalization (Submonoid.map f.toRingHom (Algebra.algebraMapSubmonoid A M)) Bₚ
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_eq_none_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, Fin.findSome? f = none ↔ ∀ (i : Fin n), f i = none
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_singleton_ne_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), s.excenter {i} ≠ s.incenter
-- Batteries.Data.UInt
UInt64.lt_iff_toNat_lt_toNat : ∀ {x y : UInt64}, x < y ↔ x.toNat < y.toNat
-- Mathlib.Algebra.Ring.Parity
neg_one_pow_eq_ite : ∀ {R : Type u_4} [inst : Monoid R] [inst_1 : HasDistribNeg R] {n : ℕ}, (-1) ^ n = if Even n then 1 else -1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context : Type
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.instMonoHSMulHomOfInvertible : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type w)
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (r : R)
  [Invertible r], CategoryTheory.Mono (r • f)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {x y : R},
  x ≠ 0 → y ≠ 0 → (IsDiscreteValuationRing.toWithBotNat x ≤ IsDiscreteValuationRing.toWithBotNat y ↔ x ∣ y)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.mk : {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} →
              [toLaxMonoidal : F.LaxMonoidal] →
                [toOplaxMonoidal : F.OplaxMonoidal] →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
                          (CategoryTheory.Functor.OplaxMonoidal.η F) =
                        CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
                      CategoryTheory.Functor.Monoidal.ε_η._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
                            (CategoryTheory.Functor.LaxMonoidal.ε F) =
                          CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
                        CategoryTheory.Functor.Monoidal.η_ε._autoParam →
                      autoParam
                          (∀ (X Y : C),
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
                                (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) =
                              CategoryTheory.CategoryStruct.id
                                (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))
                          CategoryTheory.Functor.Monoidal.μ_δ._autoParam →
                        autoParam
                            (∀ (X Y : C),
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
                                  (CategoryTheory.Functor.LaxMonoidal.μ F X Y) =
                                CategoryTheory.CategoryStruct.id
                                  (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)))
                            CategoryTheory.Functor.Monoidal.δ_μ._autoParam →
                          F.Monoidal
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k : α},
  k ∈ Std.DHashMap.filterMap f m ↔ ∃ (h : k ∈ m), (f (m.getKey k h) (Std.DHashMap.Const.get m k h)).isSome = true
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- The linear equivalence between families indexed by `p : Π i : ι, κ i` of multilinear maps
on the `fun i ↦ M i (p i)` and the space of multilinear map on `fun i ↦ Π₀ j : κ i, M i j`.  -/
MultilinearMap.fromDFinsuppEquiv : {ι : Type uι} →
  (κ : ι → Type uκ) →
    (R : Type uR) →
      {M : (i : ι) → κ i → Type uM} →
        [DecidableEq ι] →
          [Fintype ι] →
            [inst : CommSemiring R] →
              [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
                [inst_2 : (i : ι) → (k : κ i) → Module R (M i k)] →
                  {N : Type u_1} →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : Module R N] →
                        [(i : ι) → DecidableEq (κ i)] →
                          ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) N) ≃ₗ[R]
                            MultilinearMap R (fun i => Π₀ (j : κ i), M i j) N
-- Mathlib.Data.Set.Basic
Set.sep_empty : ∀ {α : Type u} (p : α → Prop), {x | x ∈ ∅ ∧ p x} = ∅
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.repr.congr_simp : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v), hv.repr = hv.repr
-- Init.Data.List.Lemmas
List.head?_eq_getElem? : ∀ {α : Type u_1} {l : List α}, l.head? = l[0]?
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k k' fallback : α},
  cmp k k' = Ordering.eq → t.getD k fallback = t.getD k' fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
        CategoryTheory.Limits.prod.fst) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.convMul_comp_coalgHom_distrib : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : Coalgebra R C] [inst_8 : AddCommMonoid B] [inst_9 : Module R B]
  [inst_10 : CoalgebraStruct R B] (f g : WithConv (C →ₗ[R] A)) (h : B →ₗc[R] C),
  (f * g).ofConv ∘ₗ h.toLinearMap =
    (WithConv.toConv (f.ofConv ∘ₗ h.toLinearMap) * WithConv.toConv (g.ofConv ∘ₗ h.toLinearMap)).ofConv
-- Mathlib.Data.DFinsupp.Defs
/-- Bijection obtained by separating the term of index `none` of a dfinsupp over `Option ι`.

This is the dfinsupp version of `Equiv.piOptionEquivProd`.  -/
DFinsupp.equivProdDFinsupp : {ι : Type u} →
  {α : Option ι → Type v} →
    [inst : (i : Option ι) → Zero (α i)] → (Π₀ (i : Option ι), α i) ≃ α none × Π₀ (i : ι), α (some i)
-- Mathlib.RingTheory.KrullDimension.Basic
ringKrullDim_ne_top : ∀ {R : Type u_1} [inst : CommSemiring R] [FiniteRingKrullDim R], ringKrullDim R ≠ ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroObject C],
  S.f = 0 → (S.Exact ↔ CategoryTheory.Mono S.g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.product_pow : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Monoid α] [inst_3 : Monoid β]
  (s : Finset α) (t : Finset β) (n : ℕ), s ×ˢ t ^ n = (s ^ n) ×ˢ (t ^ n)
-- Mathlib.Analysis.Real.Hyperreal
/-- Construct a hyperreal number from a sequence of real numbers.  -/
Hyperreal.ofSeq : (ℕ → ℝ) → ℝ*
-- Mathlib.CategoryTheory.Presentable.Presheaf
CategoryTheory.Presheaf.isStrongGenerator : ∀ {A : Type u'} [inst : CategoryTheory.Category.{v', u'} A] {P : CategoryTheory.ObjectProperty A},
  P.IsStrongGenerator →
    ∀ [inst_1 : CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Limits.HasPullbacks A] (C : Type w)
      [inst_3 : CategoryTheory.SmallCategory C],
      (CategoryTheory.ObjectProperty.ofObj fun T => CategoryTheory.Presheaf.freeYoneda T.1 ↑T.2).IsStrongGenerator
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ne_empty_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∈ t → t ≠ ∅
-- Mathlib.Algebra.Module.Submodule.Range
/-- A monomorphism is injective.  -/
LinearMap.ker_eq_bot_of_cancel : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [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₂}
  {f : M →ₛₗ[τ₁₂] M₂}, (∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v) → f.ker = ⊥
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_truncLT_of_lt : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : PartialOrder Γ] [inst_2 : DecidableLT Γ] {c i : Γ},
  i < c → ∀ (x : HahnSeries Γ R), ((HahnSeries.truncLT c) x).coeff i = x.coeff i
-- Mathlib.Order.WellFoundedSet
Set.isPWO_union : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, (s ∪ t).IsPWO ↔ s.IsPWO ∧ t.IsPWO
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Multiplication in `ℤ√d`  -/
Zsqrtd.instMul : {d : ℤ} → Mul (ℤ√d)
-- Mathlib.Data.PEquiv
/-- The partial inverse of `toFun`  -/
PEquiv.invFun : {α : Type u} → {β : Type v} → (α ≃. β) → β → Option α
-- Mathlib.Topology.NhdsKer
nhdsKer_iInter_subset : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : ι → Set X}, nhdsKer (⋂ i, s i) ⊆ ⋂ i, nhdsKer (s i)
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.appHom_apply : ∀ {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] [inst_2 : CategoryTheory.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G), (CategoryTheory.NatTrans.appHom X) α = α.app X
-- Mathlib.CategoryTheory.Galois.Basic
/-- An object is not initial if and only if its fiber is nonempty.  -/
CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  (∀ (a : CategoryTheory.Limits.IsInitial X), False) ↔ Nonempty (F.obj X).obj
-- Mathlib.Order.Disjoint
Disjoint.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] (a b : α),
  Disjoint a b = ∀ ⦃x : α⦄, x ≤ a → x ≤ b → x ≤ ⊥
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Two affine subspaces are equal if they have the same points.  -/
AffineSubspace.coe_injective : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Function.Injective SetLike.coe
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralAlgNorm_of_finiteDimensional_normal_def : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] [inst_3 : IsUltrametricDist K] (x : L),
  (spectralAlgNorm_of_finiteDimensional_normal K L) x = spectralNorm K L x
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivWithinAt.sub` -/
HasDerivWithinAt.fun_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt g g' s x → HasDerivWithinAt (fun i => f i - g i) (f' - g') s x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], ⊥.toNonUnitalSubalgebra = ⊥
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.comp_fst_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {f : α → X},
  ν ≠ 0 → (MeasureTheory.AEStronglyMeasurable (fun x => f x.1) (μ.prod ν) ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Mathlib.Order.CountableSupClosed
countableSupClosure_eq_self : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], countableSupClosure s = s ↔ CountableSupClosed s
-- Mathlib.Data.Set.Card.Arithmetic
Set.encard_iUnion_of_finite : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] {s : ι → Set α},
  Pairwise (Function.onFun Disjoint s) → (⋃ i, s i).encard = ∑ᶠ (i : ι), (s i).encard
-- Mathlib.ModelTheory.PartialEquiv
/-- For a countably generated structure `M` and a structure `N`, if any partial equivalence
between finitely generated substructures can be extended to any element in the domain,
then there exists an embedding of `M` in `N`.  -/
FirstOrder.Language.embedding_from_cg : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.CG L M → ∀ (g : L.FGEquiv M N), L.IsExtensionPair M N → ∃ f, ↑g ≤ f.toPartialEquiv
-- Mathlib.CategoryTheory.Adjunction.Whiskering
CategoryTheory.Adjunction.whiskerRight_unit_app_app : ∀ (C : Type u_1) {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor C D)
  (X_1 : C), ((CategoryTheory.Adjunction.whiskerRight C adj).unit.app X).app X_1 = adj.unit.app (X.obj X_1)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Construct a functor out of the wide pushout shape given a J-indexed collection of arrows from a
fixed object.
 -/
CategoryTheory.Limits.WidePushoutShape.wideSpan : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (objs : J → C) → ((j : J) → B ⟶ objs j) → CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) C
-- Std.Tactic.Do.Syntax
Lean.Parser.Category.mrefinePat : Lean.Parser.Category
-- Mathlib.Order.SuccPred.Basic
/-- Successor function  -/
SuccOrder.succ : {α : Type u_3} → {inst : Preorder α} → [self : SuccOrder α] → α → α
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.curr : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator → ℕ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.instMonoidalProdProd : {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] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  {C' : Type u₁'} →
                    [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] →
                      (F : CategoryTheory.Functor C D) →
                        (G : CategoryTheory.Functor E C') →
                          [inst_7 : CategoryTheory.MonoidalCategory C'] →
                            [F.Monoidal] → [G.Monoidal] → (F.prod G).Monoidal
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The cocone associated to a locally directed diagram is a colimit as locally ringed spaces.

One usually does not want to use this directly, and instead use the generic `colimit` API.
 -/
AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpace : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [inst_3 : Quiver.IsThin J] →
            [inst_4 : Small.{u, w} J] →
              CategoryTheory.Limits.IsColimit
                (AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.mapCocone
                  (AlgebraicGeometry.Scheme.IsLocallyDirected.cocone F))