mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.ofLeftInverse_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : M), (MulEquiv.ofLeftInverse f h) a = f.srangeRestrict a
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_mul : ∀ (a b : UInt8), (a * b).toUInt64 = a.toUInt64 * b.toUInt64 % 256
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- **Alias** of the reverse direction of `isCornerFree_image`. -/
IsCornerFree.image : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H}, IsAddFreimanIso 2 s t f → A ⊆ s ×ˢ s → IsCornerFree A → IsCornerFree (Prod.map f f '' A)
-- Mathlib.Data.Sigma.Basic
PSigma.exists : ∀ {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) ×' β a → Prop}, (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
-- Init.Data.Range.Polymorphic.Map
Std.Rxc.IsAlwaysFinite.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LE α] [inst_3 : LE β] [Std.Rxc.IsAlwaysFinite β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE],
  Std.Rxc.IsAlwaysFinite α
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_ne_zero : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L}, I ≠ 0 → FractionalIdeal.dual A K I ≠ 0
-- Mathlib.Logic.Function.Defs
Function.swap_comp_diag : ∀ {α : Type u_1}, Prod.swap ∘ Function.diag = Function.diag
-- Init.Data.Array.Lemmas
Array.back?_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β},
  (Array.flatMap f xs).back? = Array.findSome? (fun a => (f a).back?) xs.reverse
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.StrongCore.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η : F ⟶ G} →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅
                      CategoryTheory.CategoryStruct.comp (η.app a) (G.map f)) →
              autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
                  CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom._autoParam →
                CategoryTheory.Oplax.OplaxTrans.StrongCore η
-- Mathlib.Order.Heyting.Basic
inf_sdiff_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ⊓ a \ b = a \ b
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.coe_of : ∀ (M : Type u) [inst : Add M], ↑(AddMagmaCat.of M) = M
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToColimit.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                  {t : CategoryTheory.Limits.IsColimit c} →
                    (toLiftableCocone : CategoryTheory.LiftableCocone K F c) →
                      CategoryTheory.Limits.IsColimit toLiftableCocone.liftedCocone →
                        CategoryTheory.LiftsToColimit K F c t
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.tateNorm_eq : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  M.tateNorm = ModuleCat.ofHom ((Finsupp.lsum R) fun x => LinearMap.pi fun x => M.ρ.norm)
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaForget.eq_1 : AddCommMonCat.coyonedaForget =
  CategoryTheory.NatIso.ofComponents
    (fun X =>
      CategoryTheory.NatIso.ofComponents
        (fun Y =>
          { hom := TypeCat.ofHom fun f => AddCommMonCat.ofHom f, inv := TypeCat.ofHom fun f => AddCommMonCat.Hom.hom f,
            hom_inv_id := ⋯, inv_hom_id := ⋯ })
        ⋯)
    @AddCommMonCat.coyonedaForget._proof_4
-- Mathlib.RingTheory.RingInvo
RingInvo.mk.inj : ∀ {R : Type u_2} {inst : Semiring R} {toRingEquiv : R ≃+* Rᵐᵒᵖ}
  {involution' : ∀ (x : R), MulOpposite.unop (toRingEquiv.toFun (MulOpposite.unop (toRingEquiv.toFun x))) = x}
  {toRingEquiv_1 : R ≃+* Rᵐᵒᵖ}
  {involution'_1 : ∀ (x : R), MulOpposite.unop (toRingEquiv_1.toFun (MulOpposite.unop (toRingEquiv_1.toFun x))) = x},
  { toRingEquiv := toRingEquiv, involution' := involution' } =
      { toRingEquiv := toRingEquiv_1, involution' := involution'_1 } →
    toRingEquiv = toRingEquiv_1
-- Init.Data.Iterators.Basic
Std.IterM.Step.toPure_yield : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it it' : Std.IterM Id β} {out : β}
  {h : it.IsPlausibleStep (Std.IterStep.yield it' out)},
  Std.IterM.Step.toPure ⟨Std.IterStep.yield it' out, h⟩ = Std.PlausibleIterStep.yield it'.toIter out h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` is continuous on `s : Set X` in the topology on
`X → R →ᵤ[{spectrum R a}] → R`, and for each `x ∈ s`, `f x` is continuous on the spectrum and
maps zero to itself, then `x ↦ cfcₙ (f x) a` is continuous on `s` also.  -/
ContinuousOn.cfcₙ_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : SMulCommClass R A A] [inst_11 : IsScalarTower R A A]
  [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] [inst_13 : TopologicalSpace X] {f : X → R → R} {a : A}
  {s : Set X},
  ContinuousOn (fun x => (UniformOnFun.ofFun {quasispectrum R a}) (f x)) s →
    (∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)) → (∀ x ∈ s, f x 0 = 0) → ContinuousOn (fun x => cfcₙ (f x) a) s
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent.sizeOf_spec : ∀ (x : Lean.Grind.AC.Var) (c₁ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent x c₁) = 1 + sizeOf x + sizeOf c₁
-- Init.Data.String.Lemmas.StringOrder
String.lt_trans : ∀ {a b c : String}, a < b → b < c → a < c
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_trans : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  [inst_3 : CategoryTheory.Category.{v_7, u_7} D₃] (W : CategoryTheory.MorphismProperty C)
  (L₁ : CategoryTheory.Functor C D₁) [inst_4 : L₁.IsLocalization W] (L₂ : CategoryTheory.Functor C D₂)
  [inst_5 : L₂.IsLocalization W] (L₃ : CategoryTheory.Functor C D₃) [inst_6 : L₃.IsLocalization W] {X Y : C}
  (f : L₁.obj X ⟶ L₁.obj Y),
  (CategoryTheory.Localization.homEquiv W L₂ L₃) ((CategoryTheory.Localization.homEquiv W L₁ L₂) f) =
    (CategoryTheory.Localization.homEquiv W L₁ L₃) f
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- the morphism of homological complexes between the `r`th pages  -/
CategoryTheory.SpectralSequence.Hom.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            {E E' : CategoryTheory.SpectralSequence C c r₀} →
              E.Hom E' →
                (r : ℤ) →
                  (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯
-- Mathlib.Logic.Function.Basic
Function.partialInv_left : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β}, Function.Injective f → ∀ (x : α), Function.partialInv f (f x) = some x
-- Lean.Parser.Extension
Lean.Parser.mkParserOfConstant : Lean.Parser.ParserCategories → Lean.Name → Lean.ImportM (Bool × Lean.Parser.Parser)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_congr_ae_trim : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m₀),
  f =ᵐ[μ] g → μ[f | m] =ᵐ[μ.trim hm] μ[g | m]
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairComp_hom_app_right : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {J : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} J]
  {K : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} K] (Fₗ : CategoryTheory.Functor C E)
  (Fᵣ : CategoryTheory.Functor D E') (Gₗ : CategoryTheory.Functor E J) (Gᵣ : CategoryTheory.Functor E' K) (d : D),
  (CategoryTheory.Join.mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (CategoryTheory.Join.right d) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (Gᵣ.obj (Fᵣ.obj d)))
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y Y' : C} → (X ⟶ Y') → (s : Y ⟶ Y') → W s → W.LeftFraction X Y
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_comp_commIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  TensorProduct.mapL f g ∘SL ↑↑(TensorProduct.commIsometry 𝕜 G E) =
    ↑↑(TensorProduct.commIsometry 𝕜 H F) ∘SL TensorProduct.mapL g f
-- Mathlib.Logic.Function.Basic
Function.Injective.factorsThrough : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Injective f → ∀ (g : α → γ), Function.FactorsThrough g f
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_symm_toContinuousAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  ⇑e.toContinuousAffineEquiv.symm = ⇑e.symm
-- Mathlib.Topology.Algebra.ProperAction.Torsor
/-- If `P` is a topological torsor over `V`, the action of `V` on `P` is proper.  -/
instProperSMul : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : Torsor V P] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P], ProperSMul V P
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.isHomogeneous_addSubMap : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) (i : Fin 3), (W.addSubMap i).IsHomogeneous 2
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.OplaxTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a) (θ.app a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom)
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv))
-- Mathlib.CategoryTheory.Types.Basic
/-- The isomorphism between a `Type` which has been `ULift`ed to the same universe,
and the original type.
 -/
CategoryTheory.uliftTrivial : (V : Type u) → ULift.{u, u} V ≅ V
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀ β) (h : Monotone (↑f).toFun),
  ⇑{ toMonoidWithZeroHom := f, monotone' := h } = ⇑f
-- Mathlib.Dynamics.BirkhoffSum.Basic
/-- If a function `φ` is invariant under a function `f` (i.e., `φ ∘ f = φ`), then the Birkhoff sum
of `φ` over `f` for `n` iterations is equal to `n • φ`.  -/
birkhoffSum_of_comp_eq : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → α} {φ : α → M},
  φ ∘ f = φ → ∀ (n : ℕ), birkhoffSum f φ n = n • φ
-- Mathlib.Analysis.Distribution.DerivNotation
/-- `Δ f` is the Laplacian of `f`. The meaning of this notation is type-dependent.  -/
Laplacian.laplacian : {E : Type v} → {F : outParam (Type w)} → [self : Laplacian E F] → E → F
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toAdditive_toMultiplicative_symm_apply : ∀ {G : Type u_2} [inst : AddZeroClass G] (a : G),
  AddEquiv.toAdditive_toMultiplicative.symm a = Additive.ofMul (Multiplicative.ofAdd a)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.dnsq : ∀ {a : ℕ} (a1 : 1 < a), Zsqrtd.Nonsquare (Pell.d✝ a1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {options? : Option Lean.Lsp.CreateFile.Options} {annotationId? : Option String}
  {uri_1 : Lean.Lsp.DocumentUri} {options?_1 : Option Lean.Lsp.CreateFile.Options} {annotationId?_1 : Option String},
  { uri := uri, options? := options?, annotationId? := annotationId? } =
      { uri := uri_1, options? := options?_1, annotationId? := annotationId?_1 } →
    uri = uri_1 ∧ options? = options?_1 ∧ annotationId? = annotationId?_1
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse_reverse : ∀ {T : Type u_1} {N : Type u_2} (r : ContextFreeRule T N), r.reverse.reverse = r
-- Mathlib.Analysis.Convex.Quasiconvex
AntitoneOn.quasiconvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → QuasiconvexOn 𝕜 s f
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- Addition preserves finiteness.  -/
Set.fintypeAdd : {α : Type u_2} → [inst : Add α] → [DecidableEq α] → (s t : Set α) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s + t)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- Given maps `(r : l → m)` and `(c : o → n)` reindexing the rows and columns of
a matrix `M : Matrix m n α`, the matrix `M.submatrix r c : Matrix l o α` is defined
by `(M.submatrix r c) i j = M (r i) (c j)` for `(i,j) : l × o`.
Note that the total number of row and columns does not have to be preserved.  -/
Matrix.submatrix : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type v} → Matrix m n α → (l → m) → (o → n) → Matrix l o α
-- Mathlib.Algebra.MvPolynomial.Coeff
_private.Mathlib.Algebra.MvPolynomial.Coeff.0.MvPolynomial.coeff_linearCombination_X_pow_of_eq : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {s : σ →₀ ℕ} (a : σ →₀ R) {n : ℕ},
  (s.sum fun x m => m) = n →
    MvPolynomial.coeff s ((Finsupp.linearCombination R MvPolynomial.X) a ^ n) =
      ↑s.multinomial * s.prod fun r m => a r ^ m
-- Mathlib.Algebra.Order.Monovary
Monovary.div_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f₁ f₂ : ι → α} {g : ι → β},
  0 ≤ f₁ → StrongLT 0 f₂ → Monovary f₁ g → Antivary f₂ g → Monovary (f₁ / f₂) g
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk₀.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m₀ : M) (hm₀ : m₀ = 0) (f f_1 : X ⟶ Y),
  f = f_1 →
    CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f =
      CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_le_min!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → (cmp t.min! (t.erase k).min!).isLE = true
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallPair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C),
  CategoryTheory.ObjectProperty.Small.{w, v, u} (CategoryTheory.ObjectProperty.pair X Y)
-- Mathlib.Algebra.Group.Hom.Basic
zpowGroupHom_apply : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (n : ℤ) (x : α), (zpowGroupHom n) x = x ^ n
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalAddGroup.IsSES.isOpenQuotientMap : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C},
  TopologicalAddGroup.IsSES φ ψ → IsOpenQuotientMap ⇑ψ
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.IsContained.girth_le : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β},
  G.IsContained G' → ¬G.IsAcyclic → G'.girth ≤ G.girth
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- This is the *continuous functional calculus* of an element `a : A` applied to bare functions.
When either `a` does not satisfy the predicate `p` (i.e., `a` is not `IsStarNormal`,
`IsSelfAdjoint`, or `0 ≤ a` when `R` is `ℂ`, `ℝ`, or `ℝ≥0`, respectively), or when `f : R → R` is
not continuous on the spectrum of `a`, then `cfc f a` returns the junk value `0`.

This is the primary declaration intended for widespread use of the continuous functional calculus,
and all the API applies to this declaration. For more information, see the module documentation
for `Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`.  -/
cfc : {R : Type u_3} →
  {A : Type u_4} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : TopologicalSpace A] →
                  [inst_6 : Ring A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : Algebra R A] → [instCFC : ContinuousFunctionalCalculus R A p] → (R → R) → A → A
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_C : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R),
  Polynomial.Bivariate.swap (Polynomial.C f) = Polynomial.map Polynomial.C f
-- Mathlib.Analysis.Normed.Group.Uniform
MonoidHomClass.isometry_iff_norm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕), Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT_eq_getEntryLT : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  {hto : t.Ordered} {he : ∃ a ∈ t, compare a k = Ordering.lt},
  Std.DTreeMap.Internal.Impl.getKeyLT k t hto he = (Std.DTreeMap.Internal.Impl.getEntryLT k t hto he).fst
-- Mathlib.RingTheory.GradedAlgebra.Radical
Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommRing A] [inst_1 : AddCommMonoid ι] [inst_2 : LinearOrder ι]
  [IsOrderedCancelAddMonoid ι] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] {𝒜 : ι → σ}
  [inst_6 : GradedRing 𝒜] {I : Ideal A},
  Ideal.IsHomogeneous 𝒜 I →
    I ≠ ⊤ →
      (∀ {x y : A}, SetLike.IsHomogeneousElem 𝒜 x → SetLike.IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I) →
        I.IsPrime
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] (F : CategoryTheory.Functor J C)
  (isoBot : F.obj ⊥ ≅ X)
  (isWellOrderContinuous :
    autoParam F.IsWellOrderContinuous CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam)
  (incl : F ⟶ (CategoryTheory.Functor.const J).obj Y)
  (isColimit : CategoryTheory.Limits.IsColimit { pt := Y, ι := incl })
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp isoBot.inv (incl.app ⊥) = f)
      CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam)
  (F_1 : CategoryTheory.Functor J C) (isoBot_1 : F_1.obj ⊥ ≅ X)
  (isWellOrderContinuous_1 :
    autoParam F_1.IsWellOrderContinuous CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam)
  (incl_1 : F_1 ⟶ (CategoryTheory.Functor.const J).obj Y)
  (isColimit_1 : CategoryTheory.Limits.IsColimit { pt := Y, ι := incl_1 })
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp isoBot_1.inv (incl_1.app ⊥) = f)
      CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam),
  ({ F := F, isoBot := isoBot, isWellOrderContinuous := isWellOrderContinuous, incl := incl, isColimit := isColimit,
        fac := fac } =
      { F := F_1, isoBot := isoBot_1, isWellOrderContinuous := isWellOrderContinuous_1, incl := incl_1,
        isColimit := isColimit_1, fac := fac_1 }) =
    (F = F_1 ∧ isoBot ≍ isoBot_1 ∧ incl ≍ incl_1 ∧ isColimit ≍ isColimit_1)
-- Aesop.Percent
Aesop.Percent.toFloat : Aesop.Percent → Float
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.StableUnderCompositionWithLocalizationAwayTarget.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_mapDomainRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (e : M ≃+ N) (x : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.mapDomainRingEquiv R e) x).coeff = Finsupp.equivMapDomain (↑e) x.coeff
-- Mathlib.Data.Set.Equitable
Finset.EquitableOn.le_add_one : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α}, (↑s).EquitableOn f → a ∈ s → f a ≤ (∑ i ∈ s, f i) / s.card + 1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_nonempty : ∀ {α : Type u_2} [inst : Zero α], Set.Nonempty 0