mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Raw.Const.getD (m₁ ∪ m₂) k fallback =
          Std.DTreeMap.Raw.Const.getD m₂ k (Std.DTreeMap.Raw.Const.getD m₁ k fallback)
-- Mathlib.Algebra.Group.Defs
/-- We lower the priority of inheriting from cancellative structures.
This attempts to avoid expensive checks involving bundling and unbundling with the `IsDomain` class.
since `IsDomain` already depends on `Semiring`, we can synthesize that one first.
Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60simpNF.60.20complaining.20here.3F
 -/
LibraryNote.lower_cancel_priority : Batteries.Util.LibraryNote
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The differential mapping into `C.X j`, or zero if there isn't one.
 -/
HomologicalComplex.dTo : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (C : HomologicalComplex V c) → (j : ι) → C.xPrev j ⟶ C.X j
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.getMatcherInfo? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.Meta.MatcherInfo)
-- Mathlib.NumberTheory.Bertrand
/-- **Alias** of `Nat.exists_prime_lt_and_le_two_mul`.

---

**Bertrand's Postulate**: For any positive natural number, there is a prime which is greater than
it, but no more than twice as large.
 -/
Nat.bertrand : ∀ (n : ℕ), n ≠ 0 → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (m : ℕ) → motive 0 m.succ)
  (h_3 : (k m : ℕ) → motive k.succ m),
  (match x, 0 with
    | x, 0 => h_1 x
    | 0, m.succ => h_2 m
    | k.succ, m => h_3 k m) =
    h_1 x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.not_mem_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, k ∉ ∅
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {c : β}, c ≠ 0 → (MeasureTheory.HasFiniteIntegral (fun x => c) μ ↔ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.fst_mem_orbit_of_mem_orbit : ∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {β : Type u_1} [inst_2 : MulAction M β]
  {x y : α × β}, x ∈ MulAction.orbit M y → x.1 ∈ MulAction.orbit M y.1
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isClosedEmbedding_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], Topology.IsClosedEmbedding fun x => {x}
-- Mathlib.Topology.Algebra.Monoid.Defs
SeparatelyContinuousAdd.mk : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M],
  (∀ {a : M}, Continuous fun x => a + x) → (∀ {a : M}, Continuous fun x => x + a) → SeparatelyContinuousAdd M
-- Mathlib.Algebra.Module.LocalizedModule.Basic
localizedModuleIsLocalizedModule : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], IsLocalizedModule S (LocalizedModule.mkLinearMap S M)
-- Mathlib.Topology.ContinuousMap.Algebra
continuousSubmonoid.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : MulOneClass β]
  [inst_3 : ContinuousMul β], continuousSubmonoid α β = { carrier := {f | Continuous f}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  (M : AddSubgroup H) [inst_2 : M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M),
  QuotientAddGroup.map N M f h = QuotientAddGroup.lift N ((QuotientAddGroup.mk' M).comp f) ⋯
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `(s : S)` is in the image of `f`, then `monomial n s` lifts.  -/
Polynomial.monomial_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {s : S} (n : ℕ),
  s ∈ Set.range ⇑f → (Polynomial.monomial n) s ∈ Polynomial.lifts f
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.congr_trans : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {T : Type u_3} {U : Type u_4} [inst_3 : Semiring T] [inst_4 : Semiring U]
  (w : AbsoluteValue T S) (u : AbsoluteValue U S) (f : R ≃+* T) (g : T ≃+* U),
  WithAbs.congr v u (f.trans g) = (WithAbs.congr v w f).trans (WithAbs.congr w u g)
-- Lean.Meta.Iterator
/-- Function for getting next value and state pair.  -/
Lean.Meta.Iterator.next : {α : Type} → Lean.Meta.Iterator α → Lean.MetaM (Option (α × Lean.Meta.SavedState))
-- Mathlib.Tactic.Ring.Common
/-- `ExBaseNat e` stores the structure of a normalized expression `e : Q(ℕ)`, which appears
as the base of an exponent expression `e^n`. The `sum` constructor is only used when the exponent
`n` is not a constant.

Used to represent normalized natural number expressions in exponents.

`ExBaseNat q($e)` is equivalent to `ExBase btℕ sℕ q($e)`, and one can cast between the two.  -/
Mathlib.Tactic.Ring.Common.ExBaseNat : Q(ℕ) → Type
-- Mathlib.LinearAlgebra.Span.Defs
/-- In a non-unital algebra, if every element of a set `s` commutes with `x`, then every element of
`Submodule.span R s` commutes with `x`.  -/
Commute.span_left : ∀ {R : Type u_8} {A : Type u_9} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {x : A},
  (∀ y ∈ s, Commute y x) → ∀ y ∈ Submodule.span R s, Commute y x
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.noConfusionType : Sort v✝ → Lean.Meta.ACLt.ReduceMode → Lean.Meta.ACLt.ReduceMode → Sort v✝
-- Batteries.Data.Fin.Coding
/-- Encode `Fin m × Fin n` into `Fin (m * n)`.  -/
Fin.encodeProd : {m n : ℕ} → Fin m × Fin n → Fin (m * n)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
/-- Given matrix `A` and list `strictIndexes` of strict inequalities' indexes, we want to state the
Linear Programming problem which solution would give us a solution for the initial problem (see
`findPositiveVector`).

As an objective function (that we are trying to maximize) we use sum of coordinates from
`strictIndexes`: it suffices to find the nonnegative vector that makes this function positive.

We introduce two auxiliary variables and one constraint:
* The variable `y` is interpreted as "homogenized" `1`. We need it because dealing with a
  homogenized problem is easier, but having some "unit" is necessary.
* To bound the problem we add the constraint `x₁ + ... + xₘ + z = y` introducing new variable `z`.

The objective function also interpreted as an auxiliary variable with constraint
`f = ∑ i ∈ strictIndexes, xᵢ`.

The variable `f` has to always be basic while `y` has to be free. Our Gauss method implementation
greedy collects basic variables moving from left to right. So we place `f` before `x`-s and `y`
after them. We place `z` between `f` and `x` because in this case `z` will be basic and
`Gauss.getTableau` produce tableau with nonnegative last column, meaning that we are starting from
a feasible point.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.stateLP : {matType : ℕ → ℕ → Type} →
  [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    {n m : ℕ} → matType n m → List ℕ → matType (n + 2) (m + 3)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_ofAdd_of_toAdd_unzero_lt : ∀ {α : Type u_1} [inst : Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0),
  Multiplicative.toAdd (WithZero.unzero ha) < b → a < ↑(Multiplicative.ofAdd b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.maxKey? l = Std.Internal.List.maxKey? l'
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.HasArgminEstimator.mk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Θ]
  [inst_1 : Nonempty Θ] {𝓨 : Type u_4} [inst_2 : MeasurableSpace 𝓨] {ℓ : Θ → 𝓨 → ENNReal}
  {P : ProbabilityTheory.Kernel Θ 𝓧} [inst_3 : ProbabilityTheory.IsFiniteKernel P] {π : MeasureTheory.Measure Θ}
  [inst_4 : MeasureTheory.IsFiniteMeasure π],
  (∃ f, ProbabilityTheory.IsArgminEstimator ℓ P π f) → ProbabilityTheory.HasArgminEstimator ℓ P π
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.nhds_zero : nhds 0 = ⨅ a, ⨅ (_ : a ≠ 0), Filter.principal (Set.Iio a)
-- Mathlib.Logic.Relation
Relation.fun_eq_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} (f : γ → α),
  Relation.Comp (fun x1 x2 => f x1 = x2) r = fun x => r (f x)
-- Mathlib.CategoryTheory.IsConnected
/-- A possibly empty category for which every functor to a discrete category is constant.
 -/
CategoryTheory.IsPreconnected : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → Prop
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.alterₘ.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.isMonHom_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) {X Y : C}
  [inst_5 : CategoryTheory.MonObj X] [inst_6 : CategoryTheory.MonObj Y] (f : F.obj X ⟶ F.obj Y)
  [CategoryTheory.IsMonHom f], CategoryTheory.IsMonHom (hF.preimage f)
-- Mathlib.Data.Fintype.EquivFin
Finite.of_injective : ∀ {α : Sort u_4} {β : Sort u_5} [Finite β] (f : α → β), Function.Injective f → Finite α
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `IsPrimePow n`, `n ≠ 2` and `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`),
then the norm of `zeta n K L - 1` is `n.minFac`.  -/
IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow : ∀ {n : ℕ} [inst : NeZero n] {K : Type u} (L : Type v) [inst_1 : Field K] [inst_2 : Field L] [inst_3 : Algebra K L],
  IsPrimePow n →
    ∀ [inst_4 : IsCyclotomicExtension {n} K L],
      Irreducible (Polynomial.cyclotomic n K) →
        n ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta n K L - 1) = ↑n.minFac
-- Mathlib.Algebra.Group.Submonoid.Finite
AddSubmonoid.pi_mem_of_single_mem_aux : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → AddZeroClass (f i)] {S : Type u_3}
  [inst_1 : SetLike S ((i : η) → f i)] [AddSubmonoidClass S ((i : η) → f i)] [inst_3 : DecidableEq η] (I : Finset η)
  {H : S} (x : (i : η) → f i), (∀ i ∉ I, x i = 0) → (∀ i ∈ I, Pi.single i (x i) ∈ H) → x ∈ H
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  (CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).obj A = A.obj
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} {f : β → β},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.modify t k f) k = Option.map f (Std.ExtDTreeMap.Const.get? t k)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorRightIso_inv_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X X_1 : Cᴹᵒᵖ),
  (X.tensorRightIso.inv.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.unmop X_1.unmop)
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_singleton' : ∀ {α : Type u} [inst : Semiring α] {x y : α}, x ∈ Ideal.span {y} ↔ ∃ a, a * y = x
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.lcm_eq_zero_iff : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {x y : R},
  EuclideanDomain.lcm x y = 0 ↔ x = 0 ∨ y = 0
-- Lean.Class
/-- Registers an inductive type or structure as a type class. Using `class` or `class inductive` is
generally preferred over using `@[class] structure` or `@[class] inductive` directly.
 -/
_private.Lean.Class.0.Lean.init : IO Unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).getKey? k = t₂.getKey? k
-- Init.Data.BitVec.Lemmas
BitVec.getElem_signExtend : ∀ {w : ℕ} {x : BitVec w} {v i : ℕ} (h : i < v), (BitVec.signExtend v x)[i] = if h : i < w then x[i] else x.msb
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} (f : k.Hom l) (g : l.Hom m),
  (f.comp g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Polynomial.isRoot_cyclotomic_iff : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] {μ : R},
  (Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.d_normEq0 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (c : ℕ)
  (init p₁ p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.d_normEq0_cert c p₁ p₂ p = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p₁ →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 →
        ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.Topology.Bornology.Constructions
Prod.instBornology : {α : Type u_1} → {β : Type u_2} → [Bornology α] → [Bornology β] → Bornology (α × β)
-- Mathlib.Algebra.Lie.Graded
DirectSum.instLieAlgebraSubtypeMemSubmodule : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : CommRing R] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                (ℒ : ι → Submodule R L) → [inst_5 : GradedLieAlgebra ℒ] → LieAlgebra R (DirectSum ι fun i => ↥(ℒ i))
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.comparison_obj_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C),
  ((CategoryTheory.Comonad.comparison h).obj X).A = L.obj X
-- Mathlib.Topology.Separation.Regular
exists_mem_nhdsSet_isClosed_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {u s : Set X},
  s ∈ nhdsSet u → IsClosed u → ∃ t ∈ nhdsSet u, IsClosed t ∧ t ⊆ s
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
_private.Mathlib.Analysis.Calculus.FDeriv.OfCompLeft.0.HasFDerivAtFilter.of_comp_aux : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F}
  {f' : F →L[𝕜] G} {h' : E →L[𝕜] G} {lE : Filter (E × E)} {lF : Filter (F × F)},
  Topology.IsEmbedding ⇑f' →
    Filter.Tendsto (Prod.map g g) lE lF →
      HasFDerivAtFilter h h' lE →
        HasFDerivAtFilter f f' lF →
          Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h →
            ((fun x =>
                  match x with
                  | (x, y) => g x - g y - g' (x - y)) =O[𝕜;
                lE] fun x =>
                match x with
                | (x, y) => f' (g x - g y) - h' (x - y)) →
              HasFDerivAtFilter g g' lE
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn_cons_aux : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α}
  {f : α → β} (hxs : xs ≠ []),
  List.minIdxOn f (x :: xs) ⋯ = List.combineMinIdxOn✝ f (List.minIdxOn f [x] ⋯) (List.minIdxOn f xs hxs) ⋯ ⋯
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_le_add : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  {a b c d : M}, a ≤ b → c ≤ d → a + c ≤ b + d
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- If
```
(f 0)
(0 g)
```
is invertible, then `f` is invertible.
 -/
CategoryTheory.isIso_left_of_isIso_biprod_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)], CategoryTheory.IsIso f
-- Lean.Message
Lean.MessageData.instCoeFormat : Coe Std.Format Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint], F.PreservesZeroMorphisms
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_infty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E}, ContDiffWithinAt 𝕜 (↑⊤) f s x ↔ ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n) f s x
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.const_smul_sum : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] {𝕜' : Type} [inst_11 : DivisionSemiring 𝕜'] [inst_12 : Module 𝕜' F]
  [inst_13 : ContinuousConstSMul 𝕜' F] [inst_14 : SMulCommClass 𝕜 𝕜' F] [T2Space F] (a : 𝕜')
  (f : FormalMultilinearSeries 𝕜 E F), a • f.sum = (a • f).sum
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.isCycleOn_inv`. -/
Equiv.Perm.IsCycleOn.of_inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f⁻¹.IsCycleOn s → f.IsCycleOn s
-- Mathlib.Logic.Equiv.Set
Equiv.symm_preimage_preimage : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β), ⇑e.symm ⁻¹' ⇑e ⁻¹' s = s
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.eventually_forall_ge_atTop : ∀ {α : Type u_3} [inst : Preorder α] {p : α → Prop},
  (∀ᶠ (x : α) in Filter.atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in Filter.atTop, p x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.zero_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ} (x : ↥(Opposite.unop V)),
  ↑0 x = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_inter_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The class of morphisms in `C` that are colimits of shape `J` of
natural transformations involving morphisms in `W`.  -/
CategoryTheory.MorphismProperty.colimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.MorphismProperty C
-- Init.Data.Array.Lex.Lemmas
Array.lt_toList : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α}, xs.toList < ys.toList ↔ xs < ys
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {fst snd : S.Arrow} {r : fst.Relation snd} {fst_1 snd_1 : S.Arrow} {r_1 : fst_1.Relation snd_1},
  { fst := fst, snd := snd, r := r } = { fst := fst_1, snd := snd_1, r := r_1 } → fst = fst_1 ∧ snd = snd_1 ∧ r ≍ r_1
-- Mathlib.GroupTheory.Torsion
/-- For prime `p`, `g` lies in the additive `p`-primary component iff its additive
order is a power of `p`.  -/
AddCommGroup.mem_primaryComponent_iff_addOrderOf : ∀ {G : Type u_1} [inst : AddCommGroup G] {p : ℕ} [Fact (Nat.Prime p)] {g : G},
  g ∈ AddCommGroup.primaryComponent G p ↔ ∃ n, addOrderOf g = p ^ n
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Right unitor for the vertical composition of oplax natural transformations.  -/
CategoryTheory.Lax.OplaxTrans.rightUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id G) ≅ η
-- Mathlib.Order.CompleteLatticeIntervals
/-- `SupSet` structure on a nonempty subset `s` of a preorder with `SupSet`. This definition is
non-canonical (it uses `default s`); it should be used only as here, as an auxiliary instance in the
construction of the `ConditionallyCompleteLinearOrder` structure.  -/
subsetSupSet : {α : Type u_2} → (s : Set α) → [Preorder α] → [SupSet α] → [Inhabited ↑s] → SupSet ↑s
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.mul.eq_2 : ∀ {n : ℕ} (a a_1 : ZMod (2 * n)),
  QuaternionGroup.mul✝ (QuaternionGroup.a a) (QuaternionGroup.xa a_1) = QuaternionGroup.xa (a_1 - a)
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.integral_id_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E], ∫ (x : E), x ∂ProbabilityTheory.stdGaussian E = 0
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.natDegree_removeFactor' : ∀ {K : Type v} [inst : Field K] {f : Polynomial K} {n : ℕ}, f.natDegree = n + 1 → f.removeFactor.natDegree = n
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget_createsLimitsOfSize.eq_1 : AddCommGrpCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b