mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
Lean.Meta.Cache.mk.sizeOf_spec : ∀ (inferType : Lean.Meta.InferTypeCache) (funInfo : Lean.Meta.FunInfoCache)
  (synthInstance : Lean.Meta.SynthInstanceCache) (whnf : Lean.Meta.WhnfCache)
  (defEqTrans defEqPerm : Lean.Meta.DefEqCache),
  sizeOf
      { inferType := inferType, funInfo := funInfo, synthInstance := synthInstance, whnf := whnf,
        defEqTrans := defEqTrans, defEqPerm := defEqPerm } =
    1 + sizeOf inferType + sizeOf funInfo + sizeOf synthInstance + sizeOf whnf + sizeOf defEqTrans + sizeOf defEqPerm
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseDstOffset : Std.Time.TimeZone.Offset → Std.Internal.Parsec.String.Parser Std.Time.TimeZone.Offset
-- Lean.Level
Lean.mkLevelParamEx : Lean.Name → Lean.Level
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.below.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} (x : C),
  CategoryTheory.MorphismProperty.multiplicativeClosure.below ⋯
-- Mathlib.CategoryTheory.Yoneda
/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error.  -/
CategoryTheory.map_yonedaEquiv' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.yonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.app Y)) g.unop
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.mem_maximalAtlas_prod : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {n : WithTop ℕ∞} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I n M]
  [IsManifold I' n M'] {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M →
    ∀ {e' : OpenPartialHomeomorph M' H'},
      e' ∈ IsManifold.maximalAtlas I' n M' → e.prod e' ∈ IsManifold.maximalAtlas (I.prod I') n (M × M')
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.contPrec : Lean.PrettyPrinter.Parenthesizer.State → Option ℕ
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_pow_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ : MvPowerSeries σ R} {s : σ} {n : ℕ},
  MvPowerSeries.X s ^ n * φ = φ * MvPowerSeries.X s ^ n
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.add_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : AddZeroClass β]
  [inst_3 : ContinuousAdd β] (f g : ZeroAtInftyContinuousMap α β), (f + g) x = f x + g x
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α] (s : Set α),
  ThreeAPFree s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → a = b
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C}
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] {a : M}
  (α₁ α₂ : CategoryTheory.ShiftedHom X Y a) (F : CategoryTheory.Functor C D) [inst_7 : F.CommShift M] [F.Additive],
  (α₁ + α₂).map F = α₁.map F + α₂.map F
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.zpow_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a : α) (n : ℤ) (v₁ v : ℚ),
  (v == v₁ ^ n) = true → a = Lean.Grind.Field.NormNum.ofRat v₁ → a ^ n = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Geometry.Manifold.Algebra.Structures
ContMDiffRing.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {R : Type u_4} [inst_4 : Semiring R] [inst_5 : TopologicalSpace R] [inst_6 : ChartedSpace H R]
  [toContMDiffAdd : ContMDiffAdd I n R], (ContMDiff (I.prod I) I n fun p => p.1 * p.2) → ContMDiffRing I n R
-- Mathlib.Algebra.Notation.Support
Function.support_comp_eq_of_range_subset : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] {g : M → N} {f : ι → M},
  (∀ {x : M}, x ∈ Set.range f → (g x = 0 ↔ x = 0)) → Function.support (g ∘ f) = Function.support f
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.add b with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_3 a b
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Archimedean equivalence is preserved by `f`.  -/
HahnEmbedding.Partial.archimedeanClassMk_eq_iff : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] (x y : ↥(↑f).domain),
  ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y) ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y
-- Mathlib.LinearAlgebra.Matrix.Diagonal
Matrix.range_diagonal : ∀ {m : Type u_1} [inst : Fintype m] {K : Type u} [inst_1 : Semifield K] [inst_2 : DecidableEq m] (w : m → K),
  (Matrix.toLin' (Matrix.diagonal w)).range = ⨆ i ∈ {i | w i ≠ 0}, (LinearMap.single K (fun x => K) i).range
-- Mathlib.NumberTheory.Primorial
primorial_add : ∀ (m n : ℕ), primorial (m + n) = primorial m * ∏ p ∈ Finset.Ico (m + 1) (m + n + 1) with Nat.Prime p, p
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq_comm : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], y ≤ x → z ≤ x → (x \ y = z ↔ x \ z = y)
-- Mathlib.Topology.UnitInterval
unitInterval.prod_mem : ∀ {ι : Type u_1} {t : Finset ι} {f : ι → ℝ}, (∀ c ∈ t, f c ∈ unitInterval) → ∏ c ∈ t, f c ∈ unitInterval
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.mul.eq_1 : ∀ (m1 m2 : Tactic.ComputeAsymptotics.UnitMonomial), m1.mul m2 = List.zipWith (fun x1 x2 => x1 + x2) m1 m2
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ι_tensorHom : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ ⟶ X₂)
  (g : Y₁ ⟶ Y₂) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h)
      (CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i₁) (g i₂))
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termHS' : Lean.ParserDescr
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
has a separator, then it is complete.  -/
CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C]
  [CategoryTheory.HasSeparator C] [CategoryTheory.WellPowered.{v, v, u} Cᵒᵖ], CategoryTheory.Limits.HasLimits C
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr : Type
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIntegral : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.GeometricallyIntegral
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_modify_eq_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α] {k : α} {f : β → β}, (t.modify k f).minKey! = t.minKey!
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_zero_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Nontrivial R], LinearIndependent R 0 ↔ IsEmpty ι
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.diff_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₁).Equiv ↑m₂ → (↑(m₁.diff m₃)).Equiv ↑(m₂.diff m₃)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.Homotopic.setoid : {X : Type u_2} → [inst : TopologicalSpace X] → (N : Type u_3) → (x : X) → Setoid ↑(GenLoop N X x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyItem : Lean.ToJson Lean.Lsp.CallHierarchyItem
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSubtractionMonoid : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [SubtractionMonoid G] → SubtractionMonoid (l.Germ G)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} → (F.functor ⟶ G.functor) → F.Hom G
-- Mathlib.Order.Lattice
/-- The infimum is a lower bound on the second argument  -/
SemilatticeInf.inf_le_right : ∀ {α : Type u} [self : SemilatticeInf α] (a b : α), SemilatticeInf.inf a b ≤ b
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- A function on `Box ι` is called box additive if for every box `J` and a partition `π` of `J`
we have `f J = ∑ Ji ∈ π.boxes, f Ji`.  -/
BoxIntegral.«term_→ᵇᵃ_» : Lean.TrailingParserDescr
-- Mathlib.Data.ENat.BigOperators
/-- A sum is finite iff all summands are finite.  -/
ENat.sum_ne_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, ∑ a ∈ s, f a ≠ ⊤ ↔ ∀ a ∈ s, f a ≠ ⊤
-- Mathlib.Algebra.Opposites
MulOpposite.unop_inv : ∀ {α : Type u_1} [inst : Inv α] (x : αᵐᵒᵖ), MulOpposite.unop x⁻¹ = (MulOpposite.unop x)⁻¹
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_roi : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_roi._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun e => (cmp e bound).isGT) t.toList
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.counit_naturality : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (T.map f) (T.ε.app Y) = CategoryTheory.CategoryStruct.comp (T.ε.app X) f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (chosenPullback : CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁) →
                    (p : chosenPullback.pullback ⟶ S) →
                      (p₁ : chosenPullback.pullback ⟶ X₁) →
                        (p₃ : chosenPullback.pullback ⟶ X₃) →
                          h₁₃.LiftStruct p₁ p₃ p →
                            autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₁ h₁₂.p₁ = p₁)
                                CategoryTheory.Limits.ChosenPullback₃.hp₁._autoParam →
                              autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₂ h₂₃.p₂ = p₃)
                                  CategoryTheory.Limits.ChosenPullback₃.hp₃._autoParam →
                                CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The `fixingAddSubgroup` of `g +ᵥ s` is the conjugate
of the `fixingAddSubgroup` of `s` by `g`.  -/
SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_addConj : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s : Set α) (g : M),
  fixingAddSubgroup M (g +ᵥ s) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.addConj g)) (fixingAddSubgroup M s)
-- Mathlib.Order.Monotone.Defs
Subsingleton.strictMono : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton α] (f : α → β), StrictMono f
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Integration by parts on $(∞, a]$.**
For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`.  -/
MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {a : ℝ} {a' b' : A} {u v u' v' : ℝ → A}
  [CompleteSpace A],
  (∀ x ∈ Set.Iio a, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.Iio a, HasDerivAt v (v' x) x) →
      MeasureTheory.IntegrableOn (u * v') (Set.Iic a) MeasureTheory.volume →
        MeasureTheory.IntegrableOn (u' * v) (Set.Iic a) MeasureTheory.volume →
          Filter.Tendsto (u * v) (nhdsWithin a (Set.Iio a)) (nhds a') →
            Filter.Tendsto (u * v) Filter.atBot (nhds b') →
              ∫ (x : ℝ) in Set.Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Set.Iic a, u' x * v x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of `multiplicative_of_symm_of_total`. -/
multiplicative_of_symmetric_of_isTotal : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β) [Std.Symm p],
  (∀ {a b : α}, p a b → f a b * f b a = 1) →
    (∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c) →
      ∀ {a b c : α}, p a b → p b c → p a c → f a c = f a b * f b c
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.obj.neg_def_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] {G : C} [inst_5 : CategoryTheory.AddGrpObj G] {Z : D}
  (h : F.obj G ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.AddGrpObj.neg) h
-- Lean.ScopedEnvExtension
Lean.instInhabitedScopedEnvExtension : {a : Type} → [Inhabited a] → {a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension a a_1 a_2)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.X_sub_C_pow_dvd_iff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
  (Polynomial.X - Polynomial.C t) ^ n ∣ p ↔ Polynomial.X ^ n ∣ p.comp (Polynomial.X + Polynomial.C t)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).get!
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_of_brange_eq : ∀ {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}}
  {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}}, o.brange f = o'.brange g → o.bsup f = o'.bsup g
-- Mathlib.Data.Set.Sups
HasSups.mk : {α : Type u_4} → (α → α → α) → HasSups α
-- Mathlib.Topology.Constructions.SumProd
isClosed_sum_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set (X ⊕ Y)},
  IsClosed s ↔ IsClosed (Sum.inl ⁻¹' s) ∧ IsClosed (Sum.inr ⁻¹' s)
-- Mathlib.Analysis.Complex.Tietze
Metric.instTietzeExtensionBall : ∀ {𝕜 : Type v} [inst : RCLike 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {r : ℝ}, 0 < r → TietzeExtension ↑(Metric.ball 0 r)
-- Lean.Elab.DeclModifiers
/-- `expandDeclId` resulting type.  -/
Lean.Elab.ExpandDeclIdResult : Type
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₁_map : ∀ (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]
  {X Y : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)} (φ : X ⟶ Y),
  (CategoryTheory.Idempotents.functorExtension₁ C D).map φ = CategoryTheory.Idempotents.FunctorExtension₁.map φ
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- The **Structure Theorem For Finite Abelian Groups** in a multiplicative version:
A finite abelian group `G` is isomorphic to a finite product of finite cyclic groups.  -/
CommGroup.equiv_prod_multiplicative_zmod_of_finite : ∀ (G : Type u_1) [inst : CommGroup G] [Finite G],
  ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a `ExtHashSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toExtHashSet`.
 -/
Std.IterM.Total.toExtHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      [EquivBEq β] →
        [LawfulHashable β] →
          {m : Type w → Type w'} →
            [Monad m] →
              [inst_5 : Std.Iterator α m β] →
                [Std.Iterators.Finite α m] → [Std.IteratorLoop α m m] → Std.IterM.Total m β → m (Std.ExtHashSet β)
-- Mathlib.GroupTheory.OrderOfElement
pow_orderOf_eq_one : ∀ {G : Type u_1} [inst : Monoid G] (x : G), x ^ orderOf x = 1
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofExistsUnique.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (ht :
    ∀ (s : CategoryTheory.Limits.Cone F),
      ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.π.app j) = s.π.app j),
  CategoryTheory.Limits.IsLimit.ofExistsUnique ht =
    (fun s x => { lift := s, fac := ⋯, uniq := ⋯ }) (fun s => Classical.choose ⋯) ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertMany_list_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {l : List (α × β)},
  (Std.DHashMap.Const.insertMany m l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) m l)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rcc : ∀ {m n i : ℕ}, (m...=n).toArray[i]! = if i < n + 1 - m then m + i else 0
-- Mathlib.Data.Finset.NAry
Finset.image₂_assoc : ∀ {α : Type u_1} {β : Type u_3} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} [inst : DecidableEq ε]
  [inst_1 : DecidableEq ε'] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {γ : Type u_14} {u : Finset γ}
  {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
    Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ f' s (Finset.image₂ g' t u)
-- Init.Data.Rat.Lemmas
Rat.zero_mul : ∀ (a : ℚ), 0 * a = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
eqOn_iteratedDerivWithin_cotTerm_integerComplement : ∀ (k d : ℕ),
  Set.EqOn (iteratedDerivWithin k (fun z => cotTerm z d) Complex.integerComplement)
    (fun z => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k)))
    Complex.integerComplement
-- Mathlib.Data.Bool.Basic
Bool.injective_iff : ∀ {α : Sort u_1} {f : Bool → α}, Function.Injective f ↔ f false ≠ f true
-- Mathlib.Algebra.Group.Hom.Basic
/-- A homomorphism from an additive group to an additive monoid is injective iff
its kernel is trivial. For the iff statement on the triviality of the kernel,
see `injective_iff_map_eq_zero'`.  -/
injective_iff_map_eq_zero : ∀ {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : AddGroup G] [inst_1 : AddZeroClass H] [inst_2 : FunLike F G H]
  [AddMonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 → a = 0
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instInhabitedDistribMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_11} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_12} → [inst_4 : AddMonoid B] → [inst_5 : DistribMulAction N B] → Inhabited (A →ₑ+[φ] B)
-- Mathlib.Tactic.MoveAdd
/-- `reorderAndSimp mv op instr` takes as input an `MVarId`  `mv`, the name `op` of a binary
operation and a list of "instructions" `instr` that it passes to `permuteExpr`.

* It creates a version `permuted_mv` of `mv` with subexpressions representing `op`-sums reordered
  following `instructions`.
* It produces 2 temporary goals by applying `Eq.mpr` and unifying the resulting meta-variable with
  `permuted_mv`: `[⊢ mv = permuted_mv, ⊢ permuted_mv]`.
* It tries to solve the goal `mv = permuted_mv` by a simple-minded `simp` call, using the
  `op`-analogues of `add_comm, add_assoc, add_left_comm`.
 -/
Mathlib.MoveAdd.reorderAndSimp : Lean.Name → Lean.MVarId → List (Lean.Expr × Bool) → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instIntCast : {R : Type u_1} → [IntCast R] → IntCast (Lex R)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The canonical map sending `(m, s) ↦ m/s`  -/
LocalizedModule.mk : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} → {M : Type v} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M → ↥S → LocalizedModule S M