mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- The entries of a positive Cauchy sequence eventually have a positive lower bound.  -/
CauSeq.Pos : {α : Type u_1} → [inst : Field α] → [inst_1 : LinearOrder α] → [inst_2 : IsStrictOrderedRing α] → CauSeq α abs → Prop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.mk : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A],
  p 0 →
    ∀ [compactSpace_spectrum : ∀ (a : A), CompactSpace ↑(spectrum R a)],
      (∀ [Nontrivial A] (a : A), p a → (spectrum R a).Nonempty) →
        (∀ (a : A),
            p a →
              ∃ φ,
                Continuous ⇑φ ∧
                  Function.Injective ⇑φ ∧
                    φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧
                      (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = Set.range ⇑f) ∧
                        ∀ (f : C(↑(spectrum R a), R)), p (φ f)) →
          ContinuousFunctionalCalculus R A p
-- Mathlib.Algebra.Order.Floor.Defs
/-- `⌈a⌉₊` is the least natural `n` such that `a ≤ n`  -/
Nat.ceil : {α : Type u_2} → [inst : Semiring α] → [inst_1 : PartialOrder α] → [FloorSemiring α] → α → ℕ
-- Mathlib.RingTheory.Ideal.Prod
instIsPrincipalIdealRingProd : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] [IsPrincipalIdealRing R] [IsPrincipalIdealRing S],
  IsPrincipalIdealRing (R × S)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = false → m[a]? = none
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.isRatStieltjesPoint : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α), ProbabilityTheory.IsRatStieltjesPoint f a
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton.congr_simp : ∀ {R : Type u_5} [inst : CommRing R] (S : Submonoid R) {P : Type u_6} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x x_1 : P),
  x = x_1 → FractionalIdeal.spanSingleton S x = FractionalIdeal.spanSingleton S x_1
-- Std.Data.ExtHashMap.Lemmas
/-- Simpler variant of `getElem!_filter` when `LawfulBEq` is available.  -/
Std.ExtHashMap.getElem!_filter' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α}, (Std.ExtHashMap.filter f m)[k]! = (Option.filter (f k) m[k]?).get!
-- Mathlib.Computability.EpsilonNFA
εNFA.instOne : {α : Type u} → {σ : Type v} → One (εNFA α σ)
-- Mathlib.Order.CompleteLatticeIntervals
subset_sSup_emptyset : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : SupSet α] [inst_2 : Inhabited ↑s], sSup ∅ = default
-- Mathlib.NumberTheory.SmoothNumbers
Nat.equivProdNatSmoothNumbers_apply' : ∀ {p : ℕ} (hp : Nat.Prime p) (x : ℕ × ↑p.smoothNumbers), ↑((Nat.equivProdNatSmoothNumbers hp) x) = p ^ x.1 * ↑x.2
-- Lean.Parser.Command
Lean.Parser.Command.private.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instGeometricallyReducedOverSchemeInferInstanceOverClass : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.GeometricallyReduced (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.RingTheory.Idempotents
/-- The corner associated to an element `e` in a ring without 1
is the subring without 1 of all elements of the form `e * r * e`.  -/
NonUnitalRing.corner : {R : Type u_1} → R → [inst : NonUnitalRing R] → NonUnitalSubring R
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  m.WF → Std.HashMap.Raw.forIn f init m = forIn m.toArray init fun a b => f a.1 a.2 b
-- Mathlib.Data.Fintype.BigOperators
/-- An uncurried version of `Finset.prod_prod_type_right`.  -/
Fintype.prod_prod_type_right' : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid γ]
  (f : α₁ → α₂ → γ), ∏ x, f x.1 x.2 = ∏ y, ∏ x, f x y
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingFlipEquiv_apply_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (a : CategoryTheory.Functor D (CategoryTheory.Functor C E)) {X Y : C × D} (f : X ⟶ Y),
  (CategoryTheory.Functor.curryingFlipEquiv a).map f =
    CategoryTheory.CategoryStruct.comp ((a.map f.2).app X.1) ((a.obj Y.2).map f.1)
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Equal characteristic implies `ℚ`-algebra.  -/
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.algebraRat : {R : Type u_1} → [inst : CommRing R] → (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → Algebra ℚ R
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.instIsStrictlySupportedExtend : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c'),
  (K.extend e).IsStrictlySupported e
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- Any `v`-cover `𝒰` induces a `u`-cover indexed by the points of `X`.  -/
AlgebraicGeometry.Scheme.Cover.ulift : {X : AlgebraicGeometry.Scheme} →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X →
      AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_lt_top : ∀ {c : Cardinal.{u}}, Cardinal.toENat c < ⊤ ↔ c < Cardinal.aleph0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'_mem : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w // w.IsComplex }) {x : K},
  (NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀ ↔
    (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.solvable_iff_equiv_solvable : ∀ {R : Type u} {L : Type v} {L' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (e : L' ≃ₗ⁅R⁆ L), LieAlgebra.IsSolvable L' ↔ LieAlgebra.IsSolvable L
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.List.orderedInsert : {α : Type u_1} → autoParam (α → α → Bool) List.orderedInsert._auto_3✝ → α → List α → List α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_none : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∉ m → m.getKey? a = none
-- Std.Http.Data.Status
/-- 303 See Other
 -/
Std.Http.Status.seeOther : Std.Http.Status
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_bot : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S], Ideal.spanNorm R ⊥ = ⊥
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Help typeclass inference to infer creation of finite colimits for the forgetful functor.  -/
CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatForgetFunObjFiniteOfFinCategory : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget FintypeCat)
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.parentD_push : ∀ {a : ℕ} {arr : Array Batteries.UFNode},
  Batteries.UnionFind.parentD (arr.push { parent := arr.size, rank := 0 }) a = Batteries.UnionFind.parentD arr a
-- Batteries.Util.ProofWanted
theorem_wanted.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Antichain
IsAntichain.singleton : ∀ {α : Type u_1} {r : α → α → Prop} {a : α}, IsAntichain r {a}
-- Mathlib.Data.List.Basic
List.forall_append : ∀ {α : Type u} {p : α → Prop} {xs ys : List α}, List.Forall p (xs ++ ys) ↔ List.Forall p xs ∧ List.Forall p ys
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_inf_aux_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f p
-- Init.Prelude
Lean.Syntax.brecOn_1.go : {motive_1 : Lean.Syntax → Sort u} →
  {motive_2 : Array Lean.Syntax → Sort u} →
    {motive_3 : List Lean.Syntax → Sort u} →
      (t : Array Lean.Syntax) →
        ((t : Lean.Syntax) → t.below → motive_1 t) →
          ((t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) →
            ((t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) → motive_2 t ×' Lean.Syntax.below_1 t
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then
`f` is a strictly monotone function.  -/
strictMono_of_hasDerivAt_pos : ∀ {f f' : ℝ → ℝ}, (∀ (x : ℝ), HasDerivAt f (f' x) x) → (∀ (x : ℝ), 0 < f' x) → StrictMono f
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- If the kernel functions are uniformly bounded (`‖kerFun H x‖ ≤ C` for all `x`), then
convergence in `H`-norm implies uniform convergence of the underlying functions.  -/
RKHS.tendstoUniformly_of_norm_kerFun_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] {C : ℝ},
  (∀ (x : X), ‖RKHS.kerFun H x‖ ≤ C) →
    ∀ {ι : Type u_5} {l : Filter ι} {F : ι → H} {f : H},
      Filter.Tendsto F l (nhds f) → TendstoUniformly (fun n => ⇑(F n)) (⇑f) l
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsFunOfQuotHom_coe_coe : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} {f : R ⧸ I →+* A ⧸ J} (hf : Function.Surjective ⇑f) (X : { p // p ∣ I }),
  ↑((IsDedekindDomain.idealFactorsFunOfQuotHom hf) X) =
    Ideal.comap (Ideal.Quotient.mk J) (Ideal.map f (Ideal.map (Ideal.Quotient.mk I) ↑X))
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Sum of a multiset of elements in a `NonUnitalSubring` of a `NonUnitalRing` is
in the `NonUnitalSubring`.  -/
NonUnitalSubring.multiset_sum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (m : Multiset R),
  (∀ a ∈ m, a ∈ s) → m.sum ∈ s
-- Mathlib.Analysis.Normed.Group.Basic
indiscreteTopology_iff_forall_nnnorm_eq_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The congruence relation on `M × S`, `M` a `CommMonoid` and `S` a submonoid of `M`, whose
quotient is the localization of `M` at `S`, defined as the unique congruence relation on
`M × S` such that for any other congruence relation `s` on `M × S` where for all `y ∈ S`,
`(1, 1) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies
`(x₁, y₁) ∼ (x₂, y₂)` by `s`.  -/
Localization.r : {M : Type u_1} → [inst : CommMonoid M] → (S : Submonoid M) → Con (M × ↥S)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularEpi.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (W : C) →
          (left right : W ⟶ X) →
            (w :
                autoParam (CategoryTheory.CategoryStruct.comp left f = CategoryTheory.CategoryStruct.comp right f)
                  CategoryTheory.RegularEpi.w._autoParam) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f w) → CategoryTheory.RegularEpi f
-- Init.Data.Int.Order
Int.sub_le_sub : ∀ {a b c d : ℤ}, a ≤ b → c ≤ d → a - d ≤ b - c
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsSeparated f],
  AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.one : {R : Type u_1} → [inst : Zero R] → [One R] → One (ArithmeticFunction R)
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Bundled non-unital semiring homomorphisms `α →ₙ+* β`; use this for bundled non-unital ring
homomorphisms too.

When possible, instead of parametrizing results over `(f : α →ₙ+* β)`,
you should parametrize over `(F : Type*) [NonUnitalRingHomClass F α β] (f : F)`.

When you extend this structure, make sure to extend `NonUnitalRingHomClass`.  -/
NonUnitalRingHom : (α : Type u_5) → (β : Type u_6) → [NonUnitalNonAssocSemiring α] → [NonUnitalNonAssocSemiring β] → Type (max u_5 u_6)
-- Lean.Environment
/-- Saved `Environment`, untyped to avoid cyclic reference. Import environment for imported constants.
 -/
_private.Lean.Environment.0.Lean.RealizationContext.env : Lean.RealizationContext✝ → NonScalar
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).support = u :: p.support
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.congrRight_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] (e : Y ≃ Z) (g : LocallyConstant X Z),
  (LocallyConstant.congrRight e).symm g = LocallyConstant.map (⇑e.symm) g
-- Mathlib.Order.RelIso.Basic
RelEmbedding.trans_refl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), f.trans (RelEmbedding.refl s) = f
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_trans_self : ∀ {R : Type u_4} {S : Type u_5} [inst : Add R] [inst_1 : Add S] [inst_2 : Mul R] [inst_3 : Mul S] (e : R ≃+* S),
  e.symm.trans e = RingEquiv.refl S
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.instLE : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → LE (L.PartialEquiv M N)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Iic : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.map (finCongr h).toEmbedding (Finset.Iic i) = Finset.Iic (Fin.cast h i)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_conjTranspose : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_14} [inst : Star α]
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o),
  M.conjTranspose.blockDiag' k = (M.blockDiag' k).conjTranspose
-- Init.Data.List.ControlImpl
List.flatMapMTR.loop.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x : List (List β)) (a : α)
  (as : List α),
  List.flatMapMTR.loop f (a :: as) x = do
    let bs' ← f a
    List.flatMapMTR.loop f as (bs' :: x)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
/-- For a compact set `s`, locally uniform convergence on `s` is just uniform convergence on `s`.  -/
tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι}, IsCompact s → (TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s)
-- Init.Meta.Defs
Lean.instQuoteOfCoeHTCTTSyntaxConsSyntaxNodeKindNil : {α : Type} →
  {k k' : Lean.SyntaxNodeKind} → [Lean.Quote α k] → [CoeHTCT (Lean.TSyntax k) (Lean.TSyntax k')] → Lean.Quote α k'
-- Mathlib.RingTheory.RingHomProperties
/-- A property is `StableUnderComposition` if the composition of two such morphisms
still falls in the class.  -/
RingHom.StableUnderComposition : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The affine map from `k` to `P1` sending `0` to `p₀` and `1` to `p₁`.  -/
AffineMap.lineMap : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : Module k V1] → [inst_3 : AddTorsor V1 P1] → P1 → P1 → k →ᵃ[k] P1
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If `f^n x - x`, `n > 0`, is an integer number `m` for some point `x`, then
`τ f = m / n`. On the circle this means that a map with a periodic orbit has
a rational rotation number.  -/
CircleDeg1Lift.translationNumber_of_map_pow_eq_add_int : ∀ (f : CircleDeg1Lift) {x : ℝ} {n : ℕ} {m : ℤ}, (f ^ n) x = x + ↑m → 0 < n → f.translationNumber = ↑m / ↑n
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows.eq_1 : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R),
  A₁.fromRows A₂ = Matrix.of (Sum.elim A₁ A₂)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.erase_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  MonoidAlgebra.erase m (MonoidAlgebra.single m r) = 0
-- Mathlib.Analysis.Normed.Group.NullSubmodule
nullSubgroup.eq_1 : ∀ (M : Type u_1) [inst : SeminormedCommGroup M],
  nullSubgroup M = { carrier := {x | ‖x‖ = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_iff_mem_range_succ : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α],
  ¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ
-- Lean.Compiler.IR.CompilerM
Lean.IR.getDecl : Lean.Name → Lean.IR.CompilerM Lean.IR.Decl
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If `f` and `g` are equivariant maps, then so is `(x, y) ↦ (f x, g y)`.  -/
AddActionHom.prodMap : {M : Type u_1} →
  {N : Type u_2} →
    {α : Type u_3} →
      {β : Type u_4} →
        {γ : Type u_5} →
          {δ : Type u_6} →
            [inst : VAdd M α] →
              [inst_1 : VAdd M β] →
                [inst_2 : VAdd N γ] → [inst_3 : VAdd N δ] → {σ : M → N} → (α →ₑ[σ] γ) → (β →ₑ[σ] δ) → α × β →ₑ[σ] γ × δ
-- Std.Time.Time.PlainTime
Std.Time.instDecidableEqPlainTime : DecidableEq Std.Time.PlainTime
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.instToStringResult : ToString Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- Every isomorphism has a functorial choice of pullbacks.  -/
CategoryTheory.ChosenPullbacksAlong.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {Y X : C} → (f : Y ≅ X) → CategoryTheory.ChosenPullbacksAlong f.hom
-- Mathlib.CategoryTheory.Yoneda
/-- The "Yoneda evaluation" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
to `F.obj X`, functorially in both `X` and `F`.
 -/
CategoryTheory.yonedaEvaluation : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))
-- Mathlib.Analysis.Convex.Between
Wbtw.eq_1 : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y z : P), Wbtw R x y z = (y ∈ affineSegment R x z)
-- Mathlib.Data.Set.Lattice
Set.mem_iUnion_of_mem : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {a : α} (i : ι), a ∈ s i → a ∈ ⋃ i, s i
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.dart_fst_fiber_card_eq_degree : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V] (v : V),
  {d | d.toProd.1 = v}.card = G.degree v
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (Set.Icc a b)⁻¹ = Set.Icc b⁻¹ a⁻¹
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_comap : ∀ {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 : StarSubalgebra R B) (f : A →⋆ₐ[R] B),
  ↑(StarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift_comp_iso : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [inst_7 : IsLocalizedModule S f]
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)),
  IsLocalizedModule.lift S f g h ∘ₗ ↑(IsLocalizedModule.iso S f) = LocalizedModule.lift S g h
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {v : β k} {h₁ : a ∈ m.insert k v}, (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.instIsMulCommutative_iSup : ∀ {R : Type u_1} {A : Type u_2} [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] {ι : Type u_3} [Nonempty ι]
  [inst_7 : Preorder ι] [IsDirectedOrder ι] {S : ι →o StarSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
/-- **Alias** of `AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE`. -/
AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFinitePresentation f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation
-- Mathlib.Algebra.Tropical.Basic
Tropical.instSemigroupTropical : {R : Type u} → [AddSemigroup R] → Semigroup (Tropical R)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_le_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : Preorder M] [MulLeftMono M]
  {f : ι → M}, f ≤ 1 → ∏ i, f i ≤ 1
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define `GCDMonoid` on a structure just from the `lcm` and its properties.  -/
gcdMonoidOfLCM : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [DecidableEq α] →
        (lcm : α → α → α) →
          (∀ (a b : α), a ∣ lcm a b) →
            (∀ (a b : α), b ∣ lcm a b) → (∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a) → GCDMonoid α
-- Mathlib.Algebra.Group.Defs
Monoid.toMulOneClass : {M : Type u} → [self : Monoid M] → MulOneClass M
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A separable uniform space with countably generated uniformity filter is second countable:
one obtains a countable basis by taking the balls centered at points in a dense subset,
and with rational "radii" from a countable open symmetric antitone basis of `𝓤 α`.  -/
UniformSpace.secondCountable_of_separable : ∀ (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated]
  [TopologicalSpace.SeparableSpace α], SecondCountableTopology α