mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Lemmas
AddSubmonoid.IsLocalizationMap.surj_pi_of_finite : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {ι : Type u_4} [Finite ι] [inst : AddCommMonoid M]
  [inst_1 : AddCommMonoid N] [inst_2 : FunLike F M N] [AddHomClass F M N] {f : F} {S : AddSubmonoid M},
  S.IsLocalizationMap ⇑f → ∀ (n : ι → N), ∃ s x, ∀ (i : ι), n i + f ↑s = f (x i)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive] (F G : U.Coalgebra) (α : F ⟶ G), (-α).f = -α.f
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasLeftHomology]
  [inst_6 : F.PreservesLeftHomologyOf S] {Z : D} (h : F.obj S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.mapCyclesIso F).hom (CategoryTheory.CategoryStruct.comp (F.map S.iCycles) h) =
    CategoryTheory.CategoryStruct.comp (S.map F).iCycles h
-- Mathlib.Tactic.TermCongr
/-- Throw an internal error.  -/
Mathlib.Tactic.TermCongr.throwCongrEx : {α : Type} → Lean.Expr → Lean.Expr → Lean.MessageData → Lean.MetaM α
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.ext_evalₐ : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {x y : AdicCompletion I R},
  (∀ (n : ℕ), (AdicCompletion.evalₐ I n) x = (AdicCompletion.evalₐ I n) y) → x = y
-- Mathlib.Data.PNat.Find
/-- The `PNat` version of `Nat.findX`  -/
PNat.findX : {p : ℕ+ → Prop} → [DecidablePred p] → (∃ n, p n) → { n // p n ∧ ∀ m < n, ¬p m }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.ite.injEq : ∀ (ref : Lean.Syntax) (h? : Option Lean.Elab.Term.Do.Var) (optIdent cond : Lean.Syntax)
  (thenBranch elseBranch : Lean.Elab.Term.Do.Code) (ref_1 : Lean.Syntax) (h?_1 : Option Lean.Elab.Term.Do.Var)
  (optIdent_1 cond_1 : Lean.Syntax) (thenBranch_1 elseBranch_1 : Lean.Elab.Term.Do.Code),
  (Lean.Elab.Term.Do.Code.ite ref h? optIdent cond thenBranch elseBranch =
      Lean.Elab.Term.Do.Code.ite ref_1 h?_1 optIdent_1 cond_1 thenBranch_1 elseBranch_1) =
    (ref = ref_1 ∧
      h? = h?_1 ∧ optIdent = optIdent_1 ∧ cond = cond_1 ∧ thenBranch = thenBranch_1 ∧ elseBranch = elseBranch_1)
-- Init.Data.Fin.Bitwise
Fin.xor_val_of_uSizeSize : ∀ (a b : Fin USize.size), ↑(a ^^^ b) = ↑a ^^^ ↑b
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_sum`. -/
SkewMonoidAlgebra.ofFinsupp_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : AddCommMonoid k']
  (f : G →₀ k) (g : G → k → G' →₀ k'), { coeff := f.sum g } = { coeff := f }.sum fun x1 x2 => { coeff := g x1 x2 }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β},
  m.WF → (m.alter k f).getKeyD k fallback = if (f m[k]?).isSome = true then k else fallback
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isLE_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X : C}, CategoryTheory.Limits.IsZero X → ∀ (n : ℤ), t.IsLE X n
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation S hkf hcc fac).iso =
    CategoryTheory.Iso.refl
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).H
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForwardIsoPost_inv_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) (f : CategoryTheory.Over X)
  (X_1 : CategoryTheory.Over f),
  (CategoryTheory.Over.iteratedSliceForwardIsoPost X f).inv.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Over.mk (CategoryTheory.Over.Hom.left X_1.hom))
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPushforward : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (AlgebraicGeometry.Scheme.Modules.pushforward f).IsRightAdjoint
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.Measure.trim.congr_simp : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α),
  μ = μ_1 → ∀ (hm : m ≤ m0), μ.trim hm = μ_1.trim hm
-- Mathlib.Topology.Compactness.Bases
/-- If `X` has a basis consisting of compact opens, then an open set in `X` is compact open iff
it is a finite union of some elements in the basis  -/
isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] (b : ι → Set X),
  TopologicalSpace.IsTopologicalBasis (Set.range b) →
    (∀ (i : ι), IsCompact (b i)) → ∀ (U : Set X), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
-- Init.GrindInstances.Ring.Rat
Lean.Grind.instIsCharPRatOfNatNat : Lean.Grind.IsCharP ℚ 0
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg : ∀ (pq : ℕ × ℕ), CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat.deg pq = -↑pq.1 - ↑pq.2
-- Mathlib.Probability.Kernel.Posterior
/-- For a deterministic kernel `κ`, `κ ∘ₖ κ†μ` is `μ.map f`-a.e. equal to the identity kernel.  -/
ProbabilityTheory.deterministic_comp_posterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [MeasurableSpace.CountablyGenerated 𝓧] {f : Ω → 𝓧} (hf : Measurable f),
  ⇑((ProbabilityTheory.Kernel.deterministic f hf).comp
        (ProbabilityTheory.posterior (ProbabilityTheory.Kernel.deterministic f hf) μ)) =ᵐ[MeasureTheory.Measure.map f μ]
    ⇑ProbabilityTheory.Kernel.id
-- Lean.DocString.Add
Lean.VersoDocResult.mk.inj : ∀ {toVersoDocString : Lean.VersoDocString} {deferredChecks : Array Lean.Doc.DeferredCheck}
  {toVersoDocString_1 : Lean.VersoDocString} {deferredChecks_1 : Array Lean.Doc.DeferredCheck},
  { toVersoDocString := toVersoDocString, deferredChecks := deferredChecks } =
      { toVersoDocString := toVersoDocString_1, deferredChecks := deferredChecks_1 } →
    toVersoDocString = toVersoDocString_1 ∧ deferredChecks = deferredChecks_1
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_of_le_one`. -/
Ordinal.principal_add_of_le_one : ∀ {o : Ordinal.{u}}, o ≤ 1 → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instHasSolidNorm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [inst_3 : HasSolidNorm β] [inst_4 : IsOrderedAddMonoid β], HasSolidNorm (BoundedContinuousFunction α β)
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- **Alias** of `PowerSeries.coeff_derivative`. -/
PowerSeries.coeff_derivativeFun : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
  (PowerSeries.coeff n) ((PowerSeries.derivative R) f) = (PowerSeries.coeff (n + 1)) f * (↑n + 1)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addCommGroup.eq_1 : ∀ {M : Type u_4} [inst : AddCommGroup M] (c : AddCon M), c.addCommGroup = { toAddGroup := c.addGroup, add_comm := ⋯ }
-- Mathlib.Data.Int.SuccPred
Int.pred_eq_pred : Order.pred = Int.pred
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {Φ₁ Φ₂ : J.Point} (f : Φ₁ ⟶ Φ₂) (P : CategoryTheory.Functor Cᵒᵖ A),
  (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f).app P =
    Φ₂.presheafFiberDesc (fun X x => Φ₁.toPresheafFiber X ((CategoryTheory.ConcreteCategory.hom (f.hom.app X)) x) P) ⋯
-- Mathlib.RingTheory.Localization.Defs
Localization.sub_mk : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (a c : R) (b d : ↥M),
  Localization.mk a b - Localization.mk c d = Localization.mk (↑d * a - ↑b * c) (b * d)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_withReader_MonadWithReader_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadWithReaderOf ρ m] (f : ρ → ρ) (x : m α),
  Std.Internal.Do.wp (withReader f x) post epost = Std.Internal.Do.wp (MonadWithReaderOf.withReader f x) post epost
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `G` is a codetector if the functor `C(-, G)` reflects isomorphisms.  -/
CategoryTheory.IsCodetector : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_hom_apply_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X_1 : Cᵒᵖ)
  (x : (F.op.comp (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X))).obj X_1),
  ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftYonedaCompWhiskeringLeft.hom.app X).app X_1)) x).down =
    hF.preimage x.down
-- Aesop.Tree.Data
Aesop.GoalRef : Type
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_id_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      CategoryTheory.AddMonObj.zero
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.pi_toSubsemiring : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] (s : Set ι) (t : (i : ι) → Subalgebra R (S i)),
  (Subalgebra.pi s t).toSubsemiring =
    { carrier := (Submodule.pi s fun i => Subalgebra.toSubmodule (t i)).carrier, mul_mem' := ⋯, one_mem' := ⋯,
      add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsNonloopAt.not_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsNonloopAt e x → ∀ (y : α), ¬G.IsLoopAt e y
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSMul.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α], OrderDual.instSMul = inst
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.StrongTrans G H) {a b c : B} {a' : C}
  (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h) (θ.app c)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f
          (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f
            (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft f
              (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.whiskerRight (θ.naturality g).hom (H.map h)))
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ \ m₂).getKey? k = if k ∈ m₂ then none else m₁.getKey? k
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CochainComplex.singleFunctor.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n n_1 : ℤ),
  n = n_1 → CochainComplex.singleFunctor C n = CochainComplex.singleFunctor C n_1
-- Mathlib.MeasureTheory.Function.EssSup
essInf_mono_ae : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f g : α → β},
  f ≤ᵐ[μ] g →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) essInf_mono_ae._auto_1 →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) g) essInf_mono_ae._auto_3 →
        essInf f μ ≤ essInf g μ
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.cokernel_π_ext : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N) {x y : ↑N} (m : ↑M),
  x = y + (CategoryTheory.ConcreteCategory.hom f) m →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) y
-- Lean.Parser.Term
/-- `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.  -/
Lean.Parser.Term.attrKind : Lean.Parser.Parser
-- Lean.SubExpr
/-- Decodes a subexpression `Pos` as a sequence of coordinates `cs : Array Nat`. See `Pos.ofArray` for details.
`cs[0]` is the coordinate for the root expression.  -/
Lean.SubExpr.Pos.toArray : Lean.SubExpr.Pos → Array ℕ
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.sheafToPresheaf_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.sheafToPresheaf J A) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.sheafToPresheaf J A).obj X)
        ((CategoryTheory.sheafToPresheaf J A).obj Y))
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M),
  f.ker = ⊥ ↔ Function.Injective ⇑f
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instUnionOfTransCmp : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Union (Std.ExtDTreeMap α β cmp)
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.mem_closure_of_mem : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M}, x ∈ s → x ∈ SemigroupIdeal.closure s
-- Mathlib.Data.ENat.BigOperators
ENat.sum_iSup : ∀ {α : Type u_1} {ι : Type u_2} {s : Finset α} {f : α → ι → ℕ∞},
  (∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) → ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mopFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (unmop : C),
  (CategoryTheory.mopFunctor C).obj unmop = { unmop := unmop }
-- Mathlib.Data.List.Sigma
List.NodupKeys.pairwise_ne : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)}, l.NodupKeys → List.Pairwise (fun s s' => s.fst ≠ s'.fst) l
-- Mathlib.Topology.Closure
interior.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), interior s = ⋃₀ {t | IsOpen t ∧ t ⊆ s}
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} (𝕜 : Type u_3) [inst_3 : RCLike 𝕜] {F : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure Ω}
  {μ : MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω 𝕜),
      Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))
-- Mathlib.Topology.Order.Basic
induced_topology_eq_preorder : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace β] [OrderTopology β]
  {f : α → β},
  (∀ {x y : α}, f x < f y ↔ x < y) →
    (∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y) →
      (∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b) →
        TopologicalSpace.induced f inst_2 = Preorder.topology α
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?.go.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → ((x : Ordering) → (x = Ordering.lt → False) → motive x) → motive x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `f : M × S → α` respects the equivalence relation `LocalizedModule.r`, then
`f` descents to a map `LocalizedModule M S → α`.
 -/
LocalizedModule.liftOn : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      {M : Type v} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {α : Type u_3} → LocalizedModule S M → (f : M × ↥S → α) → (∀ (p p' : M × ↥S), p ≈ p' → f p = f p') → α
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toCoalgHom : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      {B : Type u_7} →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → A →ₗc[R] B
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`, or panics if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.Const.get! : {α : Type u} → {δ : Type w} → [Ord α] → [Inhabited δ] → (Std.DTreeMap.Internal.Impl α fun x => δ) → α → δ
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Equiv.toHomeomorphOfDiscrete.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X]
  [inst_3 : DiscreteTopology Y] (e e_1 : X ≃ Y), e = e_1 → e.toHomeomorphOfDiscrete = e_1.toHomeomorphOfDiscrete
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_inv_left_iff : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute (↑u⁻¹) a ↔ Commute (↑u) a
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensorObj_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
-- Init.ShareCommon
ShareCommon.instNonemptyState : ∀ {σ : ShareCommon.StateFactory}, Nonempty (ShareCommon.State σ)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitLeftOpIsoUnopColimit F).hom
      (CategoryTheory.Limits.colimit.ι F j).unop =
    CategoryTheory.Limits.limit.π F.leftOp (Opposite.op j)
-- Batteries.Data.List.Perm
List.isSubperm.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α), l₁.isSubperm l₂ = decide (∀ x ∈ l₁, List.count x l₁ ≤ List.count x l₂)
-- Mathlib.FieldTheory.SeparableDegree
Field.instInhabitedEmb : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → Inhabited (Field.Emb F E)
-- Mathlib.Analysis.InnerProductSpace.Defs
PreInnerProductSpace.Core.mk : {𝕜 : Type u_4} →
  {F : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          (toInner : Inner 𝕜 F) →
            (∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y) →
              (∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x)) →
                (∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z) →
                  (∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y) →
                    PreInnerProductSpace.Core 𝕜 F
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.lift_pure : ∀ {m : Type u → Type v} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n} {lift : ⦃α : Type u⦄ → m α → n α}
  [self : Std.Internal.LawfulMonadLiftFunction lift] {α : Type u} (a : α), lift (pure a) = pure a
-- Mathlib.LinearAlgebra.Matrix.WithConv
convMul_def : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Mul α] (x y : WithConv (Matrix m n α)),
  x * y = WithConv.toConv (x.ofConv.hadamard y.ofConv)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.incl_obj_I : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : C),
  ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I = PUnit.{w + 1}
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- We compute the absolute discriminant of a `p`-th cyclotomic field where `p` is prime.  -/
IsCyclotomicExtension.Rat.discr_prime : ∀ (p : ℕ) (K : Type u) [inst : Field K] [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p} ℚ K], NumberField.discr K = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)