mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.instIsLocallyInjectiveToSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ],
  PresheafOfModules.IsLocallyInjective J (PresheafOfModules.toSheafify α φ)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_div_intCast : ∀ {x : ℝ} (m : ℤ), Irrational (x / ↑m) → Irrational x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t ≠ ∅ → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Fin.Embedding.snoc.congr_simp : ∀ {α : Type u_1} {n : ℕ} (x x_1 : Fin n ↪ α) (e_x : x = x_1) {a a_1 : α} (e_a : a = a_1) (ha : a ∉ Set.range ⇑x),
  Fin.Embedding.snoc x ha = Fin.Embedding.snoc x_1 ⋯
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.one_le_coeffSubmodule : ∀ {R₀ : Type u_1} {R : Type u_2} [inst : CommRing R₀] [inst_1 : CommRing R] [inst_2 : Algebra R₀ R] {n : ℕ}
  {e : ChevalleyThm.PolynomialC.InductionObj✝ R n}, 1 ≤ ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule✝ R₀ e
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_category : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {S : C} (R : CategoryTheory.Presieve S),
  (CategoryTheory.Presieve.ofArrows (fun f => f.obj.left) fun f => f.obj.hom) = R
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.mk.inj : ∀ {lctx : Lean.LocalContext} {sources : List Lean.Meta.Grind.EMatchDiagNode} {target : Lean.Meta.Grind.EMatchDiagNode}
  {lctx_1 : Lean.LocalContext} {sources_1 : List Lean.Meta.Grind.EMatchDiagNode}
  {target_1 : Lean.Meta.Grind.EMatchDiagNode},
  { lctx := lctx, sources := sources, target := target } =
      { lctx := lctx_1, sources := sources_1, target := target_1 } →
    lctx = lctx_1 ∧ sources = sources_1 ∧ target = target_1
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {g : α → X} [MeasurableConstVAdd M X], Measurable g → ∀ (c : M), Measurable (c +ᵥ g)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousInvCoe : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Inv (R i)]
  [inst_3 : ∀ (i : ι), InvMemClass (S i) (R i)] [∀ (i : ι), ContinuousInv (R i)],
  ContinuousInv (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
IsSelfAdjoint.cfc : ∀ {R : Type u_1} {A : Type u_2} [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] [inst_9 : ContinuousFunctionalCalculus R A IsSelfAdjoint] {f : R → R}
  {a : A}, IsSelfAdjoint (cfc f a)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_2 a x
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.lift_π₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.lift φ₀ φ₁ h) (HomologicalComplex.pathObject.π₀ K) =
    φ₀
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.trans_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] [inst_4 : Add α] [inst_5 : Add β] [inst_6 : Add γ] [inst_7 : Add δ]
  (f : α ≃+o β) (g : β ≃+o γ) (h : γ ≃+o δ), (f.trans g).trans h = f.trans (g.trans h)
-- Batteries.Tactic.PermuteGoals
/-- If the current goals are `g₁ ⋯ gᵢ ⋯ gₙ`, `splitGoalsAndGetNth i` returns
`(gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ])`.

If `reverse` is passed as `true`, the `i`-th goal is picked by counting backwards.
For instance, `splitGoalsAndGetNth 1 true` puts the last goal in the first component
of the returned term.
 -/
Batteries.Tactic.splitGoalsAndGetNth : ℕ → optParam Bool false → Lean.Elab.Tactic.TacticM (Lean.MVarId × List Lean.MVarId × List Lean.MVarId)
-- Init.Data.Float.Float32
Float32.ofModel.inj : ∀ {toModel toModel_1 : Float32.Model}, { toModel := toModel } = { toModel := toModel_1 } → toModel = toModel_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Returns an updated formula f and a bool which indicates whether a contradiction was found in the
process of updating f.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRatUnits : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool
-- Mathlib.Algebra.Ring.Hom.Defs
/-- If there is a homomorphism `f : α →+* β` and `β` is nontrivial, then `α` is nontrivial.  -/
RingHom.domain_nontrivial : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [Nontrivial β],
  Nontrivial α
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_3),
  (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.Const.IteratedInsertionInto : {α : Type u} → {β : Type v} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => β) → Type (max 0 u v)
-- Mathlib.RingTheory.Localization.Finiteness
/-- If `I` is an ideal such that there exists a set `{ r }` of `R` that generates the unit ideal
and such that the image of `I` in `Rᵣ` is finitely generated for each `r`, then `I` is finitely
generated.  -/
Ideal.fg_of_localizationSpan : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} (t : Set R),
  Ideal.span t = ⊤ → (∀ (g : ↑t), (Ideal.map (algebraMap R (Localization.Away ↑g)) I).FG) → I.FG
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
to zero as `μ s` tends to zero. This lemma states this fact in terms of `ε` and `δ`.  -/
MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
-- Mathlib.Logic.Hydra
Relation.cutExpand_pair_right : ∀ {α : Type u_1} {r : α → α → Prop} {a b' b : α}, r b' b → Relation.CutExpand r {a, b'} {a, b}
-- Mathlib.Algebra.Group.Basic
inv_mul_eq_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), a⁻¹ * b = b / a
-- Std.Do.PostCond
Std.Do.ExceptConds.entails_true : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, x.entails Std.Do.ExceptConds.true
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.anchorToString : ℕ → UInt64 → String
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
CategoryTheory.Bicategory.Strict.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B]
  (id_comp :
    autoParam (∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f)
      CategoryTheory.Bicategory.Strict.id_comp._autoParam)
  (comp_id :
    autoParam (∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f)
      CategoryTheory.Bicategory.Strict.comp_id._autoParam)
  (assoc :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
          CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
      CategoryTheory.Bicategory.Strict.assoc._autoParam),
  autoParam (∀ {a b : B} (f : a ⟶ b), CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯)
      CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso._autoParam →
    autoParam (∀ {a b : B} (f : a ⟶ b), CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯)
        CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso._autoParam →
      autoParam
          (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
            CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯)
          CategoryTheory.Bicategory.Strict.associator_eqToIso._autoParam →
        CategoryTheory.Bicategory.Strict B
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.ext : ∀ {A : Type u_1} {σ : Type u_2} {inst : CommRing A} {inst_1 : SetLike σ A} {inst_2 : AddSubmonoidClass σ A} {𝒜 : ℕ → σ}
  {inst_3 : GradedRing 𝒜} {x y : ProjectiveSpectrum 𝒜}, x.asHomogeneousIdeal = y.asHomogeneousIdeal → x = y
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
PowerBasis.ofAdjoinEqTop'.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x) (hx' : R[x] = ⊤),
  PowerBasis.ofAdjoinEqTop' hx hx' =
    (Algebra.adjoin.powerBasis' hx).map ((R[x].equivOfEq ⊤ hx').trans Subalgebra.topEquiv)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.negY P = -P 1 - W'.a₁ * P 0 * P 2 - W'.a₃ * P 2 ^ 3
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_mono_left' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_7} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S T f ≤ MeasureTheory.L1.SimpleFunc.setToL1S T' f
-- Mathlib.Order.RelClasses
IsWellFounded.mk : ∀ {α : Type u} {r : α → α → Prop}, WellFounded r → IsWellFounded α r
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Implementation; see `StructuredArrow.prodEquivalence`.  -/
CategoryTheory.StructuredArrow.prodFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (S : D) →
                  (S' : D') →
                    (T : CategoryTheory.Functor C D) →
                      (T' : CategoryTheory.Functor C' D') →
                        CategoryTheory.Functor (CategoryTheory.StructuredArrow (S, S') (T.prod T'))
                          (CategoryTheory.StructuredArrow S T × CategoryTheory.StructuredArrow S' T')
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] {inst_1 : DecidableEq α} [inst_2 : DecidableEq α] (σ σ_1 : Equiv.Perm α),
  σ = σ_1 → σ.IsThreeCycle = σ_1.IsThreeCycle
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_mul : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {p q : Polynomial T},
  p * q ≠ 0 → (p * q).aroots S = p.aroots S + q.aroots S
-- Mathlib.Algebra.Lie.Quotient
LieHom.quotKerEquivRange_toFun : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a : L ⧸ (↑f).ker),
  f.quotKerEquivRange a = (↑f).quotKerEquivRange a
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_mul : ∀ {ι : Type u_1} {M : Type u_7} [inst : Mul M] (a b : M),
  Function.const ι a * Function.const ι b = Function.const ι (a * b)
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.prepathObject_p₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject],
  K.prepathObject.p₁ = HomologicalComplex.pathObject.π₁ K
-- Init.Data.String.Basic
String.Pos.Raw.lt_next : ∀ (s : String) (i : String.Pos.Raw), i < String.Pos.Raw.next s i
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {i j : 𝒰.I₀} (f : i ⟶ j),
  AlgebraicGeometry.IsOpenImmersion ((AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰).map f)
-- Init.Data.Nat.MinMax
Nat.add_min_add_right : ∀ (a b c : ℕ), min (a + c) (b + c) = min a b + c
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- A version of `fderivWithin_const_smul` without differentiability hypothesis:
in return, the constant `c` must be invertible, i.e. if `R` is a field.  -/
fderivWithin_const_smul_of_invertible : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F] (c : R) [Invertible c],
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
-- Mathlib.Algebra.AlgebraicCard
/-- [Stacks Tag 09GK](https://stacks.math.columbia.edu/tag/09GK) -/
Algebraic.cardinalMk_le_max : ∀ (R A : Type u) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A], Cardinal.mk { x // IsAlgebraic R x } ≤ max (Cardinal.mk R) Cardinal.aleph0
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearEquiv.isBigO_comp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (e : E ≃SL[σ₁₂] F) [RingHomIsometric σ₁₂]
  {α : Type u_7} (f : α → E) (l : Filter α), (fun x' => e (f x')) =O[l] f
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.coe_mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : Set α → M) (h₁ : v ∅ = 0) (h₂ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → v i = 0)
  (h₃ :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => v (f i)) (v (⋃ i, f i))),
  ⇑{ measureOf' := v, empty' := h₁, not_measurable' := h₂, m_iUnion' := h₃ } = v
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonUnitalCommRing.mul_comm : ∀ {α : Type u} [self : NonUnitalCommRing α] (a b : α), a * b = b * a
-- Init.Data.String.PosRaw
String.Pos.Raw.mk_byteIdx : ∀ (p : String.Pos.Raw), { byteIdx := p.byteIdx } = p
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Bisimulation principle using `LiftR` to match and relate children of two trees.  -/
MvQPF.Cofix.bisim : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  (r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
  (∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR (α.RelLast r) x.dest y.dest) →
    ∀ (x y : MvQPF.Cofix F α), r x y → x = y
-- Lean.Meta.Tactic.Grind.Injective
_private.Lean.Meta.Tactic.Grind.Injective.0.Lean.Meta.Grind.symbolsToNames : List Lean.HeadIndex → List Lean.Name
-- Mathlib.Tactic.DeriveEncodable
/-- Constructs a function from `S` to the inductive type.  -/
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkFromSFuns : Lean.Elab.Deriving.Context → Array Lean.Name → Lean.Elab.TermElabM (Lean.TSyntax `command)
-- Mathlib.Topology.Algebra.Order.Floor
_private.Mathlib.Topology.Algebra.Order.Floor.0.termI : Lean.ParserDescr
-- Mathlib.Algebra.Field.Equiv
IsLocalHom.isField : ∀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : FunLike F A B]
  [MonoidWithZeroHomClass F A B] {f : F} [IsLocalHom f], Function.Injective ⇑f → IsField B → IsField A
-- Std.Internal.Parsec.ByteArray
/-- Parse an ASCII digit `0-9` as a `Char`.
 -/
Std.Internal.Parsec.ByteArray.digit : Std.Internal.Parsec.ByteArray.Parser Char
-- Mathlib.Analysis.InnerProductSpace.CanonicalTensor
/-- The canonical covariant tensor corresponding to `InnerProductSpace.canonicalContravariantTensor`
under the identification of `E` with its dual.
 -/
InnerProductSpace.canonicalCovariantTensor : (E : Type u_1) →
  [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → [FiniteDimensional ℝ E] → TensorProduct ℝ E E
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.log_doublingGamma_eq : Set.EqOn (Real.log ∘ Real.doublingGamma)
  (fun s =>
    Real.log (Real.Gamma (s / 2)) + Real.log (Real.Gamma (s / 2 + 1 / 2)) + s * Real.log 2 - Real.log (2 * √Real.pi))
  (Set.Ioi 0)
-- Mathlib.Data.Set.Card
Set.ncard_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).ncard = s.ncard * t.ncard
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.isStandardOpenImmersion_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).IsStandardOpenImmersion ↔ Algebra.IsStandardOpenImmersion R S
-- Mathlib.NumberTheory.PrimesCongruentOne
/-- **Alias** of `Nat.infinite_setOfPred_prime_modEq_one`.

---

For any positive `k : ℕ` there are infinitely many primes `p` such that `p ≡ 1 [MOD k]`.  -/
Nat.infinite_setOf_prime_modEq_one : ∀ {k : ℕ}, k ≠ 0 → {p | Nat.Prime p ∧ p ≡ 1 [MOD k]}.Infinite
-- Mathlib.Probability.Independence.InfinitePi
/-- Given random variables `X i : Ω i → 𝓧 i`, they are independent when viewed as random
variables defined on the product space `Π i, Ω i`.  -/
ProbabilityTheory.iIndepFun_infinitePi : ∀ {ι : Type u_1} {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {Ω : ι → Type u_4}
  {mΩ : (i : ι) → MeasurableSpace (Ω i)} {P : (i : ι) → MeasureTheory.Measure (Ω i)}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {X : (i : ι) → Ω i → 𝓧 i},
  (∀ (i : ι), Measurable (X i)) →
    ProbabilityTheory.iIndepFun (fun i ω => X i (ω i)) (MeasureTheory.Measure.infinitePi P)
-- Mathlib.Algebra.Group.Prod
/-- Coproduct of two `AddHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 + g p.2`.
(Commutative codomain; for the general case, see `AddHom.noncommCoprod`)  -/
AddHom.coprod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : Add M] → [inst_1 : Add N] → [inst_2 : AddCommSemigroup P] → (M →ₙ+ P) → (N →ₙ+ P) → M × N →ₙ+ P
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the second quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open second quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open second quadrant
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the second quadrant.

Then `‖f z‖` is bounded from above by the same constant on the closed second quadrant.  -/
PhragmenLindelof.quadrant_II : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ x ≤ 0, ‖f ↑x‖ ≤ C) → (∀ (x : ℝ), 0 ≤ x → ‖f (↑x * Complex.I)‖ ≤ C) → z.re ≤ 0 → 0 ≤ z.im → ‖f z‖ ≤ C
-- Mathlib.Probability.ProductMeasure
/-- If we push the product measure forward by a reindexing equivalence, we get a product measure
on the reindexed product in the sense that it coincides with `piContent μ` over
measurable cylinders. See `infinitePi_map_piCongrLeft` for a general version.  -/
MeasureTheory.Measure.infinitePiNat_map_piCongrLeft : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (e : ℕ ≃ ι) {s : Set ((i : ι) → X i)},
  s ∈ MeasureTheory.measurableCylinders X →
    (MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCongrLeft X e))
          (MeasureTheory.Measure.infinitePiNat fun n => μ (e n)))
        s =
      (MeasureTheory.piContent μ) s
-- Mathlib.Analysis.Analytic.Composition
/-- The first coefficient of `id 𝕜 E` is the identity.  -/
FormalMultilinearSeries.id_apply_one : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E) (v : Fin 1 → E), (FormalMultilinearSeries.id 𝕜 E x 1) v = v 0