mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
infDist_smul₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] {c : 𝕜}, c ≠ 0 → ∀ (s : Set E) (x : E), Metric.infDist (c • x) (c • s) = ‖c‖ * Metric.infDist x s
-- Mathlib.SetTheory.ZFC.PSet
/-- Two pre-sets are equivalent iff they have the same members.  -/
PSet.Equiv.eq : ∀ {x y : PSet.{u_1}}, x.Equiv y ↔ x.toSet = y.toSet
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.HashSet.ofList l).get? k = none
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instUnionOfBEqOfHashable : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Union (Std.DHashMap.Raw α β)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `map₂` of the identity is the identity.  -/
CategoryTheory.StructuredArrow.map₂IdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {R : CategoryTheory.Functor C D} →
          (T : D) →
            (α : T ⟶ (CategoryTheory.Functor.id D).obj T) →
              (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R) →
                autoParam (α = CategoryTheory.CategoryStruct.id T) CategoryTheory.StructuredArrow.map₂IdIso._auto_1 →
                  autoParam (β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)
                      CategoryTheory.StructuredArrow.map₂IdIso._auto_3 →
                    (CategoryTheory.StructuredArrow.map₂ α β ≅
                      CategoryTheory.Functor.id (CategoryTheory.StructuredArrow T R))
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_add : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (x y : CentroidHom α), (x + y).toEnd = x.toEnd + y.toEnd
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.δ_objMk₁_of_lt : ∀ {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : j.castSucc < i),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (SSet.stdSimplex.obj { len := 1 }) j))
      (SSet.stdSimplex.objMk₁ i) =
    SSet.stdSimplex.objMk₁ (i.pred ⋯)
-- Mathlib.Analysis.Normed.Group.Basic
toReal_enorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), ‖x‖ₑ.toReal = ‖x‖
-- Mathlib.Data.ZMod.Basic
pow_zmod_val_inv_pow : ∀ {α : Type u_1} [inst : Group α] {n : ℕ}, (Nat.card α).gcd n = 1 → ∀ (a : α), (a ^ (↑n)⁻¹.val) ^ n = a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.natCast_le_toENat : ∀ {c : Cardinal.{u}} {n : ℕ}, ↑n ≤ Cardinal.toENat c ↔ ↑n ≤ c
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_neg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β], b₁ < b₂ → a < 0 → a • b₂ < a • b₁
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_decl_eq : ∀ {expr : Std.Tactic.BVDecide.BVLogicalExpr} (idx : ℕ) (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (h : idx < aig.decls.size)
  (hbounds : idx < (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig.decls.size),
  (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig.decls[idx] = aig.decls[idx]
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.map_finite_effectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [F.PreservesFiniteEffectiveEpiFamilies] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B)
  [CategoryTheory.EffectiveEpiFamily X π], CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
-- Mathlib.Data.Set.Function
Set.InjOn.comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : α → β} {g : β → γ},
  Set.InjOn f s → (Set.InjOn (g ∘ f) s ↔ Set.InjOn g (f '' s))
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanImportClosureParams.mk.inj : ∀ {importClosure importClosure_1 : Array Lean.Lsp.DocumentUri},
  { importClosure := importClosure } = { importClosure := importClosure_1 } → importClosure = importClosure_1
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `F` and `H` are finite such that `ker(G →* H) ≤ im(F →* G)`, then `G` is finite.  -/
Group.fintypeOfKerLeRange : {F : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Group F] →
        [inst_1 : Group G] →
          [inst_2 : Group H] → [Fintype F] → [Fintype H] → (f : F →* G) → (g : G →* H) → g.ker ≤ f.range → Fintype G
-- Init.Data.Nat.Gcd
Nat.gcd_self_sub_left : ∀ {m n : ℕ}, n ≤ m → (m - n).gcd m = n.gcd m
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_succ_iff_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  ¬IsMax a → ¬IsMax b → (Order.succ a ≤ Order.succ b ↔ a ≤ b)
-- Mathlib.Computability.EpsilonNFA
εNFA.mem_evalFrom_iff_exists_path : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s₁ s₂ : σ} {x : List α},
  s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.liftBaseChange_range_le : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  (LinearMap.liftBaseChange T (Algebra.Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range ≤
    (Algebra.Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
-- Mathlib.Order.Filter.AtTopBot.Archimedean
/-- See also `Filter.Tendsto.atTop_mul_const_of_neg` for a version of this lemma for
linearly ordered fields which does not require the `Archimedean` assumption.  -/
Filter.Tendsto.atTop_mul_const_of_neg' : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : Ring R] [inst_1 : LinearOrder R]
  [IsStrictOrderedRing R] [Archimedean R],
  r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atBot
-- Mathlib.Order.Filter.Defs
Filter.mem_comk : ∀ {α : Type u_1} {p : Set α → Prop} {he : p ∅} {hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s}
  {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)} {s : Set α}, s ∈ Filter.comk p he hmono hunion ↔ p sᶜ
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.ofReal_tsum_of_nonneg : ∀ {α : Type u_1} {f : α → ℝ},
  (∀ (n : α), 0 ≤ f n) → Summable f → ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.bot_def : ∀ {M : Type u_1} [inst : AddZeroClass M], ⊥ = ⊥.saturation
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          (toNonUnitalSubsemiring : NonUnitalSubsemiring A) →
            (∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier) →
              NonUnitalSubalgebra R A
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
LowerSemicontinuous.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f g : α → γ},
  LowerSemicontinuous f → LowerSemicontinuous g → LowerSemicontinuous fun z => f z + g z
-- Init.System.IO
/-- Returns metadata for the indicated file without following symlinks. Throws an exception if the file
does not exist or the metadata cannot be accessed.
 -/
System.FilePath.symlinkMetadata : System.FilePath → IO IO.FS.Metadata
-- Mathlib.Probability.Density
MeasureTheory.pdf.eq_1 : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E),
  MeasureTheory.pdf X ℙ μ = (MeasureTheory.Measure.map X ℙ).rnDeriv μ
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.mk.injEq : ∀ {α : Type u_1} (E : Set α) (IsBase Indep : Set α → Prop) (indep_iff' : ∀ ⦃I : Set α⦄, Indep I ↔ ∃ B, IsBase B ∧ I ⊆ B)
  (exists_isBase : ∃ B, IsBase B) (isBase_exchange : Matroid.ExchangeProperty IsBase)
  (maximality : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E)
  (E_1 : Set α) (IsBase_1 Indep_1 : Set α → Prop) (indep_iff'_1 : ∀ ⦃I : Set α⦄, Indep_1 I ↔ ∃ B, IsBase_1 B ∧ I ⊆ B)
  (exists_isBase_1 : ∃ B, IsBase_1 B) (isBase_exchange_1 : Matroid.ExchangeProperty IsBase_1)
  (maximality_1 : ∀ X ⊆ E_1, Matroid.ExistsMaximalSubsetProperty Indep_1 X)
  (subset_ground_1 : ∀ (B : Set α), IsBase_1 B → B ⊆ E_1),
  ({ E := E, IsBase := IsBase, Indep := Indep, indep_iff' := indep_iff', exists_isBase := exists_isBase,
        isBase_exchange := isBase_exchange, maximality := maximality, subset_ground := subset_ground } =
      { E := E_1, IsBase := IsBase_1, Indep := Indep_1, indep_iff' := indep_iff'_1, exists_isBase := exists_isBase_1,
        isBase_exchange := isBase_exchange_1, maximality := maximality_1, subset_ground := subset_ground_1 }) =
    (E = E_1 ∧ IsBase = IsBase_1 ∧ Indep = Indep_1)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.id_comp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q), f.comp (RootPairing.Equiv.id P) = f
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.merge.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Option α → Sort u_2) →
    (x x_1 : Option α) →
      (Unit → motive none none) →
        ((x : α) → motive (some x) none) →
          ((y : α) → motive none (some y)) → ((x y : α) → motive (some x) (some y)) → motive x x_1
-- Init.Data.SInt.Bitwise
Int8.not_ne_self : ∀ {a : Int8}, ~~~a ≠ a
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.power_nat_eq : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.aleph0 ≤ c → 1 ≤ n → c ^ n = c
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.mk.sizeOf_spec : ∀ (builderId ref : Lean.Name) (args : List Lean.DataValue),
  sizeOf { builderId := builderId, ref := ref, args := args } = 1 + sizeOf builderId + sizeOf ref + sizeOf args
-- Lean.Elab.DefView
/-- Snapshot after processing of a definition body.   -/
Lean.Elab.BodyProcessedSnapshot : Type
-- Mathlib.Algebra.Group.Action.Basic
AddAction.injective : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α), Function.Injective fun x => g +ᵥ x
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.pullSub_nil : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)), Descriptive.Tree.pullSub T [] = T
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₁ → (m₁ ∩ m₂)[k]! = default
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.getElem?_toList_eq : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  r.toList[i]? =
    Option.filter (fun x => decide (x ≤ r.upper)) (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = false ↔ ∃ a, a ∈ m)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_setOfPred_modeq_one : ∀ {m : ℕ}, schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹
-- Mathlib.Data.ENat.Lattice
/-- A version of `iInf_mul` with a slightly more general hypothesis.  -/
ENat.iInf_mul' : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, (a = 0 → Nonempty ι) → (⨅ i, f i) * a = ⨅ i, f i * a
-- Mathlib.Topology.Algebra.Order.Module
instContinuousSMulSubtypeLeOfNat : ∀ {R : Type u_1} {α : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : SMul R α]
  [inst_3 : TopologicalSpace α] [inst_4 : TopologicalSpace R] [ContinuousSMul R α], ContinuousSMul { r // 0 ≤ r } α
-- Batteries.Data.Array.Lemmas
Array.toList_drop : ∀ {α : Type u_1} (as : Array α) (n : ℕ), (as.drop n).toList = List.drop n as.toList
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.select.sizeOf_spec : ∀ (finished : Std.Async.Waiter (Option Std.Http.Chunk)),
  sizeOf (Std.Http.Body.Channel.Consumer.select✝ finished) = 1 + sizeOf finished
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.zero_prod_zero : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃],
  ContinuousMultilinearMap.prod 0 0 = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.map f t).isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- `U.power α` identifies to the product of copies of `U` indexed by `α`.  -/
CategoryTheory.Limits.FormalCoproduct.isLimitPowerFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Limits.FormalCoproduct C) →
      (α : Type) →
        [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] → CategoryTheory.Limits.IsLimit (U.powerFan α)
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrangeRestrict_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N),
  Function.Surjective ⇑f.mrangeRestrict
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.differentiableWithinAt : ∀ {𝕜 : Type u} [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} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → n ≠ 0 → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.aestronglyMeasurable_condExpL2 : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)),
  MeasureTheory.AEStronglyMeasurable (↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) f)) μ
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_subset_Ioo_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α} [DenselyOrdered α],
  a₁ < b₁ → (Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- Every object is a module over a monoid object via the trivial action.  -/
CategoryTheory.ModObj.trivialAction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (M : C) → [inst_2 : CategoryTheory.MonObj M] → (X : C) → CategoryTheory.ModObj M X
-- Init.Data.Nat.Basic
Nat.min_def : ∀ {n m : ℕ}, min n m = if n ≤ m then n else m
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.sectionsMap_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (s : M.sections),
  SheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.id M) s = s
-- Mathlib.Analysis.RCLike.Basic
RCLike.smul_re : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (z : K), RCLike.re (r • z) = r * RCLike.re z
-- Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
/-- The limit of the number of nonzero integral ideals of norm `≤ s` in a fixed class `C` of the
class group divided by `s` when `s → +∞`.
 -/
NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (C : ClassGroup (NumberField.RingOfIntegers K)),
  Filter.Tendsto (fun s => ↑(Nat.card { I // ↑(Ideal.absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s) Filter.atTop
    (nhds
      (2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          NumberField.Units.regulator K /
        (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|)))
-- Mathlib.Analysis.Normed.Module.Basic
ULift.normedSpace : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [NormedSpace 𝕜 E] → NormedSpace 𝕜 (ULift.{u_6, u_3} E)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_iInf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Sort u_4}
  (S : ι → Submodule R M), -⨅ i, S i = ⨅ i, -S i
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexAddEquiv_trans_reindexAddEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11)
  [inst : Add R] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n''),
  (Matrix.reindexAddEquiv R e₁ e₂).trans (Matrix.reindexAddEquiv R e₁' e₂') =
    Matrix.reindexAddEquiv R (e₁.trans e₁') (e₂.trans e₂')
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
/-- Verify that the pushout cocone is indeed the colimit.  -/
CommAlgCat.binaryCofanIsColimit : {R : Type u} → [inst : CommRing R] → (A B : CommAlgCat R) → CategoryTheory.Limits.IsColimit (A.binaryCofan B)
-- Batteries.Tactic.GeneralizeProofs
/-- Mapping from propositions to an fvar in the local context with that type.  -/
Batteries.Tactic.GeneralizeProofs.GState.propToFVar : Batteries.Tactic.GeneralizeProofs.GState → Lean.ExprMap Lean.Expr
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Context for the `OmegaM` monad, containing the user configurable options.  -/
Lean.Elab.Tactic.Omega.Context : Type
-- Lean.Elab.Tactic.Try
/-- Given a `grind` tactic syntax `tac`, sets its parameters using `params`.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.setGrindParams : Lean.TSyntax `tactic → Array (Lean.TSyntax `Lean.Parser.Tactic.grindParam) → Lean.TSyntax `tactic
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.id_naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.Lax.StrongTrans.id F).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G], (tateComplexFunctor R G).Additive
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- `AlgebraNormClass F R S` states that `F` is a type of `R`-algebra norms on the ring `S`.
You should extend this class when you extend `AlgebraNorm`.  -/
AlgebraNormClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    [inst : SeminormedCommRing R] →
      (S : outParam (Type u_3)) → [inst_1 : Ring S] → [Algebra R S] → [FunLike F S ℝ] → Prop
-- Init.Data.Vector.Lemmas
Vector.allM_toArray : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Vector α n},
  Array.allM p xs.toArray = Vector.allM p xs
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupport.mk : Lean.Lsp.CodeActionLiteralSupportValueSet → Lean.Lsp.CodeActionLiteralSupport
-- Mathlib.Probability.Kernel.Category.Stoch
instPositiveCategoryStoch : CategoryTheory.PositiveCategory Stoch
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- The canonical isomorphism `(S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S]` for `B = S ⊗[R] A`.
Also see `KaehlerDifferential.tensorKaehlerEquiv` for the version with `B ⊗[A] Ω[A⁄R]`.  -/
KaehlerDifferential.tensorKaehlerEquivBase : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [h : Algebra.IsPushout R S A B] → TensorProduct R S Ω[A⁄R] ≃ₗ[S] Ω[B⁄S]
-- Std.Time.Time.HourMarker
Std.Time.instOrdHourMarker : Ord Std.Time.HourMarker
-- Init.Data.Option.Lemmas
Option.merge_eq_none_iff : ∀ {α : Type u_1} {f : α → α → α} {o o' : Option α}, Option.merge f o o' = none ↔ o = none ∧ o' = none
-- Lean.Expr
/-- Total order on `Expr` literal values.
Natural number values are smaller than string literal values.
 -/
Lean.Literal.lt : Lean.Literal → Lean.Literal → Bool
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          (toSubsemiring : Subsemiring A) → (∀ (r : R), (algebraMap R A) r ∈ toSubsemiring.carrier) → Subalgebra R A
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication by `one` on the right is the identity  -/
DirectSum.GSemiring.mul_one : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A] (a : GradedMonoid A), a * 1 = a