mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveComp : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {E : Type u_4}
  [inst_5 : CategoryTheory.Category.{v_4, u_4} E] [inst_6 : CategoryTheory.Preadditive E]
  (G : CategoryTheory.Functor D E) [G.Additive], (F.comp G).Additive
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for monotonicity of multiplication by nonnegative elements on the left,
namely `a₁ ≤ a₂ → b * a₁ ≤ b * a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedRing`.  -/
PosMulMono : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.differentiableAt_log_log : ∀ {x : ℝ}, x ≠ 0 → x ≠ 1 → x ≠ -1 → DifferentiableAt ℝ (fun x => Real.log (Real.log x)) x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastSub.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.BinaryRefVec w → Sort u_1) →
            (input : aig.BinaryRefVec w) → ((lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }) → motive input
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.RecurringRule.mk.inj : ∀ {stdName : String} {stdOffset : Std.Time.TimeZone.Offset} {dst : Option Std.Time.TimeZone.DaylightSavingRule}
  {stdName_1 : String} {stdOffset_1 : Std.Time.TimeZone.Offset} {dst_1 : Option Std.Time.TimeZone.DaylightSavingRule},
  { stdName := stdName, stdOffset := stdOffset, dst := dst } =
      { stdName := stdName_1, stdOffset := stdOffset_1, dst := dst_1 } →
    stdName = stdName_1 ∧ stdOffset = stdOffset_1 ∧ dst = dst_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.iff_seq_eq_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)},
  ms.IsZero ↔ ms.seq = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Data.Multiset.Bind
Multiset.filterMap_eq_bind : ∀ {α : Type u_1} {β : Type v} (m : Multiset α) (f : α → Option β),
  Multiset.filterMap f m = m.bind fun a => (Option.map singleton (f a)).getD 0
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.vecMulVec_eq : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (ι : Type u_6) [inst : Mul α] [inst_1 : AddCommMonoid α]
  [inst_2 : Unique ι] (w : m → α) (v : n → α), Matrix.vecMulVec w v = Matrix.replicateCol ι w * Matrix.replicateRow ι v
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- Given a graded ring `A` and a map `f : A →+* Γ(X, ⊤)` such that the image of the
irrelevant ideal under `f` generates the whole ring, we can construct a map `X ⟶ Proj 𝒜`.  -/
AlgebraicGeometry.Proj.fromOfGlobalSections : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              {X : AlgebraicGeometry.Scheme} →
                (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) →
                  Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤ → (X ⟶ AlgebraicGeometry.Proj 𝒜)
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toBoundedOrder : {α : Type u} → [h : BooleanAlgebra α] → BoundedOrder α
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeIndOfHasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange] [CategoryTheory.Limits.HasPushouts C], P.ind.IsStableUnderCobaseChange
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.top_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring S),
  ⊤.prod s = Subsemiring.comap (RingHom.snd R S) s
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.isHaarMeasure_inducedMeasure : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B], (H.inducedMeasure μA μC).IsHaarMeasure
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_div_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α}, (s / t).card ≤ s.card * t.card
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.generalizeVars : Lean.MVarId → Lean.Syntax → Array Lean.Expr → Lean.Expr → Lean.Elab.Tactic.TacticM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.RingTheory.DedekindDomain.Factorization
Ideal.emultiplicity_bot : ∀ {R : Type u_3} [inst : CommSemiring R] (I : Ideal R), emultiplicity I ⊥ = ⊤
-- Mathlib.Algebra.Group.Action.Defs
AddSemigroupAction.toVAdd : {G : Type u_9} → {P : Type u_10} → {inst : AddSemigroup G} → [self : AddSemigroupAction G P] → VAdd G P
-- Init.Grind.AC
Lean.Grind.AC.instInhabitedExpr : Inhabited Lean.Grind.AC.Expr
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  -/
«term_≃ₜ+_» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getCast? a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => none
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      if h : (k == a) = true then some (cast ⋯ v) else Std.DHashMap.Internal.AssocList.getCast? a es
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isBounded_iff_exists_ge : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} (c : ℝ),
  Bornology.IsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Exception that triggered the error.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.exception : Lean.Meta.RefinedDiscrTree.ImportFailure✝ → Lean.Exception
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- For some natural number `n`, the type `cell C m` is empty for all `m ≥ n`.  -/
Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell : ∀ {X : Type u} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.FiniteDimensional C],
  ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.restrictUnit : {B : Type u_1} → {M : CoxeterMatrix B} → {G : Type u_5} → [inst : Monoid G] → {f : B → G} → M.IsLiftable f → B → Gˣ
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.brecOn_1.go : {motive_1 : Lean.Meta.Match.Pattern → Sort u} →
  {motive_2 : List Lean.Meta.Match.Pattern → Sort u} →
    (t : List Lean.Meta.Match.Pattern) →
      ((t : Lean.Meta.Match.Pattern) → t.below → motive_1 t) →
        ((t : List Lean.Meta.Match.Pattern) → Lean.Meta.Match.Pattern.below_1 t → motive_2 t) →
          motive_2 t ×' Lean.Meta.Match.Pattern.below_1 t
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.transvection_mul_apply_of_ne : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n]
  {m : Type u_4} (a : n) (b : m), a ≠ i → ∀ (c : R) (M : Matrix n m R), (Matrix.transvection i j c * M) a b = M a b
-- Mathlib.LinearAlgebra.SModEq.Pow
SModEq.pow_mul_of_le : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} {p : ℕ},
  ↑p ∈ I → ∀ {x y : R}, x ≡ y [SMOD J] → J ≤ I → x ^ p ≡ y ^ p [SMOD J * I]
-- Mathlib.Algebra.Group.End
/-- The inclusion map of permutations on a subtype of `α` into permutations of `α`,
fixing the other points.  -/
Equiv.Perm.ofSubtype : {α : Type u_4} → {p : α → Prop} → [DecidablePred p] → Equiv.Perm (Subtype p) →* Equiv.Perm α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical fiber”
`{a} × t`, `a ∈ s`, and is Lipschitz continuous on each “horizontal fiber” `s × {b}`, `b ∈ t`
with the same Lipschitz constant `K`. Then it is continuous on `s × t`.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space.  -/
continuousOn_prod_of_continuousOn_lipschitzOnWith : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal),
  (∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t) →
    (∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) → ContinuousOn f (s ×ˢ t)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
IsSelfAdjoint.log : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A}, IsSelfAdjoint (CFC.log a)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone' : ∀ {α : Type u_2} (f : ℕ → α → ENNReal) (x : α), Monotone fun n => ⨆ k, ⨆ (_ : k ≤ n), f k x
-- Mathlib.Tactic.Ring.Common
/-- Defines how comparisons and binary equality are computed in the base type. These are separated
from RingCompute because they can often be defined without using instance caches.  -/
Mathlib.Tactic.Ring.Common.RingCompare : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Type
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsPreprimitive.toIsPretransitive : ∀ {G : Type u_1} {X : Type u_2} {inst : VAdd G X} [self : AddAction.IsPreprimitive G X], AddAction.IsPretransitive G X
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- A strictly unitary pseudofunctor (sometimes called a "normal homomorphism")
`F` between bicategories `B` and `C` is a pseudofunctor `F` from `B` to `C`
such that the structure isomorphism `map (𝟙 X) ≅ 𝟙 (F.obj X)` is in fact an
identity 2-isomorphism for every `X : B` (in particular, there is an equality
`F.map (𝟙 X) = 𝟙 (F.obj X)`).  -/
CategoryTheory.StrictlyUnitaryPseudofunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.Algebra.Field.ULift
ULift.divisionRing : {α : Type u} → [DivisionRing α] → DivisionRing (ULift.{u_1, u} α)
-- Mathlib.SetTheory.Cardinal.Defs
/-- The cardinal number of a type  -/
Cardinal.«term#_» : Lean.ParserDescr
-- Mathlib.Data.Matrix.Mul
/-- This instance enables use with `smul_mul_assoc`.  -/
Matrix.Semiring.isScalarTower : ∀ {n : Type u_3} {R : Type u_7} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  [inst_2 : Monoid R] [inst_3 : DistribMulAction R α] [IsScalarTower R α α],
  IsScalarTower R (Matrix n n α) (Matrix n n α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_zero_iff : ∀ {x : ℝ}, Real.arcsin x = 0 ↔ x = 0
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.subset_hom : ∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} (C : G.ComponentCompl L) (h : K ⊆ L),
  ↑C ⊆ ↑(SimpleGraph.ComponentCompl.hom h C)
-- Mathlib.Analysis.MeanInequalitiesPow
Real.add_rpow_le_rpow_add : ∀ {p a b : ℝ}, 0 ≤ a → 0 ≤ b → 1 ≤ p → a ^ p + b ^ p ≤ (a + b) ^ p
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : α → ε},
  0 ≤ q → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.eLpNorm' f q μ = 0 → f =ᵐ[μ] 0
-- Batteries.Data.List.Basic
List.replaceF_eq_replaceFTR : @List.replaceF = @List.replaceFTR
-- Mathlib.Topology.Instances.Irrational
Irrational.eventually_forall_le_dist_cast_div : ∀ {x : ℝ}, Irrational x → ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in nhds 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entry.mk.sizeOf_spec : ∀ (type : Lean.MessageData) (line : Option ℕ) (depth : ℕ) (status : Mathlib.Explode.Status) (thm : Lean.MessageData)
  (deps : List (Option ℕ)) (useAsDep : Bool),
  sizeOf
      { type := type, line := line, depth := depth, status := status, thm := thm, deps := deps, useAsDep := useAsDep } =
    1 + sizeOf type + sizeOf line + sizeOf depth + sizeOf status + sizeOf thm + sizeOf deps + sizeOf useAsDep
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target_subset_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), (extChartAt I x).target ⊆ Set.range ↑I
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {n : ℕ} [hσ : Finite σ] {p : Polynomial (MvPolynomial σ R)},
  ((MvPolynomial.optionEquivLeft R σ).symm p).IsHomogeneous n → ∀ (i j : ℕ), i + j = n → (p.coeff i).IsHomogeneous j
-- Mathlib.GroupTheory.Congruence.Hom
Con.lift.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (c : Con M) (f : M →* P)
  (H : c ≤ Con.ker f), c.lift f H = { toFun := fun x => Con.liftOn x ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.coe_kleinFour_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → ↑(alternatingGroup.kleinFour α) = {1} ∪ {g | (↑g).cycleType = {2, 2}}
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- A Gaussian measure has moments of all orders.
That is, the identity is in L^p for all finite `p`.  -/
ProbabilityTheory.IsGaussian.memLp_id : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [CompleteSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ]
  (p : ENNReal), p ≠ ⊤ → MeasureTheory.MemLp id p μ
-- Mathlib.Topology.Separation.Regular
Homeomorph.normalSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace X] (h : X ≃ₜ Y),
  NormalSpace Y
-- Init.Data.String.Basic
/-- Converts a string to a list of characters.

Since strings are represented as dynamic arrays of bytes containing the string encoded using
UTF-8, this operation takes time and space linear in the length of the string.

Examples:
 * `"abc".toList = ['a', 'b', 'c']`
 * `"".toList = []`
 * `"\n".toList = ['\n']`
 -/
String.toList : String → List Char
-- Mathlib.Data.Fintype.Card
/-- **Alias** of `Fintype.card_eq_zero`. -/
Fintype.card_of_isEmpty : ∀ {α : Type u_1} [inst : Fintype α] [IsEmpty α], Fintype.card α = 0
-- Mathlib.RingTheory.Noetherian.Basic
instIsNoetherianRingProd : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] [IsNoetherianRing R] [IsNoetherianRing S],
  IsNoetherianRing (R × S)
-- Mathlib.Topology.Algebra.Group.Basic
/-- If a subgroup of a topological group is commutative, then so is its topological closure.

See note [reducible non-instances].  -/
Subgroup.commGroupTopologicalClosure : {G : Type w} →
  [inst : TopologicalSpace G] →
    [inst_1 : Group G] →
      [inst_2 : IsTopologicalGroup G] →
        [T2Space G] → (s : Subgroup G) → (∀ (x y : ↥s), x * y = y * x) → CommGroup ↥s.topologicalClosure
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) (x : B'),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).mapId x).hom.iso = F.mapId x
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- The Hausdorff dimension of the orthogonal projection of a set `s` onto a subspace `K`
is less than or equal to the Hausdorff dimension of `s`.
 -/
dimH_orthogonalProjectionOnto_le : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (s : Set E), dimH (⇑K.orthogonalProjectionOnto '' s) ≤ dimH s
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The `R`-subalgebra of continuous maps `α → A`.  -/
continuousSubalgebra : {α : Type u_1} →
  [TopologicalSpace α] →
    {R : Type u_2} →
      [inst : CommSemiring R] →
        {A : Type u_3} →
          [inst_1 : TopologicalSpace A] →
            [inst_2 : Semiring A] → [inst_3 : Algebra R A] → [IsTopologicalSemiring A] → Subalgebra R (α → A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ [inst_1 : Inhabited α] {k k' : α} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getKey! k' =
        if compare k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the
norm.  -/
Subalgebra.seminormedRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} → [inst_1 : SeminormedRing E] → [inst_2 : Algebra 𝕜 E] → (s : Subalgebra 𝕜 E) → SeminormedRing ↥s
-- Mathlib.Analysis.Fourier.AddCircle
/-- For `n ≠ 0`, a translation by `T / 2 / n` negates the function `fourier n`.  -/
fourier_add_half_inv_index : ∀ {T : ℝ} {n : ℤ}, n ≠ 0 → 0 < T → ∀ (x : AddCircle T), (fourier n) (x + ↑(T / 2 / ↑n)) = -(fourier n) x
-- Std.Sat.AIG.CNF
/-- State extension is a reflexive relation.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.IsExtensionBy_rfl : ∀ {aig : Std.Sat.AIG ℕ} {idx : ℕ} {omega : idx < aig.decls.size} (state : Std.Sat.AIG.toCNF.State✝ aig)
  {h : idx < (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state)).size},
  (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state))[idx] = true →
    Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state state idx ⋯
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.isBounded_prod_iff_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  [inst_10 : StarOrderedRing A] (s : Set (WithCStarModule A (E × F))), Bornology.IsBounded s ↔ Bornology.IsBounded s
-- Mathlib.Order.Concept
Concept.mk.inj : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {extent : Set α} {intent : Set β}
  {upperPolar_extent : upperPolar r extent = intent} {lowerPolar_intent : lowerPolar r intent = extent}
  {extent_1 : Set α} {intent_1 : Set β} {upperPolar_extent_1 : upperPolar r extent_1 = intent_1}
  {lowerPolar_intent_1 : lowerPolar r intent_1 = extent_1},
  { extent := extent, intent := intent, upperPolar_extent := upperPolar_extent,
        lowerPolar_intent := lowerPolar_intent } =
      { extent := extent_1, intent := intent_1, upperPolar_extent := upperPolar_extent_1,
        lowerPolar_intent := lowerPolar_intent_1 } →
    extent = extent_1 ∧ intent = intent_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.coe_toAddSubsemigroup_apply : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), ↑(Subsemigroup.toAddSubsemigroup S) = ⇑Additive.toMul ⁻¹' ↑S
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_map' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (F : CategoryTheory.Functor J C)
  {E₁ E₂ : CategoryTheory.Functor K J} (α : E₁ ⟶ E₂),
  CategoryTheory.Limits.colimit.pre F E₁ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Functor.whiskerRight α F))
      (CategoryTheory.Limits.colimit.pre F E₂)
-- Init.Data.Rat.Basic
/-- The absolute value of a rational number `a` is `a` if `a ≥ 0` and `-a` if `a ≤ 0`.  -/
Rat.abs : ℚ → ℚ
-- Mathlib.Order.Birkhoff
/-- **Birkhoff Representation for finite distributive lattices**. Any nonempty finite distributive
lattice is isomorphic to the lattice of lower sets of its sup-irreducible elements.  -/
OrderIso.lowerSetSupIrred : {α : Type u_1} →
  [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → [OrderBot α] → α ≃o LowerSet { a // SupIrred a }
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofOptionInfo : Lean.Elab.OptionInfo → Lean.Elab.Info
-- Lean.Compiler.IR.Basic
/-- Full application.  -/
Lean.IR.Expr.fap : Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
-- Lean.Elab.ConfigEval.Types
_private.Lean.Elab.ConfigEval.Types.0.Lean.Elab.ConfigEval.ReflectConfigItems.mk : {α : Type} →
  (α → Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.configItem)) →
    Lean.Elab.ConfigEval.ReflectConfigItems✝ α
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.η_inv_app_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : ChainComplex C ℕ) (i : ℕ),
  (CategoryTheory.Idempotents.DoldKan.η.inv.app X).f i =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.hom.app X).f i)
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map
            (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)).f
        i)
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ x⁻¹ * y` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_inv_mul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [ν.IsMulLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1⁻¹ * p.2) (μ.prod ν) ν
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
`Submonoid`.  -/
nonZeroDivisorsRight : (M₀ : Type u_1) → [inst : MonoidWithZero M₀] → Submonoid M₀