mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind : Type
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens) (x : ↥U) (hx : x ∈ V) {Z : CommRingCat}
  (h : (↑U).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ↑x ⋯)
      (CategoryTheory.CategoryStruct.comp (U.stalkIso x).inv h) =
    CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) h
-- Mathlib.FieldTheory.Perfect
surjective_frobenius : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [PerfectRing R p],
  Function.Surjective ⇑(frobenius R p)
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp : ∀ {a b c : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c),
  RingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x x_1 =
    CategoryTheory.Cat.Hom.isoMk
      (ModuleCat.restrictScalarsComp (RingCat.Hom.hom x_1.as.unop) (RingCat.Hom.hom x.as.unop))
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The differential on the alternating coface map complex is the alternate
sum of the coface maps  -/
AlgebraicTopology.AlternatingCofaceMapComplex.objD : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      (X : CategoryTheory.CosimplicialObject C) → (n : ℕ) → X.obj { len := n } ⟶ X.obj { len := n + 1 }
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.inter_eq_univ : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α],
  s ∩ t = Finset.univ ↔ s = Finset.univ ∧ t = Finset.univ
-- Mathlib.Topology.ClusterPt
mem_closure_iff_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ closure s ↔ ∀ t ∈ nhds x, (t ∩ s).Nonempty
-- Mathlib.Data.Finset.Sups
Finset.sups_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.inertia_le_stabilizer : ∀ {M : Type u_1} [inst : Group M] {R : Type u_4} [inst_1 : Ring R] (P : Ideal R) [inst_2 : MulSemiringAction M R],
  Ideal.inertia M P ≤ MulAction.stabilizer M P
-- Mathlib.Order.Antichain
isAntichain_and_greatest_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s ∧ IsGreatest s a ↔ s = {a}
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_unitInv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)),
  CategoryTheory.CategoryStruct.comp f (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unitInv.app Y) ↔
    f = f'
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α],
  UniqueFactorizationMonoid.normalizedFactors 1 = 0
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.inv.eq_1 : ∀ (α : Type u) [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α],
  OrderIso.inv α = { toEquiv := Equiv.trans (Equiv.inv α) OrderDual.toDual, map_rel_iff' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The map of a pushout cocone is a colimit iff the cofork consisting of the mapped morphisms is a
colimit. This essentially lets us commute `PushoutCocone.mk` with `Functor.mapCocone`.  -/
CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y Z : C} →
            {h : X ⟶ Z} →
              {k : Y ⟶ Z} →
                {f : W ⟶ X} →
                  {g : W ⟶ Y} →
                    (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                      CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.PushoutCocone.mk h k comm)) ≃
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Tactic.NormNum.BigOperators
/-- `norm_num` plugin for evaluating sums of finsets.

If your finset is not supported, you can add it to the match in `Finset.proveEmptyOrCons`.
 -/
Mathlib.Meta.NormNum.evalFinsetSum : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- A wide subquiver of `G` can equivalently be viewed as a total set of arrows.  -/
Quiver.wideSubquiverEquivSetTotal : {V : Type u_1} → [inst : Quiver V] → WideSubquiver V ≃ Set (Quiver.Total V)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State.mk.inj : ∀ {varMap : Lean.Meta.KExprMap ℕ} {vars : Array Lean.Expr} {varMap_1 : Lean.Meta.KExprMap ℕ} {vars_1 : Array Lean.Expr},
  { varMap := varMap, vars := vars } = { varMap := varMap_1, vars := vars_1 } → varMap = varMap_1 ∧ vars = vars_1
-- Init.Data.Int.Gcd
Int.dvd_coe_gcd : ∀ {a b c : ℤ}, c ∣ a → c ∣ b → c ∣ ↑(a.gcd b)
-- Mathlib.Analysis.SpecificLimits.Basic
NNReal.tsum_geometric : ∀ {r : NNReal}, r < 1 → ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuousOn_iInf_dom : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β' : Type u_9} [uα : UniformSpace α] {u : κ → UniformSpace β'}
  {F : ι → β' → α} {S : Set β'} {k : κ}, UniformEquicontinuousOn F S → UniformEquicontinuousOn F S
-- Mathlib.Algebra.DirectSum.Internal
/-- The difference with `DirectSum.multisetProd_apply_eq_zero` is that the indices at which
the terms of the multiset are zero is allowed to vary.  -/
multisetProd_apply_eq_zero' : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [CanonicallyOrderedAdd ι] [inst_5 : CommSemiring R] [inst_6 : SetLike σ R]
  [inst_7 : AddSubmonoidClass σ R] {A : ι → σ} [inst_8 : SetLike.GradedMonoid A]
  {s : Multiset ((DirectSum ι fun i => ↥(A i)) × ι)},
  (∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) →
    ∀ ⦃n : ι⦄, n < (Multiset.map Prod.snd s).sum → (Multiset.map Prod.fst s).prod n = 0
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X),
  Dynamics.coverEntropyInfEntourage T F U = ExpGrowth.expGrowthInf fun n => ↑(Dynamics.coverMincard T F U n)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.fderivWithin : ∀ {𝕜 : 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] {x : E}
  {s : Set E} (iso : E ≃L[𝕜] F), UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (⇑iso) s x = ↑iso
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.describeMVar.wrap : String → String
-- Mathlib.LinearAlgebra.Pi
LinearMap.proj_pi : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)]
  (f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι), LinearMap.proj i ∘ₗ LinearMap.pi f = f i
-- Mathlib.Data.List.Sym
List.length_sym : ∀ {α : Type u_1} {n : ℕ} {xs : List α}, (List.sym n xs).length = xs.length.multichoose n
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom S.homologyι =
    CategoryTheory.CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverSkip : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- **Alias** of the reverse direction of `Matrix.isHermitian_iff_isSelfAdjoint`. -/
IsSelfAdjoint.isHermitian : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, IsSelfAdjoint A → A.IsHermitian
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.left.sizeOf_spec : sizeOf Nat.Partrec.Code.left = 1
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.mk : {R : Type u} → [inst : CommRing R] → (toModuleCat : ModuleCat R) → Coalgebra R ↑toModuleCat → CoalgCat R
-- Mathlib.Algebra.CharP.Two
/-- **Alias** of `CharTwo.sq_inj`. -/
CharTwo.CommRing.sq_inj : ∀ {R : Type u_1} [inst : CommRing R] [CharP R 2] [NoZeroDivisors R] {x y : R}, x ^ 2 = y ^ 2 ↔ x = y
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.sup : ∀ {α : Type u} {β : Type v} [inst : Max β] {l : Filter α} {f f' g g' : α → β},
  f =ᶠ[l] f' → g =ᶠ[l] g' → f ⊔ g =ᶠ[l] f' ⊔ g'
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.mem_splitCenterBox : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {s : Set ι} {y : ι → ℝ},
  y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  f ∉ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q
-- Mathlib.RingTheory.Ideal.Operations
Ideal.disjoint_powers_iff_notMem_of_isPrime : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} [I.IsPrime] (y : R), Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- The number of complex roots equals the number of real roots plus
the number of roots not fixed by complex conjugation (i.e. with some imaginary component).  -/
Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv : ∀ (p : Polynomial ℚ),
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      ((Polynomial.Gal.galActionHom p ℂ)
            ((Polynomial.Gal.restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))).support.card
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define `NormalizedGCDMonoid` on a structure just from the `gcd` and its properties.  -/
normalizedGCDMonoidOfGCD : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [inst_2 : NormalizationMonoid α] →
        [DecidableEq α] →
          (gcd : α → α → α) →
            (∀ (a b : α), gcd a b ∣ a) →
              (∀ (a b : α), gcd a b ∣ b) →
                (∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b) →
                  (∀ (a b : α), normalize (gcd a b) = gcd a b) → NormalizedGCDMonoid α
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_erase_right : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b : α),
  (Finset.Icc a b).erase b = Finset.Ico a b
-- Lean.ProjFns
Lean.auxParentProjInfoExt : Lean.MapDeclarationExtension Lean.AuxParentProjectionInfo
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_pow_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (k : ℕ), Lean.Grind.CommRing.Poly.denote ctx (p.pow_nc k) = Lean.Grind.CommRing.Poly.denote ctx p ^ k
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜), HasDerivWithinAt 0 0 s x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.ae_eq_bot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.ae μ = ⊥ ↔ μ = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ULift.instBorelSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α], BorelSpace (ULift.{u_6, u_1} α)
-- Std.Data.HashMap.Basic
Std.HashMap.instUnion : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Union (Std.HashMap α β)
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsFiltration.mono : ∀ {ι : Type u_1} {σ : Type u_3} {inst : Preorder ι} {inst_1 : Preorder σ} {F : ι → σ} {F_lt : outParam (ι → σ)}
  [self : IsFiltration F F_lt], Monotone F
-- Mathlib.Order.LiminfLimsup
Filter.mem_limsup_iff_frequently_mem : ∀ {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α}, a ∈ Filter.limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLT.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β],
  (∀ ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂) → SMulPosReflectLT α β
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_id : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R}, Polynomial.eval₂ (RingHom.id R) x p = Polynomial.eval x p
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialInsert.eq_1 : ∀ (a : ℕ), SimplexCategoryGenRel.simplicialInsert a [] = [a]
-- Mathlib.Algebra.Group.Torsion
IsMulTorsionFree.zpow_eq_one_iff_left : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {n : ℤ} {a : G}, n ≠ 0 → (a ^ n = 1 ↔ a = 1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_le_size_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.size ≤ (t.erase k).size + 1
-- Mathlib.Order.RelSeries
/-- If `α` is a preorder, a LTSeries is a relation series of the less than relation.
 -/
LTSeries : (α : Type u_1) → [Preorder α] → Type u_1
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_box_iff : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] {ν : ι → ℤ} {x : ι → ℝ},
  x ∈ BoxIntegral.unitPartition.box n ν ↔ ∀ (i : ι), ↑(ν i) / ↑n < x i ∧ x i ≤ (↑(ν i) + 1) / ↑n
-- Mathlib.Topology.Category.CompHaus.Basic
/-- (Implementation) The object part of the compactification functor from topological spaces to
compact Hausdorff spaces.
 -/
stoneCechObj : TopCat → CompHaus
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
Projectivization.card_of_finrank_two : ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k],
  Module.finrank k V = 2 → Nat.card (Projectivization k V) = Nat.card k + 1
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkBVarS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → ℕ → m Lean.Expr
-- Lean.Attributes
Lean.Attribute.Builtin.getIdent : Lean.Syntax → Lean.AttrM Lean.Syntax
-- Init.Data.Order.Lemmas
Std.instLawfulOrderMaxOfIsLinearPreorderOfLawfulOrderLeftLeaningMax : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [Std.IsLinearPreorder α] [Std.LawfulOrderLeftLeaningMax α],
  Std.LawfulOrderMax α
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.map_prime_of_equiv : ∀ {T : Type u_4} [inst : CommRing T] [IsDedekindDomain T] {R : Type u_5} [inst_2 : CommRing R] [IsDedekindDomain R]
  (f : T ≃+* R) {I : Ideal T}, Prime I → I ≠ ⊥ → Prime (Ideal.map f I)
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientMapOfLE.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h : s ≤ t),
  AddSubgroup.quotientMapOfLE h = Quotient.map' id ⋯
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.HasWeakKernels.hasWeakLimit : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.Limits.HasWeakKernels C] {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasWeakKernel f
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.apply_diag_ne : ∀ {α : Type u_1} {V : Type u_2} {A : Matrix V V α} [inst : MulZeroOneClass α] [Nontrivial α],
  A.IsAdjMatrix → ∀ (i : V), ¬A i i = 1
-- Mathlib.Control.EquivFunctor.Instances
EquivFunctorFintype : EquivFunctor Fintype
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Triangle.orthocenter_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (e : Fin 3 ≃ Fin 3),
  Affine.Triangle.orthocenter (Affine.Simplex.reindex t e) = t.orthocenter
-- Mathlib.Data.EReal.Inv
EReal.div_nonneg_of_nonpos_of_nonpos : ∀ {a b : EReal}, a ≤ 0 → b ≤ 0 → 0 ≤ a / b
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
StrictAnti.const_mul_of_neg : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R],
  StrictAnti f → a < 0 → StrictMono fun x => a * f x
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.auxMat.eq_1 : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m),
  Algebra.Norm.Transitivity.auxMat M k =
    Matrix.of fun i j => if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcomp₁_map_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H)
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L')}
  (φ : X ⟶ Y) (X_1 : D),
  ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).map φ).right.app X_1 = φ.right.app (G.obj X_1)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_injective : Function.Injective Real.arsinh
-- Mathlib.Data.List.DropRight
_private.Mathlib.Data.List.DropRight.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropSuffix?_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice},
  s.copy = t.copy → Option.map String.Slice.copy (s.dropSuffix? pat) = Option.map String.Slice.copy (t.dropSuffix? pat)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimTargetView.term : Lean.Elab.Tactic.ElimTargetView → Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X Y).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd Y X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.IsFullyInvariant.isotypicComponent : ∀ (R : Type u_2) (M : Type u) (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S], (isotypicComponent R M S).IsFullyInvariant
-- Mathlib.Topology.MetricSpace.Basic
/-- Build new emetric space from an old one where the edistance is provably (but typically
non-definitionally) equal to some given edistance. We also provide convenience versions for
PseudoEMetric, PseudoMetric and Metric spaces.  -/
EMetricSpace.replaceEDist : {X : Type u_2} → (m : EMetricSpace X) → (d : X → X → ENNReal) → d = edist → EMetricSpace X
-- Mathlib.CategoryTheory.Action.Limits
Action.add_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} (f g : X ⟶ Y), (f + g).hom = f.hom + g.hom
-- Std.Sync.Notify
/-- Consumers that are blocked waiting for a notification.
- -/
Std.Notify.State.consumers : Std.Notify.State → Std.Queue (Std.Notify.Consumer Unit)
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_const_of_nonempty : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [Nonempty 𝓨],
  Measurable (Function.uncurry ℓ) →
    ∀ (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure μ] (π : MeasureTheory.Measure Θ)
      [MeasureTheory.SFinite π],
      ProbabilityTheory.bayesRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π
-- Aesop.BuiltinRules.ApplyHyps
Aesop.BuiltinRules.applyHyps : Aesop.RuleTac
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.ofHom_apply : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) (x : X),
  (CategoryTheory.ConcreteCategory.hom (TopCat.ofHom f)) x = f x