mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Composition
List.length_splitWrtCompositionAux : ∀ {α : Type u_1} (l : List α) (ns : List ℕ), (l.splitWrtCompositionAux ns).length = ns.length
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (type? : Option Lean.Expr),
  sizeOf { expr := expr, type? := type? } = 1 + sizeOf expr + sizeOf type?
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.sup : ∀ {α : Type u_1} {l l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → l'.HasBasis p' s' → (l ⊔ l').HasBasis (fun i => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.of_equiv : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (e : TensorProduct R M₁ M₂ ≃ₗ[R] M),
  (∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y) → IsTensorProduct f
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.missingDocsExt : Lean.PersistentEnvExtension (Lean.Name × Lean.Name) (Lean.Name × Lean.Name × Lean.Linter.MissingDocs.Handler)
  (List (Lean.Name × Lean.Name) × Lean.NameMap Lean.Linter.MissingDocs.Handler)
-- Init.Data.UInt.Lemmas
UInt64.zero_le : ∀ {a : UInt64}, 0 ≤ a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_neg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun (-x) = NumberField.mixedEmbedding.convexBodySumFun x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The carrier set is closed under scalar multiplication.  -/
NonUnitalSubalgebra.smul_mem' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (self : NonUnitalSubalgebra R A) (c : R) {x : A}, x ∈ self.carrier → c • x ∈ self.carrier
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.mem_range : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N}
  {x : N}, x ∈ f.range ↔ ∃ y, f y = x
-- Mathlib.Condensed.Discrete.LocallyConstant
LightCondSet.LocallyConstant.instFullFunctor : LightCondSet.LocallyConstant.functor.Full
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eraseKey_le_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        ∀ {fallback : α},
          (compare (Std.Internal.List.maxKeyD (Std.Internal.List.eraseKey k l) fallback)
                (Std.Internal.List.maxKeyD l fallback)).isLE =
            true
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.finite_fundamentalDomain : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  (IsProperLinearSet.fundamentalDomain✝ hs).Finite
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.ker_prod_ker_le_ker_coprod : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommGroup M₃] [inst_9 : Module R M₃] (f : M →L[R] M₃)
  (g : M₂ →L[R] M₃), (↑f).ker.prod (↑g).ker ≤ ((↑f).coprod ↑g).ker
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.widePullbackShapeEquiv_functor_obj : ∀ {J : Type u_1} (a : CategoryTheory.Limits.WidePullbackShape J),
  CategoryTheory.WithTerminal.widePullbackShapeEquiv.functor.obj a =
    match a with
    | some x => CategoryTheory.WithTerminal.of { as := x }
    | none => CategoryTheory.WithTerminal.star
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- For `HasSubst a`, `MvPowerSeries.subst` is an algebra morphism.  -/
MvPowerSeries.substAlgHom : {σ : Type u_1} →
  {R : Type u_3} →
    [inst : CommRing R] →
      {τ : Type u_4} →
        {S : Type u_5} →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {a : σ → MvPowerSeries τ S} → MvPowerSeries.HasSubst a → MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S
-- Mathlib.Order.Types.Defs
OrderType.pos_iff_ne_zero : ∀ {o : OrderType.{u_1}}, 0 < o ↔ o ≠ 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
    (∀ a ∈ t, (List.map Prod.fst l).contains a = false) → (t.insertMany l).size = t.size + l.length
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.endsWith_eq_backwardPatternEndsWith : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.endsWith pat = String.Slice.Pattern.BackwardPattern.endsWith pat s
-- Mathlib.GroupTheory.OrderOfElement
submonoidOfIdempotent.eq_1 : ∀ {M : Type u_6} [inst : LeftCancelMonoid M] [inst_1 : Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S * S = S),
  submonoidOfIdempotent S hS1 hS2 = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯ }
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.insertMany.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  (m : Std.DHashMap.Raw α β) (l : ρ),
  m.insertMany l = if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.insertMany ⟨m, h⟩ l) else m
-- Mathlib.Data.Num.ZNum
Num.succ_ofInt' : ∀ (n : ℤ), ZNum.ofInt' (n + 1) = ZNum.ofInt' n + 1
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.of_entourage_subset : ∀ {X : Type u_1} {T : X → X} {U V : SetRel X X} {F s : Set X} {n : ℕ},
  U ⊆ V → Dynamics.IsDynCoverOf T F U n s → Dynamics.IsDynCoverOf T F V n s
-- Mathlib.Data.List.SplitBy
List.splitBy_eq_nil : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α}, List.splitBy r l = [] ↔ l = []
-- Mathlib.Data.Set.Function
Set.MapsTo.prodMk : ∀ {α : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s : Set α} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂},
  Set.MapsTo f₁ s t₁ → Set.MapsTo f₂ s t₂ → Set.MapsTo (fun x => (f₁ x, f₂ x)) s (t₁ ×ˢ t₂)
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : Group.FG G], CommGroup.freeRank G = Group.rank (G ⧸ CommGroup.torsion G)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- If `α` has at least `n` elements, then an `n`-pretransitive action
is `m`-pretransitive for any `m ≤ n`.

For an infinite `α`, use `MulAction.isMultiplyPretransitive_of_le'`.  -/
AddAction.isMultiplyPretransitive_of_le : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {m n : ℕ}
  [AddAction.IsMultiplyPretransitive G α n],
  m ≤ n → n ≤ Nat.card α → ∀ [Finite α], AddAction.IsMultiplyPretransitive G α m
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f g (CategoryTheory.CategoryStruct.id Y)
      (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ChosenPullbacksAlong.pullbackObj f g)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.insert : {basis : Tactic.ComputeAsymptotics.Basis} →
  (ℝ → ℝ) → Tactic.ComputeAsymptotics.BasisExtension basis → Tactic.ComputeAsymptotics.BasisExtension basis
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Weak convergence of finite measures implies that the limsup of the measures of any closed set is
at most the measure of the closed set under the limit measure.
 -/
MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [HasOuterApproxClosed Ω] [inst_3 : OpensMeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}
  {μs : ι → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs L (nhds μ) → ∀ {F : Set Ω}, IsClosed F → Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
-- Mathlib.Algebra.Tropical.Basic
Tropical.le_zero : ∀ {R : Type u} [inst : LE R] [inst_1 : OrderTop R] (x : Tropical R), x ≤ 0
-- Mathlib.Data.Finsupp.Order
Finsupp.single_mono : ∀ {ι : Type u_1} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {i : ι}, Monotone (Finsupp.single i)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.pow : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {c : ℝ} {l : Filter α} [NormOneClass R] [NormOneClass S] {f : α → R} {g : α → S},
  Asymptotics.IsBigOWith c l f g → ∀ (n : ℕ), Asymptotics.IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Right.one_lt_mul_of_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [IsBotOneClass α] [MulRightStrictMono α] {a : α},
  1 < a → ∀ (b : α), 1 < a * b
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
`OrderMonoidHomClass.toOrderMonoidHom`.  -/
instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulOneClass α] →
            [inst_3 : MulOneClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [MonoidHomClass F α β] → CoeTC F (α →*o β)
-- Lean.Parser.Term
Lean.Parser.Term.namedArgument.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Group.Defs
/-- An e-seminormed monoid is an additive monoid endowed with a continuous enorm.
Note that we do not ask for the enorm to be positive definite:
non-trivial elements may have enorm zero.  -/
ESeminormedAddMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Init.RCases
/-- A low precedence `rcases` pattern is a `rcasesPatMed` optionally followed by `: ty`  -/
Lean.Parser.Tactic.rcasesPatLo : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Action.Units
SemiconjBy.smul_right_iff₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} [inst_2 : Mul β]
  [SMulCommClass α β β] [IsScalarTower α β β] {x y z : β}, a ≠ 0 → (SemiconjBy x (a • y) (a • z) ↔ SemiconjBy x y z)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_ofBoolListLE : ∀ {bs : List Bool} {i : ℕ}, (BitVec.ofBoolListLE bs).getLsbD i = bs.getD i false
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- A special case of `lift_cRank_submatrix_le` for when `m₀` and `m` are in the same universe.  -/
Matrix.cRank_submatrix_le : ∀ {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Semiring R] {m m₀ : Type um} (A : Matrix m n R) (r : m₀ → m)
  (c : n₀ → n), (A.submatrix r c).cRank ≤ A.cRank
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.coe_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Type u_3}
  [inst_2 : FunLike F X Y] [inst_3 : ContinuousMapClass F X Y] (f : F), ⇑↑f = ⇑f
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_eq_integral : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → ProbabilityTheory.variance X μ = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (self : CategoryTheory.TransfiniteCompositionOfShape J f),
  CategoryTheory.CategoryStruct.comp self.isoBot.inv (self.incl.app ⊥) = f
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddGroupWithOne : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [AddGroupWithOne G] → AddGroupWithOne (l.Germ G)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.notMem : ∀ {X : SSet} {A : X.Subcomplex} (self : A.N), self.simplex ∉ A.obj (Opposite.op { len := self.dim })
-- Init.Data.Nat.Basic
Nat.succ_eq_add_one : ∀ (n : ℕ), n.succ = n + 1
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.map_id : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V),
  Representation.Coinvariants.map ρ ρ (Representation.IntertwiningMap.id ρ) = LinearMap.id
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.closure_singleton : ∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R), closure {x} = PrimeSpectrum.zeroLocus ↑x.asIdeal
-- Std.Http.Protocol.H1.Reader
/-- Adds a header to the current message head.
 -/
Std.Http.Protocol.H1.Reader.addHeader : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V}
  [SecondCountableTopology V],
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun v => VectorFourier.fourierPowSMulRight L f v n) μ
-- Mathlib.Algebra.CharP.Reduced
ExpChar.pow_prime_pow_mul_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] (x : R), x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
-- Mathlib.Algebra.Group.Action.Option
Option.instSMul_mathlib : {M : Type u_1} → {α : Type u_3} → [SMul M α] → SMul M (Option α)
-- Mathlib.Topology.Algebra.Monoid
exists_nhds_zero_quarter : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M] {u : Set M},
  u ∈ nhds 0 → ∃ V ∈ nhds 0, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v + w + s + t ∈ u
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_single_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {a : α} {b : M} {h : α → M → N},
  h a 0 = 1 → (fun₀ | a => b).prod h = h a b
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
/-- Auxiliary definition for `Presheaf.preservesLimitHomFamily`.  -/
CategoryTheory.Presheaf.preservesLimitHomFamilySrc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} J] →
        [CategoryTheory.LocallySmall.{w, v, u} C] →
          CategoryTheory.Functor J Cᵒᵖ → [Small.{w, u'} J] → CategoryTheory.Functor Cᵒᵖ (Type w)
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Reinterpret `G ≃+ H` as `Multiplicative G ≃* Multiplicative H`.  -/
AddEquiv.toMultiplicative : {G : Type u_2} →
  {H : Type u_3} → [inst : AddZeroClass G] → [inst_1 : AddZeroClass H] → G ≃+ H ≃ (Multiplicative G ≃* Multiplicative H)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_one : Chebyshev.psi 1 = 0
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.nz_of_isNegNat : ∀ {A : Type u_1} {e : A} {n : ℕ} [inst : Ring A] [inst_1 : PartialOrder A] [IsStrictOrderedRing A],
  Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n) → Nat.ble 1 n = true → e ≠ 0
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_le : ∀ {X : AlgebraicGeometry.Scheme} (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op U.toOpens))),
  U.basicOpen f ≤ U
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.instFaithfulCompObjPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : C), (CategoryTheory.CostructuredArrow.post F G S).Faithful
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRatRingHom_apply : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β),
  CauSeq.Completion.ofRatRingHom x = CauSeq.Completion.ofRat x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {f : β → β}, cmp (t.modify k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Given `F : J ⥤ Type w₀`, this is the relation `Σ j, F.obj j` which
generates an equivalence relation such that the quotient identifies
to the colimit type of `F`.  -/
CategoryTheory.Functor.ColimitTypeRel : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J (Type w₀)) → (j : J) × F.obj j → (j : J) × F.obj j → Prop
-- Batteries.Tactic.HelpCmd
/-- The command `#help tactic` shows all tactics that have been defined in the current environment.
See `#help cat` for more information.
 -/
Batteries.Tactic.«command#help_Tactic+____» : Lean.ParserDescr
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.ratCast_mem : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ),
  ↑q ∈ s
-- Mathlib.Algebra.Category.Grp.Kernels
/-- The projection onto the quotient is a cokernel in the categorical sense.  -/
AddCommGrpCat.cokernelIsColimit : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.IsColimit (AddCommGrpCat.cokernelCocone f)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_zero : DyckWord.semilength 0 = 0
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodCongr_symm_apply : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (e : M ≃* N) (e' : M' ≃* N'),
  ⇑(e.coprodCongr e').symm = ⇑(Monoid.Coprod.map ↑e.symm ↑e'.symm)
-- Init.Data.Nat.Basic
Nat.mul_le_mul_right : ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.instIsSplitMonoF : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) [CategoryTheory.IsSplitMono f] (j : ι), CategoryTheory.IsSplitMono (f.f j)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprStdWall : Repr Std.Time.TimeZone.StdWall
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.MeasurePreserving.integral_comp' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α ≃ᵐ β},
  MeasureTheory.MeasurePreserving (⇑f) μ ν → ∀ (g : β → G), ∫ (x : α), g (f x) ∂μ = ∫ (y : β), g y ∂ν
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.neg_eq : ∀ {α : Type u_1} [inst : BooleanRing α] (a : α), -a = a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.tendsto_approx : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (x : α),
  Filter.Tendsto (fun n => (hf.approx n) x) Filter.atTop (nhds (f x))
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_of_le_one : ∀ {b : Ordinal.{u_1}}, b ≤ 1 → ∀ (o : Ordinal.{u_1}), Ordinal.CNF.coeff b o = fun₀ | 0 => o
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.CertificateOracle.mk.injEq : ∀ (produceCertificate produceCertificate_1 : List Mathlib.Tactic.Linarith.Comp → ℕ → Lean.MetaM (Std.HashMap ℕ ℕ)),
  ({ produceCertificate := produceCertificate } = { produceCertificate := produceCertificate_1 }) =
    (produceCertificate = produceCertificate_1)
-- Mathlib.NumberTheory.PythagoreanTriples
_private.Mathlib.NumberTheory.PythagoreanTriples.0.coprime_sq_sub_mul : ∀ {m n : ℤ}, m.gcd n = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0 → (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
-- Mathlib.Algebra.Ring.Units
IsUnit.neg_iff : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α), IsUnit (-a) ↔ IsUnit a
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_swapEquiv_symm_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁),
  ((QuaternionAlgebra.swapEquiv c₁ c₃).symm t).re = t.re
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.empty_or_nonempty_of_hausdorffEDist_ne_top`. -/
EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist s t ≠ ⊤ → s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.η_whiskerRight_addCommutator_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero G)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.AddGrpObj.addCommutator G) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) G))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.minKey? = some km →
    (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey?.get ⋯ = kmi → (compare kmi km).isLE = true
-- Init.Data.SInt.Bitwise
ISize.toInt32_xor : ∀ (a b : ISize), (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.sset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i offset : ℕ) (y : Lean.FVarId) (ty : Lean.Expr)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11),
  sizeOf (Lean.Compiler.LCNF.Code.sset fvarId i offset y ty k h) =
    1 + sizeOf fvarId + sizeOf i + sizeOf offset + sizeOf y + sizeOf ty + sizeOf k + sizeOf h
-- Lean.Parser.Extension
Lean.Parser.AliasValue.unary.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (p : α → α), sizeOf (Lean.Parser.AliasValue.unary p) = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_bypass_le_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} [inst : DecidableEq V], p.bypass.toSubgraph ≤ p.toSubgraph