mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- Each `X : FormalCoproduct.{w} C` is actually itself a coproduct of objects of the original
category (after coercion using `incl C`). This is the function that specifies the family for which
`X` is a coproduct of.  -/
CategoryTheory.Limits.FormalCoproduct.toFun : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.Limits.FormalCoproduct C) → X.I → CategoryTheory.Limits.FormalCoproduct C
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_pairwiseDisjoint_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) {a b : α},
  (∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b) →
    (Set.Iio (k + 1)).PairwiseDisjoint fun j =>
      Set.Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2
-- Mathlib.SetTheory.Ordinal.Basic
/-- `Ordinal.{u}` is the type of well orders in `Type u`, up to order isomorphism.  -/
Ordinal : Type (u + 1)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.inf_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousInf β] (f g : CompactlySupportedContinuousMap α β) (a : α),
  (f ⊓ g) a = f a ⊓ g a
-- Mathlib.Tactic.Simps.Basic
/-- Perform head-structure-eta-reduction on expression `e`. That is, if `e` is of the form
`⟨f.1, f.2, ..., f.n⟩` with `f` definitionally equal to `e`, then
`headStructureEtaReduce e = headStructureEtaReduce f` and `headStructureEtaReduce e = e` otherwise.
 -/
Simps.headStructureEtaReduce : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.instGroupWithZeroNonZeroDivisors : {R : Type u_1} →
  [inst : MonoidWithZero R] →
    [Nontrivial R] →
      [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)] →
        [NoZeroDivisors R] → GroupWithZero (OreLocalization (nonZeroDivisors R) R)
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instTransOrdOrdinal : Std.TransOrd Std.Time.Hour.Ordinal
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Reinterpret a `LinearIsometryEquiv` as an `IsometryEquiv`.  -/
LinearIsometryEquiv.toIsometryEquiv : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ᵢ E₂
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_comp_basis : ∀ {M : Type u_2} [inst : AddCommGroup M] {M' : Type u_3} [inst_1 : AddCommGroup M'] {ι : Type u_4}
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] {A : Type u_5} [inst_4 : CommRing A] [inst_5 : Module A M]
  [inst_6 : Module A M'] (b : Module.Basis ι A M) (b' : Module.Basis ι A M') (f : M →ₗ[A] M'),
  b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))
-- Lean.DocString.DeferredCheck
Lean.Doc.instBEqDeferredCheckSite.beq : Lean.Doc.DeferredCheckSite → Lean.Doc.DeferredCheckSite → Bool
-- Init.Grind.Norm
Lean.Grind.natCast_pow : ∀ (a b : ℕ), ↑(a ^ b) = ↑a ^ b
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- Send a function `f : V → E` to the function `f : V → Hom (W, E)` given by
`v ↦ (w ↦ -2 * π * I * L (v, w) • f v)`. This is designed so that the Fourier transform of
`fourierSMulRight L f` is the derivative of the Fourier transform of `f`.  -/
VectorFourier.fourierSMulRight : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      {V : Type u_2} →
        {W : Type u_3} →
          [inst_2 : NormedAddCommGroup V] →
            [inst_3 : NormedSpace ℝ V] →
              [inst_4 : NormedAddCommGroup W] →
                [inst_5 : NormedSpace ℝ W] → (V →L[ℝ] W →L[ℝ] ℝ) → (V → E) → V → W →L[ℝ] E
-- Mathlib.Algebra.Ring.Shrink
Shrink.instAddMonoidWithOne : {α : Type u_1} → [inst : Small.{v, u_1} α] → [AddMonoidWithOne α] → AddMonoidWithOne (Shrink.{v, u_1} α)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Reinterpret an `AffineIsometryEquiv` as an `IsometryEquiv`.  -/
AffineIsometryEquiv.toIsometryEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → P ≃ᵢ P₂
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.congr_inseparable_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι} {g : α → β},
  TendstoLocallyUniformlyOn F f p s → (∀ x ∈ s, Inseparable (f x) (g x)) → TendstoLocallyUniformlyOn F g p s
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits_comp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] {E : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E]
  [L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D] [L.Additive]
  (G : CategoryTheory.Functor D E),
  CategoryTheory.Limits.PreservesFiniteColimits (L.comp G) ↔ CategoryTheory.Limits.PreservesFiniteColimits G
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.method : Lean.Lsp.CompletionItemKind
-- Mathlib.RingTheory.Valuation.RamificationGroup
/-- The multiplicative action of the decomposition subgroup on `A`.  -/
ValuationSubring.decompositionSubgroupMulSemiringAction : (K : Type u_1) →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (A : ValuationSubring L) → MulSemiringAction ↥(ValuationSubring.decompositionSubgroup K A) ↥A
-- Mathlib.Algebra.Group.Invertible.Basic
invertibleEquivOfLeftInverse_symm_apply : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : FunLike F R S] [inst_3 : MonoidHomClass F R S] [inst_4 : FunLike G S R] [inst_5 : MonoidHomClass G S R]
  (f : F) (g : G) (r : R) (h : Function.LeftInverse ⇑g ⇑f) (x : Invertible r),
  (invertibleEquivOfLeftInverse f g r h).symm x = Invertible.map f r
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} {r : R},
  (MvPowerSeries.pderiv R i) (MvPowerSeries.C r) = 0
-- Mathlib.CategoryTheory.FintypeCat
/-- Construct a term of `FintypeCat` from a type endowed with a `Finite` instance.  -/
FintypeCat.of : (X : Type u_1) → [Finite X] → FintypeCat
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_inclusion : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E F : IntermediateField K L}
  (hEF : E ≤ F) (e : ↥E), ↑((IntermediateField.inclusion hEF) e) = ↑e
-- Std.Http.Data.Headers.Name
Std.Http.Header.instDecidableEqName : DecidableEq Std.Http.Header.Name
-- Mathlib.MeasureTheory.Function.EssSup
essInf.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] {x : MeasurableSpace α} (f : α → β)
  (μ : MeasureTheory.Measure α), essInf f μ = Filter.liminf f (MeasureTheory.ae μ)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
ProbabilityTheory.Kernel.comp_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel β γ) (μ : MeasureTheory.Measure β),
  κ.comp (ProbabilityTheory.Kernel.const α μ) = ProbabilityTheory.Kernel.const α (μ.bind ⇑κ)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.IsWeightedHomogeneous.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  (φ : MvPolynomial σ R) (m : M),
  MvPolynomial.IsWeightedHomogeneous w φ m = ∀ ⦃d : σ →₀ ℕ⦄, MvPolynomial.coeff d φ ≠ 0 → (Finsupp.weight w) d = m
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.hinv : ∀ (self : String.Slice.RevByteIterator), self.offset ≤ self.s.rawEndPos
-- Init.Data.Nat.Simproc
Nat.Simproc.add_sub_add_ge : ∀ (a c : ℕ) {b d : ℕ}, b ≥ d → a + b - (c + d) = a + (b - d) - c
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.select.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (P : ℕ → Prop) (x : WittVector p R),
  WittVector.select P x = WittVector.mk p fun n => if P n then x.coeff n else 0
-- Mathlib.Data.Option.Basic
Option.elim_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ → α → β} {x : α → β} {i : Option γ} {y : α},
  i.elim x f y = i.elim (x y) fun j => f j y
-- Mathlib.Computability.Primrec.Basic
Primrec.fin_val_iff : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ} {f : α → Fin n}, (Primrec fun a => ↑(f a)) ↔ Primrec f
-- Lean.Meta.Tactic.Intro
_private.Lean.Meta.Tactic.Intro.0.Lean.Meta.mkAuxNameImp : Bool → Bool → Bool → Lean.LocalContext → Lean.Name → Bool → List Lean.Name → Lean.MetaM (Lean.Name × List Lean.Name)
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.mk.sizeOf_spec : ∀ (numGoals nameLength replacementSize : ℕ) (name : String) (newGoals : Array Lean.Meta.AbstractMVarsResult),
  sizeOf
      { numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        newGoals := newGoals } =
    1 + sizeOf numGoals + sizeOf nameLength + sizeOf replacementSize + sizeOf name + sizeOf newGoals
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_coe_to_fun : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H), ⇑f.completion = UniformSpace.Completion.map ⇑f
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Array α → Sort u_2) (head : α) (xs : List α) (acc : Array α)
  (h_1 : (x : ℕ) → (x_1 : Array α) → motive [] x x_1)
  (h_2 : (head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc)
  (h_3 : (x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc),
  (match head :: xs, 0, acc with
    | [], x, x_1 => h_1 x x_1
    | head :: xs, 0, acc => h_2 head xs acc
    | x :: xs, n.succ, acc => h_3 x xs n acc) =
    h_2 head xs acc
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.ne_bot_of_prod_finsetApprox_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R] (J : Ideal S),
  (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ J → J ≠ ⊥
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.ofFinset_apply : ∀ {α : Type u_1} {f : α → ENNReal} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ a ∉ s, f a = 0) (a : α),
  (PMF.ofFinset f s h h') a = f a
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_right : ∀ (m n : ℕ), n.gcd (m * n) = n
-- Batteries.Data.List.Matcher
List.Matcher.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (toMatcher : Array.Matcher α) (pattern : List α),
  sizeOf { toMatcher := toMatcher, pattern := pattern } = 1 + sizeOf toMatcher + sizeOf pattern
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  r.toArray[i]? = Option.filter (fun x => decide (x < r.upper)) (Std.PRange.succMany? i r.lower)
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- If a composition is `nil`, the right component must be `nil`  -/
Quiver.Path.nil_of_comp_eq_nil_right : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} {p : Quiver.Path a b} {q : Quiver.Path b a},
  p.comp q = Quiver.Path.nil → q.length = 0
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_subsingleton : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], s.Subsingleton → Metric.diam s = 0
-- Lean.Message
Lean.MessageData.ofLevel : Lean.Level → Lean.MessageData
-- Init.Data.List.Range
List.range'_concat : ∀ {step s n : ℕ}, List.range' s (n + 1) step = List.range' s n step ++ [s + step * n]
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).hom =
    (CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯
          (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯
          ⋯).lift
      (CategoryTheory.Limits.limit.cone
        (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0))
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
/-- Any locally convex real or complex vector space is polynormable.  -/
LocallyConvexSpace.toPolynormableSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace 𝕜 E], PolynormableSpace 𝕜 E
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.ofList_nil : ∀ {α : Type u}, ↑[] = Stream'.WSeq.nil
-- Mathlib.Order.Interval.Set.Pi
/-- **Alias** of `Set.Icc_sdiff_pi_univ_Ioc_subset`.

---

If `x`, `y`, `z` are functions `Π i : ι, α i`, then
the set difference between the box `[x, z]` and the product of the intervals `(y i, z i]`
is covered by the union of the boxes `[x, update z i (y i)]`.

E.g., if `x = y`, then this lemma states that the difference between a closed box
`[x, y]` and the product of half-open intervals `{z | ∀ i, x i < z i ≤ y i}` is covered by the union
of the faces of `[x, y]` adjacent to `x`.  -/
Set.Icc_diff_pi_univ_Ioc_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)]
  (x y z : (i : ι) → α i),
  (Set.Icc x z \ Set.univ.pi fun i => Set.Ioc (y i) (z i)) ⊆ ⋃ i, Set.Icc x (Function.update z i (y i))
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_prime_pow : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n p : ℕ} [hp : Fact (Nat.Prime p)],
  ¬p ^ n • x = 0 → p ^ (n + 1) • x = 0 → addOrderOf x = p ^ (n + 1)
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    ∀ (j : Fin (n + 2)),
      j ≠ 0 →
        n + 2 ≤ ↑j + q →
          ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
            CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (X.δ j) h) =
              CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.instIsEquivalenceElemObjSmallCategoryOfSetFunctor : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C),
  h.functor.IsEquivalence
-- Mathlib.LinearAlgebra.Basis.SMul
/-- When the group in question is the automorphisms, `•` coincides with `Basis.map`.  -/
Module.Basis.smul_eq_map : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (g : M ≃ₗ[R] M) (b : Module.Basis ι R M), g • b = b.map g
-- Mathlib.Condensed.Discrete.Module
/-- `CondensedMod.LocallyConstant.functor` is left adjoint to the forgetful functor from condensed
`R`-modules to `R`-modules.
 -/
CondensedMod.LocallyConstant.adjunction : (R : Type (u + 1)) → [inst : Ring R] → CondensedMod.LocallyConstant.functor R ⊣ Condensed.underlying (ModuleCat R)
-- Batteries.Data.Char.AsciiCasing
Char.toUpper_eq_of_isLower : ∀ {c : Char}, c.isLower = true → c.toUpper = Char.ofNat (c.toNat - 32)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.int.sizeOf_spec : ∀ (i : ℤ), sizeOf (Lean.Lsp.DiagnosticCode.int i) = 1 + sizeOf i
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.subset_bot_iff : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {s : Set α},
  ChainCompletePartialOrder.IsAdmissible x f s →
    (s ⊆ ChainCompletePartialOrder.bot x f ↔ s = ChainCompletePartialOrder.bot x f)
-- Mathlib.MeasureTheory.SetSemiring
_private.Mathlib.MeasureTheory.SetSemiring.0.MeasureTheory.IsSetSemiring.exists_partition_disjointed : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)},
  MeasureTheory.IsSetSemiring C → ↑J ⊆ C → ∀ (j : ↥J), ∃ P, ↑P.parts ⊆ C
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_neg : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Neg (β i)] {x : Hamming β},
  Hamming.ofHamming (-x) = -Hamming.ofHamming x
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.one_def : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], 1 = ContinuousAlgHom.id R A
-- Mathlib.Init
/-- Define a set of linters that run once a week and get posted to Zulip.
 -/
linter.weeklyLintSet : Lean.Option Bool
-- Mathlib.Order.Filter.Extr
IsExtrFilter.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  IsExtrFilter f l a → f =ᶠ[l] g → f a = g a → IsExtrFilter g l a
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_subset : ∀ {M : Type u_1} {S T : Set M} [inst : Add M], S ⊆ T → T.addCentralizer ⊆ S.addCentralizer
-- Init.Data.SInt.Lemmas
ISize.toUSize_neg : ∀ (a : ISize), (-a).toUSize = -a.toUSize
-- Init.Data.List.Nat.Sum
List.sum_le_max_mul_length_of_max?_eq_some_nat : ∀ {x : ℕ} {xs : List ℕ}, xs.max? = some x → xs.sum ≤ x * xs.length
-- Mathlib.Combinatorics.Matroid.Circuit
/-- Fundamental circuits and cocircuits of a base `B` play dual roles;
`e` belongs to the fundamental cocircuit for `B` and `f` if and only if
`f` belongs to the fundamental circuit for `e` and `B`.
This statement isn't so reasonable unless `f ∈ B` and `e ∉ B`,
but holds due to junk values even without these assumptions.  -/
Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuit : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α}, M.IsBase B → (e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B)
-- Init.System.IO
/-- Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give
allocation-avoiding code additional “weight” and is also used to adjust the counter after resuming
from a snapshot.

Heartbeats are a means of implementing “deterministic” timeouts. The heartbeat counter is the number
of “small” memory allocations performed on the current execution thread.
 -/
IO.addHeartbeats : ℕ → BaseIO Unit
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_sdiff_singleton_one : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Set M), Submonoid.closure (s \ {1}) = Submonoid.closure s
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- **Alias** of `CategoryTheory.Triangulated.TStructure.isGE_of_ge`. -/
CategoryTheory.Triangulated.TStructure.isGE_of_GE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (p q : ℤ),
  autoParam (p ≤ q) CategoryTheory.Triangulated.TStructure.isGE_of_ge._auto_1 → ∀ [t.IsGE X q], t.IsGE X p
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- The state of one section of library search suggestions.
We use this for 4 kinds of suggestions: `rw`, `grw`, `apply` and `apply at`.  -/
Mathlib.Tactic.ClickSuggestions.SectionState : Type → Type
-- Mathlib.LinearAlgebra.TensorPower.Pairing
/-- The linear map from the tensor power of the dual to the dual of the tensor power.  -/
TensorPower.pairingDual : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (n : ℕ) → TensorPower R n (Module.Dual R M) →ₗ[R] Module.Dual R (TensorPower R n M)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- **The Third Isomorphism theorem** for rings. See `quotQuotEquivQuotSup` for a version
that does not assume an inclusion of ideals.  -/
DoubleQuot.quotQuotEquivQuotOfLE : {R : Type u} → [inst : CommRing R] → {I J : Ideal R} → I ≤ J → (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ J
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- A constructor for `DPMorphism` from a ring homomorphism `f : A →+* B` satisfying
`IsDPMorphism hI hJ f`.  -/
DividedPowers.DPMorphism.mk' : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} →
          {J : Ideal B} →
            {hI : DividedPowers I} → {hJ : DividedPowers J} → {f : A →+* B} → hI.IsDPMorphism hJ f → hI.DPMorphism hJ
-- Mathlib.Analysis.Fourier.Inversion
Real.tendsto_integral_cexp_sq_smul : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    Filter.Tendsto (fun c => ∫ (v : V), Complex.exp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v) Filter.atTop (nhds (∫ (v : V), f v))
-- Mathlib.Order.RelIso.Basic
RelEmbedding.mk : {α : Type u_5} →
  {β : Type u_6} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → (toEmbedding : α ↪ β) → (∀ {a b : α}, s (toEmbedding a) (toEmbedding b) ↔ r a b) → r ↪r s
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- See `intervalIntegrable_cpow'` for a version with a weaker hypothesis on `r`, but assuming the
measure is volume.  -/
intervalIntegral.intervalIntegrable_cpow : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℂ},
  0 ≤ r.re ∨ 0 ∉ Set.uIcc a b → IntervalIntegrable (fun x => ↑x ^ r) μ a b
-- Mathlib.Data.Fin.SuccPred
/-- Embedding a positive `Fin n` results in a positive `Fin (n + 1)`  -/
Fin.succAbove_pos : ∀ {n : ℕ} [inst : NeZero n] (p : Fin (n + 1)) (i : Fin n), 0 < i → 0 < p.succAbove i