mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Preorder
/-- Extract the underlying inequality from a morphism in a preorder category.  -/
CategoryTheory.leOfHom : ∀ {X : Type u} [inst : Preorder X] {x y : X} (h : x ⟶ y), x ≤ y
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_pi : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_7}
  {ι' : Type u_10} {N : ι' → Type u_11} [inst_3 : (i : ι') → AddCommMonoid (N i)] [inst_4 : (i : ι') → Module R (N i)]
  (f : (i : ι') → M [⋀^ι]→ₗ[R] N i), ↑(AlternatingMap.pi f) = MultilinearMap.pi fun a => ↑(f a)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instProjectiveUnopOfOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Cᵒᵖ} [CategoryTheory.Injective J],
  CategoryTheory.Projective (Opposite.unop J)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
AntitoneOn.slope_nonpos : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k} {s : Set k}, AntitoneOn f s → x ∈ s → y ∈ s → slope f x y ≤ 0
-- Init.Data.SInt.Lemmas
ISize.zero_div : ∀ {a : ISize}, 0 / a = 0
-- Mathlib.Data.Finset.Insert
/-- Combine a product with a pi type to pi of cons.  -/
Finset.prodPiCons : {α : Type u_1} →
  {s : Finset α} →
    [DecidableEq α] →
      (f : α → Type u_3) →
        {a : α} → (has : a ∉ s) → f a × ((i : α) → i ∈ s → f i) → (i : α) → i ∈ Finset.cons a s has → f i
-- Mathlib.Topology.LocallyConstant.Algebra
/-- Evaluation as a linear map  -/
LocallyConstant.evalₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      (R : Type u_6) →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid Y] → [inst_3 : Module R Y] → X → LocallyConstant X Y →ₗ[R] Y
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
  HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h =
    HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.bot_lt_under_prime : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] [IsDomain R],
  M ≤ nonZeroDivisors R → ∀ (p : Ideal S) [hpp : p.IsPrime], p ≠ ⊥ → ⊥ < Ideal.under R p
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearEquiv.alternatingMapCongrRight_apply_apply : ∀ {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} {N₂'' : Type u_14} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid M''] [inst_2 : AddCommMonoid N''] [inst_3 : AddCommMonoid N₂''] [inst_4 : Module R' M'']
  [inst_5 : Module R' N''] [inst_6 : Module R' N₂''] (e : N'' ≃ₗ[R'] N₂'') (f : M'' [⋀^ι]→ₗ[R'] N'')
  (a : (i : ι) → (fun x => M'') i), (e.alternatingMapCongrRight f) a = e (f a)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_singleton_pow : ∀ {R : Type u} [inst : CommSemiring R] (f : R) (n : ℕ),
  0 < n → PrimeSpectrum.zeroLocus {f ^ n} = PrimeSpectrum.zeroLocus {f}
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The colimit of `iterationFunctor I κ`.  -/
CategoryTheory.SmallObject.iteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [I.IsCardinalForSmallObjectArgument κ] →
              CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.symm_dual_id : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α],
  BoundedLatticeHom.dual.symm (BoundedLatticeHom.id αᵒᵈ) = BoundedLatticeHom.id α
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.LocallyLinear.edgeDisjointTriangles : ∀ {α : Type u_1} {G : SimpleGraph α}, G.LocallyLinear → G.EdgeDisjointTriangles
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.connectionContext : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Std.CancellationContext
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A scheme `X` is Noetherian if it is locally Noetherian and compact.  -/
AlgebraicGeometry.IsNoetherian : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.homAux_eq : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex C c} (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : Option ι) (i j : ι) (hi : i' = some i)
  (hj : j' = some j),
  Homotopy.extend.homAux φ i' j' =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XIso K hi).hom
      (CategoryTheory.CategoryStruct.comp (φ i j) (HomologicalComplex.extend.XIso L hj).inv)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn (fun a x d => f a d) init ↑m = forIn (↑m).keysArray init f
-- Std.Data.ExtTreeMap.Basic
/-- Folds the given function over the mappings in the map in ascending order.  -/
Std.ExtTreeMap.foldl : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {δ : Type w} → [Std.TransCmp cmp] → (δ → α → β → δ) → δ → Std.ExtTreeMap α β cmp → δ
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real from within a convex set, `derivWithin` version  -/
derivWithin.lhopital_zero_nhdsWithin_convex : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ} {s : Set ℝ},
  Convex ℝ s →
    (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), DifferentiableWithinAt ℝ f (s \ {a}) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), derivWithin g (s \ {a}) x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (s \ {a})) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (s \ {a})) (nhds 0) →
            Filter.Tendsto (fun x => derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (nhdsWithin a (s \ {a})) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (s \ {a})) l
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instCharP : ∀ (k : Type u) [inst : Field k] {p : ℕ} [CharP k p], CharP (AlgebraicClosure k) p
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
/-- The functor `N` for the equivalence is `normalizedMooreComplex A`  -/
CategoryTheory.Abelian.DoldKan.N : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] → CategoryTheory.Functor (CategoryTheory.SimplicialObject A) (ChainComplex A ℕ)
-- Mathlib.Algebra.Group.Graph
/-- **Line test** for monoid isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some
group isomorphism `f' : H ≃ I`.  -/
AddMonoidHom.exists_addEquiv_range_eq_graph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddGroup I]
  {f : G →+ H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, f.range = e.toAddMonoidHom.graph
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.some_apply : ∀ {α : Type u_1}, ⇑Function.Embedding.some = some
-- Lean.Parser.Command
Lean.Parser.Command.declValSimple.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.mk_edge : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (edge : X.obj (Opposite.op { len := 1 }))
  (src_eq :
    autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) edge = x₀) _auto_38✝)
  (tgt_eq :
    autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) edge = x₁) _auto_40✝),
  (SSet.Edge.mk edge src_eq tgt_eq).edge = edge
-- Std.Time.Format.Modifier
/-- Short form of the localized offset (e.g., "GMT+8")
 -/
Std.Time.OffsetO.short : Std.Time.OffsetO
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonPMFReal_nonneg : ∀ {r : NNReal} {n : ℕ}, 0 ≤ ProbabilityTheory.poissonPMFReal r n
-- Mathlib.Data.Multiset.Defs
Multiset.decidableDforallMultiset : {α : Type u_1} →
  {m : Multiset α} →
    {p : (a : α) → a ∈ m → Prop} →
      [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] → Decidable (∀ (a : α) (h : a ∈ m), p a h)
-- Mathlib.Topology.Order.NhdsSet
Ico_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c ≤ d → Set.Ico a d ∈ nhdsSet (Set.Ico b c)
-- Mathlib.Data.Nat.Log
Nat.log_zero_left : ∀ (n : ℕ), Nat.log 0 n = 0
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_conjTranspose_mul_self : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : PartialOrder R] [inst_4 : StarRing R] [StarOrderedRing R] (A : Matrix m n R),
  (A.conjTranspose * A).rank = A.rank
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.cocone_naturality_components : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (j j' : J)
  (f : j ⟶ j') (x : ↑(F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CommRingCat.Colimits.coconeMorphism F j'))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (CommRingCat.Colimits.coconeMorphism F j)) x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyπ_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j], (K.isoHomologyπ i j hi h).hom = K.homologyπ j
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- Given a Borel-measurable set in a Polish space, there exists a finer Polish topology making
it clopen. This is in fact an equivalence, see `isClopenable_iff_measurableSet`.  -/
MeasurableSet.isClopenable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {s : Set α},
  MeasurableSet s → PolishSpace.IsClopenable s
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode.eq_1 : Nat.Partrec.Code.ofNatCode 0 = Nat.Partrec.Code.zero
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyπ_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j] {Z : C} (h_1 : K.cycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyπ j)
      (CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h).inv h_1) =
    h_1
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.binomial_sum_eq : ∀ {m n : ℕ}, n < m → ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1
-- Mathlib.FieldTheory.Perfect
/-- The `(frobeniusEquiv R p).symm` version of `MonoidHom.map_frobenius`.
`(frobeniusEquiv R p).symm` commute with any monoid homomorphisms.
 -/
MonoidHom.map_frobeniusEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) [inst_2 : ExpChar R p]
  [inst_3 : PerfectRing R p] [inst_4 : ExpChar S p] [inst_5 : PerfectRing S p] (f : R →* S) (x : R),
  f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)
-- Mathlib.Algebra.Prime.Defs
Irreducible.dvd_comm : ∀ {M : Type u_1} [inst : Monoid M] {p q : M}, Irreducible p → Irreducible q → (p ∣ q ↔ q ∣ p)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, t₁.Equiv t₂ → t₁.getD k fallback = t₂.getD k fallback
-- Mathlib.Algebra.Torsor.Basic
/-- A product of `AddTorsor`s is an `AddTorsor`.  -/
Pi.instAddTorsor : {I : Type u} →
  {fg : I → Type v} →
    [inst : (i : I) → AddGroup (fg i)] →
      {fp : I → Type w} → [(i : I) → AddTorsor (fg i) (fp i)] → AddTorsor ((i : I) → fg i) ((i : I) → fp i)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  (Polynomial.UniversalFactorizationRing.fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Algebra.ofId R (Polynomial.UniversalFactorizationRing m k hn p)).comp ((MvPolynomial.mapEquivMonic R R n).symm p)
-- Mathlib.LinearAlgebra.Goursat
/-- For `L` a submodule of `M × N`, `L.goursatFst` is the kernel of the projection map `L → N`,
considered as a submodule of `M`.

This is the first submodule appearing in Goursat's lemma. See `Subgroup.goursat`.  -/
Submodule.goursatFst : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → Submodule R (M × N) → Submodule R M
-- Init.Data.List.Zip
List.tail_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ},
  (List.zipWithAll f as bs).tail = List.zipWithAll f as.tail bs.tail
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_liftWith_trans_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n o : Type u → Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : (α : Type u) → Std.Internal.Do.WP (o α) α Pred EPred]
  {α : Type u} {post : α → Pred} {epost : EPred} [inst_3 : MonadControl n o] [inst_4 : MonadControlT m n]
  (f : ({β : Type u} → o β → m (stM m o β)) → m α),
  Std.Internal.Do.wp (liftWith f) post epost =
    Std.Internal.Do.wp (MonadControl.liftWith fun x₂ => liftWith fun x₁ => f fun {β} => x₁ ∘ x₂) post epost
-- Mathlib.Algebra.Module.LinearMap.Defs
map_zsmul_unit : ∀ {F : Type u_16} {M : Type u_17} {N : Type u_18} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) (c : ℤˣ) (m : M), f (c • m) = c • f m
-- Batteries.Data.BinomialHeap.Basic
/-- Merge two forests of binomial trees. The forests are assumed to be ordered
by rank and `merge` maintains this invariant.
 -/
Batteries.BinomialHeap.Imp.Heap.merge : {α : Type u_1} →
  (α → α → Bool) →
    Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.mk : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {φ : U ⥤q V},
  (∀ (u : U), Function.Bijective (φ.star u)) → (∀ (u : U), Function.Bijective (φ.costar u)) → φ.IsCovering
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IntermediateField.isPurelyInseparable_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], IsPurelyInseparable F ↥⊥
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.finite_of_singleton : ∀ (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsDomain B] [h : IsCyclotomicExtension {n} A B], Module.Finite A B
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_top : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F},
  f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.evenToNeg.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q Q' : QuadraticForm R M) (h : Q' = -Q), CliffordAlgebra.evenToNeg Q Q' h = CliffordAlgebra.evenToNeg Q Q' h
-- Mathlib.Order.Circular
btw_iff_not_sbtw : ∀ {α : Type u_1} [inst : CircularOrder α] {a b c : α}, btw a b c ↔ ¬sbtw c b a
-- Qq.SortLocalDecls
Qq.SortLocalDecls.Context.mk.sizeOf_spec : ∀ (localDecls : Lean.NameMap Lean.LocalDecl), sizeOf { localDecls := localDecls } = 1 + sizeOf localDecls
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `f = g`, then `map f` is naturally isomorphic to `map g`.  -/
CategoryTheory.Under.mapCongr : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y : T} → (f g : X ⟶ Y) → f = g → (CategoryTheory.Under.map f ≅ CategoryTheory.Under.map g)
-- Mathlib.Order.CompleteLattice.Basic
biInf_le_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : Preorder ι] {f : ι → α},
  ⨅ i, ⨅ j, ⨅ (_ : j ≤ i), f j = ⨅ i, f i
-- Init.Data.SInt.Lemmas
ISize.toInt64_le : ∀ {a b : ISize}, a.toInt64 ≤ b.toInt64 ↔ a ≤ b
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hom_comp : ∀ {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T),
  CommSemiRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (CommSemiRingCat.Hom.hom g).comp (CommSemiRingCat.Hom.hom f)
-- Mathlib.Topology.Order.IntermediateValue
/-- **Alias** of `setOfPred_isPreconnected_eq_of_ordered`.

---

In a dense conditionally complete linear order, the set of preconnected sets is exactly
the set of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`, `Iic`, `Iio`, `(-∞, +∞)`,
or `∅`. Though one can represent `∅` as `(sInf s, sInf s)`, we include it into the list of
possible cases to improve readability.  -/
setOf_isPreconnected_eq_of_ordered : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α],
  {s | IsPreconnected s} =
    Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪
        Set.range (Function.uncurry Set.Ioo) ∪
      (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
-- Mathlib.Data.Finset.Defs
Finset.ext_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'} [Finite G] [hG : IsZGroup G],
  Function.Surjective ⇑f → IsZGroup G'
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- Coercion from `OpenSubgroup G` to `Opens G`.  -/
OpenSubgroup.toOpens : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → OpenSubgroup G → TopologicalSpace.Opens G
-- Mathlib.NumberTheory.Height.NumberField
Rat.mulHeight_self_one_eq_mulHeight_num_den : ∀ (q : ℚ), Height.mulHeight ![q, 1] = Height.mulHeight ![↑q.num, ↑q.den]
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStarModule : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : SMulCommClass R R F], StarModule R (WithConv (E →ₗ[R] F))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing : Lean.Expr →
  Lean.Expr →
    Lean.Grind.CommRing.Expr →
      Lean.Grind.CommRing.Expr →
        Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Mathlib.Order.Hom.Lattice
/-- The type of lattice homomorphisms from `α` to `β`.  -/
LatticeHom : (α : Type u_6) → (β : Type u_7) → [Lattice α] → [Lattice β] → Type (max u_6 u_7)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.hasLaw : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  {κ : MeasureTheory.Measure γ},
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.HasLaw f κ μ → ProbabilityTheory.HasLaw g κ ν
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- `U n` is the `n`-th Chebyshev polynomial of the second kind.  -/
Polynomial.Chebyshev.U : (R : Type u_1) → [inst : CommRing R] → ℤ → Polynomial R
-- Mathlib.Order.Interval.Set.OrdConnected
Set.dual_ordConnected : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [s.OrdConnected], (⇑OrderDual.ofDual ⁻¹' s).OrdConnected
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- If a function is `C^k` on two open sets, it is also `C^n` on their union.  -/
ContDiffOn.union_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n f t → IsOpen s → IsOpen t → ContDiffOn 𝕜 n f (s ∪ t)
-- Mathlib.Data.Set.Prod
Set.prod_mono_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → s ×ˢ t₁ ⊆ s ×ˢ t₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_inj : ∀ {x y : ℝ}, Real.sinh x = Real.sinh y ↔ x = y
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toMulDivCancelClass : ∀ {G₀ : Type u} [inst : GroupWithZero G₀], MulDivCancelClass G₀
-- Init.Data.String.Subslice
_private.Init.Data.String.Subslice.0.String.Slice.subslice!.eq_1 : ∀ (s : String.Slice) (newStart newEnd : s.Pos),
  s.subslice! newStart newEnd =
    if h : newStart ≤ newEnd then s.subslice newStart newEnd h
    else
      panicWithPosWithDecl "Init.Data.String.Subslice" "String.Slice.subslice!" 128 4
        "Trying to construct a degenerate subslice"
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associator_obj : ∀ (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] (X : (C × D) × E),
  (CategoryTheory.prod.associator C D E).obj X = (X.1.1, X.1.2, X.2)
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineMonoid.toIsCancelMul : ∀ {M : Type u_1} {inst : CommMonoid M} [self : IsAffineMonoid M], IsCancelMul M