mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.ByteArray.Lemmas
ByteArray.data_append : ∀ {l l' : ByteArray}, (l ++ l').data = l.data ++ l'.data
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Right.min_le_max_of_mul_le_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] {a b c d : α} [MulLeftMono α] [MulRightStrictMono α],
  a * b ≤ c * d → min a b ≤ max c d
-- Init.Data.SInt.Basic
/-- Converts 8-bit signed integers to 64-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.toInt64 : Int8 → Int64
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.of.eq_1 : ∀ {α : Type u_1} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) (x : α),
  PresentedAddMonoid.of rels x = (PresentedAddMonoid.mk rels) (FreeAddMonoid.of x)
-- Mathlib.Logic.Equiv.Fintype
Function.Embedding.invOfMemRange.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β) (b : ↑(Set.range ⇑f)),
  f.invOfMemRange b = ⋯.invOfMemRange b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap (φ - φ') =
    CategoryTheory.ShortComplex.rightHomologyMap φ - CategoryTheory.ShortComplex.rightHomologyMap φ'
-- Init.Data.List.Basic
/-- The first list is a contiguous sub-list of the second list. Typically written with the `<:+:`
operator.

In other words, `l₁ <:+: l₂` means that there exist lists `s : List α` and `t : List α` such that
`l₂` has the form `s ++ l₁ ++ t`.


Conventions for notations in identifiers:

 * The recommended spelling of `<:+:` in identifiers is `infix` (not `isInfix`). -/
List.«term_<:+:_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Prod
Set.range_piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} (f : (i : ι) → α i → β i),
  Set.range (Pi.map f) = Set.univ.pi fun i => Set.range (f i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyGTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGTD k fallback = t₂.getKeyGTD k fallback
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.smul_diff_smul' : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : IsMulCommutative ↥H] [inst_2 : H.FiniteIndex]
  (α β : H.LeftTransversal) [hH : H.Normal] (g : Gᵐᵒᵖ),
  Subgroup.leftTransversals.diff (MonoidHom.id ↥H) (g • α) (g • β) =
    ⟨(MulOpposite.unop g)⁻¹ * ↑(Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α β) * MulOpposite.unop g, ⋯⟩
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_faceOpposite_subset_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [ZeroLEOneClass k] {n : ℕ} [inst_6 : NeZero n]
  (s : Affine.Simplex k P n) (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.map_pmap : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x}
  {x : Std.Iterators.HetT m α} {f : (a : α) → x.Property a → β} {g : β → γ},
  Std.Iterators.HetT.map g (x.pmap f) = x.pmap fun a ha => g (f a ha)
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.getImpl.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lean.RArray α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Lean.RArray.leaf x))
  (h_2 : (p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)),
  (match Lean.RArray.leaf x with
    | Lean.RArray.leaf x => h_1 x
    | Lean.RArray.branch p l r => h_2 p l r) =
    h_1 x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.leftComm_symm_tmul : ∀ (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid P] [inst_8 : Module A P]
  [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module R P] [inst_12 : IsScalarTower R A P] (m : M)
  (p : P) (q : Q),
  (TensorProduct.AlgebraTensorModule.leftComm R A M P Q).symm (p ⊗ₜ[A] (m ⊗ₜ[R] q)) = m ⊗ₜ[A] (p ⊗ₜ[R] q)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) (c c' : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) c')
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c'))
-- Init.Core
ne_true_of_not : ∀ {p : Prop}, ¬p → p ≠ True
-- Lean.Attributes
Lean.EnumAttributes.mk.inj : ∀ {α : Type} {attrs : List Lean.AttributeImpl}
  {ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)}
  {attrs_1 : List Lean.AttributeImpl}
  {ext_1 : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)},
  { attrs := attrs, ext := ext } = { attrs := attrs_1, ext := ext_1 } → attrs = attrs_1 ∧ ext = ext_1
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.instFaithfulTriangleMapTriangle : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] [F.Faithful],
  F.mapTriangle.Faithful
-- Mathlib.Order.ModularLattice
/-- The diamond isomorphism between the open intervals `(a ⊓ b, a)` and `(b, a ⊔ b)`.  -/
infIooOrderIsoIooSup : {α : Type u_1} → [inst : Lattice α] → [IsModularLattice α] → (a b : α) → ↑(Set.Ioo (a ⊓ b) a) ≃o ↑(Set.Ioo b (a ⊔ b))
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is non-strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f a b`.  -/
map_le_lineMap_iff_slope_le_slope_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < r * (b - a) →
    (f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
      slope f a ((AffineMap.lineMap a b) r) ≤ slope f a b)
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangleh_comm₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangleh f g).mor₂
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
      (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁)
-- Init.Data.Array.MinMax
List.max_eq_max_toArray : ∀ {α : Type u_1} [inst : Max α] {l : List α} {h : l ≠ []}, l.max h = l.toArray.max ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.eq_of_tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
  CategoryTheory.Limits.IsZero X → ∀ (f g : Y ⟶ X), f = g
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `IsCoinitialFor.of_subset`. -/
LE.le.isCoinitialFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCoinitialFor s t
-- Lean.Expr
/-- Return `true` if the given expression is `.sort .zero`  -/
Lean.Expr.isProp : Lean.Expr → Bool
-- Mathlib.Algebra.CharP.Two
CharTwo.two_nsmul : ∀ {R : Type u_1} [inst : Semiring R] [CharP R 2] (x : R), 2 • x = 0
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.expect_apply_eq_ite : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Finite α] [inst_2 : DecidableEq α] (a : α),
  (Finset.univ.expect fun ψ => ψ a) = if a = 0 then 1 else 0
-- Lean.Parser.Term
Lean.Parser.Term.attributes : Lean.Parser.Parser
-- Mathlib.Topology.Compactification.StoneCech
/-- The Stone-Čech compactification of a topological space.  -/
StoneCech : (α : Type u) → [TopologicalSpace α] → Type u
-- Mathlib.RingTheory.LocalRing.Subring
/-- If in a sub(semi)ring `R` of a local (semi)ring `R'` every element is either
invertible or a zero divisor, then `R` is local.
This version is for `R` and `R'` that are both sub(semi)rings of a (semi)ring `S`.  -/
IsLocalRing.of_subring' : ∀ {S : Type u_1} [inst : Semiring S] {R R' : Subsemiring S} [IsLocalRing ↥R'],
  R ≤ R' → (∀ a ∈ nonZeroDivisors ↥R, IsUnit a) → IsLocalRing ↥R
-- Lean.Meta.Basic
Lean.Meta.getConfigWithKey : Lean.MetaM Lean.Meta.ConfigWithKey
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1
-- Lean.Parser.Extra
Lean.Parser.charLit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsOpenImmersion f ↔
    Topology.IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.map_obj_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f)
  (X_1 :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤),
  ((CategoryTheory.MorphismProperty.Over.map Q hPf).obj X_1).hom = CategoryTheory.CategoryStruct.comp X_1.hom f
-- Mathlib.Data.Vector.Defs
/-- Remove the element at position `i` from a vector of length `n`.  -/
List.Vector.eraseIdx : {α : Type u_1} → {n : ℕ} → Fin n → List.Vector α n → List.Vector α (n - 1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂)[k]! = m₂[k]!
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Lift an intermediate field of an intermediate field.  -/
IntermediateField.lift : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {F : IntermediateField K L} → IntermediateField K ↥F → IntermediateField K L
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.write : {Γ : Type u_1} → Γ → Turing.TM0.Stmt Γ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_of_forall_getKey_eq_of_forall_get?_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (∀ (k : α) (hk : m₁.contains k = true) (hk' : m₂.contains k = true), m₁.getKey k hk = m₂.getKey k hk') →
        (∀ (k : α), Std.DHashMap.Internal.Raw₀.Const.get? m₁ k = Std.DHashMap.Internal.Raw₀.Const.get? m₂ k) →
          (↑m₁).Equiv ↑m₂
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The number of parts in the partition  -/
OrderedFinpartition.length : {n : ℕ} → OrderedFinpartition n → ℕ
-- Mathlib.Algebra.CharP.CharAndCard
/-- A prime `p` is a unit in a commutative ring `R` of nonzero characteristic iff it does not divide
the characteristic.  -/
isUnit_iff_not_dvd_char_of_ringChar_ne_zero : ∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [Fact (Nat.Prime p)], ringChar R ≠ 0 → (IsUnit ↑p ↔ ¬p ∣ ringChar R)
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- A tensor product `M ⊗[R] N` is the direct limit of the modules `M ⊗[R] Q`,
where `Q` ranges over all finitely generated submodules of `N`, as a linear equivalence.  -/
Submodule.FG.lTensor.directLimit : (R : Type u) →
  (M : Type u_1) →
    (N : Type u_2) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : DecidableEq { Q // Q.FG }] →
                  (Module.DirectLimit (fun Q => TensorProduct R M ↥↑Q) fun x x_1 hPQ =>
                      LinearMap.lTensor M (Submodule.inclusion hPQ)) ≃ₗ[R]
                    TensorProduct R M N
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mul_left_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (u : M₀ˣ) {a : M₀}, a * ↑u = 0 ↔ a = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertMany_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF →
    ∀ {l : List (α × β)} {k : α} {v : β},
      Std.DHashMap.Raw.Const.insertMany m ((k, v) :: l) = Std.DHashMap.Raw.Const.insertMany (m.insert k v) l
-- Mathlib.NumberTheory.Modular
ModularGroup.re_T_inv_smul : ∀ (z : UpperHalfPlane), (ModularGroup.T⁻¹ • z).re = z.re - 1
-- Std.Data.DTreeMap.Internal.Operations
/-- Adds a new mapping to the tree, leaving the tree unchanged if the key is already present.  -/
Std.DTreeMap.Internal.Impl.insertIfNew : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      (k : α) →
        β k →
          (t : Std.DTreeMap.Internal.Impl α β) →
            t.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β t.size (t.size + 1)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.negPart_finite : ∀ {α : Type u_2} [inst : MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α),
  MeasureTheory.IsFiniteMeasure self.negPart
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.of_dense : ∀ {α : Type u_1} [inst : LT α] [DenselyOrdered α] (a : α), Order.IsSuccPrelimit a
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_inv_naturality_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))
      (CategoryTheory.Bicategory.associator f g h').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
-- Init.Data.UInt.Bitwise
UInt8.not_not : ∀ {a : UInt8}, ~~~~~~a = a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolParams.textDocument : Lean.Lsp.DocumentSymbolParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of an integrable function is smaller than its mean.  -/
MeasureTheory.exists_le_setAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → ∃ x ∈ s, f x ≤ ⨍ (a : α) in s, f a ∂μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insert k v).minKey ⋯ = k
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.m_iUnion : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {f : ℕ → Set α},
  (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun i => v (f i)) (v (⋃ i, f i))
-- Mathlib.Algebra.Group.Center
IsAddCentral.mk : ∀ {M : Type u_1} [inst : Add M] {z : M},
  (∀ (a : M), AddCommute z a) →
    (∀ (b c : M), z + (b + c) = z + b + c) → (∀ (a b : M), a + b + z = a + (b + z)) → IsAddCentral z
-- Mathlib.Analysis.Normed.Group.Continuity
/-- Special case of the sandwich theorem: if the norm of `f` is bounded by a real
function `a` which tends to `0`, then `f` tends to `0`.  -/
squeeze_zero_norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
  (∀ (n : α), ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- The natural `ℕ`-algebra homomorphism from the unitization of a non-unital subsemiring to
its `Subsemiring.closure`.  -/
NonUnitalSubsemiring.unitization : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : SetLike S R] → [hSR : NonUnitalSubsemiringClass S R] → (s : S) → Unitization ℕ ↥s →ₐ[ℕ] R
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.iInter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_3} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), BaireMeasurableSet (s i)) → BaireMeasurableSet (⋂ i, s i)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod M N = (AddMonoid.coprodCon M N).Quotient
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} {x : N},
  (f.addEquivOfLocalizations k) x = (f.lift ⋯) x
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.getD_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α}
  {fallback : β}, Std.DHashMap.Raw.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD ⟨m, ⋯⟩ a fallback
-- Mathlib.Computability.DFA
DFA.reindex.eq_1 : ∀ {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ'),
  DFA.reindex g =
    {
      toFun := fun M =>
        { step := fun s a => g (M.step (g.symm s) a), start := g M.start, accept := ⇑g.symm ⁻¹' M.accept },
      invFun := fun M =>
        { step := fun s a => g.symm (M.step (g s) a), start := g.symm M.start, accept := ⇑g ⁻¹' M.accept },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMatId_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.Mat_ C),
  CategoryTheory.Functor.mapMatId.hom.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).mapMat_.obj X)
-- Lean.Declaration
Lean.RecursorRule.mk.sizeOf_spec : ∀ (ctor : Lean.Name) (nfields : ℕ) (rhs : Lean.Expr),
  sizeOf { ctor := ctor, nfields := nfields, rhs := rhs } = 1 + sizeOf ctor + sizeOf nfields + sizeOf rhs
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.coeff_log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (n : ℕ),
  (PowerSeries.coeff n) (PowerSeries.log A) = if n = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1) / ↑n)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_sub_left : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {a : α}, (fun x => a - x) '' t = (fun x => -x + a) ⁻¹' t
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- the leading coefficient of a multivariate polynomial with respect to a monomial ordering  -/
MonomialOrder.leadingCoeff : {σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → R
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.symm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s → MonovaryOn g f s
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.zero_eq_map_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [inst : Zero β], 0 = WithTop.map f v ↔ ∃ x, v = ↑x ∧ f x = 0
-- Mathlib.Topology.Constructions
/-- `Function.update f i x` is continuous in `(f, x)`.  -/
continuous_update : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [inst : DecidableEq ι] (i : ι),
  Continuous fun f => Function.update f.1 i f.2
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_inl_inr_codiag_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] {Z : C} (h : X ⨿ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag (X ⨿ Y)) h) =
    h
-- Init.Control.Lawful.Instances
OptionT.run_mk : ∀ {α : Type u} {m : Type u → Type v} (x : m (Option α)), (OptionT.mk x).run = x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (S : Set ↑↑(D.V (i, j))),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)).base) ''
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base) ⁻¹' S =
    ⇑(CategoryTheory.ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j).base) '' S
-- Mathlib.Tactic.SimpRw
/-- A version of `withRWRulesSeq` (in core) that doesn't attempt to find equation lemmas, and simply
passes the rw rules on to `x`.  -/
Mathlib.Tactic.withSimpRWRulesSeq : Lean.Syntax → (Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.EpiMono
/-- The opposite of a split mono is a split epi.  -/
CategoryTheory.SplitMono.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : Y ⟶ X} → CategoryTheory.SplitMono f → CategoryTheory.SplitEpi f.op
-- Mathlib.Order.BoundedOrder.Basic
Pi.instOrderTop : {ι : Type u_1} →
  {α' : ι → Type u_2} → [inst : (i : ι) → LE (α' i)] → [(i : ι) → OrderTop (α' i)] → OrderTop ((i : ι) → α' i)
-- Mathlib.Order.WithBot
WithBot.decidableLE.eq_2 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (a : α), WithBot.decidableLE (some a) none = isFalse ⋯
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalence_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).inverse =
    CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c