mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_unit_right_left : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsUnit x → ∀ (y z : R), IsCoprime (y * x) z ↔ IsCoprime y z
-- Mathlib.Topology.Compactness.Lindelof
/-- In a Hereditarily Lindelöf space, `Set.univ` is a Hereditarily Lindelöf set.  -/
HereditarilyLindelofSpace.isHereditarilyLindelof_univ : ∀ {X : Type u_2} {inst : TopologicalSpace X} [self : HereditarilyLindelofSpace X], IsHereditarilyLindelof Set.univ
-- Mathlib.Data.Vector.Mem
List.Vector.mem_map_succ_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (b : β) (v : List.Vector α (n + 1)) (f : α → β),
  b ∈ (List.Vector.map f v).toList ↔ f v.head = b ∨ ∃ a ∈ v.tail.toList, f a = b
-- Mathlib.LinearAlgebra.Dimension.Finite
Set.finrank_empty : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Set.finrank R ∅ = 0
-- Lean.Meta.TryThis
/-- An option allowing the user to customize the ideal input width. Defaults to 100.
This option controls output format when
the output is intended to be copied back into a lean file  -/
Lean.Meta.Tactic.TryThis.format.inputWidth : Lean.Option ℕ
-- Std.Http.Data.URI.Basic
/-- Checks if a query parameter exists by raw key string. The key is percent-encoded before matching.
 -/
Std.Http.URI.Query.contains : Std.Http.URI.Query → String → Bool
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.hasExt_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  CategoryTheory.HasExt C ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          ((DerivedCategory.singleFunctor C 0).obj X ⟶
            (CategoryTheory.shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
/-- A multiseries is zero if it is the real constant `0` or has an empty sequence.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis → Prop
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- **Pair Reduction**: Given pseudometric spaces `T` and `E`, `c ≥ 0`, and a finite subset `J` of
`T` such that `|J| ≤ aⁿ` for some `a ≥ 0` and `n : ℕ`, `pair_reduction` states that there exists a
set `K ⊆ J²` such that for any function `f : T → E`:
1. `|K| ≤ a|J|`
2. `∀ (s, t) ∈ K, d(s, t) ≤ cn`
3. `sup_{s, t ∈ J : d(s, t) ≤ c} d(f(s), f(t)) ≤ 2 sup_{(s, t) ∈ K} d(f(s), f(t))`
 -/
EMetric.pair_reduction : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a : ENNReal} {n : ℕ} {J : Finset T},
  ↑J.card ≤ a ^ n →
    ∀ (c : ENNReal) (E : Type u_2) [inst_1 : PseudoEMetricSpace E],
      ∃ K ⊆ J ×ˢ J,
        ↑K.card ≤ a * ↑J.card ∧
          (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
            ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
-- Mathlib.Data.Nat.Init
Nat.AtLeastTwo.ne_one : ∀ {n : ℕ} [n.AtLeastTwo], n ≠ 1
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- Notation for identities up to unitors and associators.  -/
CategoryTheory.Bicategory.«term⊗𝟙» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] (c : C) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f { unmop := c }
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₁₂.τ₃ = g
-- Std.Net.Addr
Std.Net.instInhabitedSocketAddress : Inhabited Std.Net.SocketAddress
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- The isomorphism between the short complex attached to
two isomorphic distinguished triangles.  -/
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [hC : CategoryTheory.Pretriangulated C] →
              {T T' : CategoryTheory.Pretriangulated.Triangle C} →
                (e : T ≅ T') →
                  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) →
                    CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT ≅
                      CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T' ⋯
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The completion carries a uniform structure.  -/
AbstractCompletion.uniformStruct : {α : Type u} → [inst : UniformSpace α] → (self : AbstractCompletion.{v, u} α) → UniformSpace self.space
-- Init.Data.OfScientific
instOfNatFloat : {n : ℕ} → OfNat Float n
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_congr_set' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (y : 𝕜),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → (HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x)
-- Mathlib.Order.Partition.Equipartition
/-- An equipartition is a partition whose parts are all the same size, up to a difference of `1`.  -/
Finpartition.IsEquipartition : {α : Type u_1} → [inst : DecidableEq α] → {s : Finset α} → Finpartition s → Prop
-- Init.Data.Array.Zip
Array.zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, as.zip bs = Array.zipWith Prod.mk as bs
-- Lean.Elab.DeprecatedSyntax
Lean.Elab.SyntaxDeprecationEntry.mk.injEq : ∀ (kind : Lean.SyntaxNodeKind) (text? since? : Option String) (kind_1 : Lean.SyntaxNodeKind)
  (text?_1 since?_1 : Option String),
  ({ kind := kind, text? := text?, since? := since? } = { kind := kind_1, text? := text?_1, since? := since?_1 }) =
    (kind = kind_1 ∧ text? = text?_1 ∧ since? = since?_1)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andRight.injEq : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p : Mathlib.Tactic.ITauto.Proof) (ak_1 : Mathlib.Tactic.ITauto.AndKind)
  (p_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.andRight ak p = Mathlib.Tactic.ITauto.Proof.andRight ak_1 p_1) = (ak = ak_1 ∧ p = p_1)
-- Mathlib.Algebra.BigOperators.Fin
/-- For `f = (a₁, ..., aₙ)` in `αⁿ`, `partialSum f` is
`(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ)` in `αⁿ⁺¹`.  -/
Fin.partialSum : {M : Type u_2} → [AddMonoid M] → {n : ℕ} → (Fin n → M) → Fin (n + 1) → M
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.d_comp_d : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChains.d A (n + 1))
      (groupHomology.inhomogeneousChains.d A n) =
    0
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.visitedLevel : Lean.CollectLevelParams.State → Lean.LevelSet
-- Init.Data.SInt.Lemmas
ISize.ofInt_tmod : ∀ {a b : ℤ},
  ISize.minValue.toInt ≤ a →
    a ≤ ISize.maxValue.toInt →
      ISize.minValue.toInt ≤ b → b ≤ ISize.maxValue.toInt → ISize.ofInt (a.tmod b) = ISize.ofInt a % ISize.ofInt b
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.ofIso_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {M : C} [inst_4 : CategoryTheory.MonObj M] {X : D} {N : C} [inst_5 : CategoryTheory.MonObj N] (e₁ : M ≅ N)
  [inst_6 : CategoryTheory.IsMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [inst_7 : CategoryTheory.ModObj M X],
  CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom e₁.inv e₂.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul e₂.hom)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.HasTwoOutOfThreeProperty], W.op.HasTwoOutOfThreeProperty
-- Mathlib.Analysis.Matrix.Order
/-- **Alias** of the reverse direction of `Matrix.nonneg_iff_posSemidef`. -/
Matrix.PosSemidef.nonneg : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] {A : Matrix n n 𝕜}, A.PosSemidef → 0 ≤ A
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsNonloop.contractElem_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {I : Set α},
  M.IsNonloop e → ((M.contract {e}).Indep I ↔ e ∉ I ∧ M.Indep (insert e I))
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.mk : ∀ {F : Type u_3} {α : outParam (Type u_4)} {β : outParam (Type u_5)} [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : FunLike F α β], (∀ (f : F), Isometry ⇑f) → IsometryClass F α β
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_left_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (x + y * z) y ↔ IsCoprime x y
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Init.Data.Array.Lemmas
Array.getElem_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {ys : Array β} {f : α → β → γ} {i : ℕ}
  (hi : i < (Array.zipWith f xs ys).size), (Array.zipWith f xs ys)[i] = f xs[i] ys[i]
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addZeroClass : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddZeroClass α] → AddZeroClass (Matrix m n α)
-- Mathlib.FieldTheory.Normal.Closure
normalClosure_def : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L], IntermediateField.normalClosure F K L = ⨆ f, f.fieldRange
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.mk.sizeOf_spec : ∀ (imports : Array Lean.Import) (pos : String.Pos.Raw) (badModifier : Bool) (error? : Option String)
  (isModule isMeta isExported importAll : Bool),
  sizeOf
      { imports := imports, pos := pos, badModifier := badModifier, error? := error?, isModule := isModule,
        isMeta := isMeta, isExported := isExported, importAll := importAll } =
    1 + sizeOf imports + sizeOf pos + sizeOf badModifier + sizeOf error? + sizeOf isModule + sizeOf isMeta +
        sizeOf isExported +
      sizeOf importAll
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_le_valuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v ≤
    (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.

`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.find?` always terminates after finitely many steps.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none`
 -/
Std.Iter.find? : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → (β → Bool) → Option β
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.totalDegree_zero_iff_isHomogeneous : ∀ (σ : Type u_1) {R : Type u_3} [inst : CommSemiring R] {p : MvPolynomial σ R}, p.totalDegree = 0 ↔ p.IsHomogeneous 0
-- Mathlib.NumberTheory.PrimeCounting
Nat.one_lt_of_mem_primesBelow : ∀ {p n : ℕ}, p ∈ n.primesBelow → 1 < p
-- Mathlib.Topology.Category.Locale
Locale.coe_of : ∀ (α : Type u_1) [inst : Order.Frame α], ↑(Opposite.unop (Locale.of α)) = α
-- Mathlib.Condensed.Discrete.Colimit
/-- A presheaf `F`, which takes a profinite set written as a cofiltered limit to the corresponding
colimit, is isomorphic to the presheaf `LocallyConstant - F(*)`.
 -/
Condensed.isoLocallyConstantOfIsColimit : (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] →
    ((S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) →
      (F ≅
        Condensed.locallyConstantPresheaf
          (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1})))))
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_iSup_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Sort u_4} {U : Submodule 𝕜 E} {V : ι → Submodule 𝕜 E}, U ⟂ iSup V ↔ ∀ (i : ι), U ⟂ V i
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(I * J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∪ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
-- Mathlib.Topology.Homeomorph.Quotient
/-- The quotient by the trivial relation is homeomorphic to the original space.  -/
Homeomorph.quotientBot : {X : Type u_1} → [inst : TopologicalSpace X] → Quotient ⊥ ≃ₜ X
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.iso_hom_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimage.π f))
      (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom =
    CategoryTheory.Abelian.coimage.π (F.map f)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound.sizeOf_spec : ∀ (h : Lean.Expr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound h) = 1 + sizeOf h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).isEmpty = false →
        ((t.alter k f).maxKey! = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.union_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.Limits.pullback.fst f g)) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Restrict the codomain of a non-unital star algebra homomorphism `f` to `f.range`.

This is the bundled version of `Set.rangeFactorization`.  -/
NonUnitalStarAlgHom.rangeRestrict : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [inst_8 : NonUnitalAlgHomClass F R A B] →
                          [inst_9 : StarHomClass F A B] → (f : F) → A →⋆ₙₐ[R] ↥(NonUnitalStarAlgHom.range f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
act_rel_act_of_rel_of_rel : ∀ {N : Type u_2} {r : N → N → Prop} {mu : N → N → N} [IsTrans N r] [i : CovariantClass N N mu r]
  [i' : CovariantClass N N (Function.swap mu) r] {a b c d : N}, r a b → r c d → r (mu a c) (mu b d)
-- Qq.MetaM
Qq.MaybeDefEq.defEq : {u : Lean.Level} →
  {α :
      let u := u;
      Q(Sort u)} →
    {a b : Q(«$α»)} → «$a» =Q «$b» → Qq.MaybeDefEq a b
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Delaborator for `Finset.sum`. The `pp.funBinderTypes` option controls whether
to show the domain type when the sum is over `Finset.univ`.  -/
BigOperators.delabFinsetSum : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNormEssSup_const_smul_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3} [inst : NormedRing 𝕜]
  {ε : Type u_4} [inst_1 : TopologicalSpace ε] [inst_2 : ESeminormedAddMonoid ε] [inst_3 : SMul 𝕜 ε]
  [ENormSMulClass 𝕜 ε] {c : 𝕜} {f : α → ε},
  MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * MeasureTheory.eLpNormEssSup f μ
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.normal_kleinFour : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Nat.card α = 4 → (alternatingGroup.kleinFour α).Normal
-- Mathlib.Geometry.Manifold.DerivationBundle
PointedContMDiffMap.smul_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M) (f : PointedContMDiffMap 𝕜 I M (↑⊤) x) (k : 𝕜),
  f • k = f x * k
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  ↑((CategoryTheory.PreGaloisCategory.endEquivSectionsFibers F) f) A =
    (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instHasSizeInt_1 : Std.Rxo.HasSize ℤ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.D : Std.Time.GenericFormat.DateBuilder✝ → Option (Sigma Std.Time.Day.Ordinal.OfYear)
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetsResponse.mk.inj : ∀ {widgets widgets_1 : Array Lean.Widget.PanelWidgetInstance},
  { widgets := widgets } = { widgets := widgets_1 } → widgets = widgets_1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.add_left : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] {s t : Set α}, t.Nontrivial → s.Nonempty → (s + t).Nontrivial
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq : κ)
  (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le._auto_1)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le._auto_3),
  data.i₀ r' pq ⋯ ≤ data.i₀ r pq ⋯
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.add : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂)[k] = m₁[k]
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isBot : ℕ → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_X_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.coeff 1 = 1
-- Mathlib.Analysis.Normed.Field.Basic
norm_commutator_sub_one_le : ∀ {α : Type u_2} [inst : NormedDivisionRing α] {a b : α},
  a ≠ 0 → b ≠ 0 → ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖
-- Mathlib.Algebra.Ring.Action.Basic
/-- Scalar multiplication distributes across multiplication  -/
MulSemiringAction.smul_mul : ∀ {M : Type u} {R : Type v} {inst : Monoid M} {inst_1 : Semiring R} [self : MulSemiringAction M R] (g : M) (x y : R),
  g • (x * y) = g • x * g • y
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.Internal.idOpaque : {α : Sort u_1} → { f // f = id }
-- Mathlib.RingTheory.DedekindDomain.Dvr
IsDedekindDomainDvr.is_dvr_at_nonzero_prime : ∀ {A : Type u_1} {inst : CommRing A} {inst_1 : IsDomain A} [self : IsDedekindDomainDvr A] (P : Ideal A),
  P ≠ ⊥ → ∀ (x : P.IsPrime), IsDiscreteValuationRing (Localization.AtPrime P)
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The `a`-torsion submodule is an `a`-torsion module.  -/
Submodule.torsionBy_isTorsionBy : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Module.IsTorsionBy R (↥(Submodule.torsionBy R M a)) a
-- Mathlib.Topology.Algebra.Group.Basic
exists_nhds_split_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s : Set G},
  s ∈ nhds 1 → ∃ V ∈ nhds 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.ext : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι}
  {x y : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕}, (∀ (i : ι), x i = y i) → x = y
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.self_le_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulLeftMono α] {a : α}, a ≤ 1 → a ≤ a⁻¹