mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A}
  (hg : ∀ (m : M), g m ∈ I) (p : MvPolynomial (ℕ × M) R),
  (DividedPowerAlgebra.lift hI g hg) ↑p = (MvPolynomial.aeval fun nm => hI.dpow nm.1 (g nm.2)) p
-- Lean.Data.KVMap
Lean.instToStringDataValue : ToString Lean.DataValue
-- Init.Prelude
Lean.Macro.Context.mk : Lean.Macro.MethodsRef → Lean.Name → Lean.MacroScope → ℕ → ℕ → Lean.Syntax → Lean.Macro.Context
-- Mathlib.Geometry.Manifold.Instances.Real
instTopologicalSpaceEuclideanHalfSpace : (n : ℕ) → [inst : NeZero n] → TopologicalSpace (EuclideanHalfSpace n)
-- Mathlib.Order.Interval.Finset.Box
Finset.zero_mem_box : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : LocallyFiniteOrder α] {n : ℕ}
  [inst_4 : DecidableEq α], 0 ∈ Finset.box n ↔ n = 0
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs : ∀ {F : Type u_1} [inst : Field F] {v w : AbsoluteValue F ℝ},
  v.IsEquiv w → Topology.IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
-- Init.Data.Range.Polymorphic.RangeIterator
/-- The pure function mapping a range iterator of type `IterM` to the next step of the iterator.

This function is prefixed with `Monadic` in order to disambiguate it from the version for iterators
of type `Iter`.
 -/
Std.Rxi.Iterator.Monadic.step : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.IterM Id α → Std.IterStep (Std.IterM Id α) α
-- Mathlib.MeasureTheory.Group.Measure
/-- We shorten this from `measure_preimage_mul_left`, since left invariant is the preferred option
for measures in this formalization.  -/
MeasureTheory.measure_preimage_mul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulLeftInvariant] (g : G) (A : Set G), μ ((fun h => g * h) ⁻¹' A) = μ A
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Mul β] → [ContinuousMul β] → Mul C(α, β)
-- Mathlib.Order.Basic
Prod.mk_le_mk_iff_right : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b₁ b₂ : β},
  (a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂
-- Init.Data.Array.Zip
Array.map_uncurry_zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β},
  Array.map (Function.uncurry f) (as.zip bs) = Array.zipWith f as bs
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The chromatic number of an acyclic graph (forest) is at most 2.  -/
SimpleGraph.IsAcyclic.chromaticNumber_le_two : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → G.chromaticNumber ≤ 2
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_coprod : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderBinaryCoproducts] (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  P X → P Y → P (X ⨿ Y)
-- Mathlib.Data.Set.Inclusion
Set.inclusion_lt_inclusion : ∀ {α : Type u_1} [inst : LT α] {s t : Set α} (h : s ⊆ t) {x y : ↑s}, Set.inclusion h x < Set.inclusion h y ↔ x < y
-- Mathlib.Topology.Sheaves.Points
/-- Given a topological space `X` and `x : X`, this is the point of the site
`(Opens X, Opens.grothendieckTopology X)` corresponding to `x`.  -/
Opens.pointGrothendieckTopology : {X : Type u} → [inst : TopologicalSpace X] → X → (Opens.grothendieckTopology X).Point
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.maxDegree_eq_zero_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.maxDegree = 0 ↔ G = ⊥
-- Mathlib.Data.FP.Basic
FP.nextDnPos : [C : FP.FloatCfg] → (e : ℤ) → (m : ℕ) → FP.ValidFinite e m → FP.Float
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : α → ℝ},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => ↑(f x)) μ
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_sUnion : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] (S : Set (Set M)),
  ProperCone.dual p (⋃₀ S) = sInf (ProperCone.dual p '' S)
-- Mathlib.Topology.Category.UniformSpace
/-- The underlying `UniformContinuous` function.  -/
UniformSpaceCat.Hom.hom' : {X : UniformSpaceCat} → {Y : UniformSpaceCat} → X.Hom Y → { f // UniformContinuous f }
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.self_comp_symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.comp f.symm = FirstOrder.Language.Equiv.refl L N
-- Init.Data.Format.Basic
/-- Concatenates the given list after appending the given suffix to each element.

The list items are formatting using `ToFormat.format`.
 -/
Std.Format.joinSuffix : {α : Type u} → [Std.ToFormat α] → List α → Std.Format → Std.Format
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstSubNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.FieldTheory.Fixed
Subring.mk.congr_simp : ∀ {R : Type u} [inst : NonAssocRing R] (toSubsemiring toSubsemiring_1 : Subsemiring R)
  (e_toSubsemiring : toSubsemiring = toSubsemiring_1)
  (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier),
  { toSubsemiring := toSubsemiring, neg_mem' := neg_mem' } = { toSubsemiring := toSubsemiring_1, neg_mem' := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tendsto_sum_nat_add : ∀ (f : ℕ → ENNReal), ∑' (i : ℕ), f i ≠ ⊤ → Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_mem_nhds_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {U : Set E} [(nhdsWithin 0 {0}ᶜ).NeBot],
  U ∈ nhds 0 → balancedCore 𝕜 U ∈ nhds 0
-- Batteries.Data.List.Lemmas
List.getElem_mk : ∀ {α : Type u_1} {xs : List α} {i : ℕ} (h : i < xs.length), { toList := xs }[i] = xs[i]
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_μ : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.AddMon C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.AddMon.forget C) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_zero_beq : ∀ (a : BitVec 1), (!0#1 == a) = (a == 1#1)
-- Mathlib.Control.EquivFunctor
/-- `map` is functorial on equivalences.  -/
EquivFunctor.map_trans' : ∀ {f : Type u₀ → Type u₁} [self : EquivFunctor f] {α β γ : Type u₀} (k : α ≃ β) (h : β ≃ γ),
  EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_diagonal_left : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : Zero α]
  [inst_1 : Zero γ] [inst_2 : DecidableEq l] (f : α → β → γ),
  (∀ (b : β), f 0 b = 0) →
    ∀ (a : l → α) (B : Matrix m n β),
      Matrix.kroneckerMap f (Matrix.diagonal a) B =
        (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l))
          (Matrix.blockDiagonal fun i => B.map fun b => f (a i) b)
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_ker : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (K : AddSubgroup G) (f : G →+ G'),
  f.ker.relIndex K = Nat.card ↥(AddSubgroup.map f K)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The permutation representation of the automorphism group on the root index set  -/
RootPairing.Equiv.indexHom : {ι : 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] → (P : RootPairing ι R M N) → P.Aut →* ι ≃ ι
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
/-- A `1`-cocycle from `B` to `X` obtained as the boundary of
the `0`-cochain `cochain₀ sq hsq` consisting of the degreewise liftings.
This is refined below as a `1`-cocycle from `Q` to `K` where `Q` is a
cokernel of `i : A ⟶ B` and `K` a kernel of `p : X ⟶ Y` (see `cocycle₁`).  -/
CochainComplex.Lifting.cocycle₁' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B X Y : CochainComplex C ℤ} →
        {t : A ⟶ X} →
          {i : A ⟶ B} →
            {p : X ⟶ Y} →
              {b : B ⟶ Y} →
                (sq : CategoryTheory.CommSq t i p b) →
                  ((n : ℤ) → ⋯.LiftStruct) → CochainComplex.HomComplex.Cocycle B X 1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.eq_of_subset_isBase : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → B₁ ⊆ B₂ → B₁ = B₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany!_list_equiv_foldl : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ : Std.DTreeMap.Internal.Impl α fun x => β} {l : List (α × β)},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t₁ l)).Equiv
    (List.foldl (fun acc p => Std.DTreeMap.Internal.Impl.insert! p.1 p.2 acc) t₁ l)
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  IsOpen s → Set.EqOn f g s → (CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_tensorUnit_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv h)
-- Mathlib.RingTheory.WittVector.WittPolynomial
wittPolynomial.eq_1 : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] (n : ℕ),
  wittPolynomial p R n = ∑ i ∈ Finset.range (n + 1), (MvPolynomial.monomial fun₀ | i => p ^ (n - i)) (↑p ^ i)
-- Mathlib.CategoryTheory.Elements
/-- A natural transformation between functors induces a functor between the categories of elements.
 -/
CategoryTheory.CategoryOfElements.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₁ F₂ : CategoryTheory.Functor C (Type w)} → (F₁ ⟶ F₂) → CategoryTheory.Functor F₁.Elements F₂.Elements
-- Mathlib.Computability.RecursiveIn
ComputableIn.const : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {O : Set (ℕ →. ℕ)} (s : σ),
  ComputableIn O fun x => s
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- "Generalized" `nonneg`. `nonnegg c d x y` means `a √c + b √d ≥ 0`;
we are interested in the case `c = 1` but this is more symmetric  -/
Zsqrtd.Nonnegg : ℕ → ℕ → ℤ → ℤ → Prop
-- Lean.Meta.Tactic.Intro
Lean.Meta.introNCore : Lean.MVarId → ℕ → List Lean.Name → Bool → Bool → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
and `f'` is monotone on the interior, then `f` is convex on `D`.  -/
MonotoneOn.convexOn_of_deriv : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D → DifferentiableOn ℝ f (interior D) → MonotoneOn (deriv f) (interior D) → ConvexOn ℝ D f
-- Mathlib.Data.Nat.Log
Nat.log_eq_log_succ_iff : ∀ {b n : ℕ}, 1 < b → n ≠ 0 → (Nat.log b n = Nat.log b (n + 1) ↔ b ^ Nat.log b (n + 1) ≠ n + 1)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_piecewise : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (x y : Π₀ (i : ι), β i) (s : Set ι)
  [inst_1 : (i : ι) → Decidable (i ∈ s)], ⇑(x.piecewise y s) = s.piecewise ⇑x ⇑y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.ext_get_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C C' : G.EdgeLabeling K},
  C = C' ↔ ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_of_variation_apply_eq_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (f : X → E)
  {s : Set X}, μ.variation s = 0 → ∫ᵛ (x : X) in s, f x ∂[B; μ] = 0
-- Init.Data.Vector.Lemmas
Vector.getElem?_append_left : ∀ {α : Type u_1} {n m i : ℕ} {xs : Vector α n} {ys : Vector α m}, i < n → (xs ++ ys)[i]? = xs[i]?
-- Mathlib.Tactic.Core
/-- Make `nm` protected.  -/
Lean.setProtected : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → m Unit
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.instMulSemiringActionGalSplittingField : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → MulSemiringAction p.Gal p.SplittingField
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.FG : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K]
  {E : Type u_2} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace K E] [FiniteDimensional K E] [ProperSpace E]
  (L : Submodule ℤ E) [inst_9 : DiscreteTopology ↥L] [hs : IsZLattice K L], L.FG
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueData_J : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), I.glueData.J = ↑X.affineOpens
-- Mathlib.Data.Holor
/-- The CP rank of a holor `x`: the smallest N such that
`x` can be written as the sum of N holors of rank at most 1.  -/
Holor.cprank : {α : Type} → {ds : List ℕ} → [Ring α] → Holor α ds → ℕ
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.mk.sizeOf_spec : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] [inst_8 : SizeOf R] [inst_9 : SizeOf L] [inst_10 : SizeOf M]
  [inst_11 : SizeOf N] (toLinearMap : M →ₗ[R] N)
  (map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆),
  sizeOf { toLinearMap := toLinearMap, map_lie' := map_lie' } = 1 + sizeOf toLinearMap
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.smul_of : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} [inst : SMul R A] (r : R) (f : Matrix m n A),
  r • CStarMatrix.ofMatrix f = CStarMatrix.ofMatrix (r • f)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.singleton_le : ∀ {α : Type u_1} {a : α} {s : Multiset α}, {a} ≤ s ↔ a ∈ s
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_dvd : ∀ {G : Type u} [inst : AddMonoid G] {n : ℕ}, AddMonoid.exponent G ∣ n ↔ ∀ (g : G), addOrderOf g ∣ n
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, `M'` and `N'` are submodules of `M` and `N`,
respectively, such that `N` and `M'` are flat, then `M'` and `N'` are also linearly disjoint.  -/
Submodule.LinearDisjoint.of_le_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ {M' N' : Submodule R S}, M' ≤ M → N' ≤ N → ∀ [Module.Flat R ↥N] [Module.Flat R ↥M'], M'.LinearDisjoint N'
-- Lean.Parser.Command
Lean.Parser.Command.addDocString.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofLift.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (X : Type u) (of : X → G)
  (lift : {H : Type u} → [inst_1 : AddGroup H] → (X → H) ≃ (G →+ H))
  (lift_of : ∀ {H : Type u} [inst_1 : AddGroup H] (f : X → H) (a : X), (lift f) (of a) = f a),
  FreeAddGroupBasis.ofLift X of lift lift_of =
    { repr := ((FreeAddGroup.lift of).toAddEquiv (lift FreeAddGroup.of) ⋯ ⋯).symm }
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- Any graph on `n` vertices has at most `n.choose 2` edges.  -/
SimpleGraph.card_edgeFinset_le_card_choose_two : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet] [inst_1 : Fintype V],
  G.edgeFinset.card ≤ (Fintype.card V).choose 2
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.coe_comp : ∀ {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_mono : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G},
  (interior U).Nonempty →
    ∀ {K₁ K₂ : TopologicalSpace.Compacts G},
      ↑K₁ ⊆ K₂.carrier → MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂
-- Mathlib.Data.Set.Function
Function.Semiconj.injOn_preimage : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → ∀ {s : Set β}, Set.InjOn fb s → Set.InjOn f (f ⁻¹' s) → Set.InjOn fa (f ⁻¹' s)
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_im_le : ∀ (r : ℝ), Convex ℝ {c | c.im ≤ r}
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂ : CategoryTheory.Nerve.nerveFunctor₂.Faithful
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofFin : ∀ {n : Fin UInt32.size}, (UInt32.ofFin n).toUSize = USize.ofNatLT ↑n ⋯
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termHatβ_1 : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.markdown.injEq : ∀ (markup markup_1 : Lean.Lsp.MarkupContent),
  (Lean.Lsp.InlayHintTooltip.markdown markup = Lean.Lsp.InlayHintTooltip.markdown markup_1) = (markup = markup_1)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_image : ∀ {s : Set Ordinal.{u}}, BddAbove s → ∀ (f : Ordinal.{u} → Ordinal.{max u v}), BddAbove (f '' s)
-- Mathlib.Algebra.Field.Subfield.Basic
Field.fg_iff : ∀ (L : Type v) [inst : DivisionRing L], Field.FG L ↔ ∃ S, Subfield.closure ↑S = ⊤
-- Mathlib.Algebra.Ring.Pi
Pi.nonUnitalCommSemiring : {I : Type u} → {f : I → Type v} → [(i : I) → NonUnitalCommSemiring (f i)] → NonUnitalCommSemiring ((i : I) → f i)
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_div_self : ∀ {E : Type u_4} [inst : SeminormedCommGroup E] (x : E), Filter.Tendsto (fun a => ‖a / x‖) (nhds x) (nhds 0)
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.isTopCompl_of_proj : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M} {f : M →L[R] ↥p}, (∀ (x : ↥p), f ↑x = x) → Submodule.IsTopCompl p (↑f).ker
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensorFreeLEquiv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (α : Type u) [inst_2 : DecidableEq α]
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.free k G α)).ρ.Coinvariants),
  (A.coinvariantsTensorFreeToFinsupp α) x = (A.coinvariantsTensorFreeToFinsupp α) x
-- Mathlib.LinearAlgebra.Matrix.PosDef
QuadraticForm.posDef_toMatrix' : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)},
  QuadraticMap.PosDef Q → Q.toMatrix'.PosDef
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_ofNat : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (k : ℕ)
  [inst_3 : k.AtLeastTwo], (OfNat.ofNat k).charpoly = (Polynomial.X - OfNat.ofNat k) ^ Fintype.card n
-- Mathlib.Topology.Order.ProjIcc
ContinuousAt.IccExtend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LinearOrder α] {a b : α} {h : a ≤ b}
  [inst_1 : TopologicalSpace α] [OrderTopology α] [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] {x : γ}
  (f : γ → ↑(Set.Icc a b) → β) {g : γ → α},
  ContinuousAt ↿f (x, Set.projIcc a b h (g x)) →
    ContinuousAt g x → ContinuousAt (fun a_1 => Set.IccExtend h (f a_1) (g a_1)) x
-- Mathlib.Algebra.AddConstMap.Basic
/-- The identity map as `G →+c[a, a] G`.  -/
AddConstMap.id : {G : Type u_1} → [inst : Add G] → {a : G} → AddConstMap G G a a
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)]
  [Algebra ℚ 𝕜] (n : ℕ) [NeZero n], IsAddQuotientCoveringMap (fun x => n • x) ↥(nsmulAddMonoidHom n).ker
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.isSpecial_iff : ∀ (u : PNat.XgcdType), u.IsSpecial ↔ u.IsSpecial'
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bfamilyOfFamily_typein : ∀ {α : Type u_1} {ι : Type u_3} (f : ι → α) (i : ι),
  Ordinal.bfamilyOfFamily f ((Ordinal.typein WellOrderingRel).toRelEmbedding i) ⋯ = f i
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_inf : ∀ {V : Type u_1} (v : V) [inst : DecidableEq V] {G₁ G₂ : SimpleGraph V} [inst_1 : Fintype ↑((G₁ ⊓ G₂).neighborSet v)]
  [inst_2 : Fintype ↑(G₁.neighborSet v)] [inst_3 : Fintype ↑(G₂.neighborSet v)],
  (G₁ ⊓ G₂).neighborFinset v = G₁.neighborFinset v ∩ G₂.neighborFinset v
-- Init.SimpLemmas
Lean.arrow_congr : ∀ {p₁ p₂ : Sort u} {q₁ q₂ : Sort v}, p₁ = p₂ → q₁ = q₂ → Lean.Arrow p₁ q₁ = Lean.Arrow p₂ q₂
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The localization of a subring at a prime, as a local subring.
Also see `Localization.subalgebra.ofField`  -/
LocalSubring.ofPrime : {K : Type u_3} → [inst : Field K] → (A : Subring K) → (P : Ideal ↥A) → [P.IsPrime] → LocalSubring K
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.ofEq.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (k' : α) (v' v'_1 : β k'),
  v' = v'_1 →
    ∀ (hcmp : ∀ [Std.OrientedOrd α], k k' = Ordering.eq),
      Std.DTreeMap.Internal.Cell.ofEq k' v' hcmp = Std.DTreeMap.Internal.Cell.ofEq k' v'_1 hcmp
-- Init.Data.Nat.ToString
Nat.underscore_not_in_toDigits : ∀ {n : ℕ}, '_' ∉ Nat.toDigits 10 n
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The prime spectrum of a commutative semiring has discrete Zariski topology iff it is finite and
the semiring has Krull dimension zero or is trivial.  -/
PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero : ∀ {R : Type u} [inst : CommSemiring R],
  DiscreteTopology (PrimeSpectrum R) ↔ Finite (PrimeSpectrum R) ∧ Ring.KrullDimLE 0 R
-- Mathlib.Order.Filter.Defs
/-- The infimum of filters is the filter generated by intersections
of elements of the two filters.  -/
Filter.instInf : {α : Type u_1} → Min (Filter α)