mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Presentation.Submersive
_private.Mathlib.RingTheory.Extension.Presentation.Submersive.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_inr_inr : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Fintype σ] [inst_8 : Fintype σ'] (i j : σ),
  (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) = (MvPolynomial.rename Sum.inr) (P.jacobiMatrix i j)
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.liftOn.congr_simp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {α : Type u_2} (x x_1 : DivisibleHull M),
  x = x_1 →
    ∀ (f f_1 : M → ℕ+ → α) (e_f : f = f_1)
      (h : ∀ (m m' : M) (s s' : ℕ+), DivisibleHull.mk m s = DivisibleHull.mk m' s' → f m s = f m' s'),
      x.liftOn f h = x_1.liftOn f_1 ⋯
-- Lean.Language.Basic
Lean.Language.SyntaxGuarded.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (stx : Lean.Syntax) (val : α),
  sizeOf { stx := stx, val := val } = 1 + sizeOf stx + sizeOf val
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α]
  [beqOrd : Std.LawfulBEqOrd α] [Std.TransOrd α] {k : α},
  t.WF → t.keysArray.contains k = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
IsUnit.mul_le_mul_left : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] {a b c : M}, IsUnit a → (a * b ≤ a * c ↔ b ≤ c)
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Iic : ∀ (x : ↑unitInterval), MeasureTheory.volume (Set.Iic x) = ENNReal.ofReal ↑x
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) (X : C), r.degHom (CategoryTheory.CategoryStruct.id X) = r.deg X
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKey! k = default
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.le_order_subst_left' : ∀ {R : Type u_2} [inst : CommRing R] {f φ : PowerSeries R},
  PowerSeries.constantCoeff f = 0 → φ.order ≤ PowerSeries.order (PowerSeries.subst f φ)
-- Mathlib.Analysis.Complex.Basic
/-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`.  -/
Complex.reCLM : ℂ →L[ℝ] ℝ
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_inf_const : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {a : α},
  a ≤ s.inf fun x => a
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.monoidHom_ext_iff : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] {N : Subgroup G} [nN : N.Normal]
  {f g : G ⧸ N →* M}, f = g ↔ f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)
-- Init.Ext
PProd.ext_iff : ∀ {α : Sort u} {β : Sort v} {x y : α ×' β}, x = y ↔ x.fst = y.fst ∧ x.snd = y.snd
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  m.isEmpty = true → a ∉ m
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The map from nonreal embeddings to complex infinite places  -/
NumberField.InfinitePlace.mkComplex : {K : Type u_1} → [inst : Field K] → { φ // ¬NumberField.ComplexEmbedding.IsReal φ } → { w // w.IsComplex }
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_ne_zero_iff_lt : ∀ {a b : Ordinal.{u_4}}, a - b ≠ 0 ↔ b < a
-- Mathlib.GroupTheory.OrderOfElement
AddUnits.isOfFinAddOrder_val : ∀ {G : Type u_1} [inst : AddMonoid G] {u : AddUnits G}, IsOfFinAddOrder ↑u ↔ IsOfFinAddOrder u
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instIdempotentOpJoin : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l], Std.IdempotentOp fun x1 x2 => Lean.Order.join x1 x2
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.isMulCommutative_iSup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_1} [Nonempty ι] {S : ι → NonUnitalSubring R}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {I : Ideal S}, Ideal.absNorm I ≠ 0 ↔ I ∈ nonZeroDivisors (Ideal S)
-- Mathlib.Data.Finset.Density
Finset.dens_strictMono : ∀ {α : Type u_2} [inst : Fintype α], StrictMono Finset.dens
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_of_mul_dvd_mul_left : ∀ {a m n : ℤ}, a ≠ 0 → a * m ∣ a * n → m ∣ n
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isIso_truncLE_map_truncLEι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) [CategoryTheory.IsTriangulated C] (a b : ℤ),
  a ≤ b → ∀ (X : C), CategoryTheory.IsIso ((t.truncLE a).map ((t.truncLEι b).app X))
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- To check that a measure `ν` is the projective limit of a projective family of measures indexed
by `Finset ℕ`, it is enough to check on intervals of the form `Iic n`.  -/
MeasureTheory.isProjectiveLimit_nat_iff : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {μ : (I : Finset ℕ) → MeasureTheory.Measure ((i : ↥I) → X ↑i)},
  MeasureTheory.IsProjectiveMeasureFamily μ →
    ∀ (ν : MeasureTheory.Measure ((n : ℕ) → X n)),
      MeasureTheory.IsProjectiveLimit ν μ ↔
        ∀ (n : ℕ), MeasureTheory.Measure.map (Preorder.frestrictLe n) ν = μ (Finset.Iic n)
-- Mathlib.Algebra.Ring.Divisibility.Basic
Dvd.dvd.linear_comb : ∀ {α : Type u_1} [inst : NonUnitalCommSemiring α] {d x y : α}, d ∣ x → d ∣ y → ∀ (a b : α), d ∣ a * x + b * y
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionRight_unop : ∀ (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]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] (c : Cᵒᵖ) {d d' : Dᵒᵖ} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight (Opposite.unop c) f.unop =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)
-- Mathlib.Algebra.Field.Equiv
MulEquiv.isField_congr : ∀ {A : Type u_1} {B : Type u_2} [inst : Semiring A] [inst_1 : Semiring B] (e : A ≃* B), IsField A ↔ IsField B
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.flipMultilinear_flipLinear : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')),
  f.flipLinear.flipMultilinear = f
-- Std.Net.Addr
Std.Net.IPv6Addr.instCoeIPAddr : Coe Std.Net.IPv6Addr Std.Net.IPAddr
-- Init.Data.Vector.Perm
Vector.Perm.push_comm : ∀ {α : Type u_1} {n : ℕ} (x y : α) {xs ys : Vector α n}, xs.Perm ys → ((xs.push x).push y).Perm ((ys.push y).push x)
-- Lean.Parser.Basic
Lean.Parser.peekToken : Lean.Parser.ParserContext →
  Lean.Parser.ParserState → Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.instQuasiIsoNatεToSingle₀ : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G], QuasiIso (Rep.standardComplex.εToSingle₀ k G)
-- Mathlib.MeasureTheory.SetAlgebra
/-- **Alias** of `MeasureTheory.IsSetAlgebra.sdiff_mem`.

---

An algebra of sets is closed by difference.  -/
MeasureTheory.IsSetAlgebra.diff_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetAlgebra 𝒜 → s ∈ 𝒜 → t ∈ 𝒜 → s \ t ∈ 𝒜
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- In a preprimitive additive action,
any normal subgroup that acts nontrivially is pretransitive (Wielandt, th. 7.1).  -/
AddAction.IsPreprimitive.isQuasiPreprimitive : ∀ {M : Type u_3} [inst : AddGroup M] {α : Type u_4} [inst_1 : AddAction M α] [AddAction.IsPreprimitive M α],
  AddAction.IsQuasiPreprimitive M α
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_add_ofNat : ∀ {n : ℕ} [inst : n.AtLeastTwo], Cardinal.continuum + OfNat.ofNat n = Cardinal.continuum
-- Mathlib.Algebra.Group.Basic
mul_inv_eq_mul_inv_iff_mul_eq_mul : ∀ {G : Type u_3} [inst : CommGroup G] {a b c d : G}, a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.normalized_count_X_eq_of_coe : ∀ {k : Type u_2} [inst : Field k] {P : Polynomial k},
  P ≠ 0 →
    Multiset.count PowerSeries.X (UniqueFactorizationMonoid.normalizedFactors ↑P) =
      Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map
`p → M₂`.  -/
LinearMap.domRestrict : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] → {σ₁₂ : R →+* R₂} → (M →ₛₗ[σ₁₂] M₂) → (p : Submodule R M) → ↥p →ₛₗ[σ₁₂] M₂
-- Mathlib.Order.UpperLower.Closure
upperClosure_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} (f : α ≃o β),
  upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.isEmbedding_coeFn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
  Topology.IsEmbedding (⇑UniformFun.ofFun ∘ DFunLike.coe)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan_strictMono : StrictMono fun x => Real.sin (Real.arctan x)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_cons : ∀ {m n : ℕ} {α : Sort u_2} (a : α) (as : Fin n → α) (bs : Fin m → α),
  Fin.append (Fin.cons a as) bs = Fin.cons a (Fin.append as bs) ∘ Fin.cast ⋯
-- Mathlib.RingTheory.Binomial
Ring.multichoose_zero_right' : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R),
  Ring.multichoose r 0 = r ^ 0
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.rightAdj_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type (max w v u)))
  {X Y : CategoryTheory.Functor C (Type (max w v u))} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.FunctorToTypes.rightAdj F).map f).app X_1 =
    TypeCat.ofHom fun a =>
      { app := fun d b => CategoryTheory.CategoryStruct.comp (a.app d b) (f.app d), naturality := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.hasProd_iff_of_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → α} (e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)),
  (∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x) → (HasProd f a ↔ HasProd g a)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instCommRing : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [CommRing β] → CommRing (MeasureTheory.SimpleFunc α β)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The category of magmas and magma morphisms.  -/
MagmaCat : Type (u + 1)
-- Mathlib.MeasureTheory.Function.EssSup
iSup_eq_essSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLinearOrder β]
  {f : α → β}, (∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0) → ⨆ x, f x = essSup f μ
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.match_1.splitter : (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) →
  (x : ByteArray.utf8DecodeChar?.FirstByte) →
    (Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid) →
      (Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done) →
        (Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore) →
          (Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore) →
            (Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore) → motive x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_singleton_append : ∀ {m n : ℤ}, m < n → (m...n).toArray = #[m] ++ ((m + 1)...n).toArray
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.comp : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {m n : ℕ},
  n ≠ 0 → p.IsMonicOfDegree m → q.IsMonicOfDegree n → (p.comp q).IsMonicOfDegree (m * n)
-- Init.Data.List.Basic
List.takeWhile_nil : ∀ {α : Type u} {p : α → Bool}, List.takeWhile p [] = []
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.generatorsOfIsCokernelFree_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)),
  (SheafOfModules.generatorsOfIsCokernelFree f g H H').I = σ
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_one_of_utf8Size_eq_four : ∀ {c : Char} (h : c.utf8Size = 4), (String.utf8EncodeChar c)[1].toBitVec = 2#2 ++ BitVec.extractLsb' 12 6 c.val.toBitVec
-- Mathlib.NumberTheory.Real.Irrational
irrational_intCast_div_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable topological additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Because an additive topological group is not equipped with a `UniformSpace` instance by default,
we must explicitly provide it in order to consider completeness. See
`QuotientAddGroup.completeSpace_left` for a version in which `G` is already equipped with a uniform
structure.  -/
QuotientAddGroup.completeSpace_left' : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [FirstCountableTopology G] (N : AddSubgroup G) [inst_4 : N.Normal] [hG : CompleteSpace G], CompleteSpace (G ⧸ N)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C} {X Y X' : C}
  {s : X' ⟶ X} {hs : W s} {f : X' ⟶ Y} {X'_1 : C} {s_1 : X'_1 ⟶ X} {hs_1 : W s_1} {f_1 : X'_1 ⟶ Y},
  { X' := X', s := s, hs := hs, f := f } = { X' := X'_1, s := s_1, hs := hs_1, f := f_1 } →
    X' = X'_1 ∧ s ≍ s_1 ∧ f ≍ f_1
-- Std.Http.Data.URI.Basic
/-- Adds a query parameter without a value (flag parameter). The key will be automatically
percent-encoded when building.
 -/
Std.Http.URI.Builder.addQueryFlag : Std.Http.URI.Builder → String → Std.Http.URI.Builder
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_sub_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ),
  ⌈a - ↑n⌉ = ⌈a⌉ - ↑n
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_sub_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubNegMonoid G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (g : G), MeasureTheory.Measure.map (fun x => x - g) μ = μ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_unitIso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapIso i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k))
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.alter! k f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      match f none with
      | none => Std.DTreeMap.Internal.Impl.leaf
      | some v => Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' =>
      match h : compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.balance! k' v' (Std.DTreeMap.Internal.Impl.alter! k f l') r'
      | Ordering.gt => Std.DTreeMap.Internal.Impl.balance! k' v' l' (Std.DTreeMap.Internal.Impl.alter! k f r')
      | Ordering.eq =>
        match f (some (cast ⋯ v')) with
        | none => l'.glue! r'
        | some v => Std.DTreeMap.Internal.Impl.inner sz k v l' r'
-- Mathlib.Data.Int.ModEq
Int.ModEq.rfl : ∀ {n a : ℤ}, a ≡ a [ZMOD n]
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_univ : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], NonUnitalSubsemiring.closure Set.univ = ⊤
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableAt_atlas_symm : ∀ {𝕜 : 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 : OpenPartialHomeomorph M H} [IsManifold I 1 M],
  e ∈ atlas H M → ∀ {x : H}, x ∈ e.target → MDiffAt ↑e.symm x
-- Mathlib.FieldTheory.Galois.Notation
/-- Pretty printer for the `Gal(L/K)` notation.  -/
delabGal : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Convex.Topology
Convex.nhdsWithin_inter_Ioi_eq_nhdsGT : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜}, a ∈ closure s → (s ∩ Set.Ioi a).Nonempty → nhdsWithin a (s ∩ Set.Ioi a) = nhdsWithin a (Set.Ioi a)
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local max on `s` at `a`, `f'` is a derivative of `f` at `a` within `s`, and
both `y` and `-y` belong to the positive tangent cone of `s` at `a`, then `f' y ≤ 0`.  -/
IsLocalMaxOn.hasFDerivWithinAt_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {a y : E},
  IsLocalMaxOn f s a → HasFDerivWithinAt f f' s a → y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → f' y = 0
-- Mathlib.Algebra.Group.EvenFunction
Function.Odd.mul_even : ∀ {α : Type u_1} [inst : Neg α] {R : Type u_3} [inst_1 : Mul R] {f g : α → R} [inst_2 : HasDistribNeg R],
  Function.Odd f → Function.Even g → Function.Odd (f * g)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_one : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : MulActionWithZero R S]
  [inst_3 : Monoid S] (x : Sˣ), LaurentPolynomial.smeval 1 x = 1
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Icc_sub_one_right_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α},
  a ≤ b → insert b (Set.Icc a (b - 1)) = Set.Icc a b
-- Lean.Elab.DocString
Lean.Doc.WithSyntax.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (val : α) (stx : Lean.Syntax),
  sizeOf { val := val, stx := stx } = 1 + sizeOf val + sizeOf stx
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.comap_mono : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {S₁ S₂ : StarSubalgebra R B} {f : A →⋆ₐ[R] B},
  S₁ ≤ S₂ → StarSubalgebra.comap f S₁ ≤ StarSubalgebra.comap f S₂
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.ppPattern.ppArg : Lean.Expr → Lean.MessageData
-- Mathlib.Analysis.SumIntegralComparisons
AntitoneOn.sum_le_integral_Ico : ∀ {a b : ℕ} {f : ℝ → ℝ},
  a ≤ b → AntitoneOn f (Set.Icc ↑a ↑b) → ∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x
-- Mathlib.GroupTheory.Transfer
MonoidHom.ker_transferSylow_disjoint : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex] (Q : Subgroup G),
  IsPGroup p ↥Q → Disjoint (MonoidHom.transferSylow P hP).ker Q
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.Iso.mk_inv : ∀ {α β : NonemptyFinLinOrd} (e : ↑α.toLinOrd ≃o ↑β.toLinOrd),
  (NonemptyFinLinOrd.Iso.mk e).inv = NonemptyFinLinOrd.ofHom ↑e.symm
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.postComp_φ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z Z' : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z)
  (h : Z ⟶ Z'), (f.postComp h).φ = CategoryTheory.CategoryStruct.comp f.φ h
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- `MeasureTheory.OuterMeasure.mkMetric'.pre m r` is a trimmed measure provided that
`m (closure s) = m s` for any set `s`.  -/
MeasureTheory.OuterMeasure.mkMetric'.trim_pre : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] (m : Set X → ENNReal),
  (∀ (s : Set X), m (closure s) = m s) →
    ∀ (r : ENNReal), (MeasureTheory.OuterMeasure.mkMetric'.pre m r).trim = MeasureTheory.OuterMeasure.mkMetric'.pre m r
-- Init.Data.Rat.Lemmas
/-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `mk' n d` with `d ≠ 0`.  -/
Rat.numDenCasesOn'' : {C : ℚ → Sort u} →
  (a : ℚ) →
    ((n : ℤ) →
        (d : ℕ) → (nz : d ≠ 0) → (red : n.natAbs.Coprime d) → C { num := n, den := d, den_nz := nz, reduced := red }) →
      C a
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_gcd_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b c : α), a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c