mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_eq_one_iff_eq : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η] {a : α},
  (κ a).AbsolutelyContinuous (η a) → ((∀ᵐ (b : γ) ∂η a, κ.rnDeriv η a b = 1) ↔ κ a = η a)
-- Mathlib.Algebra.Module.FinitePresentation
/-- A finitely presented module is isomorphic to the quotient of a finite free module by a finitely
generated submodule.  -/
Module.FinitePresentation.equiv_quotient : ∀ (R : Type u) (M : Type u_1) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M] [Small.{v, u} R], ∃ L x x_1 K x_2, Module.Free R L ∧ Module.Finite R L ∧ K.FG
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.find?_string_eq_find?_toSlice : ∀ {pat : String} {s : String.Slice}, s.find? pat = s.find? pat.toSlice
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.assoc : {R : Type u} →
  [inst : Rack R] → (a b c : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R ((a.mul b).mul c) (a.mul (b.mul c))
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.ext_iff : ∀ {R : Type u_2} {inst : CommRing R} {n : ℕ} {x y : ChevalleyThm.PolynomialC.InductionObj✝ R n},
  x = y ↔ ChevalleyThm.PolynomialC.InductionObj.val✝ x = ChevalleyThm.PolynomialC.InductionObj.val✝ y
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_add_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a + x) '' Set.uIcc b c = Set.uIcc (a + b) (a + c)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k a : α} {v : β k},
  (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ k ∉ m then k else m.getKey! a
-- Mathlib.Algebra.Lie.Rank
/-- Let `x` be an element of a Lie algebra `L` over `R`, and write `n` for `rank R L`.
Then `x` is *regular*
if the `n`-th coefficient of the characteristic polynomial of `ad R L x` is non-zero.  -/
LieAlgebra.IsRegular : (R : Type u_1) →
  {L : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → [Module.Finite R L] → [Module.Free R L] → L → Prop
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMonoid.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid Y],
  LocallyConstant.instMonoid = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_incl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C],
  (Φ.transfiniteCompositionOfShapeιIteration J).incl = (Φ.iterationCocone J).ι
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm_X : ∀ {A : Type u_1} [inst : SeminormedRing A] [NormOneClass A], Polynomial.X.supNorm = 1
-- Init.Data.ByteArray.Basic
ByteArray.foldlM.loop : {β : Type v} →
  {m : Type v → Type w} →
    [Monad m] → (β → UInt8 → m β) → (as : ByteArray) → (stop : ℕ) → stop ≤ as.size → ℕ → ℕ → β → m β
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwLemma.mk.injEq : ∀ (name : Mathlib.Tactic.ClickSuggestions.Premise) (symm : Bool) (relName : Lean.Name)
  (name_1 : Mathlib.Tactic.ClickSuggestions.Premise) (symm_1 : Bool) (relName_1 : Lean.Name),
  ({ name := name, symm := symm, relName := relName } = { name := name_1, symm := symm_1, relName := relName_1 }) =
    (name = name_1 ∧ symm = symm_1 ∧ relName = relName_1)
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.summable : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ {f : (i : α) → E i}, Memℓp f p → Summable fun i => ‖f i‖ ^ p.toReal
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_I : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], RCLike.sqrt RCLike.I = ↑√2⁻¹ * (1 - RCLike.I) * RCLike.I
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.skipPrefix?_string_eq_skipPrefix?_toSlice : ∀ {pat : String} {s : String.Slice}, s.skipPrefix? pat = s.skipPrefix? pat.toSlice
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_toMonoidHom : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N), ⇑e.toMonoidHom = ⇑e
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- Adjoining a single element is compact in the lattice of intermediate fields.  -/
IntermediateField.adjoin_simple_isCompactElement : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (x : E),
  IsCompactElement F⟮x⟯
-- Mathlib.GroupTheory.Commutator.Basic
instNormalAddCommutator : ∀ (G : Type u_1) [inst : AddGroup G], (addCommutator G).Normal
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.range_swap : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H], (AddMonoid.Coprod.swap G H).range = ⊤
-- Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
/-- A `forget₂ C D` forgetful functor between concrete categories `C` and `D`
where `forget C` reflects isomorphisms, itself reflects isomorphisms.  -/
CategoryTheory.reflectsIsomorphisms_forget₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type t₁)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] (D : Type u_2) [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  {FD : outParam (D → D → Type t₂)} {CD : outParam (D → Type w)}
  [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : CategoryTheory.HasForget₂ C D] [(CategoryTheory.forget C).ReflectsIsomorphisms],
  (CategoryTheory.forget₂ C D).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- The zero pseudoelement is the class of a zero morphism.  -/
CategoryTheory.Abelian.Pseudoelement.pseudoZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → {P : C} → CategoryTheory.Abelian.Pseudoelement P
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_eq_zero_of_lt : ∀ {n k : ℕ}, n < k → n.stirlingSecond k = 0
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Y : CategoryTheory.Abelian.SpectralObject C EInt) [Y.IsFirstQuadrant],
  Y.HasSpectralSequence CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat
-- Std.Http.Data.Body.Stream
/-- Receives the next chunk, stopping at EOF or (in `ContextAsync`) when the context is cancelled.
 -/
Std.Http.Body.Stream.NextChunk.nextChunk : {m : Type → Type} → [self : Std.Http.Body.Stream.NextChunk m] → Std.Http.Body.Stream → m (Option Std.Http.Chunk)
-- Lean.Linter.Init
Lean.Linter.LinterSetsState.localEntries : Lean.Linter.LinterSetsState → Array (Lean.Name × Lean.NameSet)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getKeyLT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.le_inducedOuterMeasure : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  {μ : MeasureTheory.OuterMeasure α},
  μ ≤ MeasureTheory.inducedOuterMeasure m P0 m0 ↔ ∀ (s : Set α) (hs : P s), μ s ≤ m s hs
-- Init.System.IO
IO.TaskState.waiting.sizeOf_spec : sizeOf IO.TaskState.waiting = 1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.Hom.ext : ∀ {A B : ProfiniteGrp.{u}} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.elabAbelNFConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.Abel.AbelNF.Config
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_fill : ∀ {w i : ℕ} {v : Bool}, (BitVec.fill w v).getLsbD i = (v && decide (i < w))
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- Construct a product of `n` elements of the module within the tensor algebra.

See also `PiTensorProduct.tprod`.  -/
TensorAlgebra.tprod : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_2) →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (n : ℕ) → MultilinearMap R (fun x => M) (TensorAlgebra R M)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_nnrpow_two : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  CFC.abs a ^ 2 = star a * a
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n d : ℕ} (h : d ∣ n), (DirichletCharacter.changeLevel h) 1 = 1
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞} {c : M'},
  ContMDiff I I' n fun x => c
-- Std.Http.Server.Connection
Std.Http.Server.RemoteAddr.mk.inj : ∀ {addr addr_1 : Std.Net.SocketAddress}, { addr := addr } = { addr := addr_1 } → addr = addr_1
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.add_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M}, Continuous f → ∀ (b : M), Continuous fun x => f x + b
-- Mathlib.Algebra.Homology.ExactSequence
/-- The (exact) short complex consisting of maps `S.map' i j` and `S.map' j k` when we know
that `S : ComposableArrows C n` is exact.  -/
CategoryTheory.ComposableArrows.Exact.sc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S : CategoryTheory.ComposableArrows C n} →
          S.Exact →
            (i j k : ℕ) →
              autoParam (i + 1 = j) CategoryTheory.ComposableArrows.Exact.sc'._auto_1 →
                autoParam (j + 1 = k) CategoryTheory.ComposableArrows.Exact.sc'._auto_3 →
                  autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.sc'._auto_5 → CategoryTheory.ShortComplex C
-- Init.Data.SInt.Bitwise
Bool.toBitVec_toISize : ∀ {b : Bool}, b.toISize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)
-- Mathlib.RingTheory.SimpleModule.Isotypic
LinearEquiv.isIsotypic_iff : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (e : M ≃ₗ[R] N), IsIsotypic R M ↔ IsIsotypic R N
-- Mathlib.Data.Complex.BigOperators
Complex.ofReal_expect : ∀ {α : Type u_1} (s : Finset α) (f : α → ℝ), ↑(s.expect fun i => f i) = s.expect fun i => ↑(f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.baseChange_polynomial : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomial = (MvPolynomial.map ↑f) (W'.baseChange A).polynomial
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformlyOn_iff_restrict : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {K : Set α}, TendstoUniformlyOn F f p K ↔ TendstoUniformly (fun n => K.domRestrict (F n)) (K.domRestrict f) p
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
_private.Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric.0.Complex.tendsto_multiset_prod_div_add_one : ∀ (a : Multiset ℂ), Filter.Tendsto (fun n => (Multiset.map (fun x => x / ↑n + 1) a).prod) Filter.atTop (nhds 1)
-- Mathlib.Algebra.Ring.Defs
NonUnitalSemiring.mk : {α : Type u} →
  [toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring α] →
    (∀ (a b c : α), a * b * c = a * (b * c)) → NonUnitalSemiring α
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.coe_toUnitHom : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ),
  ↑(χ.toUnitHom a) = χ ↑a
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- A predicate singling out finite places among the absolute values on a number field `K`.  -/
NumberField.IsFinitePlace : {K : Type u_1} → [inst : Field K] → [NumberField K] → AbsoluteValue K ℝ → Prop
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The linear map version of `Function.Surjective.injective_comp_right`  -/
Function.Surjective.injective_linearMapComp_right : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₁ →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑g → Function.Injective fun f => f ∘ₛₗ g
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.workspace? : Lean.Lsp.ClientCapabilities → Option Lean.Lsp.WorkspaceClientCapabilities
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremWith_nat_int_rat_tfae : ∀ (n : ℕ), [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_uInt8ToNat : ∀ (n : UInt8), UInt16.ofNatLT n.toNat ⋯ = n.toUInt16
-- Batteries.Recycling.RBTree.Alter
/-- The property of a path returned by `t.zoom cut`. Each of the parents visited along the path have
the appropriate ordering relation to the cut.
 -/
RBTree.RBNode.Path.Zoomed : {α : Type u_1} → (α → Ordering) → RBTree.RBNode.Path α → Prop
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_mul_cancel_right : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x y : M₀), IsUnit x → y * Ring.inverse x * x = y
-- Batteries.Data.Stream
Std.Stream.take.eq_2 : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (n : ℕ),
  Std.Stream.take s n.succ =
    match Std.Stream.next? s with
    | none => ([], s)
    | some (a, s) =>
      match Std.Stream.take s n with
      | (as, s) => (a :: as, s)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.ofIso_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G' X : C} [inst_2 : CategoryTheory.AddGrpObj G'] (e : G' ≅ X),
  CategoryTheory.AddMonObj.zero = CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom
-- Mathlib.Topology.Order.LocalExtr
IsExtrOn.localize : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → IsLocalExtrOn f s a
-- Lean.Server.Snapshots
/-- Run a `TermElabM` computation using the data in the given snapshot. -/
Lean.Server.Snapshots.Snapshot.runTermElabM : {α : Type} → Lean.Server.Snapshots.Snapshot → Lean.Server.DocumentMeta → Lean.Elab.TermElabM α → EIO Lean.Exception α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for `OneHypercoverDenseData.essSurj.presheaf`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          {X Y : C} →
                            (X ⟶ Y) →
                              (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ Y ⟶
                                CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzOnWith.of_dist_le' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {s : Set α} {f : α → β} {K : ℝ},
  (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) → LipschitzOnWith K.toNNReal f s
-- Init.Data.Array.Zip
Array.getElem_zip : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {i : ℕ} {h : i < (as.zip bs).size},
  (as.zip bs)[i] = (as[i], bs[i])
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.trans_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {L : Type u_3} [inst_4 : Mul L] [inst_5 : TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (m : M),
  (e₁.trans e₂) m = e₂ (e₁ m)
-- Mathlib.Algebra.Category.Ring.FinitePresentation
/-- Given a filtered diagram `F` of rings over `R`, `S` an (essentially) of finite type `R`-algebra,
and two ring homs `a : S ⟶ Fᵢ` and `b : S ⟶ Fⱼ` over `R`.
If `a` and `b` agree at `S ⟶ colimit F`,
then there exists `k` such that `a` and `b` are equal at `S ⟶ F_k`.
In other words, the map `colimᵢ Hom_R(S, Fᵢ) ⟶ Hom_R(S, colim F)` is injective.
 -/
RingHom.EssFiniteType.exists_comp_map_eq_of_isColimit : ∀ {J : Type uJ} [inst : CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat)
  (F : CategoryTheory.Functor J CommRingCat) (α : (CategoryTheory.Functor.const J).obj R ⟶ F) {S : CommRingCat}
  (f : R ⟶ S) (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget CommRingCat)],
  (CommRingCat.Hom.hom f).EssFiniteType →
    ∀ {i : J} (a : S ⟶ F.obj i),
      CategoryTheory.CategoryStruct.comp f a = α.app i →
        ∀ {j : J} (b : S ⟶ F.obj j),
          CategoryTheory.CategoryStruct.comp f b = α.app j →
            CategoryTheory.CategoryStruct.comp a (c.ι.app i) = CategoryTheory.CategoryStruct.comp b (c.ι.app j) →
              ∃ k hik hjk,
                CategoryTheory.CategoryStruct.comp a (F.map hik) = CategoryTheory.CategoryStruct.comp b (F.map hjk)
-- Mathlib.Algebra.Category.Ring.Instances
IsLocalization.epi : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S))
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.eq_2 : ∀ {α : Type u_1} (xs : List α) (le : α → α → Bool), (xs = [] → False) → xs.merge [] le = xs
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
linear in both variables.  -/
CategoryTheory.Preadditive.comp_add : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (P Q R : C) (f : P ⟶ Q)
  (g g' : Q ⟶ R),
  CategoryTheory.CategoryStruct.comp f (g + g') =
    CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g'
-- Mathlib.NumberTheory.ModularForms.Cusps
CongruenceSubgroup.strictPeriods_Gamma : ∀ (N : ℕ),
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)).strictPeriods =
    AddSubgroup.zmultiples ↑N
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_inv : ∀ (Y : Type u_1) (X : Type u_2) [inst : TopologicalSpace Y],
  (CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap Y X).inv =
    TypeCat.ofHom fun f => { toFun := ⇑f, isLocallyConstant := ⋯ }
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.instLawfulMonadAttachExceptTOfLawfulMonad.match_2.eq_2 : ∀ {ε α : Type (max u_1 u_2)} {P : α → Prop} (motive : Except ε (Subtype P) → Sort u_3) (e : ε)
  (h_1 : (a : Subtype P) → motive (Except.ok a)) (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.CategoryTheory.Square
CategoryTheory.Functor.mapSquare_map_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (F.mapSquare.map φ).τ₁ = F.map φ.τ₁
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.tensorQuotientTensorEquiv_tmul : ∀ {R : Type u_1} {R' : Type u_2} {R'' : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing R']
  [inst_2 : CommRing R''] [inst_3 : CommRing S] [inst_4 : Algebra R R'] [inst_5 : Algebra R R'']
  [inst_6 : Algebra R' R''] [inst_7 : IsScalarTower R R' R''] [inst_8 : Algebra R S] (e : TensorProduct R R' S)
  (a : R'') (b : R') (c : S),
  (Algebra.tensorQuotientTensorEquiv R'' e) (a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (b ⊗ₜ[R] c)) =
    (Ideal.Quotient.mk (Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e}))
      ((a * (algebraMap R' R'') b) ⊗ₜ[R] c)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The natural transformation from identity functor on `R`-module to the composition of extension and
restriction of scalars.
 -/
ModuleCat.ExtendRestrictScalarsAdj.unit : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          CategoryTheory.Functor.id (ModuleCat R) ⟶ (ModuleCat.extendScalars f).comp (ModuleCat.restrictScalars f)
-- Mathlib.Topology.Bornology.Constructions
/-- **Alias** of the reverse direction of `boundedSpace_val_set_iff`. -/
Bornology.IsBounded.boundedSpace_val : ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, Bornology.IsBounded s → BoundedSpace ↑s
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.isIso_top_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C}, CategoryTheory.IsIso ⊤.arrow
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instFiniteResidueFieldOfQuotientIdeal : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] [Finite (R ⧸ I)], Finite I.ResidueField
-- Lean.Util.Trace
Lean.bombEmoji : String
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a division monoid under pointwise operations if `α` is.  -/
Filter.divisionMonoid : {α : Type u_2} → [DivisionMonoid α] → DivisionMonoid (Filter α)