mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.degree_eq_one_of_irreducible : ∀ (k : Type u) [inst : Field k] [IsSepClosed k] {p : Polynomial k}, Irreducible p → p.Separable → p.degree = 1
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_top : ∀ {α : Type u_1} {r : α → α → Prop}, Filter.IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierSMul : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  FourierSMul ℂ ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Init.Data.Array.Bootstrap
Array.empty_append : ∀ {α : Type u_1} {xs : Array α}, #[] ++ xs = xs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {fallback : β k'} {f : Option (β k) → Option (β k)},
  (m.alter k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback
-- Lean.Meta.Tactic.Cleanup
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore.addDeps : Lean.FVarId → StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
-- Mathlib.Topology.Sequences
/-- The quotient of a sequential space is a sequential space.  -/
Quotient.instSequentialSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SequentialSpace X] {s : Setoid X}, SequentialSpace (Quotient s)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (g : B →A[R] C)
  (f : A →A[R] B) (x : A), (g.comp f) x = g (f x)
-- Mathlib.Topology.IsLocalHomeomorph
/-- A function `f : X → Y` satisfies `IsLocalHomeomorph f` if each `x : x` is contained in
the source of some `e : OpenPartialHomeomorph X Y` with `f = e`.  -/
IsLocalHomeomorph : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Lean.Server.References
/-- Syntax of this reference.  -/
Lean.Server.Reference.stx : Lean.Server.Reference → Lean.Syntax
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.mk.eq_1 : ∀ {α : Type u_1} (rels : FreeMonoid α → FreeMonoid α → Prop),
  PresentedMonoid.mk rels = { toFun := Quotient.mk (conGen rels).toSetoid, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.Comp
deriv_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'},
  DifferentiableAt 𝕜' h₂ (h x) → DifferentiableAt 𝕜 h x → deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
-- Mathlib.Order.Monotone.Union
/-- If `f` is strictly monotone both on `(-∞, a]` and `[a, ∞)`, then it is strictly monotone on the
whole line.  -/
StrictMonoOn.Iic_union_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
  StrictMonoOn f (Set.Iic a) → StrictMonoOn f (Set.Ici a) → StrictMono f
-- Mathlib.Analysis.Calculus.ContDiff.Operations
HasFTaylorSeriesUpToOn.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {𝕜' : Type u_3} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
  [inst_7 : NormedSpace 𝕜' E] [inst_8 : IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : IsScalarTower 𝕜 𝕜' F] {p' : E → FormalMultilinearSeries 𝕜' E F} {n : WithTop ℕ∞},
  HasFTaylorSeriesUpToOn n f p' s →
    HasFTaylorSeriesUpToOn n f (fun x => FormalMultilinearSeries.restrictScalars 𝕜 (p' x)) s
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
/-- If `k` is algebraically closed,
then the closed points of `X` are in bijection with the `k`-points of `X`.  -/
AlgebraicGeometry.pointEquivClosedPoint : {X : AlgebraicGeometry.Scheme} →
  {K : Type u} →
    [inst : Field K] →
      [IsAlgClosed K] →
        (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) →
          [AlgebraicGeometry.LocallyOfFiniteType f] →
            { p //
                CategoryTheory.CategoryStruct.comp p f =
                  CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) } ≃
              ↑(closedPoints ↥X)
-- Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
GenContFract.of_convs_eq_convs' : ∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K],
  (GenContFract.of v).convs = (GenContFract.of v).convs'
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isCompact : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens}, AlgebraicGeometry.IsAffineOpen U → IsCompact ↑U
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.mul_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  (∀ i ∈ s, 0 ≤ g₁ i) → (∀ i ∈ s, 0 ≤ g₂ i) → MonovaryOn f g₁ s → MonovaryOn f g₂ s → MonovaryOn f (g₁ * g₂) s
-- Mathlib.CategoryTheory.Action
/-- A multiplicative action M ↻ X induces a category structure on X, where a morphism
from x to y is a scalar taking x to y. Due to implementation details, the object type
of this category is not equal to X, but is in bijection with X.  -/
CategoryTheory.ActionCategory : (M : Type u_1) → [inst : Monoid M] → (X : Type u) → [MulAction M X] → Type (max 0 u)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.linearEquiv_apply : ∀ (R : Type u_1) (A : Type u_3) (E : Type u_4) [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E],
  ⇑(WithCStarModule.linearEquiv R A E) = ⇑(WithCStarModule.equiv A E)
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `SeminormedAddCommGroup E` instance from a `SeminormedSpace.Core` on a type
that already has an existing uniform space structure. This requires a proof that the uniformity
induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].  -/
SeminormedAddCommGroup.ofCoreReplaceUniformity : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            [U : UniformSpace E] →
              (core : SeminormedSpace.Core 𝕜 E) → uniformity E = uniformity E → SeminormedAddCommGroup E
-- Lean.Compiler.LCNF.Basic
/-- The type of the declaration. Note that this is an erased LCNF type
instead of the fully dependent one that might have been the original
type of the declaration in the `Environment`. Furthermore, once in the
impure staged of LCNF this type is only the return type.
 -/
Lean.Compiler.LCNF.Signature.type : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu → Lean.Expr
-- Mathlib.CategoryTheory.Adjunction.Comma
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_symm_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor D C)
  [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C)
  (g : B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left),
  (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A).symm g =
    CategoryTheory.CategoryStruct.comp (G.map g) (⊤_ CategoryTheory.CostructuredArrow G A).hom
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)]
  [hAcompact : ∀ (i : ι), CompactSpace ↥(B i)],
  LocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_inv_left`. -/
Antivary.inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary f g → Monovary f⁻¹ g
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.sum_antidiagonal_succ : ∀ {N : Type u_2} [inst : AddCommMonoid N] {n : ℕ} {f : ℕ × ℕ → N},
  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f p =
    f (0, n + 1) + ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f (p.1 + 1, p.2)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∉ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone : ∀ {α : Type u_2} (f : ℕ → α → ENNReal), Monotone fun n x => ⨆ k, ⨆ (_ : k ≤ n), f k x
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- `MonoidHom.toAdditiveRight` as a `MulEquiv`.  -/
MonoidHom.toAdditiveRightMulEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddMonoid M] → [inst_1 : CommMonoid N] → (Multiplicative M →* N) ≃* Multiplicative (M →+ Additive N)
-- Mathlib.Algebra.DirectSum.Internal
/-- Build a `DirectSum.GNonUnitalNonAssocSemiring` instance for a collection of additive
submonoids.  -/
SetLike.gnonUnitalNonAssocSemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : Add ι] →
        [inst_1 : NonUnitalNonAssocSemiring R] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubmonoidClass σ R] →
              (A : ι → σ) → [SetLike.GradedMul A] → DirectSum.GNonUnitalNonAssocSemiring fun i => ↥(A i)
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the minimum element of the map, or panics if the map is empty.  -/
RBTree.RBMap.min! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → [Inhabited β] → RBTree.RBMap α β cmp → α × β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∈ t → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey? k = t.getKey? k
-- Init.Grind.Attr
/-- Like `@[grind!]`, but also prints the pattern(s) selected by `grind`
as info messages. Combines minimal subexpression selection with debugging output.
 -/
Lean.Parser.Attr.grind!? : Lean.ParserDescr
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
/-- Variant of the second 4-lemma for complexes of any size  -/
CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono'' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {n k : ℕ}
  (h : k + 3 ≤ n) {R₁ R₂ : CategoryTheory.ComposableArrows C n},
  R₁.Exact →
    R₂.Exact →
      ∀ (φ : R₁ ⟶ R₂) (k₀ k₁ k₂ k₃ : ℕ) (hk₀ : k₀ = k) (hk₁ : k₁ = k + 1) (hk₂ : k₂ = k + 2) (hk₃ : k₃ = k + 3),
        CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ k₀ ⋯) →
          CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ k₂ ⋯) →
            CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ k₃ ⋯) →
              CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ k₁ ⋯)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
/-- Force `RespectsIso`.  -/
CategoryTheory.MorphismProperty.sourceLocalClosure.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y')
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g),
  CategoryTheory.MorphismProperty.sourceLocalClosure K P f → CategoryTheory.MorphismProperty.sourceLocalClosure K P g
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modifyGet_MonadStateOf_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n : Type u → Type v} [inst : MonadLift m n]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : (α : Type u) → Std.Internal.Do.WP (n α) α Pred EPred] {σ α : Type u} {post : α → Pred} {epost : EPred}
  [inst_4 : MonadStateOf σ m] (f : σ → α × σ),
  Std.Internal.Do.wp (MonadStateOf.modifyGet f) post epost =
    Std.Internal.Do.wp (MonadLift.monadLift (modifyGet f)) post epost
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_sub_C_sq : ∀ {R : Type u} [inst : CommRing R] (c : R),
  Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X - Polynomial.C c)
-- Init.Data.List.Scan.Lemmas
List.getElem_scanr_zero : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β}, (List.scanr f b l)[0] = List.foldr f b l
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Polynomial.IsDistinguishedAt.algEquivQuotient.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {g : Polynomial A} {I I_1 : Ideal A} (e_I : I = I_1) (H : g.IsDistinguishedAt I)
  [inst_1 : IsAdicComplete I A], H.algEquivQuotient = ⋯.algEquivQuotient
-- Mathlib.FieldTheory.SeparableDegree
/-- If a field `F` is of exponential characteristic `q`, then `Polynomial.expand F (q ^ n) f`
and `f` have the same separable degree.  -/
Polynomial.natSepDegree_expand : ∀ {F : Type u} [inst : Field F] (f : Polynomial F) (q : ℕ) [hF : ExpChar F q] {n : ℕ},
  ((Polynomial.expand F (q ^ n)) f).natSepDegree = f.natSepDegree
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion, then it is exponentially close to the partial
sums of this power series on strict subdisks of the disk of convergence.

This version provides an upper estimate that decreases both in `‖y‖` and `n`. See also
`HasFPowerSeriesOnBall.uniform_geometric_approx` for a weaker version.  -/
HasFPowerSeriesOnBall.uniform_geometric_approx' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesOnBall f p x r →
    ↑r' < r →
      ∃ a ∈ Set.Ioo 0 1,
        ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
-- Plausible.Functions
/-- Apply a total function to an argument.  -/
Plausible.TotalFunction.apply : {α : Type u} → {β : Type v} → [DecidableEq α] → Plausible.TotalFunction α β → α → β
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.liftInclusion.eq_1 : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M),
  FirstOrder.Language.DirectLimit.liftInclusion S =
    FirstOrder.Language.DirectLimit.lift L ι (fun i => ↥(S i))
      (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) (fun x => (S x).subtype) ⋯
-- Mathlib.Analysis.Normed.Group.Basic
enorm_eq_zero : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ENormedAddMonoid E] {a : E}, ‖a‖ₑ = 0 ↔ a = 0
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitude_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] {m n : ℕ} (s : Affine.Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)),
  (s.reindex e).altitude = s.altitude ∘ ⇑e.symm
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_mono : ∀ (k k' n : ℕ), k ≤ k' → (ArithmeticFunction.sigma k) n ≤ (ArithmeticFunction.sigma k') n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forIn_eq_forIn_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toList init f
-- Mathlib.Geometry.Manifold.Notation
/-- `MDiff[s] f` elaborates to `MDifferentiableOn I J f s`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termMDiff[_]__» : Lean.ParserDescr
-- Init.Data.Float.Float32
/-- Negates 32-bit floating-point numbers according to IEEE 754. Typically used via the `-` prefix
operator.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C negation operator.
 -/
Float32.neg : Float32 → Float32
-- Mathlib.RingTheory.Congruence.Basic
RingCon.coe_algebraMap : ∀ {α : Type u_1} {R : Type u_3} [inst : CommSemiring α] [inst_1 : Semiring R] [inst_2 : Algebra α R] (c : RingCon R)
  (s : α), ↑((algebraMap α R) s) = (algebraMap α c.Quotient) s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Dense.borel_eq_generateFrom_Icc_mem : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  [DenselyOrdered α] [NoMinOrder α] {s : Set α},
  Dense s → borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Set.Icc l u = S}
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂Comp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f g h : a ⟶ b} →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
            [inst_3 : Mathlib.Tactic.BicategoryCoherence.LiftHom h] →
              (η : f ⟶ g) →
                (θ : g ⟶ h) →
                  [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] →
                    [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ θ] →
                      Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.CategoryStruct.comp η θ)
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToAction F).ReflectsMonomorphisms
-- Mathlib.Order.Sublocale
Sublocale.mem_mk : ∀ {X : Type u_1} [inst : Order.Frame X] {a : X} (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier)
  (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier),
  a ∈ { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } ↔ a ∈ carrier
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioi : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a : ι → α},
  Filter.Tendsto a l Filter.atBot → ∀ [NoMinOrder α], MeasureTheory.AECover μ l fun i => Set.Ioi (a i)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.op_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), AddOpposite.op ↑n = ↑n
-- Std.Time.Format.Modifier
Std.Time.OffsetO.full.sizeOf_spec : sizeOf Std.Time.OffsetO.full = 1
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_eq_bot_iff' : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)}, Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapIdx.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → Array β → Sort u_3) (a : α) (as : List α) (acc : Array β)
  (h_1 : (acc : Array β) → motive [] acc) (h_2 : (a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc),
  (match a :: as, acc with
    | [], acc => h_1 acc
    | a :: as, acc => h_2 a as acc) =
    h_2 a as acc
-- Mathlib.Topology.Basic
Classical.indefiniteDescription.congr_simp : ∀ {α : Sort u} (p : α → Prop) (h : ∃ x, p x), Classical.indefiniteDescription p h = Classical.indefiniteDescription p h
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H0IsoOfIsTrivial_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 0) (groupCohomology.H0IsoOfIsTrivial A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0) (groupCohomology.cochainsIso₀ A).hom
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Augmented.stdSimplex_map_left : ∀ {X Y : SimplexCategory} (θ : X ⟶ Y), (SSet.Augmented.stdSimplex.map θ).left = SSet.stdSimplex.map θ
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ κ_1 : ProbabilityTheory.Kernel α (γ × β)),
  κ = κ_1 →
    ∀ (ν ν_1 : ProbabilityTheory.Kernel α γ),
      ν = ν_1 →
        ∀ (a a_1 : α),
          a = a_1 →
            ∀ (x x_1 : γ), x = x_1 → ∀ (s s_1 : Set β), s = s_1 → κ.density ν a x s = κ_1.density ν_1 a_1 x_1 s_1
-- Mathlib.Order.Fin.Tuple
Fin.strictMono_insertNth_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} (q : Fin (n + 1)) (x : α) (f : Fin n → α),
  StrictMono (q.insertNth x f) ↔
    StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i
-- Lean.Data.KVMap
Lean.KVMap.setNat : Lean.KVMap → Lean.Name → ℕ → Lean.KVMap