mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.tensor_right' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.MonoidalCoherence Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] →
          CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) X
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.and : Lean.Meta.Grind.Result✝ → Lean.Meta.Grind.Result✝ → Lean.Meta.Grind.Result✝
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- If `M` is an `R`-module and `ι` is a nonempty type, then every additive endomorphism
of `ι →₀ M` that commutes with all `R`-endomorphisms of `ι →₀ M` comes from an additive
endomorphism of `M` that commutes with all `R`-endomorphisms of `M`.
See (15) in F4 of §28 on p.131 of [Lorenz2008].  -/
Module.End.ringEquivEndFinsupp : {ι : Type u_4} →
  {R : Type u_5} →
    {M : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → ι → Module.End (Module.End R M) M ≃+* Module.End (Module.End R (ι →₀ M)) (ι →₀ M)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_exists : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {α : Type u_1} {Φ : α → Prop},
  (Lean.Order.iSup fun x => Lean.Order.CompleteLattice.ofProp (Φ x)) = Lean.Order.CompleteLattice.ofProp (∃ x, Φ x)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.mk.sizeOf_spec : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} [inst_2 : SizeOf X] [inst_3 : SizeOf Y] [inst_4 : (a : C(X, Y)) → SizeOf (P a)]
  (toHomotopy : f₀.Homotopy f₁)
  (prop' : ∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy.toFun (t, x), continuous_toFun := ⋯ }),
  sizeOf { toHomotopy := toHomotopy, prop' := prop' } = 1 + sizeOf toHomotopy
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Const.insertMany m l).getKey! k' = k
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- A `with`-clause in a big operator. Example usage: `∑ i < 100 with Even i, f i`.  -/
BigOperators.BigOpWith : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.norm_map_init_le : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G)
  (m : (i : Fin n.succ) → Ei i), ‖(f (Fin.init m)) (m (Fin.last n))‖ ≤ ‖f‖ * ∏ i, ‖m i‖
-- Lean.Parser.Extra
Lean.Parser.notSymbol.parenthesizer : String → Lean.PrettyPrinter.Parenthesizer
-- Init.Core
DoResultBC.continue.injEq : ∀ {σ : Type u} (a a_1 : σ), (DoResultBC.continue a = DoResultBC.continue a_1) = (a = a_1)
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.measurable_condLExp' : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (X : Ω → ENNReal),
  Measurable P⁻[X | mΩ]
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.equivalence_inverse_map : ∀ {X Y : CommMonCat} (f : X ⟶ Y),
  AddCommMonCat.equivalence.inverse.map f = AddCommMonCat.ofHom (MonoidHom.toAdditive (CommMonCat.Hom.hom f))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ \ m₂)[k]? = if k ∈ m₂ then none else m₁[k]?
-- Mathlib.Algebra.Order.Field.Basic
one_div_pow_le_one_div_pow_of_le : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 ≤ a → ∀ {m n : ℕ}, m ≤ n → 1 / a ^ n ≤ 1 / a ^ m
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_toBitVec : ∀ (x : Int8), Int8.ofBitVec x.toBitVec = x
-- Mathlib.Topology.Order.Basic
tendstoIxxNhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) {s t : Set α} {Ixx : α → α → Set α}
  [Filter.TendstoIxxClass Ixx (nhds a) (nhds a)] [Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t)],
  Filter.TendstoIxxClass Ixx (nhdsWithin a s) (nhdsWithin a t)
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.etaExpandedBody : Lean.Expr → ℕ → ℕ → Option Lean.Expr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.forIn_eq_forIn_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  forIn t init f = forIn t.toList init f
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] (d : D) (x x_1 : C) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.mop d
-- Mathlib.Order.CompleteLattice.Basic
Monotone.iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : Preorder α] [inst_1 : CompleteLattice β] {f : ι → α → β},
  (∀ (i : ι), Monotone (f i)) → Monotone (⨅ i, f i)
-- Mathlib.Topology.Metrizable.Uniformity
/-- Construct on a metrizable space a metric compatible with the topology.  -/
TopologicalSpace.metrizableSpaceMetric : (X : Type u_2) → [inst : TopologicalSpace X] → [TopologicalSpace.MetrizableSpace X] → MetricSpace X
-- Std.Http.Data.Chunk
/-- Creates an `ExtensionValue` from a string, panicking with an error message if the string contains
characters that cannot be encoded as an HTTP quoted-string.
 -/
Std.Http.Chunk.ExtensionValue.ofString! : String → Std.Http.Chunk.ExtensionValue
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Zero is well-ordered.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_sorted : ∀ {basis : Tactic.ComputeAsymptotics.Basis}, Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted 0
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableAt_fst : ∀ {𝕜 : 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] {p : E × F},
  DifferentiableAt 𝕜 Prod.fst p
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerived_fac : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft (RF.rightDerivedDesc α W G β)) = β
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.augmentedCechConerve_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom],
  f.augmentedCechConerve.left = f.left
-- Mathlib.Order.WithBot
WithTop.monotone_map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone (WithTop.map f) ↔ Monotone f
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNatClamp n).toNat = n
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.desc.aux_trans : ∀ {ι : Type u_1} {X : ι → Type u_5} {i j k : ι} (hij : i = j) (hjk : j = k) (x : X i),
  (ComplexShape.Embedding.AreComplementary.desc.aux X j k hjk)
      ((ComplexShape.Embedding.AreComplementary.desc.aux X i j hij) x) =
    (ComplexShape.Embedding.AreComplementary.desc.aux X i k ⋯) x
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- An `r + 1`-cliquefree Turán-maximal graph is _not_ `r`-cliquefree
if it can accommodate such a clique.  -/
SimpleGraph.not_cliqueFree_of_isTuranMaximal : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ},
  r ≤ Fintype.card V → G.IsTuranMaximal r → ¬G.CliqueFree r
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, i < r.toArray.size → (Std.PRange.succMany? i r.lower).isSome = true
-- Mathlib.Data.Fintype.Quotient
Quotient.finHRecOn_mk : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {C : ((i : ι) → Quotient (S i)) → Sort u_4} (a : (i : ι) → α i), (Quotient.finHRecOn fun x => ⟦a x⟧) = fun f x => f a
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.augmentedCechConerve_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (f : CategoryTheory.Arrow C), CategoryTheory.CosimplicialObject.augmentedCechConerve.obj f = f.augmentedCechConerve
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.restrict_apply_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {H : Type u_6}
  [inst_6 : Monoid H] (π : ContRepresentation R G V) (φ : H →* G) (h : H) (v : V), ((π.restrict φ) h) v = (π (φ h)) v
-- Mathlib.GroupTheory.Transfer
/-- Explicit computation of the transfer homomorphism.  -/
MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  [inst_2 : H.FiniteIndex] (g : G) [inst_3 : Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))],
  ϕ.transfer g =
    ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.srange_eq_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), f.srange = AddSubsemigroup.map f ⊤
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.tendsto_atBot_iff : ∀ {x : ℝ*}, Filter.Germ.Tendsto x Filter.atBot ↔ x < 0 ∧ ArchimedeanClass.mk x < 0
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.compProd_fst_condKernelReal : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ))
  [inst_1 : ProbabilityTheory.IsFiniteKernel κ], κ.fst.compProd κ.condKernelReal = κ
-- Mathlib.Data.Set.Image
Set.image_compl_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f '' (f ⁻¹' s)ᶜ = Set.range f \ s
-- Mathlib.Order.Interval.Finset.Nat
Nat.cauchy_induction : ∀ {P : ℕ → Prop},
  (∀ (n : ℕ), P (n + 1) → P n) →
    ∀ (seed : ℕ), P seed → ∀ (f : ℕ → ℕ), (∀ (x : ℕ), seed ≤ x → P x → x < f x ∧ P (f x)) → ∀ (n : ℕ), P n
-- Mathlib.Algebra.Group.Hom.Defs
map_mul_eq_one : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) {a b : M}, a * b = 1 → f a * f b = 1
-- Lean.Parser.Term
/-- Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.

When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.

Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.

Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.

`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
 -/
Lean.Parser.Term.match : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.exists_of_isPullback : ∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPullback t l r b →
    ∀ (x₂ : X₂) (x₃ : X₃),
      (CategoryTheory.ConcreteCategory.hom r) x₂ = (CategoryTheory.ConcreteCategory.hom b) x₃ →
        ∃ x₁, (CategoryTheory.ConcreteCategory.hom t) x₁ = x₂ ∧ (CategoryTheory.ConcreteCategory.hom l) x₁ = x₃
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two maps into an equalizer are equal if they are equal when composed with the equalizer map.  -/
CategoryTheory.Limits.equalizer.hom_ext : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.equalizer f g},
  CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) =
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) →
    k = l
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.associator_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv
-- Init.Data.BitVec.Basic
/-- Converts a list of `Bool`s into a little-endian `BitVec`.  -/
BitVec.ofBoolListLE : (bs : List Bool) → BitVec bs.length
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.inv U.toSpecΓ =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)))
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- The type of monoidal natural transformations between (bundled) lax monoidal functors.  -/
CategoryTheory.LaxMonoidalFunctor.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            CategoryTheory.LaxMonoidalFunctor C D → CategoryTheory.LaxMonoidalFunctor C D → Type (max u₁ v₂)
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_pos : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [q.IsPrime] [Module.Finite R S], 0 < q.ramificationIdx R
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddOpposite.opUniformEquivRight.eq_1 : ∀ (G : Type u_2) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  AddOpposite.opUniformEquivRight G =
    { toEquiv := AddOpposite.opEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.natCast_eq_toENat : ∀ {c : Cardinal.{u}} {n : ℕ}, ↑n = Cardinal.toENat c ↔ ↑n = c
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSumLocallyUniformly_weierstrassP : ∀ (L : PeriodPair), HasSumLocallyUniformly (fun l z => 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) L.weierstrassP
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instOne : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              (x : Submonoid A) →
                [inst_3 : AddCommMonoid ι] →
                  [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → One (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instCommGroup : (A : Type u_2) →
  (E : Type u_6) →
    [inst : Monoid A] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : CommGroup E] → [inst_3 : TopologicalSpace E] → [IsTopologicalGroup E] → CommGroup (A →ₜ* E)
-- Mathlib.Logic.Equiv.Defs
Equiv.conj_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.conj.symm = e.symm.conj
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)) {Z : CommRingCat} (h : CommRingCat.of x.asIdeal.ResidueField ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).residue x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.stalkIso R x).hom
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom (algebraMap (Localization.AtPrime x.asIdeal) x.asIdeal.ResidueField)) h)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R),
  algebraMap ↑R
      ↑(((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
              (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
          p) =
    CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le : ∀ {X : AlgebraicGeometry.Scheme} (I : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))),
  (AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals I).ideal ≤ I
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List ((a : α) × β a)} {k : α}, k ∈ m.insertMany l → (List.map Sigma.fst l).contains k = false → k ∈ m
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_ringHom_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β) (a : α), ↑f a = f a
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- This is a slightly more convenient method to verify that a cotrident is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.Cotrident.IsColimit.mk : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            (t : CategoryTheory.Limits.Cotrident f) →
              (desc : (s : CategoryTheory.Limits.Cotrident f) → t.pt ⟶ s.pt) →
                (∀ (s : CategoryTheory.Limits.Cotrident f), CategoryTheory.CategoryStruct.comp t.π (desc s) = s.π) →
                  (∀ (s : CategoryTheory.Limits.Cotrident f) (m : t.pt ⟶ s.pt),
                      (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
                          CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) →
                        m = desc s) →
                    CategoryTheory.Limits.IsColimit t
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.instAlgEquivClassGalSplittingField : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F), AlgEquivClass p.Gal F p.SplittingField p.SplittingField
-- Mathlib.Analysis.Analytic.Constructions
analyticOn_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E}, AnalyticOn 𝕜 (fun x x_1 => f x_1 x) s ↔ ∀ (i : ι), AnalyticOn 𝕜 (f i) s
-- Init.Data.String.Lemmas.Intercalate
String.join_cons : ∀ {s : String} {l : List String}, String.join (s :: l) = s ++ String.join l
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instSMulRat : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → SMul ℚ ↥(selfAdjoint R)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.denote_mkFullAdderOut : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign : α → Bool) (aig : Std.Sat.AIG α)
  (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig),
  ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧ ^^
      ⟦assign, { aig := aig, ref := input.cin }⟧)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_le : ∀ {α : Type u_1} {m : Set α → ENNReal} (s : Set α), (MeasureTheory.OuterMeasure.boundedBy m) s ≤ m s
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β],
  CovariantClass α (Filter β) (fun x1 x2 => x1 +ᵥ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.id_hComp : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)) η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.eqToHom ⋯))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instInhabited : Inhabited SemiNormedGrp₁
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.pi_comp : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [inst_7 : (i : ι) → TopologicalSpace (φ i)]
  [inst_8 : (i : ι) → AddCommMonoid (φ i)] [inst_9 : (i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i)
  (g : M₂ →L[R] M), ContinuousLinearMap.pi f ∘SL g = ContinuousLinearMap.pi fun i => f i ∘SL g