mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- A version of `setIntegral_rnDeriv_smul` that requires both measures to be σ-finite,
but doesn't require `s` to be a measurable set.  -/
MeasureTheory.setIntegral_rnDeriv_smul' : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {E : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [MeasureTheory.SigmaFinite μ] {f : α → E} [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν → ∀ (s : Set α), ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.le.inj : ∀ {lhs rhs : ℕ} {proof : Lean.Expr} {lhs_1 rhs_1 : ℕ} {proof_1 : Lean.Expr},
  Mathlib.Tactic.Order.AtomicFact.le lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.le lhs_1 rhs_1 proof_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Given a submodules basis, the basis elements as open additive subgroups in the associated
topology.  -/
SubmodulesBasis.openAddSubgroup : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : Nonempty ι] → {B : ι → Submodule R M} → (hB : SubmodulesBasis B) → ι → OpenAddSubgroup M
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.addSubmonoidClosure_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], AddSubmonoid.closure {x | ∃ m r, x = MonoidAlgebra.single m r} = ⊤
-- Mathlib.Topology.Algebra.Constructions
/-- The additive units of a monoid are equipped with a topology, via the embedding into `M × M`.  -/
AddUnits.instTopologicalSpaceAddUnits : {M : Type u_1} → [TopologicalSpace M] → [inst : AddMonoid M] → TopologicalSpace (AddUnits M)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.hasMeasurablePow : MeasurablePow ℂ ℂ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts of shape `J` if it preserves biproducts of `f` for every
`f : J → C`.  -/
CategoryTheory.Limits.PreservesBiproductsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            Type w₁ → (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.Analysis.Convolution
/-- A sufficient condition to prove that `f ⋆[L, μ] g` exists.
We assume that the integrand has compact support and `g` is bounded on this support (note that
both properties hold if `g` is continuous with compact support). We also require that `f` is
integrable on the support of the integrand, and that both functions are strongly measurable.

This is a variant of `BddAbove.convolutionExistsAt'` in an abelian group with a left-invariant
measure. This allows us to state the boundedness and measurability of `g` in a more natural way.  -/
BddAbove.convolutionExistsAt : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddCommGroup G]
  [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd₂ G] [MeasureTheory.SFinite μ] {x₀ : G} {s : Set G},
  BddAbove ((fun i => ‖g i‖) '' (fun t => x₀ - t) ⁻¹' s) →
    MeasurableSet s →
      (Function.support fun t => (L (f t)) (g (x₀ - t))) ⊆ s →
        MeasureTheory.IntegrableOn f s μ →
          MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.ConvolutionExistsAt f g x₀ L μ
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.mk.inj : ∀ {α β σ : Type} {name : autoParam Lean.Name Lean.PersistentEnvExtensionDescrCore.name._autoParam} {mkInitial : IO σ}
  {addImportedFn : Array (Array α) → Lean.ImportM σ} {addEntryFn : σ → β → σ}
  {exportEntriesFnEx : Lean.Environment → σ → Lean.OLeanEntries (Array α)} {statsFn : σ → Std.Format}
  {asyncMode : Lean.EnvExtension.AsyncMode} {replay? : Option (Lean.ReplayFn σ)}
  {name_1 : autoParam Lean.Name Lean.PersistentEnvExtensionDescrCore.name._autoParam} {mkInitial_1 : IO σ}
  {addImportedFn_1 : Array (Array α) → Lean.ImportM σ} {addEntryFn_1 : σ → β → σ}
  {exportEntriesFnEx_1 : Lean.Environment → σ → Lean.OLeanEntries (Array α)} {statsFn_1 : σ → Std.Format}
  {asyncMode_1 : Lean.EnvExtension.AsyncMode} {replay?_1 : Option (Lean.ReplayFn σ)},
  { name := name, mkInitial := mkInitial, addImportedFn := addImportedFn, addEntryFn := addEntryFn,
        exportEntriesFnEx := exportEntriesFnEx, statsFn := statsFn, asyncMode := asyncMode, replay? := replay? } =
      { name := name_1, mkInitial := mkInitial_1, addImportedFn := addImportedFn_1, addEntryFn := addEntryFn_1,
        exportEntriesFnEx := exportEntriesFnEx_1, statsFn := statsFn_1, asyncMode := asyncMode_1,
        replay? := replay?_1 } →
    name = name_1 ∧
      mkInitial = mkInitial_1 ∧
        addImportedFn = addImportedFn_1 ∧
          addEntryFn = addEntryFn_1 ∧
            exportEntriesFnEx = exportEntriesFnEx_1 ∧
              statsFn = statsFn_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1
-- Lean.Data.Json.Elab
/-- Allows to use Json syntax in a Lean file.  -/
Lean.Json.«termJson%_» : Lean.ParserDescr
-- Mathlib.Algebra.Category.Ring.Limits
/-- We show that the forgetful functor `CommSemiRingCat ⥤ SemiRingCat` creates limits.

All we need to do is notice that the limit point has a `CommSemiring` instance available,
and then reuse the existing limit.
 -/
CommSemiRingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommSemiRingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomLeft : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] {d d' : D} (f : d ⟶ d') (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c = (F.obj c).map f
-- Mathlib.Data.Analysis.Topology
instInhabitedRealizerEmptyCollectionSet : {α : Type u_1} → [inst : TopologicalSpace α] → Inhabited (Compact.Realizer ∅)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.goal.injEq : ∀ (ctx : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) (g : Lean.MVarId) (ctx_1 : Lean.Elab.ContextInfo)
  (lctx_1 : Lean.LocalContext) (g_1 : Lean.MVarId),
  (Lean.Widget.EmbedFmt.goal✝ ctx lctx g = Lean.Widget.EmbedFmt.goal✝ ctx_1 lctx_1 g_1) =
    (ctx = ctx_1 ∧ lctx = lctx_1 ∧ g = g_1)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `α →*o β` is the type of functions `α → β` that preserve the ordered monoid structure.

`OrderMonoidHom` is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over `(f : α →*o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N] (f : F)`.  -/
OrderMonoidHom : (α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → [MulOneClass α] → [MulOneClass β] → Type (max u_6 u_7)
-- Mathlib.Topology.Category.Stonean.Basic
Profinite.projective_of_extrDisc : ∀ {X : Profinite}, ExtremallyDisconnected ↑X.toTop → CategoryTheory.Projective X
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The coefficients of a presentation are the coefficients of the relations.  -/
Algebra.Presentation.coeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Set R
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : { w // w.IsComplex }),
  (NumberField.mixedEmbedding.indexEquiv K) (Sum.inr (w, 1)) = NumberField.ComplexEmbedding.conjugate (↑w).embedding
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Internal.iter_roo_eq_iter_rco_of_isSome_succ? : ∀ {α : Type u} [LT α] [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {lo hi : α}
  (h : (Std.PRange.succ? lo).isSome = true),
  (Std.Roo.Internal.iter lo<...hi) = Std.Rco.Internal.iter ((Std.PRange.succ? lo).get h)...hi
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.map_mono : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {F : Type u_3}
  [inst_2 : FunLike F R S] (f : F) {I J : TwoSidedIdeal R}, I ≤ J → TwoSidedIdeal.map f I ≤ TwoSidedIdeal.map f J
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_iff`. -/
Set.diff_subset_iff : ∀ {α : Type u_1} {s t u : Set α}, s \ t ⊆ u ↔ s ⊆ t ∪ u
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, (m.insertManyIfNewUnit l).size ≤ m.size + l.length
-- Mathlib.Data.Rat.Floor
Rat.IsRat.isInt_round : ∀ {R : Type u_3} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (n : ℤ) (d : ℕ) (res : ℤ),
  round (↑n / ↑d) = res → Mathlib.Meta.NormNum.IsRat r n d → Mathlib.Meta.NormNum.IsInt (round r) res
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.edgeSet_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).edgeSet = Sym2.map ⇑f '' p.edgeSet
-- Mathlib.MeasureTheory.Measure.Support
/-- A point `x` is in the support of measure `μ` iff any neighborhood of `x` contains a
subset with positive measure.  -/
MeasureTheory.Measure.mem_support_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {x : X},
  x ∈ μ.support ↔ ∃ᶠ (u : Set X) in (nhds x).smallSets, 0 < μ u
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.Equivalence.congrFullSubcategory_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D)
  [inst_2 : Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P),
  (e.congrFullSubcategory h).unitIso =
    (P.fullyFaithfulι.whiskeringRight P.FullSubcategory).preimageIso (P.ι.isoWhiskerLeft e.unitIso)
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_left_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.instModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecAbPresheafOp : {R : CommRingCat} →
  {M : (AlgebraicGeometry.Spec R).Modules} →
    {U : (AlgebraicGeometry.Spec R).Opens} → Module ↑R ↑(M.presheaf.obj (Opposite.op U))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, (m.getKey? a).isSome = true ↔ a ∈ m
-- Mathlib.Algebra.Group.AddChar
AddChar.mk.inj : ∀ {A : Type u_1} {inst : AddMonoid A} {M : Type u_2} {inst_1 : Monoid M} {toFun : A → M}
  {map_zero_eq_one' : toFun 0 = 1} {map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b} {toFun_1 : A → M}
  {map_zero_eq_one'_1 : toFun_1 0 = 1} {map_add_eq_mul'_1 : ∀ (a b : A), toFun_1 (a + b) = toFun_1 a * toFun_1 b},
  { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } =
      { toFun := toFun_1, map_zero_eq_one' := map_zero_eq_one'_1, map_add_eq_mul' := map_add_eq_mul'_1 } →
    toFun = toFun_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Applying an affine map to an affine combination of two points yields an affine combination of
the images.  -/
Convex.combo_affine_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {x y : E} {a b : 𝕜} {f : E →ᵃ[𝕜] F},
  a + b = 1 → f (a • x + b • y) = a • f x + b • f y
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent : ∀ {R : Type u_1} {r : R} [inst : Semiring R] (n : ℕ), IsNilpotent r → IsNilpotent (Polynomial.C r * Polynomial.X ^ n)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.mk.inj : ∀ {α : Type} {inst : DecidableEq α} {inst_1 : Hashable α} {decls : Array (Std.Sat.AIG.Decl α)} {idx max : ℕ}
  {map : Std.HashMap α ℕ} {inv1 : Std.Sat.AIG.RelabelNat.State.Inv1 max map}
  {inv2 : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map} {max_1 : ℕ} {map_1 : Std.HashMap α ℕ}
  {inv1_1 : Std.Sat.AIG.RelabelNat.State.Inv1 max_1 map_1} {inv2_1 : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map_1},
  { max := max, map := map, inv1 := inv1, inv2 := inv2 } =
      { max := max_1, map := map_1, inv1 := inv1_1, inv2 := inv2_1 } →
    max = max_1 ∧ map = map_1
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.isClosedEmbedding_coe : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [DiscreteTopology A] [ContinuousAdd B] [T2Space B],
  Topology.IsClosedEmbedding DFunLike.coe
-- Init.Data.SInt.Lemmas
Int8.ofIntLE.eq_1 : ∀ (i : ℤ) (_hl : Int8.minValue.toInt ≤ i) (_hr : i ≤ Int8.maxValue.toInt), Int8.ofIntLE i _hl _hr = Int8.ofInt i
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?_mem_ub : ∀ {α : Type u_1} {cut : α → Ordering} {ub : Option α} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.upperBound? cut t ub = some x → x ∈ t ∨ ub = some x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- `baseChange` as an `AlgHom`.  -/
Module.End.baseChangeHom : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Module.End R M →ₐ[R] Module.End A (TensorProduct R A M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentHighlight : Lean.ToJson Lean.Lsp.DocumentHighlight
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq : (x x_1 : Std.Tactic.BVDecide.BVUnOp) → Decidable (x = x_1)
-- Mathlib.Combinatorics.Matroid.Dual
/-- Given `M : Matroid α`, the `IndepMatroid α` whose independent sets are
the subsets of `M.E` that are disjoint from some base of `M`  -/
Matroid.dualIndepMatroid : {α : Type u_1} → Matroid α → IndepMatroid α
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
Finset.nsmul_right_strictMono : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {X : Finset G},
  0 ∈ X → (↑(AddSubgroup.closure ↑X)).Infinite → StrictMono fun n => n • X
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_uIcc : ∀ (x y : NNReal), NNReal.toReal '' Set.uIcc x y = Set.uIcc ↑x ↑y
-- Mathlib.Data.Part
/-- The bind operation has value `g (f.get)`, and is defined when all the
parts are defined.  -/
Part.bind : {α : Type u_1} → {β : Type u_2} → Part α → (α → Part β) → Part β
-- Mathlib.Data.List.Basic
List.forall_cons : ∀ {α : Type u} (p : α → Prop) (x : α) (l : List α), List.Forall p (x :: l) ↔ p x ∧ List.Forall p l
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.X_eq_normalize : ∀ {R : Type u} [inst : CommRing R] [inst_1 : NoZeroDivisors R] [inst_2 : NormalizationMonoid R],
  Polynomial.X = normalize Polynomial.X
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatTrans.isIso_iff_isIso_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G), CategoryTheory.IsIso τ ↔ ∀ (X : C), CategoryTheory.IsIso (τ.app X)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.cantor' : ∀ (a : Cardinal.{u_1}) {b : Cardinal.{u_1}}, 1 < b → a < b ^ a
-- Mathlib.Analysis.Matrix.Order
Matrix.nonneg_iff_posSemidef : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] {A : Matrix n n 𝕜}, 0 ≤ A ↔ A.PosSemidef
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_exp_pos : ∀ {a₁ a₂ : ℕ} (n : ℕ), 0 < a₁ → 0 < a₂ → 0 < a₁ ^ n * a₂
-- Mathlib.Order.Hom.Basic
/-- Copy of an `OrderHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
OrderHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (f : α →o β) → (f' : α → β) → f' = ⇑f → α →o β
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.lift.eq_1 : ∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G],
  Algebra.GrothendieckGroup.lift =
    { toFun := fun f => (Localization.monoidOf ⊤).lift ⋯, invFun := fun f => f.comp Algebra.GrothendieckGroup.of,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.cons_toList : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i)
  (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  (Monoid.PushoutI.NormalWord.cons g w hmw hgr).toList = ⟨i, ↑(⋯.equiv (g * (φ i) w.head)).2⟩ :: w.toList
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.termπ_ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_eq_zero_iff : ∀ (s : ℝ), Real.Gamma s = 0 ↔ ∃ m, s = -↑m
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_mono_right_of_nonneg : ∀ {G : Type uG} {x : G} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] {f g g' : G → ℝ},
  MeasureTheory.ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ) μ →
    (∀ (x : G), 0 ≤ f x) →
      (∀ (x : G), g x ≤ g' x) →
        (∀ (x : G), 0 ≤ g' x) →
          MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x ≤
            MeasureTheory.convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) μ x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getD k' fallback =
    if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
-- Lean.Meta.Sym.Canon
/-- Canonicalize `e` by normalizing types, instances, and support arguments.
Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions;
eta reduction is applied only inside types. Instances are re-synthesized.
Runs at reducible transparency.
 -/
Lean.Meta.Sym.canon : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.CategoryTheory.Yoneda
/-- Taking the `unop` of morphisms is a natural isomorphism.  -/
CategoryTheory.Coyoneda.objOpOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) → CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X)) ≅ CategoryTheory.yoneda.obj X
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.continuousOn_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj), ContinuousOn proj e.source
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instSetLike.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instSetLike = { coe := UpperSet.carrier, coe_injective := ⋯ }
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertList.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l toInsert : List ((a : α) × β a)),
  Std.Internal.List.insertList l toInsert =
    match toInsert with
    | [] => l
    | ⟨k, v⟩ :: toInsert => Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) toInsert
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.exists_egirth_eq_length : ∀ {α : Type u_1} {G : SimpleGraph α}, (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunction : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ} {c : ℕ → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
      (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
        HasFPowerSeriesOnBall (UpperHalfPlane.cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag_insert : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ),
  (insert a s).finsuppAntidiag n =
    (Finset.HasAntidiagonal.antidiagonal n).biUnion fun p =>
      Finset.map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (z : A → A → (CategoryTheory.CatCenter C)ˣ) →
            autoParam (z 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam →
              autoParam (∀ (a b c : A), z (a + b) c * z a b = z a (b + c) * z b c)
                  CategoryTheory.TwistShiftData.assoc._autoParam →
                autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z a b)) A)
                    CategoryTheory.TwistShiftData.commShift._autoParam →
                  CategoryTheory.TwistShiftData C A
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_succ_right_eq_cons_map : ∀ {m n : ℤ}, m ≤ n → (m<...=n + 1).toList = (m + 1) :: List.map (fun x => x + 1) (m<...=n).toList
-- Mathlib.Algebra.Ring.Subring.Units
RingHom.isUnit_eqLocusS_mk_iff : ∀ {R : Type u_1} {T : Type u_2} [inst : Semiring T] [inst_1 : Semiring R] (f g : R →+* T) {r : R} (hr : f r = g r),
  IsUnit ⟨r, hr⟩ ↔ IsUnit r
-- Mathlib.LinearAlgebra.Dimension.Finrank
/-- The rank of a module as a natural number.

For a finite-dimensional vector space `V` over a field `k`, `Module.finrank k V` is equal to
the dimension of `V` over `k`.

For a general module `M` over a ring `R`, `Module.finrank R M` is defined to be the supremum of the
cardinalities of the `R`-linearly independent subsets of `M`, if this supremum is finite. It is
defined by convention to be `0` if this supremum is infinite. See `Module.rank` for a
cardinal-valued version where infinite rank modules have rank an infinite cardinal.

Note that if `R` is not a field then there can exist modules `M` with `¬(Module.Finite R M)` but
`finrank R M ≠ 0`. For example `ℚ` has `finrank` equal to `1` over `ℤ`, because the nonempty
`ℤ`-linearly independent subsets of `ℚ` are precisely the nonzero singletons.  -/
Module.finrank : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → ℕ