mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} (x : C),
  W.multiplicativeClosure' (CategoryTheory.CategoryStruct.id x)
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.mapPiLocalization_naturality : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  (PrimeSpectrum.mapPiLocalization f).comp ↑(PrimeSpectrum.toPiLocalization R) =
    (PrimeSpectrum.toPiLocalization S).comp f
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.FibrantObject C),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans.app X)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_div_left : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s t : Set α}, 1 ∈ t → s ⊆ s / t
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.eq_loopyOn_iff : ∀ {α : Type u_1} {M : Matroid α} {E : Set α}, M = Matroid.loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅
-- Mathlib.Probability.Distributions.Cauchy
/-- The pdf of the cauchy distribution integrates to 1.  -/
ProbabilityTheory.lintegral_cauchyPDF_eq_one : ∀ (x₀ : ℝ) {γ : NNReal}, γ ≠ 0 → ∫⁻ (x : ℝ), ProbabilityTheory.cauchyPDF x₀ γ x = 1
-- Mathlib.CategoryTheory.Subterminal
/-- If the unique morphism from `A` to the terminal object is a monomorphism, `A` is subterminal.
The converse of `IsSubterminal.mono_terminal_from`.
 -/
CategoryTheory.isSubterminal_of_mono_terminal_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)], CategoryTheory.IsSubterminal A
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l)).isSome = true
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- **Alias** of `PeriodPair.compl_lattice_sdiff_singleton_mem_nhds`. -/
PeriodPair.compl_lattice_diff_singleton_mem_nhds : ∀ (L : PeriodPair) (x : ℂ), (↑L.lattice \ {x})ᶜ ∈ nhds x
-- Mathlib.Algebra.WithConv
WithConv.toConv_multisetSum : ∀ {A : Type u_2} [inst : AddCommMonoid A] (s : Multiset A), WithConv.toConv s.sum = (Multiset.map WithConv.toConv s).sum
-- Mathlib.Algebra.Order.Floor.Div
/-- Ceiling division. If `a > 0`, then `b ⌈/⌉ a` is the least `c` such that `b ≤ a • c`.  -/
«term_⌈/⌉_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKey! k' = k
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapSetEmbedding_ground : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : ↑M.E ↪ β), (M.mapSetEmbedding f).E = Set.range ⇑f
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.IsHadamard.mk : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R},
  (∀ (i j : n), A i j ∈ unitary R) →
    A * A.conjTranspose = ↑(Fintype.card n) • 1 → A.conjTranspose * A = ↑(Fintype.card n) • 1 → A.IsHadamard
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.mkQCoalgHom_apply : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C) [inst_4 : I.IsCoideal] (x : C),
  (Coalgebra.Quotient.mkQCoalgHom I) x = Submodule.Quotient.mk x
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.coe_comap : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  (e : F →ₗ[K] E), ↑(ZLattice.comap K L e) = ⇑e ⁻¹' ↑L
-- Mathlib.Data.List.ReduceOption
List.length_eq_reduceOption_length_add_filter_none : ∀ {α : Type u_1} {l : List (Option α)}, l.length = l.reduceOption.length + (List.filter Option.isNone l).length
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (α.naturality (CategoryTheory.CategoryStruct.comp f g)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (α.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (α.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (α.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (α.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (α.naturality f).hom (G.map g))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (α.app a) (G.map f) (G.map g)).hom
                (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapComp f g).inv))))))
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_1.eq_3 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_3 ()
-- Init.Data.Vector.Lemmas
Vector.getElem_setIfInBounds_ne : ∀ {α : Type u_1} {n j i : ℕ} {xs : Vector α n} {x : α} (hj : j < n), i ≠ j → (xs.setIfInBounds i x)[j] = xs[j]
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.gcd_left : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a : α} (b : α),
  Squarefree a → Squarefree (gcd a b)
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.exists_iso_Q_obj_of_isGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) [hX : X.IsGE n],
  ∃ K, ∃ (_ : K.IsStrictlyGE n), Nonempty (X ≅ DerivedCategory.Q.obj K)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.isEmpty : {α : Type} → {x : Hashable α} → {x_1 : BEq α} → Lean.Meta.Try.Collector.OrdSet α → Bool
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsZeroOrMarkovKernel κ]
  (hg : Measurable g), ProbabilityTheory.IsZeroOrMarkovKernel (κ.comap g hg)
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A family with only finitely many nonzero elements is summable.  -/
HahnSeries.SummableFamily.ofFinsupp : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → (α →₀ HahnSeries Γ R) → HahnSeries.SummableFamily Γ R α
-- Mathlib.Order.Category.DistLat
DistLat.ext_iff : ∀ {X Y : DistLat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Init.Data.Option.Lemmas
Option.get!_inj : ∀ {α : Type u_1} [inst : Inhabited α] {o₁ o₂ : Option α},
  o₁.isSome = true → o₂.isSome = true → (o₁.get! = o₂.get! ↔ o₁ = o₂)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.dec : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Bool →
        Bool →
          Option ℕ →
            autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_13 →
              Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Topology.Algebra.FilterBasis
/-- A `RingFilterBasis` on a ring is a `FilterBasis` satisfying some additional axioms.
Example : if `R` is a topological ring then the neighbourhoods of the identity are a
`RingFilterBasis`. Conversely given a `RingFilterBasis` on a ring `R`, one can define a
topology on `R` which is compatible with the ring structure.  -/
RingFilterBasis : (R : Type u) → [Ring R] → Type u
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.homFromEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C},
  α.homFromEquiv =
    { toFun := fun f => CategoryTheory.CategoryStruct.comp α.inv f,
      invFun := fun g => CategoryTheory.CategoryStruct.comp α.hom g, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.unop_Z : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  {f : X ⟶ Y} (φ : W₁.MapFactorizationData W₂ f), φ.unop.Z = Opposite.unop φ.Z
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Sub` across an `Equiv`  -/
Equiv.sub : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Sub β] → Sub α
-- Lean.Parser.Basic
/-- Parse `$[p]suffix`, e.g. `$[p],*`.  -/
Lean.Parser.mkAntiquotSplice : Lean.SyntaxNodeKind → Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Analysis.Convex.StrictConvexSpace
StrictConvexSpace.strictConvex_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : NormedField 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : NormedAddCommGroup E}
  {inst_3 : NormedSpace 𝕜 E} [self : StrictConvexSpace 𝕜 E] (r : ℝ), 0 < r → StrictConvex 𝕜 (Metric.closedBall 0 r)
-- Mathlib.CategoryTheory.Functor.Currying
/-- The uncurrying functor, taking a functor `C ⥤ (D ⥤ E)` and producing a functor `(C × D) ⥤ E`.
 -/
CategoryTheory.Functor.uncurry : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E))
              (CategoryTheory.Functor (C × D) E)
-- Mathlib.Algebra.MvPolynomial.Cardinal
MvPolynomial.cardinalMk_eq_one : ∀ {σ : Type u} {R : Type v} [inst : CommSemiring R] [Subsingleton R], Cardinal.mk (MvPolynomial σ R) = 1
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- A bicategory structure on the lax functors between bicategories, with oplax transformations.  -/
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (CategoryTheory.LaxFunctor B C)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `ModuleCat R`.  -/
ModuleCat.of : (R : Type u) → [inst : Ring R] → (X : Type v) → [inst_1 : AddCommGroup X] → [Module R X] → ModuleCat R
-- Init.Data.Iterators.Consumers.Loop
/-- Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.
 -/
Std.Iter.fold : {α β : Type w} →
  {γ : Type x} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → (γ → β → γ) → γ → Std.Iter β → γ
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.invOf_iff : ∀ {R : Type u} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
  [inst_3 : Invertible x], IsAlgebraic R ⅟x ↔ IsAlgebraic R x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint],
  ((SheafOfModules.pullbackPushforwardAdjunction φ).homEquiv (SheafOfModules.unit S) (SheafOfModules.unit R))
      (SheafOfModules.pullbackObjUnitToUnit φ) =
    SheafOfModules.unitToPushforwardObjUnit φ
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.toRingNorm : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} → [inst_1 : Ring S] → [inst_2 : Algebra R S] → AlgebraNorm R S → RingNorm S
-- Mathlib.Algebra.Module.Defs
neg_one_smul : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M), -1 • x = -x
-- Mathlib.Data.Fintype.Defs
Fintype.decidableSurjectiveFintype : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [Fintype α] → [Fintype β] → DecidablePred Function.Surjective
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Functor.instEssSurjSkeletonMapSkeleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.EssSurj], F.mapSkeleton.EssSurj
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getKey! : {α : Type u} → {β : α → Type v} → [BEq α] → [Inhabited α] → α → Std.DHashMap.Internal.AssocList α β → α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousAdd.measurableAdd : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [inst_3 : Add γ]
  [SeparatelyContinuousAdd γ], MeasurableAdd γ
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.discreteTopology_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology (TopologicalSpace.Compacts α) ↔ DiscreteTopology α
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.top_mem : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α}, ⊤ ∈ L
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_map_le : ∀ {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  (x : HahnSeries Γ R) (f : ZeroHom R S), (x.map f).cardSupp ≤ x.cardSupp
-- Mathlib.Algebra.Module.TransferInstance
/-- Transfer `NoZeroSMulDivisors` across an `Equiv`  -/
Equiv.noZeroSMulDivisors : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) (R : Type u_4) [inst : Zero R] [inst_1 : Zero β] [inst_2 : SMul R β]
  [NoZeroSMulDivisors R β],
  have this := e.zero;
  have this_1 := Equiv.smul R e;
  NoZeroSMulDivisors R α
-- Mathlib.Topology.Connected.PathConnected
Joined.listSum : ∀ {M : Type u_4} [inst : AddZeroClass M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {l l' : List M},
  List.Forall₂ Joined l l' → Joined l.sum l'.sum
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the
Picard-Lindelöf/Cauchy-Lipschitz theorem.  -/
integral_pow_abs_sub_uIoc : ∀ {a b : ℝ} (n : ℕ), ∫ (x : ℝ) in Set.uIoc a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.sepDegree_top : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.sepDegree F ↥⊤ = Field.sepDegree F K
-- Mathlib.ModelTheory.Order
FirstOrder.Language.realize_denselyOrdered : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : Preorder M]
  [L.OrderedStructure M] [h : DenselyOrdered M], M ⊨ L.denselyOrderedSentence
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.hermiteTheorem.finite_of_finite_generating_set : ∀ (A : Type u_2) [inst : Field A] [inst_1 : CharZero A] {p : IntermediateField ℚ A → Prop} (S : Set { F // p F })
  {T : Set A}, T.Finite → (∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯) → S.Finite
-- Init.Data.Int.Gcd
Int.gcd_mul_left_right_of_gcd_eq_one : ∀ {n m k : ℤ}, n.gcd m = 1 → n.gcd (k * m) = n.gcd k
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.rat_dense' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (q : ℚ_[p]) {ε : ℚ}, 0 < ε → ∃ r, padicNormE (q - ↑r) < ε
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatch_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch p pos ↔
    ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
AddGroup.int_smulCommClass' : ∀ {M : Type u_1} {A : Type u_7} [inst : AddGroup A] [inst_1 : DistribSMul M A], SMulCommClass M ℤ A
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.inter_indicator_mul : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] {s t : Set ι} (f g : ι → M₀) (i : ι),
  (s ∩ t).indicator (fun j => f j * g j) i = s.indicator f i * t.indicator g i
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
/-- On objects, the functor which sends a formal direct factor `P` of a
functor `F : J ⥤ C` to the functor `J ⥤ Karoubi C` which sends `(j : J)` to
the corresponding direct factor of `F.obj j`.  -/
CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C) →
          CategoryTheory.Functor J (CategoryTheory.Idempotents.Karoubi C)
-- Std.Http.Data.Chunk
/-- Represents a chunk of data with optional extensions (key-value pairs).

The interpretation of a chunk depends on the protocol layer consuming it:

- HTTP/1.1: The zero-size wire encoding (`0\r\n\r\n`) is reserved
exclusively as the `last-chunk` terminator. The HTTP/1.1 writer silently discards
any empty chunk (including its extensions) rather than emitting a premature
end-of-body signal. `Encode.encode` on a `Chunk.empty` value does produce
`"0\r\n\r\n"`, but that path bypasses the writer's framing logic.

- HTTP/2 (not yet implemented): Chunked transfer encoding does not exist; HTTP/2 uses DATA
frames instead. This type is specific to the HTTP/1.1 wire format.

Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.7.1
 -/
Std.Http.Chunk : Type
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
CategoryTheory.Functor.mapPresheaf_map_f : ∀ {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)
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y), (F.mapPresheaf.map f).base = f.base
-- Mathlib.GroupTheory.Congruence.Defs
/-- The 1 of the quotient of a monoid by a congruence relation is the equivalence class of the
monoid's 1.  -/
Con.coe_one : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : One M] {c : Con M}, ↑1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.EdgeDisjointTriangles.instDecidable : {α : Type u_1} →
  {G : SimpleGraph α} → [DecidableEq α] → [Fintype α] → [DecidableRel G.Adj] → Decidable G.EdgeDisjointTriangles
-- Mathlib.Topology.Bornology.Constructions
Bornology.cobounded_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β],
  Bornology.cobounded (α × β) = (Bornology.cobounded α).coprod (Bornology.cobounded β)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.mk.inj : ∀ {J : Type u_1} {inst : LinearOrder J} {as as_1 : J}, { as := as } = { as := as_1 } → as = as_1
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_hom_app_of_add_eq_zero_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C) {Z : C}
  (h : (CategoryTheory.shiftFunctor C m).obj ((CategoryTheory.shiftFunctor C n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m n).hom.app X) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).inv.app X) h)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.nsmul_mk : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (n : ℕ) {x : α} (hx : 0 ≤ x),
  n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩
-- Init.Data.UInt.Bitwise
UInt8.toUSize_and : ∀ (a b : UInt8), (a &&& b).toUSize = a.toUSize &&& b.toUSize
-- Init.Data.List.Lemmas
List.one_lt_length_of_tail_ne_nil : ∀ {α : Type u_1} {l : List α}, l.tail ≠ [] → 1 < l.length
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The transpose of a matrix.

This is available in bundled forms as:
* `Matrix.transposeAddEquiv`
* `Matrix.transposeLinearEquiv`
* `Matrix.transposeRingEquiv`
* `Matrix.transposeAlgEquiv`
* `RingEquiv.mopMatrix`
* `AlgEquiv.mopMatrix`
 -/
Matrix.«term_ᵀ» : Lean.TrailingParserDescr
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedAtom : Inhabited Mathlib.Tactic.BicategoryLike.Atom
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- In an additive monoid with a single unit, irreducible elements lie in all generating sets.  -/
addIrreducible_subset_of_addSubmonoidClosure_eq_top : ∀ {M : Type u_1} [inst : AddCommMonoid M] [Subsingleton (AddUnits M)] {S : Set M},
  AddSubmonoid.closure S = ⊤ → {p | AddIrreducible p} ⊆ S
-- Mathlib.Algebra.Group.Prod
divMonoidHom_apply : ∀ {α : Type u_6} [inst : DivisionCommMonoid α] (a : α × α), divMonoidHom a = a.1 / a.2
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The map between indexing types of the coverings of `S`  -/
CategoryTheory.PreZeroHypercover.Hom.s₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} → {F : CategoryTheory.PreZeroHypercover S} → E.Hom F → E.I₀ → F.I₀
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- Given a root pairing, this is an invariant symmetric bilinear form satisfying a positivity
condition.  -/
RootPairing.RootPositiveForm : {ι : Type u_1} →
  {R : Type u_2} →
    (S : Type u_3) →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommRing S] →
            [LinearOrder S] →
              [inst_2 : CommRing R] →
                [inst_3 : Algebra S R] →
                  [inst_4 : AddCommGroup M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommGroup N] →
                        [inst_7 : Module R N] → (P : RootPairing ι R M N) → [P.IsValuedIn S] → Type (max u_2 u_4)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
_private.Std.Data.Iterators.Lemmas.Equivalence.Basic.0.Std.quotOfQuot : {α : Sort u_1} → {R S : α → α → Prop} → (∀ (a b : α), R a b → S a b) → Quot R → Quot S
-- Mathlib.Data.Stream.Init
Stream'.interleave_tail_tail : ∀ {α : Type u} (s₁ s₂ : Stream' α), s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail