mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C}
  (toColimitPresentation : CategoryTheory.Limits.ColimitPresentation J X)
  (prop_diag_obj : ∀ (j : J), P (toColimitPresentation.diag.obj j))
  (toColimitPresentation_1 : CategoryTheory.Limits.ColimitPresentation J X)
  (prop_diag_obj_1 : ∀ (j : J), P (toColimitPresentation_1.diag.obj j)),
  ({ toColimitPresentation := toColimitPresentation, prop_diag_obj := prop_diag_obj } =
      { toColimitPresentation := toColimitPresentation_1, prop_diag_obj := prop_diag_obj_1 }) =
    (toColimitPresentation = toColimitPresentation_1)
-- Mathlib.Data.PFun
PFun.res.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), PFun.res f s = (↑f).restrict ⋯
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
rootsOfUnitytoCircle.congr_simp : ∀ (n : ℕ) [inst : NeZero n], rootsOfUnitytoCircle n = rootsOfUnitytoCircle n
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBase_of_forall_insert : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.Indep B → (∀ e ∈ M.E \ B, ¬M.Indep (insert e B)) → M.IsBase B
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.toPlots_sInf : ∀ {X : Type u_1} {D : Set (DiffeologicalSpace X)}, (sInf D).toPlots = ⋂ d ∈ D, d.toPlots
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.mem_split_iff' : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {i : ι} {x : ℝ},
  J ∈ BoxIntegral.Prepartition.split I i x ↔ ↑J = ↑I ∩ {y | y i ≤ x} ∨ ↑J = ↑I ∩ {y | x < y i}
-- Aesop.Nanos
Aesop.Nanos.instToJson : Lean.ToJson Aesop.Nanos
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.div_eq_const : ∀ {α : Type u_1} {a b : α} [inst : Div α], a = b → ∀ (c : α), a / c = b / c
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Qary entropy is strictly decreasing in the interval [1 - q⁻¹, 1].  -/
Real.qaryEntropy_strictAntiOn : ∀ {q : ℕ}, 2 ≤ q → StrictAntiOn (Real.qaryEntropy q) (Set.Icc (1 - 1 / ↑q) 1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α}
  [inst_3 : Inhabited (β a)] {c : ℕ}, (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).get! a = default
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mk_zero : ∀ {K : Type u_1} [inst : Field K], ⟨0, ⋯⟩ = 0
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace : {α : Type u_1} → [inst : TopologicalSpace α] → [CompactSpace α] → BoundedOrder (TopologicalSpace.Compacts α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_left_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C), (X.homologyData₀ R).left.K = (X.chainComplex R).X 0
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.types_tensorObj_def : ∀ {X Y : Type u}, CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = (X × Y)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- If the kernel of a linear map is disjoint from the span of a family of vectors,
then the family is linearly independent iff it is linearly independent after composing with
the linear map.  -/
LinearMap.linearIndependent_iff_of_disjoint : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M'] [inst_3 : Module R M] [inst_4 : Module R M'] {v : ι → M} (f : M →ₗ[R] M'),
  Disjoint (Submodule.span R (Set.range v)) f.ker → (LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v)
-- Mathlib.Algebra.GroupWithZero.Associated
unit_associated_one : ∀ {M : Type u_1} [inst : Monoid M] {u : Mˣ}, Associated (↑u) 1
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If `E : C ≌ D` is an equivalence and we have a `CommShift` structure on `E.functor`,
this constructs the unique compatible `CommShift` structure on `E.inverse`.
 -/
CategoryTheory.Equivalence.commShiftInverse : {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] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddGroup A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] → [E.functor.CommShift A] → E.inverse.CommShift A
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- `R` is integrally closed in `A` iff all integral elements of `A` are also elements of `R`.  -/
isIntegrallyClosedIn_iff : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  IsIntegrallyClosedIn R A ↔
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_norm_div : ∀ {E : Type u_5} [inst : SeminormedGroup E] (u v : E), ‖v‖ ≤ ‖u‖ + ‖u / v‖
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux.eq_1 : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g)
  (hg : Function.Surjective ⇑g) {k : ℕ} (hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range))
  (x : AdicCompletion.AdicCauchySequence I N) (hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤),
  AdicCompletion.mapExactAux✝ hf hfg hg hkn x hker Nat.zero = ⟨⋯.choose, ⋯⟩
-- Mathlib.Data.Fintype.Option
instFintypeOption : {α : Type u_3} → [Fintype α] → Fintype (Option α)
-- Mathlib.Analysis.Complex.Convex
Complex.rectangle_eq_convexHull : ∀ (z w : ℂ), z.Rectangle w = (convexHull ℝ) {z, ↑z.re + ↑w.im * Complex.I, ↑w.re + ↑z.im * Complex.I, w}
-- Mathlib.Order.Interval.Set.Image
StrictMono.mapsTo_Ioi : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictMono f → Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.ofRaw.sizeOf_spec : ∀ (val : ℕ), sizeOf { val := val } = 1 + sizeOf val
-- Init.Data.Fin.Basic
Fin.instInhabited : {n : ℕ} → [NeZero n] → Inhabited (Fin n)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.IsFiniteKernel.compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel η],
  ProbabilityTheory.IsFiniteKernel (κ.compProd η)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.IsPrincipal.iterate_lt`. -/
Ordinal.Principal.iterate_lt : ∀ {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  a < o → Ordinal.IsPrincipal op o → ∀ (n : ℕ), (op a)^[n] a < o
-- Std.Time.Time.PlainTime
/-- Subtracts milliseconds from a `PlainTime`.
 -/
Std.Time.PlainTime.subMilliseconds : Std.Time.PlainTime → Std.Time.Millisecond.Offset → Std.Time.PlainTime
-- Mathlib.Algebra.Ring.Equiv
/-- The "plain" equivalence of types underlying an equivalence of (semi)rings.  -/
RingEquiv.toEquiv : {R : Type u_7} →
  {S : Type u_8} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → R ≃+* S → R ≃ S
-- Batteries.Data.List.Basic
List.sigma.eq_1 : ∀ {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)),
  l₁.sigma l₂ = List.flatMap (fun a => List.map (Sigma.mk a) (l₂ a)) l₁
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  -/
TensorProduct.«term_⊗_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.Dioph
Dioph.xn_dioph : Dioph.DiophPFun fun v => { Dom := 1 < v (Fin2.ofNat' 0), get := fun h => Pell.xn h (v (Fin2.ofNat' 1)) }
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
le_comap_range_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N →ₗ[R] P) (q : Q),
  g.range ≤ Submodule.comap ((TensorProduct.mk R Q P) q) (LinearMap.lTensor Q g).range
-- Mathlib.Analysis.Normed.Module.Ball.Action
mulActionSphereSphere : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → MulAction ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.nest_ne_zero : ∀ {p : DyckWord}, p.nest ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.ext_iff : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {x y : SSet.Truncated.Edge x₀ x₁}, x = y ↔ x.edge = y.edge
-- Mathlib.Logic.Basic
cast_heq_iff_heq : ∀ {α β γ : Sort u_1} (e : α = β) (a : α) (c : γ), cast e a ≍ c ↔ a ≍ c
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_rotateR : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.rotateR x r).dual = r.dual.rotateL x l.dual
-- Mathlib.Analysis.Convex.Visible
/-- One cannot see any point of an open set.  -/
IsOpen.eq_of_isVisible_of_left_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] {s : Set V} {x y : V} [inst_5 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  [inst_7 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V],
  IsOpen s → IsVisible 𝕜 s x y → y ∈ s → x = y
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- Let `G` act on a space `X`. An `Equidecomposition` with respect to `X` and `G` is a partial
bijection `f : PartialEquiv X X` with the property that for some set `elements : Finset G`,
(which we record), for each `a ∈ f.source`, `f a` can be obtained by applying some `g ∈ elements`
instead. We call `f` an equidecomposition of `f.source` with `f.target`.

More familiarly, `f` is the result of partitioning `f.source` into finitely many pieces,
then applying a single element of `G` to each to get a partition of `f.target`.
 -/
Equidecomp : (X : Type u_1) → (G : Type u_2) → [SMul G X] → Type u_1
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.dropSuffix_string_eq_dropSuffix_toSlice : ∀ {pat : String} {s : String.Slice}, s.dropSuffix pat = s.dropSuffix pat.toSlice
-- Mathlib.Analysis.Normed.Group.NullSubmodule
mem_nullSubgroup_iff : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {x : M}, x ∈ nullSubgroup M ↔ ‖x‖ = 0
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instMonoid : (M : Type u_4) → [inst : MulOne M] → Monoid (Monoid.End M)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- A non-unital `k`-algebra homomorphism from `SkewMonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`.  -/
SkewMonoidAlgebra.nonUnitalAlgHom_ext : ∀ {k : Type u_1} {G : Type u_2} {A : Type u_6} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Monoid G]
  [inst_2 : Semiring k] [inst_3 : MulSemiringAction G k] [inst_4 : DistribMulAction k A]
  {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A},
  (∀ (x : G), φ₁ (SkewMonoidAlgebra.single x 1) = φ₂ (SkewMonoidAlgebra.single x 1)) → φ₁ = φ₂
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} [inst_2 : SizeOf J] [inst_3 : SizeOf C] (pt : C)
  (π : (CategoryTheory.Functor.const J).obj pt ⟶ F), sizeOf { pt := pt, π := π } = 1 + sizeOf pt + sizeOf π
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatInt32SintOfNatNat : Lean.Grind.ToInt.OfNat Int32 (Lean.Grind.IntInterval.sint 32)
-- Init.Data.Bool
Bool.cond_then_self : ∀ (c b : Bool), (bif c then c else b) = (c || b)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.two_opow_log_add : ∀ {o : Ordinal.{u_1}}, o ≠ 0 → 2 ^ Ordinal.log 2 o + o % 2 ^ Ordinal.log 2 o = o
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'_neg_mem : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w // w.IsComplex }),
  ∀ x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀, -x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psum_one : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.psum σ R 1 = ∑ i, MvPolynomial.X i
-- Mathlib.GroupTheory.Congruence.Opposite
Con.orderIsoOp_apply : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), Con.orderIsoOp c = c.op
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Copy of a non-unital subalgebra with a new `carrier` equal to the old one.
Useful to fix definitional equalities.  -/
NonUnitalSubalgebra.copy : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → (s : Set A) → s = ↑S → NonUnitalSubalgebra R A
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.nonempty_hom_of_preconnected_groupoid : ∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [CategoryTheory.IsPreconnected G] (x y : G), Nonempty (x ⟶ y)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- `f` is left homotopic to `g` iff `f - g` is left homotopic to `0`.  -/
CategoryTheory.Arrow.LeftHomotopy.equivSubZero : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f g : u ⟶ v} → CategoryTheory.Arrow.LeftHomotopy f g ≃ CategoryTheory.Arrow.LeftHomotopy (f - g) 0
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- Shortcut instance for commutative rings.  -/
Ideal.instHasQuotient_1 : {R : Type u_1} → [inst : CommRing R] → HasQuotient R (Ideal R)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.uniformCauchySeqOn_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Group G] [u : UniformSpace G] [inst_1 : IsTopologicalGroup G]
  (F : ι → α → G) (p : Filter ι) (s : Set α),
  IsTopologicalGroup.rightUniformSpace G = u →
    (UniformCauchySeqOn F p s ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a / F m.1 a ∈ u_1)
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.groupLift : {B : Type u_1} →
  {W : Type u_3} →
    [inst : Group W] →
      {M : CoxeterMatrix B} →
        CoxeterSystem M W → {G : Type u_5} → [inst_1 : Group G] → {f : B → G} → M.IsLiftable f → W →* G
-- Mathlib.Probability.Distributions.Uniform
PMF.toOuterMeasure_uniformOfFintype_apply : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] (s : Set α) [inst_2 : Fintype ↑s],
  (PMF.uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
-- Mathlib.Probability.Distributions.Gaussian.Basic
InnerProductSpace.toDualMap.eq_1 : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  InnerProductSpace.toDualMap 𝕜 E = { toLinearMap := ↑(innerSL 𝕜), norm_map' := ⋯ }
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.MonoOver F),
  (CategoryTheory.Subfunctor.equivalenceMonoOver F).inverse.obj X = CategoryTheory.Subfunctor.range X.arrow
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeriesBilinear.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : (x : ℕ) → motive x),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | x => h_4 x) =
    h_2 ()
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest merging adjacent `intro`-like tactics whose effect is equivalent to a single `intro`.  -/
Mathlib.TacticAnalysis.introMerge : Mathlib.TacticAnalysis.Config
-- Mathlib.RingTheory.Valuation.PrimeMultiplicity
/-- `multiplicity` of a prime in an integral domain as an additive valuation to `ℕ∞`.  -/
multiplicity_addValuation : {R : Type u_1} → [inst : CommRing R] → [IsDomain R] → {p : R} → Prime p → AddValuation R ℕ∞
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative
squares in `T`.  -/
CategoryTheory.Arrow : (T : Type u) → [CategoryTheory.Category.{v, u} T] → Type (max u v)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- In a manifold with `C^n` inverse away from `0`, the inverse is continuous away from `0`.
This is not an instance for technical reasons, see
note [Design choices about smooth algebraic structures].  -/
continuousInv₀_of_contMDiffInv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] [ContMDiffInv₀ I n G],
  ContinuousInv₀ G
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.lTensor_counit_comul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A), (LinearMap.lTensor A CoalgebraStruct.counit) (CoalgebraStruct.comul a) = a ⊗ₜ[R] 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      (m.insertMany l)[k]? =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if (a == k) = true then some b else none)
              l).or
          m[k]?
-- Mathlib.Data.List.ModifyLast
List.modifyLast.go.eq_1 : ∀ {α : Type u_1} (f : α → α) (a : Array α), List.modifyLast.go f [] a = []
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.BooleanAlgebra : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} →
      [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → BooleanAlgebra { P // IsLprojection X P }
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppLinarith : Lean.Meta.Grind.M✝ Unit
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.toLinearMap_restrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}
  {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (h : ∀ x ∈ p, f x ∈ q), ↑(f.restrict h) = (↑f).restrict h
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.instCountable : ∀ {α : Type u_1} {f : α → α}, Countable (IterateAddAct f)
-- Mathlib.Algebra.Module.Submodule.Range
AddMonoidHom.coe_toIntLinearMap_range : ∀ {M : Type u_10} {M₂ : Type u_11} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] (f : M →+ M₂),
  f.toIntLinearMap.range = AddSubgroup.toIntSubmodule f.range
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instOne.eq_1 : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : One β],
  BoundedContinuousFunction.instOne = { one := BoundedContinuousFunction.const α 1 }
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- Convert a `Partition n` to a member of `(Finset.Icc 1 n).finsuppAntidiag n`
(see `Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag` for the proof).
`p.toFinsuppAntidiag i` is defined as `i` times the number of occurrence of `i` in `p`.  -/
Nat.Partition.toFinsuppAntidiag : {n : ℕ} → n.Partition → ℕ →₀ ℕ
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.instHashableMatcherKey.hash : Lean.Meta.Match.MatcherKey✝ → UInt64
-- Mathlib.Tactic.NormNum.Ineq
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLE.core.intArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LE «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b →
            have e := q(«$a» ≤ «$b»);
            Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.BinaryRefVec.cast.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        {aig1 : Std.Sat.AIG α} →
          (motive : aig1.BinaryRefVec len → Sort u_1) →
            (s : aig1.BinaryRefVec len) → ((lhs rhs : aig1.RefVec len) → motive { lhs := lhs, rhs := rhs }) → motive s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey! k = default
-- Mathlib.Analysis.Analytic.CPolynomial
HasFiniteFPowerSeriesAt.neg : ∀ {𝕜 : 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 : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ},
  HasFiniteFPowerSeriesAt f pf x n → HasFiniteFPowerSeriesAt (-f) (-pf) x n
-- Mathlib.GroupTheory.Perm.List
List.zipWith_swap_prod_support' : ∀ {α : Type u_1} [inst : DecidableEq α] (l l' : List α),
  {x | (List.zipWith Equiv.swap l l').prod x ≠ x} ⊆ ↑(l.toFinset ⊔ l'.toFinset)
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. the standard measure on a set `s`.

It is equal to `(volume s)⁻¹ * ∫⁻ x, f x`, so it takes value zero if `s` has infinite measure. If
`s` has measure `1`, then the average of any function is equal to its integral.  -/
MeasureTheory.«term⨍⁻_In_,_» : Lean.ParserDescr
-- Mathlib.Analysis.Complex.Circle
Submonoid.unitSphere.congr_simp : ∀ (𝕜 : Type u_2) [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜],
  Submonoid.unitSphere 𝕜 = Submonoid.unitSphere 𝕜
-- Mathlib.Topology.MetricSpace.Gluing
Metric.glueDist_swap : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x y : X ⊕ Y), Metric.glueDist Ψ Φ ε x.swap y.swap = Metric.glueDist Φ Ψ ε x y
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_τ₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  (groupCohomology.mapShortComplexH1 f φ).τ₁ = Rep.Hom.toModuleCatHom φ
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_injective_iff_injective : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_4}
  {N' : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N] [inst_6 : Module R N']
  (f : N →ₗ[R] N') [Module.FaithfullyFlat R M], Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.pos_dist_of_ne : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Connected → u ≠ v → 0 < G.dist u v