mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ExactSequence
/-- Functoriality maps for `ComposableArrows.sc'`.  -/
CategoryTheory.ComposableArrows.sc'Map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S₁ S₂ : CategoryTheory.ComposableArrows C n} →
          (S₁ ⟶ S₂) →
            (h₁ : S₁.IsComplex) →
              (h₂ : S₂.IsComplex) →
                (i j k : ℕ) →
                  (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'Map._auto_1) →
                    (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'Map._auto_3) →
                      (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'Map._auto_5) →
                        S₁.sc' h₁ i j k hij hjk hk ⟶ S₂.sc' h₂ i j k hij hjk hk
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.snd : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {M' : Type u_3} [inst_1 : One M'] {f : α → M × M'},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport fun a => (f a).2
-- Mathlib.LinearAlgebra.AffineSpace.Slope
/-- `slope f a b = (b - a)⁻¹ • (f b -ᵥ f a)` is the slope of a function `f` on the interval
`[a, b]`. Note that `slope f a a = 0`, not the derivative of `f` at `a`.  -/
slope : {k : Type u_1} →
  {E : Type u_2} →
    {PE : Type u_3} →
      [inst : Field k] → [inst_1 : AddCommGroup E] → [Module k E] → [AddTorsor E PE] → (k → PE) → k → k → E
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.instZeroHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → Zero (S₁ ⟶ S₂)
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.not_isNilpotent : ∀ (G : Type u_1) [inst : Group G] [Nontrivial G] [Group.IsPerfect G], ¬Group.IsNilpotent G
-- Mathlib.Algebra.Category.Grp.Basic
/-- Universe lift functor for additive groups.  -/
AddGrpCat.uliftFunctor : CategoryTheory.Functor AddGrpCat AddGrpCat
-- Mathlib.Data.Num.ZNum
PosNum.divMod_to_nat_aux : ∀ {n d : PosNum} {q r : Num},
  ↑r + ↑d * (↑q + ↑q) = ↑n →
    ↑r < 2 * ↑d → ↑(d.divModAux q r).2 + ↑d * ↑(d.divModAux q r).1 = ↑n ∧ ↑(d.divModAux q r).2 < ↑d
-- Init.Data.List.Attach
List.countP_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {g : (a : α) → p a → β} {f : β → Bool} {l : List α} (H₁ : ∀ a ∈ l, p a),
  List.countP f (List.pmap g l H₁) =
    List.countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      l.attach
-- Mathlib.Algebra.Group.Units.Opposite
IsUnit.op : ∀ {M : Type u_2} [inst : Monoid M] {m : M}, IsUnit m → IsUnit (MulOpposite.op m)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ (k : α), t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Copy of a subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Subalgebra.copy : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → (s : Set A) → s = ↑S → Subalgebra R A
-- Mathlib.Algebra.Group.Units.Equiv
/-- The `αˣ` type is equivalent to a subtype of `α × α`.  -/
unitsEquivProdSubtype : (α : Type u_2) → [inst : Monoid α] → αˣ ≃ { p // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → ∀ {h : k' ∈ Std.DHashMap.ofList l}, (Std.DHashMap.ofList l).getKey k' h = k
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.toHasGroupoid : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {M : Type u_4} {inst_4 : TopologicalSpace M} {inst_5 : ChartedSpace H M} [self : IsManifold I n M],
  HasGroupoid M (contDiffGroupoid n I)
-- Init.Data.SInt.Bitwise
Int16.shiftLeft_and : ∀ {a b c : Int16}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two measures which are finite on closed-open intervals are equal if they agree on all
closed-open intervals.  -/
MeasureTheory.Measure.ext_of_Ico' : ∀ {α : Type u_5} [inst : TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ ν : MeasureTheory.Measure α),
  (∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) ≠ ⊤) → (∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) = ν (Set.Ico a b)) → μ = ν
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.map_ofFixingSubgroupUnion_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α},
  Function.Bijective ⇑(SubMulAction.map_ofFixingSubgroupUnion M s t)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.comp_obj : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  {D : Type u₂} {E : Type u₃} [inst_2 : CategoryTheory.EnrichedCategory V C]
  [inst_3 : CategoryTheory.EnrichedCategory V D] [inst_4 : CategoryTheory.EnrichedCategory V E]
  (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (X : C),
  (CategoryTheory.EnrichedFunctor.comp V F G).obj X = G.obj (F.obj X)
-- Lean.Elab.InfoTree.Basic
_private.Lean.Elab.InfoTree.Basic.0.Lean.Elab.Info.setStx : Lean.Syntax → Lean.Elab.Info → Lean.Elab.Info
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_natDegree : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) [Nontrivial R], (φ.polyCharpoly b).natDegree = Module.finrank R M
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Resets the assignment of any variable bigger or equal to `x`.  -/
Lean.Meta.Grind.Arith.Linear.resetAssignmentFrom : Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.clift.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))),
  Monoid.Coprod.clift f hM₁ hN₁ hM hN = (Monoid.coprodCon M N).lift f ⋯
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected.congr_simp : ∀ {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover)
  [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  {Y : CategoryTheory.Over S} (g g_1 : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (e_g : g = g_1)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom),
  𝒰.glueMorphismsOverOfLocallyDirected g h w = 𝒰.glueMorphismsOverOfLocallyDirected g_1 ⋯ ⋯
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_eq_same : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  (r : G i), (RestrictedProduct.mulSingle A i r) i = r
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.firstObjEqFamily_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X),
  (CategoryTheory.Equalizer.firstObjEqFamily P R).hom =
    TypeCat.ofHom fun t x x_1 hf =>
      (CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨x, ⟨x_1, hf⟩⟩))
        t
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Every entry of a row stochastic matrix is nonnegative.  -/
Matrix.nonneg_of_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.rowStochastic R n → ∀ {i j : n}, 0 ≤ M i j
-- Init.Data.List.Nat.Basic
List.length_intersperse : ∀ {α : Type u_1} {l : List α} {sep : α}, (List.intersperse sep l).length = 2 * l.length - 1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.prod_snd : ∀ (ι : Type w) (self : ι × ι), (CategoryTheory.Limits.MultispanShape.prod ι).snd self = self.2
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.equivRange.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  (hf : MeasurableEmbedding f),
  hf.equivRange =
    (MeasurableEquiv.Set.univ α).symm.trans
      ((MeasurableEmbedding.equivImage Set.univ hf).trans (MeasurableEquiv.cast ⋯ ⋯))
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_apply : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] (I : Ideal S),
  Ideal.absNorm I = Submodule.cardQuot I
-- Mathlib.Order.Lattice
/-- A `SemilatticeSup` is a join-semilattice, that is, a partial order
with a join (a.k.a. lub / least upper bound, sup / supremum) operation
`⊔` which is the least element larger than both factors.  -/
SemilatticeSup : Type u → Type u
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instMonoι : ∀ {X : SSet} (A : X.Subcomplex), CategoryTheory.Mono A.ι
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.of_algEquiv : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [inst_6 : CommRing S]
  [inst_7 : Algebra A S] [inst_8 : Algebra R S] (f : B ≃ₐ[R] S),
  (∀ (x : A), (algebraMap A S) x = f ((algebraMap A B) x)) → IsIntegralClosure A R S
-- Init.Data.List.Attach
List.flatMap_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → List β} {g : α → List β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.flatMap f l = List.flatMap g l.unattach
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. If `f` is a bounded continuous real-valued function defined on a closed set in a normal
topological space, then it can be extended to a bounded continuous function of the same norm defined
on the whole space.  -/
BoundedContinuousFunction.exists_norm_eq_domRestrict_eq_of_closed : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ),
  IsClosed s → ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.add.injEq : ∀ (a : Lean.Name) (a_1 : Lean.Syntax) (a_2 : Lean.Name) (a_3 : Lean.Syntax),
  (Simps.ProjectionRule.add a a_1 = Simps.ProjectionRule.add a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Batteries.Data.List.Perm
List.subperm_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l₁ ++ l).Subperm (l₂ ++ l) ↔ l₁.Subperm l₂
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_toRingEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.symm.toRingEquiv = e.toRingEquiv.symm
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_zero : ∀ {α β : Type u} (f : α → β), f <$> 0 = 0
-- Mathlib.Algebra.Lie.Basis.Basic
/-- The nilpotent part of the "lower" Borel subalgebra associated to a basis.  -/
LieAlgebra.Basis.borelLower : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → LieSubmodule R (↥H) L
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationAdjunctionLeft_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (Y : D),
  (CategoryTheory.evaluationAdjunctionLeft D c).counit.app Y =
    CategoryTheory.Limits.Pi.π (fun x => Y) (CategoryTheory.CategoryStruct.id c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool}
  (h : t.WF), (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.toList = List.filter (fun p => f p.fst p.snd) t.toList
-- Mathlib.Topology.Spectral.Hom
SpectralMap.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : SpectralMap α β),
  (SpectralMap.id β).comp f = f
-- Mathlib.Topology.Irreducible
/-- An irreducible set `s` is one that is nonempty and
where there is no non-trivial pair of disjoint opens on `s`.  -/
IsIrreducible : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalarsRange₂_apply_eq_zero_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7}
  {P' : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M]
  [inst_4 : Module R M] [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : AddCommMonoid P]
  [inst_8 : Module R P] [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : Module S P]
  [inst_12 : IsScalarTower S R M] [inst_13 : IsScalarTower S R N] [inst_14 : IsScalarTower S R P]
  [inst_15 : AddCommMonoid M'] [inst_16 : Module S M'] [inst_17 : AddCommMonoid N'] [inst_18 : Module S N']
  [inst_19 : AddCommMonoid P'] [inst_20 : Module S P'] [inst_21 : SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N)
  (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P)
  (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range) (m : M') (n : N'),
  ((i.restrictScalarsRange₂ j k hk B hB) m) n = 0 ↔ (B (i m)) (j n) = 0
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- If there is no `i` so `c.Rel i j`, then `C.xPrev j` is isomorphic to `C.X j`.  -/
HomologicalComplex.xPrevIsoSelf : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (C : HomologicalComplex V c) → {j : ι} → ¬c.Rel (c.prev j) j → (C.xPrev j ≅ C.X j)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A version of `liftPropWithinAt_indep_chart`, that uses `LiftPropWithinAt` on both sides.  -/
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart' : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e : OpenPartialHomeomorph M H} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    e ∈ StructureGroupoid.maximalAtlas M G →
      x ∈ e.source →
        f ∈ StructureGroupoid.maximalAtlas M' G' →
          g x ∈ f.source →
            (ChartedSpace.LiftPropWithinAt P g s x ↔
              ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Full.comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Full] [G.Full], (F.comp G).Full
-- Mathlib.Analysis.RCLike.Basic
RCLike.exists_norm_eq_mul_self : ∀ {K : Type u_1} [inst : RCLike K] (x : K), ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.ground_indep_iff_eq_freeOn : ∀ {α : Type u_1} {M : Matroid α}, M.Indep M.E ↔ M = Matroid.freeOn M.E
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom).app X) ((Φ.colon Ψ).ι.app X) =
    Φ.ι.app X
-- Std.Sync.Mutex
Std.instNonemptyBaseMutex : Nonempty Std.BaseMutex
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M},
  (∀ {f : M → 𝕜} {σ : (x : M) → V x}, MDiffAt f x → MDiffAt (T% σ) x → Φ (f • σ) = f x • Φ σ) →
    (∀ {σ σ' : (x : M) → V x}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → Φ (σ + σ') = Φ σ + Φ σ') → TensorialAt I F Φ x
-- Mathlib.Computability.Language
Language.zero_def : ∀ {α : Type u_1}, 0 = ∅
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.indexRealUnits.eq_1 : ∀ (K : Type u_1) [inst : Field K],
  NumberField.IsCMField.indexRealUnits K = (NumberField.IsCMField.realUnits K ⊔ NumberField.Units.torsion K).index
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.deltaBetaDefinition : {α : Type} →
  Lean.ConstantInfo →
    List Lean.Level →
      Array Lean.Expr → (Unit → Lean.MetaM α) → (Lean.Expr → Lean.MetaM α) → optParam Bool false → Lean.MetaM α
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.toExtension.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι),
  P.toExtension =
    { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
      algebra₂ := P.instRing, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }
-- Mathlib.Order.Hom.Bounded
BotHom.instBotHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β], BotHomClass (BotHom α β) α β
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.WidePullbackShape.fintypeHom : {J : Type v} → (j j' : CategoryTheory.Limits.WidePullbackShape J) → Fintype (j ⟶ j')
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.le_card_nonuniformWitness : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t → ↑s.card * ε ≤ ↑(G.nonuniformWitness ε s t).card
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.brecOn.go t F_1 F_2).2
-- Lean.Environment
Lean.ModuleData.mk.sizeOf_spec : ∀ (isModule : Bool) (imports : Array Lean.Import) (constNames : Array Lean.Name) (constants : Array Lean.ConstantInfo)
  (extraConstNames : Array Lean.Name) (entries : Array (Lean.Name × Array Lean.EnvExtensionEntry)),
  sizeOf
      { isModule := isModule, imports := imports, constNames := constNames, constants := constants,
        extraConstNames := extraConstNames, entries := entries } =
    1 + sizeOf isModule + sizeOf imports + sizeOf constNames + sizeOf constants + sizeOf extraConstNames +
      sizeOf entries
-- Mathlib.Analysis.Meromorphic.Order
/-- At zeros and poles of a meromorphic function `f`, the logarithmic derivative has a simple pole: its
meromorphic order equals `-1`.
 -/
meromorphicOrderAt_logDeriv_eq_neg_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} [CharZero 𝕜],
  MeromorphicAt f x → meromorphicOrderAt f x ≠ 0 → meromorphicOrderAt f x ≠ ⊤ → meromorphicOrderAt (logDeriv f) x = -1
-- Mathlib.Order.Filter.Ring
Filter.eventually_sub_nonneg : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] [inst_1 : LE β] [AddRightMono β] {l : Filter α} {f g : α → β},
  0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g
-- Mathlib.Topology.PartitionOfUnity
/-- the functions are non-negative  -/
PartitionOfUnity.nonneg' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ}
  (self : PartitionOfUnity ι X s), 0 ≤ self.toFun
-- Mathlib.Algebra.Order.Hom.Monoid
MonoidHomClass.ext_iff_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : Monoid β] {F : Type u_6} [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] [inst : PartialOrder β] [MulRightMono β] [MulLeftMono β] {f g : F},
  f = g ↔ ∀ (x : α), f x ≤ g x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.instInhabited : {R : Type u_1} →
  {E : Type u_5} →
    [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → Inhabited (E ≃ₗᵢ[R] E)
-- Std.Time.Date.Basic
Std.Time.instHSubOffset_2 : HSub Std.Time.Second.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.below.of_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsExistential → Prop}
  {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF), FirstOrder.Language.BoundedFormula.IsExistential.below ⋯
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.Nonempty.csSup_mem : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Finset α}, s.Nonempty → sSup ↑s ∈ s
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_add`. -/
ModularForm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g