mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.FreeCoequalizer.bottomMap_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  (CategoryTheory.Monad.FreeCoequalizer.bottomMap X).f = T.μ.app X.A
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The map taking the pi product of a family of fundamental groupoids to the fundamental
groupoid of the pi product. This is actually an isomorphism (see `piIso`)
 -/
FundamentalGroupoidFunctor.piToPiTop : {I : Type u} →
  (X : I → TopCat) →
    CategoryTheory.Functor ((i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i)))
      ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))
-- Mathlib.Analysis.Calculus.FDeriv.Star
DifferentiableWithinAt.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} {s : Set E} [TrivialStar 𝕜],
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun y => star (f y)) s x
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_lt_iff_le : ∀ {s : String.Slice} {p q : s.Pos} {h : p ≠ s.startPos}, p.prev h < q ↔ p ≤ q
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuousAt.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  UpperSemicontinuousAt f a → UpperSemicontinuousAt g a → UpperSemicontinuousAt (fun x => max (f x) (g x)) a
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instAddCommSemigroup : {d : ℤ} → AddCommSemigroup (ℤ√d)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.parserOfStack.formatter : ℕ → optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instOfIsClosedImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.IsIntegralHom f
-- Mathlib.Geometry.Euclidean.SignedDist
/-- The signed distance between two points `p` and `q`, in the direction of a reference vector `v`.
It is the size of `q - p` in the direction of `v`.
In the degenerate case `v = 0`, it returns `0`.

TODO: once we have a topology on `P →ᴬ[ℝ] ℝ`, the type should be `P →ᴬ[ℝ] P →ᴬ[ℝ] ℝ`.
 -/
signedDist : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → V → P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Coloring.sum_sumLeft_sumRight : ∀ {V : Type u_3} {W : Type u_5} {γ : Type u_7} {G : SimpleGraph V} {H : SimpleGraph W} (c : (G ⊕g H).Coloring γ),
  c.sumLeft.sum c.sumRight = c
-- Aesop.Tree.Data
Aesop.TreeSpec.elimMVarCluster : (self : Aesop.TreeSpec) → self.MVarCluster → Aesop.MVarClusterData self.Goal self.Rapp
-- Mathlib.Algebra.Group.Center
Set.div_mem_centralizer : ∀ {M : Type u_1} {S : Set M} [inst : Group M] {a b : M}, a ∈ S.centralizer → b ∈ S.centralizer → a / b ∈ S.centralizer
-- Mathlib.Algebra.GroupWithZero.NeZero
/-- Pullback a `Nontrivial` instance along a function sending `0` to `0` and `1` to `1`.  -/
domain_nontrivial : ∀ {M₀ : Type u_1} {M₀' : Type u_2} [inst : MulZeroOneClass M₀] [Nontrivial M₀] [inst_2 : Zero M₀'] [inst_3 : One M₀']
  (f : M₀' → M₀), f 0 = 0 → f 1 = 1 → Nontrivial M₀'
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.toRingEquiv_eq_coe : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B), e.toRingEquiv = e.toRingEquiv
-- Mathlib.Data.List.Sort
List.sortedLT_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, (List.map (⇑OrderDual.toDual) l).SortedLT ↔ l.SortedGT
-- Mathlib.Algebra.Quaternion
Quaternion.imI_im : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a.im.imI = a.imI
-- Lean.Environment
/-- If `when` is true, sets `Environment.isExporting` to false while executing `x`.  -/
Lean.withoutExporting : {m : Type → Type} →
  {α : Type} → [Monad m] → [Lean.MonadEnv m] → [MonadFinally m] → [Lean.MonadOptions m] → m α → optParam Bool true → m α
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits of `K.leftOp : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : Cᵒᵖ ⥤ D`
reflects limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsLimit_of_rightOp : ∀ {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) [CategoryTheory.Limits.ReflectsColimit K.leftOp F.rightOp],
  CategoryTheory.Limits.ReflectsLimit K F
-- Std.Time.Date.Unit.Week
Std.Time.Week.instInhabitedOrdinal : Inhabited Std.Time.Week.Ordinal
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.inverse_zero : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ContinuousLinearMap.inverse 0 = 0
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.addOrderOf_dvd_natCard : ∀ {G : Type u_6} [inst : AddGroup G] (s : AddSubgroup G) {x : G}, x ∈ s → addOrderOf x ∣ Nat.card ↥s
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i j : J) {k : J}
  (fi : k ⟶ i) (fj : k ⟶ j),
  CategoryTheory.CategoryStruct.comp ((F.obj i).homOfLE ⋯) (AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map fi)).inv (F.map fj)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.notMem_of_notMem_closure : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {P : K}, P ∉ Subfield.closure s → P ∉ s
-- Init.Data.Vector.OfFn
Vector.ofFn.eq_1 : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α), Vector.ofFn f = Vector.mk (Array.ofFn f) ⋯
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instHasCardinalFilteredColimits : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular],
  CategoryTheory.HasCardinalFilteredColimits (CategoryTheory.CardinalDirectedPoset κ) κ
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : g ⟶ f)
  [inst_1 : CategoryTheory.IsIso sq],
  CategoryTheory.Arrow.Hom.right (CategoryTheory.inv sq) = CategoryTheory.inv (CategoryTheory.Arrow.Hom.right sq)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.p : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Int.Internal.Linear.Poly
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The infimum edistance of a point to a set is positive if and only if the point is not in the
closure of the set.  -/
Metric.infEDist_pos_iff_notMem_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α}, 0 < Metric.infEDist x E ↔ x ∉ closure E
-- Init.Data.Bool
Bool.ne_false_iff : ∀ {b : Bool}, b ≠ false ↔ b = true
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A homology map data for a morphism `φ : S₁ ⟶ S₂` where both `S₁` and `S₂` are
equipped with homology data consists of left and right homology map data.  -/
CategoryTheory.ShortComplex.HomologyMapData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → S₁.HomologyData → S₂.HomologyData → Type v
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Continuous f → Function.Injective f → IsClosedMap f → Topology.IsClosedEmbedding f
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `K / E / F` is a field extension tower, then `E` adjoin `algebraicClosure F K` is contained
in `algebraicClosure E K`.  -/
algebraicClosure.adjoin_le : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_3)
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K],
  IntermediateField.adjoin E ↑(algebraicClosure F K) ≤ algebraicClosure E K
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.asNamed : Lean.Syntax → Option (Lean.Ident × Lean.TSyntax `arg_val)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.insert_toList_zoom : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {t' : RBTree.RBNode α} {p : RBTree.RBNode.Path α}
  {v : α} {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.zoom (cmp v) t = (t', p) →
      (RBTree.RBNode.insert cmp t v).toList = p.withList (RBTree.RBNode.setRoot v t').toList
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_fst_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).fst.obj X_1 =
    S.fst.obj (U.obj X_1)
-- Mathlib.Order.Heyting.Basic
Prod.instCoheytingAlgebra : {α : Type u_2} → {β : Type u_3} → [CoheytingAlgebra α] → [CoheytingAlgebra β] → CoheytingAlgebra (α × β)
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  (h : ProbabilityTheory.IsAEKolmogorovProcess X P p q M) (t : T),
  X t =ᵐ[P] ProbabilityTheory.IsAEKolmogorovProcess.mk X h t
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.eq_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m)
  [inst_5 : IsAdicComplete I N] {F : M →ₗ[R] N},
  (∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n) → F = IsAdicComplete.StrictMono.lift I ha f ⋯
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The inductively constructed sequence `qₖ` in the proof of Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.seq : {A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} → {I : Ideal A} → g.IsWeierstrassDivisorAt I → PowerSeries A → ℕ → PowerSeries A
-- Mathlib.FieldTheory.IsSepClosed
/-- A separably closed perfect field is also algebraically closed.  -/
IsSepClosed.isAlgClosed_of_perfectField : ∀ (k : Type u) [inst : Field k] [IsSepClosed k] [PerfectField k], IsAlgClosed k
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (L : FiniteGaloisIntermediateField k K), IsOpen (⇑(InfiniteGalois.mulEquivToLimit k K) '' ↑L.fixingSubgroup)
-- Mathlib.Analysis.Meromorphic.Order
/-- If a function is both meromorphic and continuous at a point, then it is analytic there.  -/
MeromorphicAt.analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicAt f x → ContinuousAt f x → AnalyticAt 𝕜 f x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'_zero : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS' b c d k 0 = 0
-- Mathlib.Tactic.Linter.Header
/-- `inLibraryRootMutex` caches whether the current file is imported in the library root file
(e.g. `Mathlib.lean`), as computed by `isInLibraryRoot`. It is
* `none` at initialization time;
* `some true` if the `header` linter has already discovered that the current file
  is imported in the library root file;
* `some false` if the `header` linter has already discovered that the current file
  is *not* imported in the library root file.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.inLibraryRootMutex : Std.Mutex (Option Bool)
-- Mathlib.RingTheory.Localization.FractionRing
/-- If `A` is a commutative ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to
`f : K →+* L`, `s` is a set such that the image of `g` is the subring generated by `s`,
then the image of `f` is the subfield generated by `s`.  -/
IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  {L : Type u_8} [inst_4 : Field L] {g : A →+* L} {f : K →+* L},
  f.comp (algebraMap A K) = g → ∀ {s : Set L}, g.range = Subring.closure s → f.fieldRange = Subfield.closure s
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.autEquivPow.congr_simp : ∀ {n : ℕ} [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] (L : Type u_2) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)),
  IsCyclotomicExtension.autEquivPow L h = IsCyclotomicExtension.autEquivPow L h
-- Mathlib.Data.Multiset.Sym
Multiset.Nodup.sym2 : ∀ {α : Type u_1} {m : Multiset α}, m.Nodup → m.sym2.Nodup
-- Mathlib.GroupTheory.Index
AddSubgroup.dvd_index_map : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) {f : G →+ G'},
  f.ker ≤ H → H.index ∣ (AddSubgroup.map f H).index
-- Lean.Structure
/-- Returns the parent structures that are embedded in the structure.
This is the array of all results from `Lean.isSubobjectField?` in order.

Note: this is *not* a subset of the parents from `getStructureParentInfo`.
If a direct parent cannot itself be represented as a subobject,
sometimes one of its parents (or one of their parents, etc.) can.
 -/
Lean.getStructureSubobjects : Lean.Environment → Lean.Name → Array Lean.Name
-- Mathlib.Algebra.Group.Hom.Instances
/-- Flipping arguments of monoid morphisms (`MonoidHom.flip`) as a monoid morphism.  -/
MonoidHom.flipHom : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} → {x : MulOneClass M} → {x_1 : MulOneClass N} → {x_2 : CommMonoid P} → (M →* N →* P) →* N →* M →* P
-- Lean.Meta.Tactic.Util
/-- Rethrows the error as a nested error with the given tactic name prepended.
If the error was tagged, prepends `nested` to the tag and preserves it.
 -/
Lean.Meta.throwNestedTacticEx : {α : Type} → Lean.Name → Lean.Exception → Lean.MetaM α
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.secondMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks],
  CategoryTheory.Equalizer.Presieve.secondMap P R =
    CategoryTheory.Limits.Pi.lift fun fg =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) fg.2)
        (P.map (CategoryTheory.Limits.pullback.snd ↑fg.1.snd ↑fg.2.snd).op)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `SummableUniformly f` means that there is some infinite sum to which
`f` converges uniformly. Use `fun x ↦ ∑' i, f i x` to get the product function.  -/
SummableUniformly : {α : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → [UniformSpace α] → Prop
-- Lean.Setup
Lean.instReprIRPhases.repr : Lean.IRPhases → ℕ → Std.Format
-- Mathlib.RingTheory.HahnSeries.PowerSeries
Polynomial.algebraMap_hahnSeries_apply : ∀ (Γ : Type u_1) {R : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ] (f : Polynomial R),
  (algebraMap (Polynomial R) (HahnSeries Γ R)) f = (HahnSeries.ofPowerSeries Γ R) ↑f
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.mem_inv_smul_set_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (A : Set β) (x : β), x ∈ a⁻¹ • A ↔ a • x ∈ A
-- Mathlib.Algebra.Group.Commute.Defs
/-- Two elements `a` and `b` commute if `a * b = b * a`.
 -/
commute_iff_eq : ∀ {S : Type u_3} [inst : Mul S] (a b : S), Commute a b ↔ a * b = b * a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.cancelVar' : ℤ → Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp₂_map_right : ∀ {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'] {F₀ : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {F₁ : CategoryTheory.Functor D H} (L' : CategoryTheory.Functor D D') (α : F₀ ⟶ L.comp F₁) {X Y : L'.LeftExtension F₁}
  (f : X ⟶ Y), ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).map f).right = f.right
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_sum_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq σ] (s : Finset ι)
  (f : ι → MvPolynomial σ R), (∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk.injEq : ∀ {M : Type u_3} [inst : AddZeroClass M] (toAddSubsemigroup : AddSubsemigroup M)
  (zero_mem' : 0 ∈ toAddSubsemigroup.carrier) (toAddSubsemigroup_1 : AddSubsemigroup M)
  (zero_mem'_1 : 0 ∈ toAddSubsemigroup_1.carrier),
  ({ toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' } =
      { toAddSubsemigroup := toAddSubsemigroup_1, zero_mem' := zero_mem'_1 }) =
    (toAddSubsemigroup = toAddSubsemigroup_1)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.norm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun a => ‖f a‖) μ
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_lt_log : ∀ {x y : ENNReal}, x < y → x.log < y.log
-- Mathlib.Algebra.Category.CommBialgCat
/-- Typecheck a `BialgHom` as a morphism in `CommBialgCat R`.  -/
CommBialgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      {x : CommRing X} →
        {x_1 : CommRing Y} →
          {x_2 : Bialgebra R X} → {x_3 : Bialgebra R Y} → (X →ₐc[R] Y) → (CommBialgCat.of R X ⟶ CommBialgCat.of R Y)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The expression for the right whiskering `η ▷ f`.  -/
Mathlib.Tactic.BicategoryLike.MonadWhiskerRight.whiskerRightM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.WhiskerRight →
      Mathlib.Tactic.BicategoryLike.Atom₁ → m Mathlib.Tactic.BicategoryLike.WhiskerRight
-- Lean.Exception
Lean.instMonadRecDepthReaderT : {m : Type → Type} → {ρ : Type} → [Lean.MonadRecDepth m] → Lean.MonadRecDepth (ReaderT ρ m)
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandParen : Lean.Macro
-- Mathlib.Order.Interval.Finset.Defs
WithTop.instLocallyFiniteOrder.eq_1 : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α],
  WithTop.instLocallyFiniteOrder α =
    {
      finsetIcc := fun a b =>
        match a, b with
        | none, none => {⊤}
        | none, some b => ∅
        | some a, none => WithTop.insertTop (Finset.Ici a)
        | some a, some b => Finset.map Function.Embedding.coeWithTop (Finset.Icc a b),
      finsetIco := fun a b =>
        match a, b with
        | none, x => ∅
        | some a, none => Finset.map Function.Embedding.coeWithTop (Finset.Ici a)
        | some a, some b => Finset.map Function.Embedding.coeWithTop (Finset.Ico a b),
      finsetIoc := fun a b =>
        match a, b with
        | none, x => ∅
        | some a, none => WithTop.insertTop (Finset.Ioi a)
        | some a, some b => Finset.map Function.Embedding.coeWithTop (Finset.Ioc a b),
      finsetIoo := fun a b =>
        match a, b with
        | none, x => ∅
        | some a, none => Finset.map Function.Embedding.coeWithTop (Finset.Ioi a)
        | some a, some b => Finset.map Function.Embedding.coeWithTop (Finset.Ioo a b),
      finset_mem_Icc := ⋯, finset_mem_Ico := ⋯, finset_mem_Ioc := ⋯, finset_mem_Ioo := ⋯ }
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.countableObj : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} [self : CategoryTheory.CountableCategory J], Countable J
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.eraseList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.eraseList l [] = l
-- Mathlib.NumberTheory.Real.Irrational
Irrational.neg : ∀ {x : ℝ}, Irrational x → Irrational (-x)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_mul_distrib : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f g : ι → M},
  ∏ x ∈ s, f x * g x = (∏ x ∈ s, f x) * ∏ x ∈ s, g x
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.restrict.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (J : BoxIntegral.Box ι),
  π.restrict J = BoxIntegral.Prepartition.ofWithBot (Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes) ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_pi_div_two : ∀ (x : ℝ), Real.cos (x + Real.pi / 2) = -Real.sin x
-- Mathlib.Algebra.Order.Hom.Monoid
map_inv_le_map_inv_iff_map_le_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : Monoid β] {F : Type u_6} [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] [inst_4 : LE β] [MulRightMono β] [MulLeftMono β] {f g : F} {x : α}, f x⁻¹ ≤ g x⁻¹ ↔ g x ≤ f x
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x`. If all functions in the series are differentiable
with a summable bound on the derivatives, then the series is differentiable.
Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise
convergence then the series is zero everywhere so the result still holds.  -/
differentiable_tsum' : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F},
  Summable u →
    (∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) →
      (∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) → Differentiable 𝕜 fun z => ∑' (n : α), g n z