mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_lt_one_iff : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ}, n ≠ 0 → (x ^ n < 1 ↔ x < 1)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeft_map_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  {X Y : CategoryTheory.MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapLeft R l hl).map f).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right
-- Lean.Declaration
Lean.ConstantInfo.inductInfo.inj : ∀ {val val_1 : Lean.InductiveVal}, Lean.ConstantInfo.inductInfo val = Lean.ConstantInfo.inductInfo val_1 → val = val_1
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {n : ℕ}, ⊤.lowerCentralSeries n = ⊥ ↔ AddSubgroup.upperCentralSeries G n = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The homotopy.  -/
SSet.RelativeMorphism.Homotopy.h : {X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        {f g : SSet.RelativeMorphism A B φ} →
          f.Homotopy g → (CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- Alternative description of `χ₄ n` for odd `n : ℕ` in terms of powers of `-1`  -/
ZMod.χ₄_eq_neg_one_pow : ∀ {n : ℕ}, n % 2 = 1 → ZMod.χ₄ ↑n = (-1) ^ (n / 2)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_map_real : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (f : ℝ →+*o K) (r : ℝ),
  ArchimedeanClass.stdPart (f r) = r
-- Mathlib.Algebra.Star.Pointwise
Set.iUnion_star : ∀ {α : Type u_1} {ι : Sort u_2} [inst : Star α] (s : ι → Set α), star (⋃ i, s i) = ⋃ i, star (s i)
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_coe : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H) (g : G), f.completion ↑g = ↑(f g)
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.opOp_symm_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : Aᵐᵒᵖᵐᵒᵖ),
  (AlgEquiv.opOp R A).symm a = MulOpposite.unop (MulOpposite.unop a)
-- Mathlib.GroupTheory.Divisible
Pi.rootableBy : {ι : Type u_3} →
  {β : Type u_4} →
    (B : ι → Type u_5) →
      [inst : (i : ι) → Pow (B i) β] →
        [inst_1 : Zero β] →
          [inst_2 : (i : ι) → Monoid (B i)] → [(i : ι) → RootableBy (B i) β] → RootableBy ((i : ι) → B i) β
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_strictMono_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f → StrictMono (AddSubsemigroup.map f)
-- Init.Data.Random
/-- Seeds the random number generator state used by `IO.rand`.
 -/
IO.setRandSeed : ℕ → BaseIO Unit
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState.mk.injEq : ∀ (map : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns) (eqns : Lean.PHashSet Lean.Name)
  (map_1 : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns) (eqns_1 : Lean.PHashSet Lean.Name),
  ({ map := map, eqns := eqns } = { map := map_1, eqns := eqns_1 }) = (map = map_1 ∧ eqns = eqns_1)
-- Init.Data.SInt.Lemmas
Int64.neg_ofInt : ∀ {n : ℤ}, -Int64.ofInt n = Int64.ofInt (-n)
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Consider, for each `x` in a set `s`, a radius `r x ∈ (0, 1]`. Then one can find finitely
many disjoint balls of the form `closedBall x (r x)` covering a proportion `1/(N+1)` of `s`, if
there are no satellite configurations with `N+1` points.
 -/
Besicovitch.exist_finset_disjoint_balls_large_measure : ∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {N : ℕ} {τ : ℝ},
  1 < τ →
    IsEmpty (Besicovitch.SatelliteConfig α N τ) →
      ∀ (s : Set α) (r : α → ℝ),
        (∀ x ∈ s, 0 < r x) →
          (∀ x ∈ s, r x ≤ 1) →
            ∃ t,
              ↑t ⊆ s ∧
                μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧
                  (↑t).PairwiseDisjoint fun x => Metric.closedBall x (r x)
-- Mathlib.Data.Fin.Tuple.Take
/-- Taking the first `m ≤ n` elements of an `addCases u v`, where `u` is an `n`-tuple, is the same
as taking the first `m` elements of `u`.  -/
Fin.take_addCases_left : ∀ {n n' : ℕ} {motive : Fin (n + n') → Sort u_2} (m : ℕ) (h : m ≤ n) (u : (i : Fin n) → motive (Fin.castAdd n' i))
  (v : (i : Fin n') → motive (Fin.natAdd n i)), (Fin.take m ⋯ fun i => Fin.addCases u v i) = Fin.take m h u
-- Mathlib.CategoryTheory.Sites.Point.Conservative
/-- [Stacks Tag 00YL](https://stacks.math.columbia.edu/tag/00YL) ((2)) -/
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ (A : Type u') [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
      [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
      [inst_4 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory A FC]
      [(CategoryTheory.forget A).ReflectsIsomorphisms]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.HasWeakSheafify J A]
      [CategoryTheory.Limits.HasProducts A], CategoryTheory.JointlyReflectEpimorphisms fun Φ => Φ.obj.sheafFiber
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coeMonoidHom_injective`. -/
SlashInvariantForm.coeHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β], Function.Injective ⇑(FunLike.coeMonoidHom F α β)
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.instDecidableMemOfDecidableLEOfDecidableLT : {α : Type u} →
  {r : Std.Roc α} → {a : α} → [inst : LE α] → [DecidableLE α] → [inst_2 : LT α] → [DecidableLT α] → Decidable (a ∈ r)
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- A measure is said to be `IsOpenPosMeasure` if it is positive on nonempty open sets.  -/
MeasureTheory.Measure.IsOpenPosMeasure : {X : Type u_1} → [TopologicalSpace X] → {m : MeasurableSpace X} → MeasureTheory.Measure X → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_mul_bmod_self_right : ∀ (a b : ℤ) (c : ℕ), (a + -(b * ↑c)).bmod c = a.bmod c
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {R : Type u_9} [inst_5 : NormedRing R]
  [inst_6 : Module R F] [inst_7 : IsBoundedSMul R F] [inst_8 : SMulCommClass 𝕜 R F] {c : R},
  HasFPowerSeriesOnBall f pf x r → HasFPowerSeriesOnBall (c • f) (c • pf) x r
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.cast_eq_of_cons_eq_cons : ∀ {U : Type u_1} [inst : Quiver U] {u v v' w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w}
  {e' : v' ⟶ w} (h : p.cons e = p'.cons e'), Quiver.Path.cast ⋯ ⋯ p = p'
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_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.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.sumSMulInv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Fintype G] {X : FDRep k G} (v : ↑X.V) (f : G → k),
  (TannakaDuality.FiniteGroup.sumSMulInv v) f = ∑ s, f s • (X.ρ s⁻¹) v
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.insertMany_list_eq_foldl : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β}
  {l : List (α × β)}, ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l) = List.foldl (fun a b => a.insert b.1 b.2) m l
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.zero_inv : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k], 0⁻¹ = 0
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPushoutsAlong.hasPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y}
  [self : P.HasPushoutsAlong f] {W : C} (g : X ⟶ W), P g → CategoryTheory.Limits.HasPushout g f
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof) →
      ((t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof) → t.below → motive_2 t) → motive_2 t ×' t.below
-- Init.System.IO
/-- A monad that supports arbitrary side effects and throwing exceptions of type `IO.Error`.
 -/
IO : Type → Type
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.swap.eq_1 : ∀ (R : Type u_1) {n : Type u_2} [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq n] (i j : n),
  Matrix.swap R i j = Equiv.Perm.permMatrix R (Equiv.swap i j)
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.norm_mk' : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (p : E), ‖SeparationQuotient.mk p‖ = ‖p‖
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- The map from `𝒜 0` to the degree `0` part of `𝒜ₓ` sending `f ↦ f/1`.  -/
HomogeneousLocalization.fromZeroRingHom : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                (𝒜 : ι → σ) → [inst_5 : GradedRing 𝒜] → (x : Submonoid A) → ↥(𝒜 0) →+* HomogeneousLocalization 𝒜 x
-- Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup
/-- `PSL(n, R)` is the projective special linear group `SL(n, R)/Z(SL(n, R))`.  -/
MatrixGroups.«termPSL(_,_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.vertexSubgroup : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C),
  S.IsNormal → ∀ (c : C) (cS : c ∈ S.objs), (S.vertexSubgroup cS).Normal
-- Mathlib.Logic.Function.FromTypes
/-- The definitional equality between `![]`-ary heterogeneous functions into `τ` and `τ`.  -/
Function.fromTypes_nil_equiv : (τ : Type u) → Function.FromTypes ![] τ ≃ τ
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.completeSpace : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  [ContinuousSMul 𝕜₂ F] [CompleteSpace F] {𝔖 : Set (Set E)},
  Topology.IsCoherentWith 𝔖 → ⋃₀ 𝔖 = Set.univ → CompleteSpace (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.toEquiv_homeomorphProd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  (WithLp.homeomorphProd p α β).toEquiv = WithLp.equiv p (α × β)
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The coend of a bifunctor valued in `Type`, defined as a quotient.  -/
CategoryTheory.Limits.Types.coend : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u))) → Type (max w u)
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_forIn'_loop : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : Array α)
  (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (i : ℕ) (h : i ≤ as.size) (b : β),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.forIn'.loop as (f x) i h b
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  a ∈ (HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).source
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.min! ∈ t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.ExtTreeMap.unitOfList l cmp).getKey? k' = some k
-- Mathlib.Data.Multiset.ZeroCons
Multiset.lt_iff_cons_le : ∀ {α : Type u_1} {s t : Multiset α}, s < t ↔ ∃ a, a ::ₘ s ≤ t
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ProjRestricts.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i),
  Profinite.NobelingProof.ProjRestricts C h =
    ⇑(Homeomorph.setCongr ⋯) ∘ Profinite.NobelingProof.ProjRestrict (Profinite.NobelingProof.π C K) J
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α}
  {h : k ∈ Std.ExtDHashMap.Const.unitOfList l}, Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.unitOfList l) k h = ()
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The forgetful map from `NonUnitalSubalgebra` to `Submodule` as an `OrderEmbedding`  -/
NonUnitalSubalgebra.toSubmodule' : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → NonUnitalSubalgebra R A ↪o Submodule R A
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.centerAndRescale.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ),
  a.centerAndRescale =
    { c := fun i => (a.r (Fin.last N))⁻¹ • (a.c i - a.c (Fin.last N)), r := fun i => (a.r (Fin.last N))⁻¹ * a.r i,
      rpos := ⋯, h := ⋯, hlast := ⋯, inter := ⋯ }
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.image_ι_op_comp_imageUnopOp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.unop).op (CategoryTheory.imageUnopOp g).hom =
    CategoryTheory.Limits.factorThruImage g
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.algebraBase_injective : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsDomain A]
  [IsFractionRing A K], Function.Injective ⇑(algebraMap A (CyclotomicRing n A K))
-- Mathlib.Algebra.GroupWithZero.Basic
mul_right_surjective₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → Function.Surjective fun g => g * a
-- Mathlib.Order.CompleteLattice.Basic
iSup_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] (f : β → γ → α),
  ⨆ i, ⨆ j, f i j = ⨆ x, f x.1 x.2
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_univ' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, nhdsSetWithin Set.univ s = Filter.principal s
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat : ∀ (X : AlgebraicGeometry.Scheme), QuasiSober ↥X
-- Lean.Parser.Command
Lean.Parser.Command.initializeKeyword.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).get! a =
        if h : compare k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get! a
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientQuotientEquivQuotientAux_mk : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M)
  (x : G ⧸ N),
  (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientAddGroup.map N M (AddMonoidHom.id G) h) x
-- Mathlib.Order.SuccPred.Archimedean
antitone_of_succ_le : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f (Order.succ a) ≤ f a) → Antitone f
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- `F` is lax monoidal given a unit morphism `ε : 𝟙_ D ⟶ F.obj (𝟙_ C))` and a tensorator
`μ : F - ⊗ F - ⟶ F (- ⊗ -)` as a natural transformation between bifunctors, satisfying the
relevant compatibilities.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (ε :
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (μ :
                    CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                      CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                  CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap μ =
                      CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap μ →
                    CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ F =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ ε)
                          (CategoryTheory.CategoryStruct.comp
                            (μ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                            (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ F)) →
                      CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ F =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ ε)
                            (CategoryTheory.CategoryStruct.comp
                              (((CategoryTheory.flipFunctor C C D).map μ).app
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                              (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ F)) →
                        F.LaxMonoidal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.erase : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α), m₁.Equiv m₂ → (m₁.erase k).Equiv (m₂.erase k)
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerSeries.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] (a : ℕ → E), PadicInt.mahlerSeries a = ∑' (n : ℕ), PadicInt.mahlerTerm (a n) n
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientMulEquivOfEq.eq_1 : ∀ {G : Type u} [inst : Group G] {M N : Subgroup G} [inst_1 : M.Normal] [inst_2 : N.Normal] (h : M = N),
  QuotientGroup.quotientMulEquivOfEq h = { toEquiv := Subgroup.quotientEquivOfEq h, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ext_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj adj' : G ⊣ F},
  adj.counit = adj'.counit → adj = adj'
-- Mathlib.Order.Category.Semilat
/-- The category of inf-semilattices with a top element.  -/
SemilatInfCat : Type (u + 1)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.inv_hom_id_eval_assoc : ∀ {C : Type u_1} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.GradedObject J C}
  (e : X ≅ Y) (j : J) {Z : C} (h : Y j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv j) (CategoryTheory.CategoryStruct.comp (e.hom j) h) = h
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.coe_toOrderHom : ∀ {α : Type u_2} [inst : Preorder α] (c : OmegaCompletePartialOrder.Chain α), ⇑c.toOrderHom = ⇑c
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMulticospan_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F)
  {X Y : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape} (x : X ⟶ Y),
  f.mapMulticospan.map x =
    match X, Y, x with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) =>
      CategoryTheory.Limits.WalkingMulticospan.Hom.id
        (match x with
        | CategoryTheory.Limits.WalkingMulticospan.left i => CategoryTheory.Limits.WalkingMulticospan.left (f.s₀ i)
        | CategoryTheory.Limits.WalkingMulticospan.right i => CategoryTheory.Limits.WalkingMulticospan.right (f.s₁' i))
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.fst i =>
      CategoryTheory.Limits.WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.snd i =>
      CategoryTheory.Limits.WalkingMulticospan.Hom.snd (f.s₁' i)