mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Basic
Lean.Parser.ParserState.replaceLongest : Lean.Parser.ParserState → ℕ → Lean.Parser.ParserState
-- Lean.Environment
/-- Checks if, in the public scope (`Environment.isExporting`), the given name refers to a
definition with a visible body, i.e. `ConstantInfo.hasValue`. Recall that outside the module
system, this is any definition.  -/
Lean.Environment.hasExposedBody : Lean.Environment → Lean.Name → Bool
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIci : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → (a : α) → Fintype ↑(Set.Ici a)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_discrete_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {c d : C} (f : c ⟶ d),
  f ∈ CategoryTheory.Subgroupoid.discrete.arrows c d ↔ ∃ (h : c = d), f = CategoryTheory.eqToHom h
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toList.isEmpty = m.isEmpty
-- Mathlib.RingTheory.SimpleModule.Isotypic
isIsotypic_submodule_iff : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  IsIsotypic R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], IsIsotypicOfType R ↥N ↥m
-- Std.Data.TreeSet.Basic
/-- Returns the `n`-th smallest element, or `none` if `n` is at least `t.size`.  -/
Std.TreeSet.atIdx? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → ℕ → Option α
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.GridLines.T_univ : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] {p : ℝ} [inst_2 : Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i),
  MeasureTheory.GridLines.T μ p f Finset.univ x =
    ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑(Fintype.card ι) - 1) * p) *
        ∏ i, (∫⁻ (t : A i), f (Function.update x i t) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instSemigroupWithZero : {α : Type u_1} → [Semigroup α] → SemigroupWithZero (WithZero α)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.createsFiniteColimits : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {T : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} T] →
        {G : CategoryTheory.Functor A T} →
          {X : T} →
            [CategoryTheory.Limits.PreservesFiniteColimits G] →
              CategoryTheory.Limits.CreatesFiniteColimits (CategoryTheory.CostructuredArrow.proj G X)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_le_exp_iff_le_emultiplicity : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R}
  {n : ℕ}, v.intValuation r ≤ WithZero.exp (-↑n) ↔ ↑n ≤ emultiplicity v.asIdeal (Ideal.span {r})
-- Mathlib.Tactic.FunProp.Theorems
/-- Identity theorem e.g. `Continuous fun x ↦ x`  -/
Mathlib.Meta.FunProp.LambdaTheoremArgs.id : Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mem_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R}, x ∈ s.toSubsemigroup ↔ x ∈ s
-- Std.Async.TCP
/-- Shuts down the write side of the client socket.
 -/
Std.Async.TCP.Socket.Client.shutdown : Std.Async.TCP.Socket.Client → Std.Async.Async Unit
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : { x // x.Compatible }),
  ↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible x) = (↑x).sieveExtend
-- Mathlib.Data.Set.Image
Set.empty_eq_image : ∀ {α : Type u_5} {β : Type u_6} {f : α → β} {s : Set α}, ∅ = f '' s ↔ s = ∅
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpace.toInnerProductSpaceable : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E],
  InnerProductSpaceable E
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_forall_map_le : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K ≤ K
-- Mathlib.Data.Finset.NAry
Finset.Nonempty.image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  s.Nonempty → t.Nonempty → (Finset.image₂ f s t).Nonempty
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  φ.IsQF → ψ.IsPrenex → (φ.toPrenexImpRight ψ).IsPrenex
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₃_map : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  Polynomial.C (RatFunc.Luroth.Q₃✝ h) = RatFunc.Luroth.Q₂✝ h
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The target vertex of `coherentIso`.  -/
SSet.coherentIso.x₁ : SSet.coherentIso.obj (Opposite.op { len := 0 })
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.MutuallySingular.rnDeriv_ae_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.MutuallySingular ν → μ.rnDeriv ν =ᵐ[ν] 0
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsStable.locally_and_iff : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : Zero E] [inst_3 : TopologicalSpace ι] [inst_4 : OrderTopology ι],
  ProbabilityTheory.IsStable 𝓕 p →
    ProbabilityTheory.IsStable 𝓕 q →
      (ProbabilityTheory.Locally (fun Y => p Y ∧ q Y) 𝓕 X P ↔
        ProbabilityTheory.Locally p 𝓕 X P ∧ ProbabilityTheory.Locally q 𝓕 X P)
-- Init.Data.Nat.Lemmas
Nat.div_eq_iff_eq_mul_right : ∀ {a b c : ℕ}, 0 < b → b ∣ a → (a / b = c ↔ a = b * c)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.oset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.Compiler.LCNF.Arg pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_3) (fvarId_1 : Lean.FVarId)
  (i_1 : ℕ) (y_1 : Lean.Compiler.LCNF.Arg pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_3),
  (Lean.Compiler.LCNF.CodeDecl.oset fvarId i y h = Lean.Compiler.LCNF.CodeDecl.oset fvarId_1 i_1 y_1 h_1) =
    (fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1)
-- Mathlib.GroupTheory.Exponent
/-- The exponent of product of two monoids is the `lcm` of the exponents of the
individual monoids.  -/
Monoid.exponent_prod : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Monoid M₁] [inst_1 : Monoid M₂],
  Monoid.exponent (M₁ × M₂) = lcm (Monoid.exponent M₁) (Monoid.exponent M₂)
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.aeval_verschiebung_poly' : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  (MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = x.verschiebungFun.coeff n
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.ExtTreeMap.maxEntryD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α × β → α × β
-- Mathlib.Algebra.BigOperators.Finprod
/-- The torsion-free assumption makes sure that the result holds even when the support of `f` is
infinite. For a more usual version assuming `HasFiniteSupport f` instead, see `smul_finsum'`.  -/
smul_finsum : ∀ {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] (c : R) (f : ι → M), c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.insert₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {a : α}
  {b : β a} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.attachJP : Lean.Elab.Term.Do.JPDecl → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Mathlib.CategoryTheory.Core
/-- The object of the base category underlying an object in `Core C`.  -/
CategoryTheory.Core.of : {C : Type u₁} → CategoryTheory.Core C → C
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRccSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Rcc.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RccSlice α)
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.coe_smul_primesOver : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  {G : Type u_3} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (σ : G)
  (P : ↑(p.primesOver B)), ↑(σ • P) = σ • ↑P
-- Mathlib.Order.Closure
LowerAdjoint.closure_le_closed_iff_le : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α)
  {y : α}, y ∈ l.closed → (u (l.toFun x) ≤ y ↔ x ≤ y)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), AdjoinRoot.mk f = Ideal.Quotient.mk (Ideal.span {f})
-- Mathlib.CategoryTheory.Localization.Bousfield
/-- Given `P : ObjectProperty C`, this is the class of morphisms `f : X ⟶ Y`
such that for all `Z : C` such that `P Z`, the precomposition with `f` induces
a bijection `(Y ⟶ Z) ≃ (X ⟶ Z)`. (One of the applications of this notion
is the left Bousfield localization of model categories.)  -/
CategoryTheory.ObjectProperty.isLocal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C
-- Lean.Data.KVMap
Lean.DataValue.ofName.inj : ∀ {v v_1 : Lean.Name}, Lean.DataValue.ofName v = Lean.DataValue.ofName v_1 → v = v_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_mulSupport : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [inst : TopologicalSpace E]
  [TopologicalSpace.MetrizableSpace E] [inst_2 : One E] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.NullMeasurableSet (Function.mulSupport f) μ
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context.mk.inj : ∀ {m returnType : Lean.Syntax} {uvars : Array Lean.Elab.Term.Do.Var} {kind : Lean.Elab.Term.Do.ToTerm.Kind}
  {m_1 returnType_1 : Lean.Syntax} {uvars_1 : Array Lean.Elab.Term.Do.Var} {kind_1 : Lean.Elab.Term.Do.ToTerm.Kind},
  { m := m, returnType := returnType, uvars := uvars, kind := kind } =
      { m := m_1, returnType := returnType_1, uvars := uvars_1, kind := kind_1 } →
    m = m_1 ∧ returnType = returnType_1 ∧ uvars = uvars_1 ∧ kind = kind_1
-- Std.Data.HashMap.Basic
Std.HashMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (inner : Std.DHashMap α fun x => β), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.RingTheory.IntegralDomain
mul_left_bijective_of_finite₀ : ∀ {M : Type u_1} [inst : MonoidWithZero M] [Finite M] [IsRightCancelMulZero M] {a : M},
  a ≠ 0 → Function.Bijective fun b => b * a
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_eq_reflTransGen : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Symm r], Relation.EqvGen r = Relation.ReflTransGen r
-- Mathlib.Topology.Path
Path.extend_extends' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t : ↑(Set.Icc 0 1)), γ.extend ↑t = γ t
-- Mathlib.Analysis.Convex.Function
ConcaveOn.add_strictConcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β},
  ConcaveOn 𝕜 s f → StrictConcaveOn 𝕜 s g → StrictConcaveOn 𝕜 s (f + g)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncate_comp : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃),
  (TruncatedWittVector.truncate h1).comp (TruncatedWittVector.truncate h2) = TruncatedWittVector.truncate ⋯
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toNatClampNeg = b.toInt.toNat
-- Mathlib.Algebra.Order.Pi
Pi.isOrderedAddCancelMonoid : ∀ {I : Type u_1} {f : I → Type u_5} [inst : (i : I) → AddCommMonoid (f i)] [inst_1 : (i : I) → Preorder (f i)]
  [∀ (i : I), IsOrderedCancelAddMonoid (f i)], IsOrderedCancelAddMonoid ((i : I) → f i)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_sum : ∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : Semiring R] (s : Finset ι) (f : ι → AddMonoidAlgebra R M),
  (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  AlgebraicTopology.DoldKan.P 0 = CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
IsIntegralClosure.isIntegral_iff : ∀ {A : Type u_1} {R : Type u_2} {B : Type u_3} {inst : CommRing R} {inst_1 : CommSemiring A} {inst_2 : CommRing B}
  {inst_3 : Algebra R B} {inst_4 : Algebra A B} [self : IsIntegralClosure A R B] {x : B},
  IsIntegral R x ↔ ∃ y, (algebraMap A B) y = x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.strongInnerAnodyneExtensions_le_strongAnodyneExtensions : SSet.strongInnerAnodyneExtensions ≤ SSet.strongAnodyneExtensions
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.pNilradical_eq_bot : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p], pNilradical R p = ⊥
-- Mathlib.Computability.ContextFreeGrammar
/-- Inductive definition of a single application of a given context-free rule `r` to a string `u`;
`r.Rewrites u v` means that the `r` sends `u` to `v` (there may be multiple such strings `v`).  -/
ContextFreeRule.Rewrites : {T : Type u_1} → {N : Type u_2} → ContextFreeRule T N → List (Symbol T N) → List (Symbol T N) → Prop
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_right_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).inv)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).inv Z)
            (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)))
-- Mathlib.Order.GameAdd
/-- **Alias** of `Sym2.GameAdd.recursion_eq`. -/
Sym2.GameAdd.fix_eq : ∀ {α : Type u_1} {rα : α → α → Prop} {C : α → α → Sort u_3} (hr : WellFounded rα)
  (IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α),
  Sym2.GameAdd.recursion hr IH a b = IH a b fun a' b' x => Sym2.GameAdd.recursion hr IH a' b'
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_coe_toRingHom : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] (f : F), RingHom.ker ↑f = RingHom.ker f
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.measurable_charFun : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [OpensMeasurableSpace E] [SecondCountableTopology E] [MeasureTheory.SFinite μ],
  Measurable (MeasureTheory.charFun μ)
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.mulEquivToLimit_symm_continuous : ∀ {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],
  Continuous ⇑(InfiniteGalois.mulEquivToLimit k K).symm
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.continuous_snd : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M], Continuous TrivSqZeroExt.snd
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Copying a mono factorisation to another mono factorisation with propositionally equal
`m` and `e` fields.
 -/
CategoryTheory.Limits.MonoFactorisation.copy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.MonoFactorisation f) →
          (m : F.I ⟶ Y) →
            (e : X ⟶ F.I) →
              autoParam (m = F.m) CategoryTheory.Limits.MonoFactorisation.copy._auto_1 →
                autoParam (e = F.e) CategoryTheory.Limits.MonoFactorisation.copy._auto_3 →
                  CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Construct a term of `ProfiniteAddGrp` from a type endowed with the structure of a
compact and totally disconnected topological additive group.
(The condition of being Hausdorff can be omitted here because totally disconnected implies that
`{0}` is a closed set, thus implying Hausdorff in a topological additive group.)  -/
ProfiniteAddGrp.of : (G : Type u) →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] → [CompactSpace G] → [TotallyDisconnectedSpace G] → ProfiniteAddGrp.{u}
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₂.sizeOf_spec : ∀ (a : Turing.PartrecToTM2.Cont'), sizeOf a.cons₂ = 1 + sizeOf a
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_pnat_eq_tsum_of_eq_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  f 0 = 0 → ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mk.injEq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (pt : C₃) (inl : (F.obj Y₁).obj X₂ ⟶ pt) (inr : (F.obj X₁).obj Y₂ ⟶ pt)
  (isPushout : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr) (ι : pt ⟶ (F.obj Y₁).obj Y₂)
  (inl_ι :
    autoParam (CategoryTheory.CategoryStruct.comp inl ι = (F.obj Y₁).map f₂)
      CategoryTheory.Functor.PushoutObjObj.inl_ι._autoParam)
  (inr_ι :
    autoParam (CategoryTheory.CategoryStruct.comp inr ι = (F.map f₁).app Y₂)
      CategoryTheory.Functor.PushoutObjObj.inr_ι._autoParam)
  (pt_1 : C₃) (inl_1 : (F.obj Y₁).obj X₂ ⟶ pt_1) (inr_1 : (F.obj X₁).obj Y₂ ⟶ pt_1)
  (isPushout_1 : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl_1 inr_1)
  (ι_1 : pt_1 ⟶ (F.obj Y₁).obj Y₂)
  (inl_ι_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inl_1 ι_1 = (F.obj Y₁).map f₂)
      CategoryTheory.Functor.PushoutObjObj.inl_ι._autoParam)
  (inr_ι_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inr_1 ι_1 = (F.map f₁).app Y₂)
      CategoryTheory.Functor.PushoutObjObj.inr_ι._autoParam),
  ({ pt := pt, inl := inl, inr := inr, isPushout := isPushout, ι := ι, inl_ι := inl_ι, inr_ι := inr_ι } =
      { pt := pt_1, inl := inl_1, inr := inr_1, isPushout := isPushout_1, ι := ι_1, inl_ι := inl_ι_1,
        inr_ι := inr_ι_1 }) =
    (pt = pt_1 ∧ inl ≍ inl_1 ∧ inr ≍ inr_1 ∧ ι ≍ ι_1)
-- Init.Data.Option.Lemmas
Option.isSome_pfilter_iff_get : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).isSome = true ↔ ∃ (h : o.isSome = true), p (o.get h) ⋯ = true
-- Mathlib.Topology.Category.LightProfinite.Basic
instFaithfulLightDiagramProfiniteLightDiagramToProfinite : lightDiagramToProfinite.Faithful
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_mk_comp_iff_of_compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] {f : X → Y},
  Continuous (⇑(CompactCoherentification.mk Y) ∘ f) ↔ Continuous f
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero'_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (a : A) (ha : a = 0) (X : C),
  (CategoryTheory.Functor.CommShift.isoZero' F A a ha).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero' D a ha).hom.app (F.obj X))
      (F.map ((CategoryTheory.shiftFunctorZero' C a ha).inv.app X))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app : ∀ {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 α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  (M : SheafOfModules R),
  (SheafOfModules.toSheaf R).map ((PresheafOfModules.sheafificationAdjunction α).counit.app M) =
    (CategoryTheory.sheafificationAdjunction J AddCommGrpCat).counit.app ((SheafOfModules.toSheaf R).obj M)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_meet_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.join P (Lean.Order.meet Q R) = Lean.Order.meet (Lean.Order.join P Q) (Lean.Order.join P R)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedEmbedding : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] =>
    Topology.IsClosedEmbedding).RespectsIso
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Intermediate stage of assembling the unit.  -/
CategoryTheory.OverPresheafAux.unitAuxAuxAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (η : F ⟶ A) →
        (X : C) →
          CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X ≅
            F.obj (Opposite.op X)
-- Lean.Elab.BuiltinNotation
/-- Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))`  -/
Lean.Elab.Term.mkPPairs : Array Lean.Term → Lean.MacroM Lean.Term