mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.involutiveInv.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_3} [inst : Inv M₂] [inst_1 : InvolutiveInv M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹), Function.Surjective.involutiveInv f hf inv = { toInv := inst, inv_inv := ⋯ }
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_enorm_eq_lintegral_edist : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β), ∫⁻ (a : α), ‖f a‖ₑ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.smul_trans : ∀ {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} {G : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : SeminormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (α : ↥(unitary 𝕜)) (e : V ≃ₗᵢ[𝕜] G) (f : G ≃ₗᵢ[𝕜] W),
  (α • e).trans f = α • e.trans f
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) ⁻¹' Set.Ioo b c = Set.Ioo (b + a) (c + a)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVecEntry.aig : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] → [inst_2 : DecidableEq α] → {w : ℕ} → Std.Sat.AIG.RefVecEntry α w → Std.Sat.AIG α
-- Init.Data.Nat.Basic
Nat.mul_le_mul_left_iff : ∀ {n m k : ℕ}, 0 < k → (k * n ≤ k * m ↔ n ≤ m)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_of_pos_of_nonneg'`.

---

**Alias** of `mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`. -/
mul_lt_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α]
  [MulPosStrictMono α], a < b → c ≤ d → 0 < c → 0 ≤ b → a * c < b * d
-- Mathlib.Order.Cover
toDual_covBy_toDual_iff : ∀ {α : Type u_1} [inst : LT α] {a b : α}, OrderDual.toDual b ⋖ OrderDual.toDual a ↔ a ⋖ b
-- Mathlib.Data.List.DropRight
List.rtake_zero : ∀ {α : Type u_1} (l : List α), l.rtake 0 = []
-- Lean.Parser.Command
Lean.Parser.Command.structure.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.CompleteBooleanAlgebra
Prod.instCompleteBooleanAlgebra : {α : Type u} → {β : Type v} → [CompleteBooleanAlgebra α] → [CompleteBooleanAlgebra β] → CompleteBooleanAlgebra (α × β)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitor_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.f = CategoryTheory.Limits.prod.fst
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_sub_natCast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  [inst_4 : Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ), ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- **Mignotte's coefficient bound**: if `f = g * h` and `h` has Mahler measure at least 1
(which holds in particular when `h` has integer coefficients with nonzero leading coefficient),
then the coefficients of `g` are bounded by a binomial coefficient times the Mahler measure
of `g * h`.

Combined with `mahlerMeasure_le_sqrt_sum_sq_norm_coeff` (Landau's inequality), this gives
the classical Mignotte bound
`‖g.coeff n‖ ≤ C(deg g, n) · √(∑ i ∈ f.support, ‖f.coeff i‖ ^ 2)`
used in polynomial factorization algorithms (Berlekamp–Zassenhaus).  -/
Polynomial.norm_coeff_le_choose_mul_mahlerMeasure_of_one_le_mahlerMeasure : ∀ (n : ℕ) (g h : Polynomial ℂ), 1 ≤ h.mahlerMeasure → ‖g.coeff n‖ ≤ ↑(g.natDegree.choose n) * (g * h).mahlerMeasure
-- Mathlib.GroupTheory.Congruence.Basic
/-- The first isomorphism theorem for `AddMonoid`s in the case of a homomorphism
with right inverse.  -/
AddCon.quotientKerEquivOfRightInverse : {M : Type u_1} →
  {P : Type u_3} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass P] → (f : M →+ P) → (g : P → M) → Function.RightInverse g ⇑f → (AddCon.ker f).Quotient ≃+ P
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_singleton : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (x : X), Metric.externalCoveringNumber ε {x} = 1
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.rightUniformSpace.congr_simp : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  IsTopologicalGroup.rightUniformSpace G = IsTopologicalGroup.rightUniformSpace G
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The rightmost object of the fork diagram of the Stacks entry.
The difference between this and `Equalizer.Presieve.SecondObj P (ofArrows X π)` arises if the
family of arrows `π` contains duplicates. The `Presieve.ofArrows` doesn't see those.
 -/
CategoryTheory.Equalizer.Presieve.Arrows.SecondObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type w) →
      {B : C} →
        {I : Type t} →
          [Small.{w, t} I] →
            (X : I → C) →
              (π : (i : I) → X i ⟶ B) → [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] → Type w
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.isHadamard_transpose_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : StarRing R] {A : Matrix n n R}, A.transpose.IsHadamard ↔ A.IsHadamard
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasLimitsOfShapeWalkingParallelPairInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C],
  CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind C)
-- Init.Data.String.Slice
/-- Returns the first character in `s`. If `s` is empty, returns `(default : Char)`.

Examples:

* `"abc".toSlice.front = 'a'`

* `"".toSlice.front = (default : Char)`
 -/
String.Slice.front : String.Slice → Char
-- Batteries.Util.Cache
Batteries.Tactic.DeclCache.mk'.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (cache : Batteries.Tactic.Cache α)
  (addDecl addLibraryDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α),
  sizeOf { cache := cache, addDecl := addDecl, addLibraryDecl := addLibraryDecl } = 1 + sizeOf cache
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.ofTree.eq_1 : DyckWord.ofTree BinaryTree.nil = 0
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The preimage of a finitely generated normal subgroup by a surjective homomorphism with
a finitely generated kernel is finitely generated.  -/
Subgroup.IsFinitelyNormallyGenerated.comap : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {N : Subgroup H},
  N.IsFinitelyNormallyGenerated →
    ∀ {f : G →* H},
      Function.Surjective ⇑f → f.ker.IsFinitelyNormallyGenerated → (Subgroup.comap f N).IsFinitelyNormallyGenerated
-- Mathlib.Data.Finset.Sym
Finset.isDiag_mk_of_mem_diag : ∀ {α : Type u_1} {s : Finset α} {a b : α}, (a, b) ∈ s.diag → s(a, b).IsDiag
-- Mathlib.LinearAlgebra.TensorProduct.Free
/-- The `A`-algebra isomorphism `A ⊗[R] V ≃ₗ[A] (ι →₀ A)` coming from an
`ι`-indexed basis of a free `R`-module `V`.
 -/
Algebra.TensorProduct.equivFinsuppOfBasis : {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring R] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → {ι : Type u_4} → Module.Basis ι R V → TensorProduct R A V ≃ₗ[A] ι →₀ A
-- Mathlib.RingTheory.Multiplicity
dvd_of_multiplicity_pos : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, 0 < multiplicity a b → a ∣ b
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_of_nonneg : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X} {g : X → ℝ},
  (∀ x ∈ s, 0 ≤ f x) →
    (∀ x ∈ s, f x ≤ g x) → MeasureTheory.IntegrableOn g s μ → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.getElem_sdiv.match_1.splitter : (motive : Bool → Bool → Sort u_1) →
  (x x_1 : Bool) →
    (Unit → motive false false) →
      (Unit → motive false true) → (Unit → motive true false) → (Unit → motive true true) → motive x x_1
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth.  -/
ContMDiffWithinAt.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (x : B) → NormedAddCommGroup (E x)] [inst_9 : (x : B) → InnerProductSpace ℝ (E x)]
  [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E] {EM : Type u_6} [inst_12 : NormedAddCommGroup EM]
  [inst_13 : NormedSpace ℝ EM] {HM : Type u_7} [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM}
  {M : Type u_8} [inst_15 : TopologicalSpace M] [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E]
  {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} {x : M},
  ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun m => ⟨b m, v m⟩) s x →
    ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun m => ⟨b m, w m⟩) s x →
      ContMDiffWithinAt IM (modelWithCornersSelf ℝ ℝ) n (fun m => inner ℝ (v m) (w m)) s x
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedClassifyResult.default : Lean.Meta.Sym.Arith.ClassifyResult
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRatUnits.eq_1 : ∀ {n : ℕ} (ls : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.insertRatUnits ls =
    match List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (ratUnits, assignments, false) ls with
    | (ratUnits, assignments, foundContradiction) =>
      ({ clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments },
        foundContradiction)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balRight.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α)
  (c : RBTree.RBNode α),
  l = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) →
    (match l with
      | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
      | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
      | l => h_3 l) ≍
      h_2 a x b y c
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
contDiffOn_one_iff_derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜},
  UniqueDiffOn 𝕜 s → (ContDiffOn 𝕜 1 f s ↔ DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux.eq_1 : Complex.GammaAux✝ 0 = Complex.GammaIntegral
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.comp_refl : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N), f.comp (FirstOrder.Language.Embedding.refl L M) = f
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid of some points.  Although defined for any `s`, this
is intended to be used in the case where the number of points,
converted to `k`, is not zero.  -/
Finset.centroid : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : DivisionRing k] →
        [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → P
-- Init.Data.List.Basic
List.replicate.eq_2 : ∀ {α : Type u} (x : α) (n : ℕ), List.replicate n.succ x = x :: List.replicate n x
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.eq_1 : ∀ (s : String.Slice), s.intercalate [] = ""
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prodEquiv.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (K : Subgroup N),
  H.prodEquiv K = { toEquiv := Equiv.Set.prod ↑H ↑K, map_mul' := ⋯ }
-- Init.Data.Array.Lex.Lemmas
/-- `l₁` is *not* lexicographically less than `l₂`
(which you might think of as "`l₂` is lexicographically greater than or equal to `l₁`"") if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length` or
- there exists an index `i` such that
  - for all `j < i`, `l₁[j] == l₂[j]` and
  - `l₂[i] < l₁[i]`

This formulation requires that `==` and `lt` are compatible in the following senses:
- `==` is symmetric
  (we unnecessarily further assume it is transitive, to make use of the existing typeclasses)
- `lt` is irreflexive with respect to `==` (i.e. if `x == y` then `lt x y = false`
- `lt` is asymmetric  (i.e. `lt x y = true → lt y x = false`)
- `lt` is antisymmetric with respect to `==` (i.e. `lt x y = false → lt y x = false → x == y`)
 -/
Array.lex_eq_false_iff_exists : ∀ {α : Type u_1} {l₁ l₂ : Array α} [inst : BEq α] [PartialEquivBEq α] (lt : α → α → Bool),
  (∀ (x y : α), (x == y) = true → lt x y = false) →
    (∀ (x y : α), lt x y = true → lt y x = false) →
      (∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true) →
        (l₁.lex l₂ lt = false ↔
          (l₂.isEqv (l₁.take l₂.size) fun x1 x2 => x1 == x2) = true ∨
            ∃ i,
              ∃ (h₁ : i < l₁.size) (h₂ : i < l₂.size),
                (∀ (j : ℕ) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true)
-- Mathlib.RingTheory.Morita.Basic
MoritaEquivalence.linear : ∀ {R : Type u₀} [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (self : MoritaEquivalence R A B),
  CategoryTheory.Functor.Linear R self.eqv.functor
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofQuotient_fromQuotient : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A),
  (Module.Relations.Solution.ofQuotient relations).fromQuotient = LinearMap.id
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k k' : α}, t.getKey? k = some k' → (Std.ExtTreeMap.filterMap f t)[k]? = t[k]?.bind (f k')
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.subset_mul_set : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R} {I : TwoSidedIdeal R}, s ⊆ ↑I → ∀ (t : Set R), s * t ⊆ ↑I
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ \ m₂)[k]? = m₁[k]?
-- Mathlib.Logic.Basic
Decidable.and_forall_ne : ∀ {α : Sort u_1} [DecidableEq α] (a : α) {p : α → Prop}, (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
-- Mathlib.Topology.Algebra.UniformConvergence
instDistribMulActionUniformFun : {α : Type u_1} →
  {β : Type u_2} →
    {M : Type u_5} →
      [inst : Monoid M] → [inst_1 : AddMonoid β] → [DistribMulAction M β] → DistribMulAction M (UniformFun α β)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.homCategory_comp_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {X Y Z : F ⟶ G} (Γ : CategoryTheory.Oplax.LaxTrans.Hom X Y)
  (Δ : CategoryTheory.Oplax.LaxTrans.Hom Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp Γ Δ).as.app a = CategoryTheory.CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of a strictly monotone function and a monotone function is
strictly monotone.  -/
StrictMono.add_monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [AddLeftMono α]
  [AddRightStrictMono α], StrictMono f → Monotone g → StrictMono fun x => f x + g x
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.id_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.NatTrans.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstKey.mk.sizeOf_spec : ∀ (constName : Lean.Name), sizeOf { constName := constName } = 1 + sizeOf constName
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The (total) mass of a finite measure `μ` is `μ univ`, i.e., the cast to `NNReal` of
`(μ : measure Ω) univ`.  -/
MeasureTheory.FiniteMeasure.mass : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → NNReal
-- Mathlib.Order.Interval.Multiset
Multiset.Ioo.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), Multiset.Ioo a b = (Finset.Ioo a b).val
-- Batteries.Control.Nondet.Basic
/-- Convert a non-deterministic value into a list in the monad, retaining the backtrackable state.
 -/
Nondet.toList : {σ : Type} →
  {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Nondet m α → m (List (α × σ))
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.toPolynormableSpace : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [t : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι}, WithSeminorms p → PolynormableSpace 𝕜 E
-- Mathlib.Algebra.Field.Basic
/-- Pullback a `DivisionSemiring` along an injective function.  -/
Function.Injective.divisionRing : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Zero K] →
      [inst_1 : Add K] →
        [inst_2 : Neg K] →
          [inst_3 : Sub K] →
            [inst_4 : One K] →
              [inst_5 : Mul K] →
                [inst_6 : Inv K] →
                  [inst_7 : Div K] →
                    [inst_8 : SMul ℕ K] →
                      [inst_9 : SMul ℤ K] →
                        [inst_10 : SMul ℚ≥0 K] →
                          [inst_11 : SMul ℚ K] →
                            [inst_12 : Pow K ℕ] →
                              [inst_13 : Pow K ℤ] →
                                [inst_14 : NatCast K] →
                                  [inst_15 : IntCast K] →
                                    [inst_16 : NNRatCast K] →
                                      [inst_17 : RatCast K] →
                                        (f : K → L) →
                                          Function.Injective f →
                                            [inst_18 : DivisionRing L] →
                                              f 0 = 0 →
                                                f 1 = 1 →
                                                  (∀ (x y : K), f (x + y) = f x + f y) →
                                                    (∀ (x y : K), f (x * y) = f x * f y) →
                                                      (∀ (x : K), f (-x) = -f x) →
                                                        (∀ (x y : K), f (x - y) = f x - f y) →
                                                          (∀ (x : K), f x⁻¹ = (f x)⁻¹) →
                                                            (∀ (x y : K), f (x / y) = f x / f y) →
                                                              (∀ (n : ℕ) (x : K), f (n • x) = n • f x) →
                                                                (∀ (n : ℤ) (x : K), f (n • x) = n • f x) →
                                                                  (∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) →
                                                                    (∀ (q : ℚ) (x : K), f (q • x) = q • f x) →
                                                                      (∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                                        (∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) →
                                                                          (∀ (n : ℕ), f ↑n = ↑n) →
                                                                            (∀ (n : ℤ), f ↑n = ↑n) →
                                                                              (∀ (q : ℚ≥0), f ↑q = ↑q) →
                                                                                (∀ (q : ℚ), f ↑q = ↑q) → DivisionRing K
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- A functor `PreservesLimit₂ K₁ K₂` if whenever `c₁` is a limit cone and `c₂` is a limit
cone then `G.mapCone₂ c₁ c₂` is a limit cone. This can be thought of as the data of an
isomorphism $\lim_{(j_1,j_2)} G(K_1(j_1), K_2(j_2)) \simeq G(\lim K_1, \lim K_2)$.
 -/
CategoryTheory.Limits.PreservesLimit₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    CategoryTheory.Functor J₁ C₁ →
                      CategoryTheory.Functor J₂ C₂ → CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C) → Prop
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- A version of `exists_ne_zero_mem_ideal_lt'` for the ring of integers of `K`.  -/
NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt' : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {f : NumberField.InfinitePlace K → NNReal}
  (w₀ : { w // w.IsComplex }),
  NumberField.mixedEmbedding.minkowskiBound K 1 <
      MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀) →
    ∃ a,
      a ≠ 0 ∧
        (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧
          |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_A' : ∀ (q r : ℕ+), ADEInequality.Admissible (ADEInequality.A' q r)
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.ιIso_hom_left : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (SSet.Subcomplex.unionProd.ιIso S T).hom.left = ⋯.isoPushout.hom
-- Init.Data.UInt.Lemmas
USize.toNat_lt : ∀ (n : USize), n.toNat < 2 ^ 64
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_false_of_isEmpty_erase!_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false → t.isEmpty = false
-- Lean.Parser.Basic
Lean.Parser.LeadingIdentBehavior.symbol.sizeOf_spec : sizeOf Lean.Parser.LeadingIdentBehavior.symbol = 1