mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetricProjection.isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → T.IsSymmetric
-- Init.Notation
/-- `p*` is shorthand for `many(p)`. It uses parser `p` 0 or more times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

If `p` has arity more than 1, it is auto-grouped in the items generated by the parser.
 -/
«stx_*» : Lean.TrailingParserDescr
-- Init.Data.String.Basic
String.substrEq : String → String.Pos.Raw → String → String.Pos.Raw → ℕ → Bool
-- Mathlib.Algebra.Order.Module.Pointwise
bddAbove_smul_iff_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : GroupWithZero α] [inst_3 : Zero β]
  [inst_4 : MulActionWithZero α β] [PosSMulMono α β] [PosSMulReflectLE α β] {s : Set β} {a : α},
  0 < a → (BddAbove (a • s) ↔ BddAbove s)
-- Mathlib.Data.ENat.Basic
ENat.map_natCast_inj : ∀ {m n : ℕ∞} {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α]
  [CharZero α], ENat.map Nat.cast m = ENat.map Nat.cast n ↔ m = n
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- An `apply` suggestion section.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.app : Array Mathlib.Tactic.ClickSuggestions.ApplyLemma → Mathlib.Tactic.ClickSuggestions.Candidates✝
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map.eq_1 : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (x : MonoidAlgebra R M), MonoidAlgebra.map f x = MonoidAlgebra.ofCoeff (Finsupp.mapRange ⇑f ⋯ x.coeff)
-- Std.Time.Date.Unit.Month
/-- Transforms `Month.Ordinal` into `Minute.Offset`.
 -/
Std.Time.Month.Ordinal.toMinutes : Bool → Std.Time.Month.Ordinal → Std.Time.Minute.Offset
-- Init.Data.UInt.Lemmas
UInt64.instLawfulOrderLT : Std.LawfulOrderLT UInt64
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_le_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f₁ f₂ g₁ g₂ : Filter β}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂
-- Init.Data.Option.Lemmas
Option.pelim_eq_elim : ∀ {α : Type u_1} {o : Option α} {α_1 : Sort u_2} {b : α_1} {f : α → α_1}, (o.pelim b fun a x => f a) = o.elim b f
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_comp_sub_const_eq_meromorphicOrderAt`

---

`meromorphicOrderAt` is invariant under translation.  -/
meromorphicOrderAt_fun_comp_sub_const_eq_meromorphicOrderAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E},
  meromorphicOrderAt (fun x => f (x - c)) x = meromorphicOrderAt f (x - c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_erase_eq_of_not_compare_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {he : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false},
  ¬compare k (t.maxKey ⋯) = Ordering.eq → (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey he = t.maxKey ⋯
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonUnitalNonAssocSemiring : {R : Type u_1} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring (Lex R)
-- Mathlib.NumberTheory.WellApproximable
/-- A general version of **Dirichlet's approximation theorem**.

See also `AddCircle.exists_norm_nsmul_le`.  -/
NormedAddCommGroup.exists_norm_nsmul_le : ∀ {A : Type u_1} [inst : NormedAddCommGroup A] [CompactSpace A] [PreconnectedSpace A] [inst_3 : MeasurableSpace A]
  [BorelSpace A] {μ : MeasureTheory.Measure A} [μ.IsAddHaarMeasure] (ξ : A) {n : ℕ},
  0 < n → ∀ (δ : ℝ), μ Set.univ ≤ (n + 1) • μ (Metric.closedBall 0 (δ / 2)) → ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ δ
-- Aesop.Forward.LevelIndex
Aesop.instBEqLevelIndex.beq : Aesop.LevelIndex → Aesop.LevelIndex → Bool
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_lt_add_floor_translationNumber_add_one : ∀ (f : CircleDeg1Lift) (x : ℝ), f x < x + ↑⌊f.translationNumber⌋ + 1
-- Mathlib.Algebra.Free
_private.Mathlib.Algebra.Free.0.FreeMagma.liftAux.match_1.splitter : {α : Type u_1} →
  (motive : FreeMagma α → Sort u_2) →
    (x : FreeMagma α) → ((x : α) → motive (FreeMagma.of x)) → ((x y : FreeMagma α) → motive (x.mul y)) → motive x
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f),
  (CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor F sq sq₃).obj D =
    CategoryTheory.Pseudofunctor.DescentData'.ofDescentData sq sq₃ D
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instVAdd.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α], Lex.instVAdd = inst
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A **right-uniform additive group** is a topological additive group endowed with the associated
right uniform structure: the uniformity filter `𝓤 G` is the inverse image of `𝓝 0` by the map
`(x, y) ↦ y + (-x)`.

In other words, we declare that two points `x` and `y` are infinitely close
precisely when `y + (-x)` is infinitely close to `0`.  -/
IsRightUniformAddGroup : (G : Type u_7) → [UniformSpace G] → [AddGroup G] → Prop
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.Hopf.hopf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (self : CategoryTheory.Hopf C) → CategoryTheory.HopfObj self.X
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.mk.injEq : ∀ {X : SSet.Truncated 1} {n : ℕ}
  (vertex : Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 }))
  (arrow : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 }))
  (arrow_src :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.castSucc)
  (arrow_tgt :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.succ)
  (vertex_1 : Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 }))
  (arrow_1 : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 }))
  (arrow_src_1 :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow_1 i) =
        vertex_1 i.castSucc)
  (arrow_tgt_1 :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow_1 i) =
        vertex_1 i.succ),
  ({ vertex := vertex, arrow := arrow, arrow_src := arrow_src, arrow_tgt := arrow_tgt } =
      { vertex := vertex_1, arrow := arrow_1, arrow_src := arrow_src_1, arrow_tgt := arrow_tgt_1 }) =
    (vertex = vertex_1 ∧ arrow = arrow_1)
-- Lean.Parser.Extension
Lean.Parser.AliasValue.const.injEq : ∀ {α : Type} (p p_1 : α), (Lean.Parser.AliasValue.const p = Lean.Parser.AliasValue.const p_1) = (p = p_1)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.dist_le_mul_of_le : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β}
  {x y : α} {r : ℝ}, LipschitzWith K f → dist x y ≤ r → dist (f x) (f y) ≤ ↑K * r
-- Mathlib.Analysis.Matrix.Hermitian
/-- The diagonal elements of a complex Hermitian matrix are real.  -/
Matrix.IsHermitian.coe_re_apply_self : ∀ {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [inst : RCLike 𝕜],
  A.IsHermitian → ∀ (i : n), ↑(RCLike.re (A i i)) = A i i
-- Mathlib.Data.PFunctor.Univariate.M
/-- Internal definition for `M`. It is needed to avoid name clashes
between `M.mk` and `M.casesOn` and the declarations generated for
the structure  -/
PFunctor.MIntl : PFunctor.{uA, uB} → Type (max uA uB)
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.mem_range_algebraMap_iff_fixed : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K] (x : K),
  x ∈ Set.range ⇑(algebraMap k K) ↔ ∀ (f : Gal(K/k)), f x = x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- An `I : Ideal A` is homogeneous if for every `r ∈ I`, all homogeneous components
of `r` are in `I`.  -/
Ideal.IsHomogeneous : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            (𝒜 : ι → σ) → [inst_3 : DecidableEq ι] → [inst_4 : AddMonoid ι] → [GradedRing 𝒜] → Ideal A → Prop
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The submonoid of elements `x : M` such that `f x = g x`  -/
MonoidHom.eqLocusM : {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (M →* N) → (M →* N) → Submonoid M
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- A `C^n` function with compact support is Lipschitz.  -/
ContDiff.lipschitzWith_of_hasCompactSupport : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F']
  {f : E' → F'}, HasCompactSupport f → ContDiff 𝕂 n f → n ≠ 0 → ∃ C, LipschitzWith C f
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.below : {α : Type u_2} →
  {𝒜 : Set (Set α)} →
    {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop} →
      {a : Set α} → MeasureTheory.generateSetAlgebra 𝒜 a → Prop
-- Mathlib.Data.UInt
UInt32.toBitVec_injective : Function.Injective UInt32.toBitVec
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_left_pure : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto Int.ceil (nhdsWithin (↑n) (Set.Iic ↑n)) (pure n)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_neg_natCast_nonneg : ∀ (n : ℕ), 0 ≤ Real.log (-↑n)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.rfl : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β}, m.Equiv m
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.summand_smul_def' : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d),
  g • w =
    (Monoid.PushoutI.NormalWord.equivPair i).symm
      (let __src := (Monoid.PushoutI.NormalWord.equivPair i) w;
      { head := g * ((Monoid.PushoutI.NormalWord.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯,
        normalized := ⋯ })
-- Mathlib.Algebra.GroupWithZero.Defs
IsLeftCancelMulZero.to_noZeroDivisors : ∀ (M₀ : Type u_1) [inst : MulZeroClass M₀] [IsLeftCancelMulZero M₀], NoZeroDivisors M₀
-- Std.Internal.Do.Order.Basic
Lean.Order.right_le_join : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x y : α), Lean.Order.PartialOrder.rel y (Lean.Order.join x y)
-- Mathlib.Order.Nucleus
Nucleus.toFun_eq_coe : ∀ {X : Type u_1} [inst : SemilatticeInf X] (n : Nucleus X), n.toFun = ⇑n
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedMethods.default : Lean.Meta.Grind.Methods
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- An upper estimate on the complex distance between two points in terms of the hyperbolic distance
and the imaginary part of one of the points.  -/
UpperHalfPlane.dist_coe_le : ∀ (z w : UpperHalfPlane), dist ↑z ↑w ≤ w.im * (Real.exp (dist z w) - 1)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.bot_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}, S ∈ ⊥ X ↔ S = ⊤
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.instIsLeftCancelAddSubtypeLeOfNat : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [IsLeftCancelAdd α],
  IsLeftCancelAdd { x // 0 ≤ x }
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.unify : Lean.Meta.Sym.UnifyM.Context✝ → Bool
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Three points are collinear if and only if the first or third point equals the second or
the sine of the angle between three points is zero.  -/
EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0
-- Mathlib.Algebra.Order.Sub.Unbundled.Hom
le_mul_tsub : ∀ {R : Type u_3} [inst : Distrib R] [inst_1 : Preorder R] [inst_2 : Sub R] [OrderedSub R] [MulLeftMono R] {a b c : R},
  a * b - a * c ≤ a * (b - c)
-- Std.Time.DateTime.PlainDateTime
Std.Time.instLawfulEqOrdPlainDateTime : Std.LawfulEqOrd Std.Time.PlainDateTime
-- Lean.Linter.Sets
/-- Declare a new linter set by giving the set of options that will be enabled along with the set.  -/
Lean.Linter.«command_Register_linter_set_:=_» : Lean.ParserDescr
-- Lean.Data.PrefixTree
Lean.PrefixTree.forM : {m : Type → Type u_1} →
  {α : Type u_2} → {β : Type u_3} → {p : α → α → Ordering} → [Monad m] → Lean.PrefixTree α β p → (β → m Unit) → m Unit
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.ofUpperSet_symm : ∀ {α : Type u_1}, Topology.WithUpperSet.ofUpperSet.symm = Topology.WithUpperSet.toUpperSet
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk.inj : ∀ {α : Sort u_1} {β : Sort u_2} {toFun : α → β} {inj' : Function.Injective toFun} {toFun_1 : α → β}
  {inj'_1 : Function.Injective toFun_1},
  { toFun := toFun, inj' := inj' } = { toFun := toFun_1, inj' := inj'_1 } → toFun = toFun_1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (hxx' : x = x') {Z : CommRingCat}
  (h : X.presheaf.stalk x' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x') h)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Std.TransCmp cmp] {k : α}, t.toList.contains k = t.contains k
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.powers_eq_closure : ∀ {M : Type u_1} [inst : Monoid M] (n : M), Submonoid.powers n = Submonoid.closure {n}
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.index_powMonoidHom_ker : ∀ (G : Type u_2) [inst : CommGroup G] [IsCyclic G] [Finite G] (d : ℕ),
  (powMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxoHasSize : {n : ℕ} → Std.Rxo.HasSize (BitVec n)
-- Lean.Declaration
Lean.instInhabitedRecursorVal.default : Lean.RecursorVal
-- Init.Data.String.Lemmas.FindPos
String.posLT_toSlice : ∀ {s : String} {p : String.Pos.Raw} (h : 0 < p), s.toSlice.posLT p h = (s.posLT p h).toSlice
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.mul_self : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G] (x : G), x * x = 1
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) This new cone is used to construct the algebra structure  -/
CategoryTheory.Monad.ForgetCreatesLimits.newCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) →
            CategoryTheory.Limits.Cone (D.comp T.forget) → CategoryTheory.Limits.Cone (D.comp T.forget)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.Mono (CategoryTheory.Limits.image.lift F')
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Preconnected.coe : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Preconnected → H.coe.Preconnected
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul_comm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Data.Nat.Cast.Basic
Pi.instOfNat : {α : Type u_1} → {π : α → Type u_3} → (n : ℕ) → [(i : α) → OfNat (π i) n] → OfNat ((i : α) → π i) n
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.ne_zero_of_supDegree_ne_bot : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p : AddMonoidAlgebra R A}, AddMonoidAlgebra.supDegree D p ≠ ⊥ → p ≠ 0
-- Mathlib.Order.RelSeries
/-- Given two relations `r, s` on `α` such that `r ≤ s`, any relation series of `r` induces a relation
series of `s`
 -/
RelSeries.ofLE : {α : Type u_1} → {r : SetRel α α} → RelSeries r → {s : SetRel α α} → r ⊆ s → RelSeries s
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.continuous_iff_surjective : ∀ (f : CircleDeg1Lift), Continuous ⇑f ↔ Function.Surjective ⇑f
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.List.fixedLengthDigits.eq_1 : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ), List.fixedLengthDigits hb l = {L | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset
-- Std.Sat.AIG.Lemmas
/-- `AIG.mkAtom` never shrinks the underlying AIG.
 -/
Std.Sat.AIG.mkAtom_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (var : α),
  aig.decls.size ≤ (aig.mkAtom var).aig.decls.size
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.retract_r_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Idempotents.Karoubi C),
  X.retract.r.f = X.p
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.UnderMorphism.ext : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f g : U ⟶ V},
  CategoryTheory.Under.Hom.right f = CategoryTheory.Under.Hom.right g → f = g
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ A ⟹ X),
  CategoryTheory.MonoidalClosed.curry f = g ↔ f = CategoryTheory.MonoidalClosed.uncurry g
-- Batteries.Lean.Meta.Simp
/-- Construct a `Simp.DischargeWrapper` from the `Syntax` for a `simp` discharger.  -/
Lean.Meta.Simp.mkDischargeWrapper : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.Simp.DischargeWrapper
-- Init.Data.UInt.Lemmas
UInt8.le_of_lt : ∀ {a b : UInt8}, a < b → a ≤ b
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S) (x : S), ∃ p n, x * (Polynomial.aeval P.x) P.g ^ n = (Polynomial.aeval P.x) p
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFOn` is invariant under translation.  -/
meromorphicNFOn_comp_sub_const_iff_meromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicNFOn (f ∘ fun x => x - c) U ↔ MeromorphicNFOn f (U - {c})
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_self_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ‖z‖ * ‖z‖ = RCLike.normSq z
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- `b i` is the `i`th basis vector.  -/
OrthonormalBasis.instFunLike : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : Fintype ι] → FunLike (OrthonormalBasis ι 𝕜 E) ι E
-- Lean.Meta.Tactic.Grind.Inv
/-- Checks invariants if `grind.debug` is enabled.  -/
Lean.Meta.Grind.Goal.checkInvariants : Lean.Meta.Grind.Goal → optParam Bool false → Lean.Meta.Grind.GrindM Unit
-- Mathlib.Order.Grade
/-- A `Fin n`-graded order is also `ℕ`-graded. We do not mark this an instance because `n` is not
inferable.  -/
GradeOrder.finToNat : {α : Type u_3} → [inst : Preorder α] → (n : ℕ) → [GradeOrder (Fin n) α] → GradeOrder ℕ α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelComparison_comp_kernel_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] {X' Y' : C} [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] (g : X' ⟶ Y') [inst_7 : CategoryTheory.Limits.HasKernel g]
  [inst_8 : CategoryTheory.Limits.HasKernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y')
  (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
      (CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.map f g p q hpq))
      (CategoryTheory.Limits.kernelComparison g G)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_toSubmonoid : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (K : Subgroup G),
  (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_neg_right : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {x y : E}, inner A x (-y) = -inner A x y