mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₂_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂), ¬c₂.Rel i₂ (c₂.next i₂) → K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.liftOn₂_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α : Type u_3} (f : M × ↥S → M × ↥S → α) (wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q') (m m' : M)
  (s s' : ↥S), (LocalizedModule.mk m s).liftOn₂ (LocalizedModule.mk m' s') f wd = f (m, s) (m', s')
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_toEnd_of_isNilpotent : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsNilpotent L M] (x : L), IsNilpotent ((LieModule.toEnd R L M) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- `e : Edge x₀ x₁` is a composition of `e` with `Edge.id x₁`  -/
SSet.Edge.CompStruct.compId : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → (e : SSet.Edge x₀ x₁) → e.CompStruct (SSet.Edge.id x₁) e
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instHasFiniteLimitsProEt : ∀ (S : AlgebraicGeometry.Scheme), CategoryTheory.Limits.HasFiniteLimits S.ProEt
-- Mathlib.Computability.RE
ComputablePred.decide : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  ComputablePred p → Computable fun a => decide (p a)
-- Lean.Meta.Match.Basic
/-- `Syntax` object for providing position information  -/
Lean.Meta.Match.Alt.ref : Lean.Meta.Match.Alt → Lean.Syntax
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix₃_eq_apply : ∀ {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
  {F :
    (a : α) →
      (b : β a) →
        (c : γ a b) →
          ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c},
  WellFounded R →
    ∀ {a : α} {b : β a} {c : γ a b},
      WellFounded.extrinsicFix₃ R F a b c = F a b c fun a_1 b_1 c_1 x => WellFounded.extrinsicFix₃ R F a_1 b_1 c_1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.unique : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α} {x y : α} [Std.TransCmp cmp],
  RBTree.RBNode.Ordered cmp t → x ∈ t → y ∈ t → cmp x y = Ordering.eq → x = y
-- Lean.Syntax
Lean.Syntax.ifNodeKind : {β : Sort u_1} → Lean.Syntax → Lean.SyntaxNodeKind → (Lean.SyntaxNode → β) → (Unit → β) → β
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E},
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      (IsSymmSndFDerivWithinAt 𝕜 f s x ↔
        ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x) =
          iteratedFDerivWithin 𝕜 2 f s x)
-- Batteries.Data.UInt
UInt64.toNat_max : ∀ (x y : UInt64), (x ⊔ y).toNat = max x.toNat y.toNat
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext₂_left_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y Z : C}
  {g h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y)
          g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y)
          h
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instInfSet : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → InfSet (ClosedSubmodule R M)
-- Lean.Meta.LetToHave
/-- Transforms nondependent `let` expressions into `have` expressions.
If `e` is not type correct, returns `e`.
The `Meta.letToHave` trace class logs errors and messages.
 -/
Lean.Meta.letToHave : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_map_hom : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  {j j' : J} (f : j ⟶ j'),
  ((CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).map f).hom = CategoryTheory.Limits.colim.map (F.map f)
-- Mathlib.RingTheory.Trace.Defs
/-- The trace map from `R` to itself is the identity map.  -/
Algebra.trace_self : ∀ {R : Type u_1} [inst : CommRing R], Algebra.trace R R = LinearMap.id
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_iff_getValueCast?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {v : β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → (⟨k, v⟩ ∈ l ↔ Std.Internal.List.getValueCast? k l = some v)
-- Mathlib.Order.Hom.Bounded
TopHom.instMax : {α : Type u_2} →
  {β : Type u_3} → [inst : Top α] → [inst_1 : SemilatticeSup β] → [inst_2 : OrderTop β] → Max (TopHom α β)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N : CategoryTheory.Mat_ C} (f g : M ⟶ N), (∀ (i : M.ι) (j : N.ι), f i j = g i j) → f = g
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map_le_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ),
  CategoryTheory.Functor.OfSequence.map f i (i + 1) ⋯ = f i
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.dvd_iff_mod_eq_zero : ∀ {a b : Ordinal.{u_4}}, b ∣ a ↔ a % b = 0
-- Mathlib.Algebra.Group.Defs
mul_inv_rev : ∀ {G : Type u_1} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
-- Mathlib.Topology.Homotopy.Lifting
/-- Choosing an arbitrary basepoint `e ∈ f ⁻¹' {x}` induces a bijection `f ⁻¹' {x} ≃ G`, and the
`G`-action on `f ⁻¹' {x}` corresponds to left multiplication. The monodromy action commutes
with the `G`-action, so each monodromy must corresponds must correspond to a right multiplication.
 -/
IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} →
          {G : Type u_4} →
            [inst_2 : AddGroup G] →
              [inst_3 : AddAction G E] →
                IsAddQuotientCoveringMap p G → {x : X} → ↑(p ⁻¹' {x}) → FundamentalGroup X x →* (Multiplicative G)ᵐᵒᵖ
-- Init.Data.ByteArray.Lemmas
ByteArray.size_append : ∀ {a b : ByteArray}, (a ++ b).size = a.size + b.size
-- Mathlib.Data.Multiset.Filter
Multiset.filter_cons : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
  Multiset.filter p (a ::ₘ s) = (if p a then {a} else 0) + Multiset.filter p s
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.postcomposeId`.

---

Postcomposing by the identity does not change the cone up to isomorphism.  -/
CategoryTheory.Limits.Cones.postcomposeId : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.id F) ≅
            CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)
-- Init.Data.UInt.Lemmas
UInt64.toFin_mul : ∀ (a b : UInt64), (a * b).toFin = a.toFin * b.toFin
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of `Asymptotics.IsBigOTVS.isBigO`.

---

**Alias** of the forward direction of `Asymptotics.isBigOTVS_iff_isBigO`. -/
Asymptotics.isBigOTVS.isBigO : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =O[𝕜; l] g → f =O[l] g
-- Mathlib.Geometry.Polygon.Basic
/-- A polygon has nondegenerate edges if adjacent vertices are distinct.  -/
Polygon.HasNondegenerateEdges : {P : Type u_3} → {n : ℕ} → Polygon P n → Prop
-- Init.WFExtrinsicFix
/-- The function implemented as the loop
`opaqueFix₂ R F a b = F a b (fun a' b' _ => opaqueFix₂ R F a' b')`.
`opaqueFix₂ R F` is the fixpoint of the functional `F`, as long as the loop is
well-founded.

The loop might run forever depending on `F`. It is opaque, i.e., it is impossible to prove
nontrivial properties about it.
 -/
_private.Init.WFExtrinsicFix.0.WellFounded.opaqueFix₂ : {α : Sort u_1} →
  {β : α → Sort u_2} →
    {C₂ : (a : α) → β a → Sort u_3} →
      [∀ (a : α) (b : β a), Nonempty (C₂ a b)] →
        (R : (a : α) ×' β a → (a : α) ×' β a → Prop) →
          ((a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) →
            (a : α) → (b : β a) → C₂ a b
-- Mathlib.RingTheory.AdicCompletion.Exactness
AdicCompletion.AdicCauchySequence.mk.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f f_1 : ℕ → M) (e_f : f = f_1) (h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]),
  AdicCompletion.AdicCauchySequence.mk I M f h = AdicCompletion.AdicCauchySequence.mk I M f_1 ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.isOrtho_smul_left : ∀ {R₄ : Type u_7} {M₄ : Type u_8} [inst : CommRing R₄] [IsDomain R₄] [inst_2 : AddCommGroup M₄] [inst_3 : Module R₄ M₄]
  {G : LinearMap.BilinForm R₄ M₄} {x y : M₄} {a : R₄}, a ≠ 0 → (G.IsOrtho (a • x) y ↔ G.IsOrtho x y)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_empty : ∀ {m n : ℤ}, n < m → (m...=n).toArray = #[]
-- Mathlib.Logic.Relation
Relation.ReflTransGen.cases_tail : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α},
  Relation.ReflTransGen r a b → b = a ∨ ∃ c, Relation.ReflTransGen r a c ∧ r c b
-- Mathlib.Order.WithBot
WithTop.denselyOrdered_iff : ∀ {α : Type u_1} [inst : LT α] [NoMaxOrder α], DenselyOrdered (WithTop α) ↔ DenselyOrdered α
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.biInter_gt_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) (r : ℝ),
  ⋂ r', ⋂ (_ : r' > r), Metric.closedBall x r' = Metric.closedBall x r
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.coe_subtype : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [inst_2 : NonUnitalSubsemiringClass S R] (s : S), ⇑(NonUnitalSubsemiringClass.subtype s) = Subtype.val
-- Mathlib.Analysis.Convex.Basic
convex_iff_openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E} [ZeroLEOneClass 𝕜],
  Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.nonempty_unique : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (self : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y),
  Nonempty (Unique (W₁.MapFactorizationData W₂ f))
-- Lean.Linter.Init
/-- Returns true if `msg` was produced by `Lean.Linter.logLint` (and therefore by a linter).  -/
Lean.MessageData.isLinterMessage : Lean.MessageData → Bool
-- Lean.Meta.MethodSpecs
Lean.MethodSpecsAttrData.clsName : Lean.MethodSpecsAttrData → Lean.Name
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange f).hom
      (AlgebraicGeometry.Scheme.Hom.opensRange f).ι =
    f
-- Lean.Declaration
Lean.RecursorVal.toConstantVal : Lean.RecursorVal → Lean.ConstantVal
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The complements of the upper closures of finite sets are a collection of lower sets
which form a basis for the lower topology.  -/
Topology.IsLower.lowerBasis : (α : Type u_3) → [Preorder α] → Set (Set α)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tmod : ∀ (a b n : ℤ), (a * b).tmod n = (a.tmod n * b.tmod n).tmod n
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.isClosedEmbedding_hom : ∀ (R A : CommRingCat) [inst : TopologicalSpace ↑R] [IsTopologicalRing ↑R] [T1Space ↑R],
  Topology.IsClosedEmbedding fun f => ⇑(CommRingCat.Hom.hom f)
-- Mathlib.Data.Sym.Sym2.Finsupp
/-- The composition of a `Finsupp` with `Sym2.mul` as a `Finsupp`.  -/
Finsupp.sym2Mul : {α : Type u_1} → {M₀ : Type u_2} → [inst : CommMonoidWithZero M₀] → (α →₀ M₀) → Sym2 α →₀ M₀
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.zero_def : ∀ (α : Type u_2), 0 = FirstOrder.Language.Constants.term FirstOrder.Ring.zeroFunc
-- Mathlib.SetTheory.Ordinal.Notation
ONote.scale_eq_mul : ∀ (x : ONote) [x.NF] (o : ONote) [o.NF], x.scale o = x.oadd 1 0 * o
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The action on a valuation subring corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
ValuationSubring.pointwiseHasSMul : {K : Type u} →
  [inst : Field K] → {G : Type u_1} → [inst_1 : Group G] → [MulSemiringAction G K] → SMul G (ValuationSubring K)
-- Init.Data.Int.Order
Int.lt_or_gt_of_ne : ∀ {a b : ℤ}, a ≠ b → a < b ∨ b < a
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivAtFilter.const_smul` -/
HasDerivAtFilter.fun_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasDerivAtFilter f f' L → HasDerivAtFilter (fun i => c • f i) (c • f') L
-- Std.Http.Data.Status
Std.Http.Status.insufficientStorage.sizeOf_spec : sizeOf Std.Http.Status.insufficientStorage = 1
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- The equivalence `IsTerminal X ≃ Unique (ToType X)` if the forgetful functor
preserves and reflects terminals.  -/
CategoryTheory.Limits.Concrete.terminalIffUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
              [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
                (X : C) → CategoryTheory.Limits.IsTerminal X ≃ Unique (CategoryTheory.ToType X)
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.comm : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s t : Set X), SeparatedNhds s t ↔ SeparatedNhds t s
-- Mathlib.Order.Cover
Set.OrdConnected.apply_wcovBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
  (Set.range ⇑f).OrdConnected → (f a ⩿ f b ↔ a ⩿ b)
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Ioo_eq_nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → nhdsWithin b (Set.Ioo b a) = nhdsWithin b (Set.Ioi b)
-- Init.GrindInstances.ToInt
Lean.Grind.instAddUInt8UintOfNatNat : Lean.Grind.ToInt.Add UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedRing.toNorm : {α : Type u_5} → [self : SeminormedRing α] → Norm α
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.utf8Len.match_1.splitter : (motive : List Char → Sort u_1) →
  (x : List Char) → (Unit → motive []) → ((c : Char) → (cs : List Char) → motive (c :: cs)) → motive x
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.modifyₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (f : β a → β a), m.modifyₘ a f = m.alterₘ a fun x => Option.map f x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.addCommSemigroup.eq_1 : ∀ {α : Type u_2} [inst : AddCommSemigroup α],
  Set.addCommSemigroup = { toAddSemigroup := Set.addSemigroup, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_subtype_lt : ∀ {α : Type u_1} [Finite α] {p : α → Prop} {x : α}, ¬p x → Nat.card { x // p x } < Nat.card α
-- Mathlib.RingTheory.Multiplicity
/-- **Alias** of the reverse direction of `dvd_iff_multiplicity_pos`. -/
Dvd.multiplicity_pos : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → 0 < multiplicity a b
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.norm_irreducible_pos : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] {ϖ : ↥(Valued.integer K)},
  Irreducible ϖ → 0 < ‖ϖ‖
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.snd.comp AddMonoid.Coprod.inr = AddMonoidHom.id N
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.op_adj₁ : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.op.adj₁ = q.adj₃.op
-- Init.Omega.IntList
Lean.Omega.IntList.set_cons_succ : ∀ {x : ℤ} {xs : List ℤ} {i : ℕ} {y : ℤ}, Lean.Omega.IntList.set (x :: xs) (i + 1) y = x :: Lean.Omega.IntList.set xs i y
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative.property : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} {f : X ⟶ Y},
  CategoryTheory.MorphismProperty.relative F P f →
    ∀ ⦃a b : C⦄ (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a),
      CategoryTheory.IsPullback fst (F.map snd) f g → P snd
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.rightFractionRel_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (z₁ z₂ : W.LeftFraction X Y),
  CategoryTheory.MorphismProperty.RightFractionRel z₁.op z₂.op ↔ CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `pi_comparison G f` is an isomorphism, then `G` preserves the limit of `f`.  -/
CategoryTheory.Limits.PreservesProduct.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
/-- `QuadraticMap.toBilin` as an S-linear map  -/
QuadraticMap.toBilinHom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [LinearOrder ι] →
          [inst : CommRing R] →
            [inst_1 : AddCommGroup M] →
              [inst_2 : AddCommGroup N] →
                [inst_3 : Module R M] →
                  [inst_4 : Module R N] →
                    (S : Type u_5) →
                      [inst_5 : CommSemiring S] →
                        [inst_6 : Algebra S R] →
                          [inst_7 : Module S N] →
                            [inst_8 : IsScalarTower S R N] →
                              Module.Basis ι R M → QuadraticMap R M N →ₗ[S] LinearMap.BilinMap R M N
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
MulEquiv.ofBijective.congr_simp : ∀ {M : Type u_9} {N : Type u_10} {F : Type u_11} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f f_1 : F) (e_f : f = f_1) (hf : Function.Bijective ⇑f),
  MulEquiv.ofBijective f hf = MulEquiv.ofBijective f_1 ⋯
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.to_raw_eq : ∀ {α : Type u} {a : α} {n : ℤ} [inst : Ring α], Mathlib.Meta.NormNum.IsInt a n → a = n.rawCast
-- Mathlib.NumberTheory.Padics.PadicNumbers
instRingPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Ring ℚ_[p]
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.le_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  J₁ ≤ J₂ ↔ ⇑J₁ ≤ ⇑J₂
-- Mathlib.Order.WellFounded
/-- A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`.  -/
StrictMono.id_le : ∀ {β : Type u_2} [inst : LinearOrder β] [WellFoundedLT β] {f : β → β}, StrictMono f → id ≤ f
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.geometricallyIntegral_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.GeometricallyIntegral f ↔ AlgebraicGeometry.geometrically AlgebraicGeometry.IsIntegral f
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.getUnsolvedGoals : Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instPartialOrder : {α : Type u_1} → [inst : CompleteLattice α] → PartialOrder (CompleteSublattice α)