mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₂] [P.IsClosedUnderIsomorphisms],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- Constructor for morphisms in `FibrantObject C`.  -/
HomotopicalAlgebra.FibrantObject.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] →
      [inst_2 : CategoryTheory.Limits.HasTerminal C] →
        {X Y : C} →
          [inst_3 : HomotopicalAlgebra.IsFibrant X] →
            [inst_4 : HomotopicalAlgebra.IsFibrant Y] →
              (X ⟶ Y) → (HomotopicalAlgebra.FibrantObject.mk X ⟶ HomotopicalAlgebra.FibrantObject.mk Y)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_codetector : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C]
  [inst_2 : CategoryTheory.HasCodetector C], CategoryTheory.IsCoseparator (CategoryTheory.codetector C)
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E), p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
-- Mathlib.Algebra.Group.Equiv.Defs
AddMonoid.End.equiv_symm_apply : ∀ {M : Type u_9} [inst : AddZero M] (f : M →+ M) (x : M), ((AddMonoid.End.equiv M).symm f) x = f x
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The subgroups generate the group  -/
MulAction.IwasawaStructure.is_generator : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] (self : MulAction.IwasawaStructure M α),
  iSup self.T = ⊤
-- Mathlib.Algebra.GradedMonoid
SetLike.coe_gnpow : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  (A : ι → S) [inst_3 : SetLike.GradedMonoid A] {i : ι} (x : ↥(A i)) (n : ℕ), ↑(GradedMonoid.GMonoid.gnpow n x) = ↑x ^ n
-- Mathlib.Data.TwoPointing
TwoPointing.pi_fst : ∀ (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [inst : Nonempty α],
  (TwoPointing.pi α q).toProd.1 = Function.const α q.toProd.1
-- Init.Data.BitVec.Lemmas
BitVec.zero_add : ∀ {n : ℕ} (x : BitVec n), 0#n + x = x
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.DSmooth.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y]
  [inst_2 : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z},
  Diffeology.DSmooth g → Diffeology.DSmooth f → Diffeology.DSmooth (g ∘ f)
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Variant of `ofπ` where the vanishing condition is expressed in terms
of a composition of linear maps.  -/
Module.Relations.Solution.ofπ' : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] → (π : (relations.G →₀ A) →ₗ[A] M) → π ∘ₗ relations.map = 0 → relations.Solution M
-- Std.Data.DHashMap.Basic
Std.DHashMap.instMembership : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Membership α (Std.DHashMap α β)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.singleton : ∀ {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.QuasiCompactCover (CategoryTheory.PreZeroHypercover.singleton f)
-- Lean.Elab.Level
Lean.Elab.Level.maxUniverseOffset : Lean.Option ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- Given a pre-path object `P` for `Y`, two maps `f` and `g` in `X ⟶ Y` are
homotopic relative to `P` when there is a morphism `h : X ⟶ P.P`
such that `h ≫ P.p₀ = f` and `h ≫ P.p₁ = g`.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} → HomotopicalAlgebra.PrepathObject Y → {X : C} → (X ⟶ Y) → (X ⟶ Y) → Type v
-- Mathlib.Data.Set.Lattice
Set.iInter_mono'' : ∀ {α : Type u_1} {ι : Sort u_5} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → Set.iInter s ⊆ Set.iInter t
-- Lean.Meta.Coe
/-- Coerces `expr` to `expectedType` using `CoeT`.  -/
Lean.Meta.coerceSimpleRecordingNames? : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.LOption (Lean.Expr × List Lean.Name))
-- Mathlib.CategoryTheory.Abelian.Basic
/-- There is a canonical isomorphism between the abelian image and the categorical image of a
morphism.  -/
CategoryTheory.Abelian.imageIsoImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Abelian.image f ≅ CategoryTheory.Limits.image f
-- Init.Data.UInt.Bitwise
UInt16.xor_right_inj : ∀ {a b : UInt16} (c : UInt16), c ^^^ a = c ^^^ b ↔ a = b
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_of : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (FreeAddGroup.of a).toWord = [(a, true)]
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.Iio_mem_nhds_zero : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀}, γ ≠ 0 → Set.Iio γ ∈ nhds 0
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.apply_ofInjective_symm : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} (hf : Function.Injective ⇑f)
  (x : ↥f.range), f ((MonoidHom.ofInjective hf).symm x) = ↑x
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `MorphismProperty.Under.pushout` commutes with `MorphismProperty.Under.forget`.  -/
CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          (f : X ⟶ Y) →
            [inst_2 : CategoryTheory.Limits.HasPushoutsAlong f] →
              [inst_3 : P.IsStableUnderCobaseChangeAlong f] →
                [inst_4 : Q.IsStableUnderCobaseChange] →
                  (CategoryTheory.MorphismProperty.Under.pushout P Q f).comp
                      (CategoryTheory.MorphismProperty.Under.forget P Q Y) ≅
                    (CategoryTheory.MorphismProperty.Under.forget P Q X).comp (CategoryTheory.Under.pushout f)
-- Init.Data.AC
Lean.Data.AC.Context.mk.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α] (op : α → α → α) (assoc : Std.Associative op)
  (comm : Option (PLift (Std.Commutative op))) (idem : Option (PLift (Std.IdempotentOp op)))
  (vars : List (Lean.Data.AC.Variable op)) (arbitrary : α),
  sizeOf { op := op, assoc := assoc, comm := comm, idem := idem, vars := vars, arbitrary := arbitrary } =
    1 + sizeOf assoc + sizeOf comm + sizeOf idem + sizeOf vars + sizeOf arbitrary
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If `s` is a family of linearly independent vectors contained in a set `t` spanning `V`,
then one can get a basis of `V` containing `s` and contained in `t`.  -/
Module.Basis.extendLe : {K : Type u_3} →
  {V : Type u_4} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {s t : Set V} →
            (hs : LinearIndepOn K id s) → (hst : s ⊆ t) → ⊤ ≤ Submodule.span K t → Module.Basis (↑(hs.extend hst)) K V
-- Mathlib.Data.Num.Basic
/-- Greatest Common Divisor (GCD) of two `Num`s.  -/
Num.gcd : Num → Num → Num
-- Mathlib.Analysis.Complex.PhragmenLindelof
_private.Mathlib.Analysis.Complex.PhragmenLindelof.0.termExpR : Lean.ParserDescr
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instSymmetricCategory : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] →
          [CategoryTheory.SymmetricCategory V] → CategoryTheory.SymmetricCategory (Action V G)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_toNonUnitalSubsemiring : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F},
  (NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_fst : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ↑(ContinuousLinearMap.fst R M₁ M₂) = LinearMap.fst R M₁ M₂
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? k' (Std.Internal.List.modifyKey k f l) =
      if h : (k == k') = true then cast ⋯ (Option.map f (Std.Internal.List.getValueCast? k l))
      else Std.Internal.List.getValueCast? k' l
-- Mathlib.Data.Ineq
Mathlib.Ineq.le.sizeOf_spec : sizeOf Mathlib.Ineq.le = 1
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.antidiagonal_mono_right`. -/
Finset.addAntidiagonal_mono_right : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO},
  u ⊆ t → Finset.antidiagonal hs hu a ⊆ Finset.antidiagonal hs ht a
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.right_quotientAction : ∀ {G : Type u} [inst : Group G] (H : Subgroup G), MulAction.QuotientAction (↥(Subgroup.normalizer ↑H).op) H
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsometryEquiv.prodProdProdComm_invFun : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R N₁] [inst_9 : Module R N₂]
  [inst_10 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P)
  (Q₄ : QuadraticMap R N₂ P) (mmnn : (M₁ × N₁) × M₂ × N₂),
  (QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄).invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeParams.mk.inj : ∀ {textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier},
  { textDocument := textDocument } = { textDocument := textDocument_1 } → textDocument = textDocument_1
-- Aesop.Tree.Data
Aesop.Goal.isNormal : Aesop.Goal → Bool
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  HomologicalComplex.homotopyCofiber.inlX φ i j hij =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).inv
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C}
  (k : CategoryTheory.IsKernelPair f a b) (p q : S ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f),
  CategoryTheory.CategoryStruct.comp (k.lift p q w) a = p
-- Batteries.Data.List.Lemmas
List.disjoint_of_subset_left : ∀ {α : Type u_1} {l₁ l l₂ : List α}, l₁ ⊆ l → l.Disjoint l₂ → l₁.Disjoint l₂
-- Mathlib.NumberTheory.Dioph
/-- A partial function is Diophantine if its graph is Diophantine.  -/
Dioph.DiophPFun : {α : Type u} → ((α → ℕ) →. ℕ) → Prop
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The empty manifold is boundaryless.  -/
ModelWithCorners.BoundarylessManifold.of_empty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsEmpty M], BoundarylessManifold I M
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_iff_int : ∀ (L : Type v) (M : Type w) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M],
  LieModule.IsNilpotent L M ↔ ∃ k, LieModule.lowerCentralSeries ℤ L M k = ⊥
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatLT n hn).toUInt16 = UInt16.ofNat n
-- Mathlib.RingTheory.Valuation.AlgebraInstances
ValuationSubring.isIntegral_of_mem_ringOfIntegers' : ∀ {K : Type u_1} [inst : Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [inst_1 : Field L]
  [inst_2 : Algebra K L] {x : ↥(integralClosure (↥v.valuationSubring) L)}, IsIntegral (↥v.valuationSubring) x
-- Mathlib.GroupTheory.CommutingProbability
Subgroup.commProb_quotient_le : ∀ {G : Type u_2} [inst : Group G] [Finite G] (H : Subgroup G) [inst_2 : H.Normal],
  commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instLawfulUpwardEnumerableLE : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β],
  Std.PRange.LawfulUpwardEnumerableLE α
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.instInjectiveXObjSingle : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : DecidableEq ι] (i j : ι) (I : C) [CategoryTheory.Injective I],
  CategoryTheory.Injective (((HomologicalComplex.single C c i).obj I).X j)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.hom_ext_iff : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {X : C} {g₁ g₂ : ∐ f ⟶ X},
  g₁ = g₂ ↔
    ∀ (b : β),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₁ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₂
-- Mathlib.Topology.VectorBundle.Riemannian
/-- In a continuous Riemannian bundle, local changes of coordinates given by the trivialization at
a point distort the norm by a factor arbitrarily close to 1.  -/
eventually_norm_symmL_trivializationAt_comp_self_lt : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F : Type u_2) [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  (E : B → Type u_3) [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E]
  [h : IsContinuousRiemannianBundle F E] (x : B) {r : ℝ},
  1 < r →
    ∀ᶠ (y : B) in nhds x,
      ‖Bundle.Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
            Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
        r
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `K` is contained in `Kᗮᗮ`.  -/
Submodule.le_orthogonal_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), K ≤ Kᗮᗮ
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.pair : ∀ {f g : ℕ → ℕ}, Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun n => Nat.pair (f n) (g n)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k : α} {fallback : Unit},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.unitOfList l cmp) k fallback = ()
-- Mathlib.Order.ModularLattice
Codisjoint.codisjoint_inf_left_of_codisjoint_inf_right : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : OrderTop α] [IsModularLattice α],
  Codisjoint b c → Codisjoint a (b ⊓ c) → Codisjoint (a ⊓ b) c
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_unitOfList_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashMap.Raw.unitOfList l).size ≤ l.length
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.biproductComparison_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] (j : J) {Z : D} (h : (F.obj ∘ f) j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.biproductComparison f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (F.obj ∘ f) j) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.biproduct.π f j)) h
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
/-- A morphism of schemes `X ⟶ Y` is integral if the preimage of any affine open subset of `Y` is
affine and the induced ring hom on sections is integral.  -/
AlgebraicGeometry.IsIntegralHom : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A trail doesn't go through a vertex that is disconnected from its endpoints by an edge.  -/
SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v},
  w.IsTrail → ¬(G.deleteEdges {s(x, y)}).Reachable u y → ¬(G.deleteEdges {s(x, y)}).Reachable v y → y ∉ w.support
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientGroup.measurable_from_quotient : ∀ {α : Type u_1} [inst : MeasurableSpace α] {G : Type u_6} [inst_1 : Group G] [inst_2 : MeasurableSpace G]
  {S : Subgroup G} {f : G ⧸ S → α}, Measurable f ↔ Measurable (f ∘ QuotientGroup.mk)
-- Mathlib.Analysis.Analytic.Inverse
/-- The left inverse does not depend on the zeroth coefficient of a formal multilinear
series.  -/
FormalMultilinearSeries.leftInv_removeZero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E), p.removeZero.leftInv i x = p.leftInv i x
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_finset_preimage_atTop_atTop : ∀ {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f),
  Filter.Tendsto (fun s => s.preimage f ⋯) Filter.atTop Filter.atTop
-- Mathlib.Data.List.MinMax
/-- Auxiliary definition for `argmax` and `argmin`.  -/
List.argAux : {α : Type u_1} → (r : α → α → Prop) → [DecidableRel r] → Option α → α → Option α
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.reflectsIsomorphisms_forget : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G],
  (CategoryTheory.forget (Rep.{w, u, v} k G)).ReflectsIsomorphisms
-- Lean.Data.KVMap
Lean.KVMap.getSyntax : Lean.KVMap → Lean.Name → optParam Lean.Syntax Lean.Syntax.missing → Lean.Syntax
-- Mathlib.Computability.DFA
/-- Regular languages are closed under complement.  -/
Language.IsRegular_compl : ∀ {T : Type u} {L : Language T}, Lᶜ.IsRegular ↔ L.IsRegular
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_smul : ∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : NormedSpace 𝕜 E] (c : 𝕜)
  (f : α → E) (m : MeasurableSpace α), μ[c • f | m] =ᵐ[μ] c • μ[f | m]
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightResult : Type
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_neg : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] (x : WithLp p V), (-x).ofLp = -x.ofLp
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_ciSup : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompletePartialOrderSup α] [SupConvergenceClass α] {f : ι → α},
  Monotone f → BddAbove (Set.range f) → Filter.Tendsto f Filter.atTop (nhds (⨆ i, f i))
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
FiberBundle.trivializationAt_continuousAlternatingMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (x₀ : B),
  trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀ =
    Bundle.Trivialization.continuousAlternatingMap 𝕜 ι (trivializationAt F₁ E₁ x₀) (trivializationAt F₂ E₂ x₀)
-- Mathlib.Data.PNat.Xgcd
/-- Final value of `x`  -/
PNat.gcdX : ℕ+ → ℕ+ → ℕ
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} (f g : X ⟶ Y),
  f + g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
      (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGE?ₘ k t =
    Std.DTreeMap.Internal.Impl.applyPartition (compare k) t fun x c x_1 r => c.inner.or r.head?