mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.mk.injEq : ∀ (toAddGrp : AddGrpCat) [isFinite : Finite ↑toAddGrp] (toAddGrp_1 : AddGrpCat) (isFinite_1 : Finite ↑toAddGrp_1),
  ({ toAddGrp := toAddGrp, isFinite := isFinite } = { toAddGrp := toAddGrp_1, isFinite := isFinite_1 }) =
    (toAddGrp = toAddGrp_1)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_one : ∀ {R : Type u_1} {a b : R} [inst : Zero R] [inst_1 : One R], QuadraticAlgebra.re 1 = 1
-- Mathlib.Algebra.Quaternion
Quaternion.imI_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a + b).imI = a.imI + b.imI
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.HasLimit.productLimitCone_cone_π : ∀ {J : Type w} (f : J → AddCommGrpCat),
  (AddCommGrpCat.HasLimit.productLimitCone f).cone.π =
    CategoryTheory.Discrete.natTrans fun j => AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as)
-- Lean.Message
Lean.BaseMessage.fileName : {α : Type u} → Lean.BaseMessage α → String
-- Mathlib.Algebra.BigOperators.Group.List.Basic
map_list_prod : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_8} [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) (l : List M), f l.prod = (List.map (⇑f) l).prod
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t`, then the support of `G` is a subset of `s ∪ t`.  -/
SimpleGraph.isBipartiteWith_support_subset : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → G.support ⊆ s ∪ t
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.IsScalarTower.compatibleSMul' : ∀ {M : Type u_8} [inst : AddCommMonoid M] {R : Type u_14} {S : Type u_15} [inst_1 : Semiring S] [inst_2 : SMul R M]
  [inst_3 : Module S M] [inst_4 : SMul R S] [IsScalarTower R S M], LinearMap.CompatibleSMul S M R S
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRii : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
/-- Morphisms between two direct sums over a hom orthogonal family `s : ι → C`
are equivalent to block diagonal matrices,
with blocks indexed by `ι`,
and matrix entries in `i`-th block living in the endomorphisms of `s i`.  -/
CategoryTheory.HomOrthogonal.matrixDecomposition : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {s : ι → C} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            CategoryTheory.HomOrthogonal s →
              {α β : Type} →
                [inst_3 : Finite α] →
                  [inst_4 : Finite β] →
                    {f : α → ι} →
                      {g : β → ι} →
                        ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃
                          ((i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
-- Mathlib.Algebra.Module.Rat
/-- A `ℚ≥0`-module is torsion-free as a group.

This instance will fire for any monoid `M`, so is local unless needed elsewhere.  -/
IsAddTorsionFree.of_module_nnrat : ∀ (M : Type u_1) [inst : AddCommMonoid M] [Module ℚ≥0 M], IsAddTorsionFree M
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mul_div_self_cancel_iff : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K},
  I * (1 / I) = 1 ↔ ∃ J, I * J = 1
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.map (AddMonoidHom.id R) x = x
-- Mathlib.RingTheory.Adjoin.Singleton
Algebra.instSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : CommSemiring C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → Algebra ↥A[b] ↥A[(algebraMap B C) b]
-- Init.Data.List.Lemmas
List.filterMap_eq_cons_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α} {b : α_1} {bs : List α_1},
  List.filterMap f l = b :: bs ↔
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ x ∈ l₁, f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = bs
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {c : ℝ},
  x ∈ NumberField.mixedEmbedding.fundamentalCone K → c ≠ 0 → c • x ∈ NumberField.mixedEmbedding.fundamentalCone K
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_comp : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} {M₅ : Type u_1} {M₆ : Type u_2}
  [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : AddCommMonoid M₄] [inst_5 : AddCommMonoid M₅] [inst_6 : AddCommMonoid M₆] [inst_7 : Module R M]
  [inst_8 : Module R M₂] [inst_9 : Module R M₃] [inst_10 : Module R M₄] [inst_11 : Module R M₅] [inst_12 : Module R M₆]
  (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆),
  f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : MulZeroOneClass γ] [inst_3 : MulZeroOneClass δ] (f : α →*₀ β) (g : β →*₀ γ) (h : γ →*₀ δ),
  (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.coe_mul : ∀ (M : Type u_4) [inst : AddZero M] (f g : AddMonoid.End M), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.Nonempty.zero_div : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α] {s : Finset α}, s.Nonempty → 0 / s = 0
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.getCallerParam? : ℕ → ℕ → ℕ → Lean.Elab.FixedParams.Info → Option ℕ
-- Init.Data.Nat.Basic
Nat.zero_eq : Nat.zero = 0
-- Init.Notation
/-- A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.

The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through

If no filter is specified, `check all` is assumed.  Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
 -/
Lean.guardMsgsFilter : Lean.ParserDescr
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  -/
SchwartzMap.«term𝓢(_,_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- The typeclass saying that `P : ObjectProperty C` is stable under binary coproducts.  -/
CategoryTheory.ObjectProperty.IsClosedUnderBinaryCoproducts : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.red : Lean.Lsp.Color → Float
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.norm_ofCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : (↑v).Completion), ‖{ toCompletion := x }‖ = ‖x‖
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.quoted.inj : ∀ {e e_1 : Lean.Expr}, Qq.Impl.ExprBackSubstResult.quoted e = Qq.Impl.ExprBackSubstResult.quoted e_1 → e = e_1
-- Mathlib.Analysis.Convex.Join
convexJoin_iUnion_right : ∀ {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E) (t : ι → Set E), convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)
-- Mathlib.Analysis.Normed.Field.Basic
/-- The norm is multiplicative.  -/
NormedField.norm_mul : ∀ {α : Type u_5} [self : NormedField α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
-- Mathlib.Tactic.TypeStar
/-- Given a `namePrefix` (`` `u`` by default), returns the first name out of `namePrefix_1`,
`namePrefix_2`, ... which does not appear in `usedLevelNames`. Note `mkFreshLevelName` does not
attempt to use `namePrefix` itself as a level name.
 -/
Lean.Elab.Term.mkFreshLevelName : List Lean.Name → optParam Lean.Name `u → Lean.Name
-- Mathlib.Data.Finset.Option
Finset.card_eraseNone_of_mem : ∀ {α : Type u_1} {s : Finset (Option α)}, none ∈ s → (Finset.eraseNone s).card = s.card - 1
-- Lean.Attributes
Lean.ParametricAttributeImpl.afterSet : {α : Type} → Lean.ParametricAttributeImpl α → Lean.Name → α → Lean.AttrM Unit
-- Init.Data.List.Lemmas
List.getLast?_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, (List.map f l).getLast? = Option.map f l.getLast?
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {combined w : ℕ} →
          (n : ℕ) → aig.RefVec w → combined = w * n → Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig combined
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The Mahler measure of a polynomial `p` defined as `e ^ (logMahlerMeasure p)` if `p` is nonzero
and `0` otherwise  -/
Polynomial.mahlerMeasure : Polynomial ℂ → ℝ
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_natAbs_self : ∀ {a : ℤ}, a ∣ ↑a.natAbs
-- Mathlib.CategoryTheory.Localization.Predicate
/-- the functor inverts the given `MorphismProperty`  -/
CategoryTheory.Functor.IsLocalization.inverts : ∀ {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} {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} [self : L.IsLocalization W], W.IsInvertedBy L
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_carrier : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), x ∈ A.carrier ↔ x ∈ A
-- Mathlib.MeasureTheory.Order.Lattice
Measurable.sup_const : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : α → M} [inst_1 : Max M]
  [MeasurableSup M], Measurable f → ∀ (c : M), Measurable fun x => f x ⊔ c
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.le_iff_Icc : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, I ≤ J ↔ BoxIntegral.Box.Icc I ⊆ BoxIntegral.Box.Icc J
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.toRange_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.toRange p) (CategoryTheory.Subfunctor.range p).ι = p
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_toList_perm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.toList.Perm m₂.toList → m₁.Equiv m₂
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- The Hurwitz zeta function, which is the meromorphic continuation of
`∑ (n : ℕ), 1 / (n + a) ^ s` if `0 ≤ a ≤ 1`. See `hasSum_hurwitzZeta_of_one_lt_re` for the relation
to the Dirichlet series in the convergence range.  -/
HurwitzZeta.hurwitzZeta : UnitAddCircle → ℂ → ℂ
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_toEuclideanCLM : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜),
  ‖Matrix.toEuclideanCLM A‖ = ‖A‖
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mkIso_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f : M.X ≅ N.X)
  (f_counit :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
      CategoryTheory.Comon.mkIso._auto_1)
  (f_comul :
    autoParam
      (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.comul =
        CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom))
      CategoryTheory.Comon.mkIso._auto_3),
  (CategoryTheory.Comon.mkIso f f_counit f_comul).inv.hom = f.inv
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.ExprVisited.mk.injEq : ∀ (e e_1 : Lean.Expr), ({ e := e } = { e := e_1 }) = (e = e_1)
-- Lean.Util.PPExt
Lean.ppTerm : Lean.PPContext → Lean.Term → BaseIO Std.Format
-- Mathlib.Analysis.InnerProductSpace.Symmetric
_private.Mathlib.Analysis.InnerProductSpace.Symmetric.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Data.Fintype.EquivFin
Fintype.bijective_iff_surjective_and_card : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Bijective f ↔ Function.Surjective f ∧ Fintype.card α = Fintype.card β
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `exp(x) / x ^ s` tends to `+∞` at `+∞`, for any real number `s`.  -/
tendsto_exp_div_rpow_atTop : ∀ (s : ℝ), Filter.Tendsto (fun x => Real.exp x / x ^ s) Filter.atTop Filter.atTop
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
ContMDiff.smoothSheafHom_hom_app_hom : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] {N : Type u}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] {EP : Type u_7} [inst_11 : NormedAddCommGroup EP]
  [inst_12 : NormedSpace 𝕜 EP] {HP : Type u_8} [inst_13 : TopologicalSpace HP] (IP : ModelWithCorners 𝕜 EP HP)
  (P : Type u) [inst_14 : TopologicalSpace P] [inst_15 : ChartedSpace HP P] (f : M → P) (hf : ContMDiff IM IP (↑⊤) f)
  (U : (TopologicalSpace.Opens ↑(TopCat.of P))ᵒᵖ),
  CategoryTheory.ConcreteCategory.hom ((ContMDiff.smoothSheafHom IP P f hf).hom.app U) =
    { toFun := fun g => ⟨↑g ∘ (↑(Opposite.unop U)).restrictPreimage f, ⋯⟩ }
-- Mathlib.Order.Fin.InsertNth
Fin.strictMono_insertNth_last : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  StrictMono f → ∀ (x : α), f (Fin.last n) < x → StrictMono ((Fin.last (n + 1)).insertNth x f)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.unop_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ} {P : HomotopicalAlgebra.PrepathObject Y}
  {f g : X ⟶ Y} (h : P.RightHomotopy f g), h.unop.h = h.h.unop
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.associator_hom_hom : ∀ (X Y Z : SFinKer),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom =
    ProbabilityTheory.Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯
-- Init.SimpLemmas
Or.imp : ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∨ b → c ∨ d
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst_neg_right : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A.addConst (-B) = A.subConst B
-- Init.Data.Nat.Basic
Nat.eq_zero_of_add_eq_zero_left : ∀ {n m : ℕ}, n + m = 0 → m = 0
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_map_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : UpperSet β),
  ↑((UpperSet.map f).symm s) = ⇑f ⁻¹' ↑s
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilterDistortion_mono : ∀ {ι : Type u_1} [inst : Fintype ι] {c₁ c₂ : NNReal} {l₁ l₂ : BoxIntegral.IntegrationParams} (I : BoxIntegral.Box ι),
  l₁ ≤ l₂ → c₁ ≤ c₂ → l₁.toFilterDistortion I c₁ ≤ l₂.toFilterDistortion I c₂
-- Init.Data.Nat.Bitwise.Lemmas
Nat.right_le_or : ∀ {n m : ℕ}, m ≤ n ||| m
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.rightUnitor_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C)))
      (CategoryTheory.Limits.prod.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom f
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSubtractionMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionMonoid α],
  OrderDual.instSubtractionMonoid =
    { toSubNegMonoid := OrderDual.instSubNegAddMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.Order.CompactlyGenerated.Basic
WellFoundedLT.finite_ne_bot_of_iSupIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α},
  iSupIndep t → {i | t i ≠ ⊥}.Finite
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_strictAnti₀` for the implication from right-to-left with one fewer assumption.  -/
inv_lt_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → 0 < b → (a⁻¹ < b⁻¹ ↔ b < a)
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_mono : ∀ {x y : ZFSet.{u}}, x ⊆ y → x.card ≤ y.card
-- Init.Data.Rat.Lemmas
Rat.num_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).num = OfNat.ofNat n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.image_tan_Ioo : Real.tan '' Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) = Set.univ
-- Mathlib.Algebra.Order.Group.Abs
abs_le_max_abs_abs : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  a ≤ b → b ≤ c → |b| ≤ max |a| |c|
-- Batteries.Data.AssocList
/-- Add a `key, value` pair to the list  -/
Batteries.AssocList.cons : {α : Type u} → {β : Type v} → α → β → Batteries.AssocList α β → Batteries.AssocList α β
-- Mathlib.Data.Fin.Tuple.Basic
Fin.range_cons : ∀ {α : Type u_1} {n : ℕ} (x : α) (b : Fin n → α), Set.range (Fin.cons x b) = insert x (Set.range b)
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `ℂ_[p]` extends the norm on `PadicAlgCl p`.  -/
PadicComplex.norm_extends : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), ‖↑x‖ = ‖x‖
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_7} {G' : Type u_8}
  [inst : NormedAddCommGroup G'] [inst_1 : PartialOrder G'] [IsOrderedAddMonoid G'] [inst_3 : NormedSpace ℝ G']
  [inst_4 : NormedAddCommGroup G''] [inst_5 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_7 : NormedSpace ℝ G'']
  {T : Set α → G'' →L[ℝ] G'},
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x) →
        ∀ {f g : ↥(α →₁ₛ[μ] G'')},
          f ≤ g → MeasureTheory.L1.SimpleFunc.setToL1S T f ≤ MeasureTheory.L1.SimpleFunc.setToL1S T g
-- Mathlib.Data.Stream.Init
Stream'.mem_append_stream_left : ∀ {α : Type u} {a : α} {l : List α} (s : Stream' α), a ∈ l → a ∈ l ++ₛ s
-- Lean.Meta.Sym.Arith.MonadCanon
Lean.Meta.Sym.Arith.MonadCanon.synthInstance : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Expr → m Lean.Expr
-- Mathlib.RingTheory.IdealFilter.Basic
/-- **Axiom T3.**  See [stenstrom1975].  -/
IdealFilter.IsUniform.colon_mem : ∀ {A : Type u_1} {inst : Ring A} {F : IdealFilter A} [self : F.IsUniform] {I : Ideal A},
  I ∈ F → ∀ (a : A), Submodule.colon I {a} ∈ F
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitCocone F =
    { pt := AddMonCat.FilteredColimits.colimit F,
      ι := { app := AddMonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.proj_prop_eq_self : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
  (∀ (i : I), ∀ x ∈ C, x i ≠ false → J i) → Profinite.NobelingProof.π C J = C
-- Lean.Elab.Do.Basic
/-- Build `pure (α:=α) e : m α`.  -/
Lean.Elab.Do.DoOps.mkPureApp : Lean.Elab.Do.DoOps → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.int_lcm_helper : ∀ {x y : ℤ} {x' y' d : ℕ}, x.natAbs = x' → y.natAbs = y' → x'.lcm y' = d → x.lcm y = d
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
/-- Gluing `Ioc a b` and `Ioc b c` into `Ioc a c`.  -/
IocProdIoc : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : LocallyFiniteOrder ι] →
      [DecidableLE ι] →
        {X : ι → Type u_2} →
          (a b c : ι) →
            ((i : ↥(Finset.Ioc a b)) → X ↑i) × ((i : ↥(Finset.Ioc b c)) → X ↑i) → (i : ↥(Finset.Ioc a c)) → X ↑i
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.forgetFunctorToCore_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  (F : CategoryTheory.Functor G (CategoryTheory.Core C)) {X Y : G} (f : X ⟶ Y),
  (CategoryTheory.Core.forgetFunctorToCore.obj F).map f = (F.map f).iso.hom
-- Init.Dynamic
/-- Dynamic type name information.
Types with an instance of `TypeName` can be stored in an `Dynamic`.
The type class contains the declaration name of the type,
which must not have any universe parameters
and be of type `Sort ..` (i.e., monomorphic).

The preferred way to declare instances of this type is using the derive
handler, which will internally use the unsafe `TypeName.mk` function.

Morally, this is the same as:
```lean
class TypeName (α : Type) where unsafe mk ::
  typeName : Name
```
 -/
TypeName : Type u → Type
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∈ m → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey? k = m.getKey? k
-- Init.Internal.Order.Lemmas
Array.foldrM.fold.induct : ∀ {α : Type u} {β : Type v} (as : Array α) (stop : ℕ) (motive : (i : ℕ) → i ≤ as.size → β → Prop),
  (∀ (t : ℕ) (h : t ≤ as.size) (b : β), (t == stop) = true → motive t h b) →
    (∀ (b : β) (x : 0 ≤ as.size), ¬(0 == stop) = true → motive 0 x b) →
      (∀ (b : β) (i : ℕ) (h : i + 1 ≤ as.size) (this : i < as.size),
          ¬(i.succ == stop) = true → (∀ (__do_lift : β), motive i ⋯ __do_lift) → motive i.succ h b) →
        ∀ (i : ℕ) (h : i ≤ as.size) (b : β), motive i h b
-- Mathlib.Order.SuccPred.Basic
Order.succ_lt_succ_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Order.succ a < Order.succ b ↔ a < b
-- Init.Data.Vector.Lemmas
Vector.replace_extract : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n} {i : ℕ},
  (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- `∮ z in C(c, R), f z` is the circle integral $\oint_{|z-c|=R} f(z)\,dz$.  -/
«term∮_InC(_,_),_» : Lean.ParserDescr
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_biUnion_finset_le : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  {μ : F} (I : Finset ι) (s : ι → Set α), μ (⋃ i ∈ I, s i) ≤ ∑ i ∈ I, μ (s i)
-- Init.Data.Bool
Bool.exists_bool' : ∀ {p : Bool → Prop} (b : Bool), (∃ x, p x) ↔ p b ∨ p !b