mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Suppose `{ Xᵢ }` is an inverse system of qcqs schemes with affine transition maps.
If `lim Xᵢ` is affine, then some `Xᵢ` is affine.  -/
AlgebraicGeometry.Scheme.exists_isAffine_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)]
  [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] [AlgebraicGeometry.IsAffine c.pt],
  ∃ i, AlgebraicGeometry.IsAffine (D.obj i)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_some_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.max? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Torsor.Basic
/-- Pushforward of a torsor along a surjective map.  -/
Function.Surjective.torsor : {G : Type u_1} →
  {P : Type u_2} →
    {Q : Type u_3} →
      [inst : Group G] →
        [inst_1 : Torsor G P] →
          [inst_2 : SMul G Q] →
            [inst_3 : SDiv G Q] →
              (f : P → Q) →
                Function.Surjective f →
                  (∀ (c : G) (x : P), f (c • x) = c • f x) → (∀ (x y : P), x /ₛ y = f x /ₛ f y) → Torsor G Q
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence follows from pairwise preserved non-negative distance. Backward direction of
`congruent_iff_pairwise_nndist_eq`.  -/
Congruent.of_pairwise_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (Pairwise fun i₁ i₂ => nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ↑(RootPairing.chainBotCoeff i j) + ↑(RootPairing.chainTopCoeff i j) = P.pairingIn ℤ (RootPairing.chainTopIdx i j) i
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.algebraMap_eq : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R],
  algebraMap R (IsLocalRing.ResidueField R) = IsLocalRing.residue R
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
CommMagma.mul_comm : ∀ {G : Type u} [self : CommMagma G] (a b : G), a * b = b * a
-- Mathlib.Data.Matrix.Mul
/-- Bilinear form identity: `(x ᵥ* Aᵀ) ⬝ᵥ y = (y ᵥ* A) ⬝ᵥ x` for commutative semirings.  -/
Matrix.dotProduct_vecMul_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalCommSemiring α] [inst_1 : Fintype m] [inst_2 : Fintype n]
  (A : Matrix m n α) (x : n → α) (y : m → α), Matrix.vecMul x A.transpose ⬝ᵥ y = Matrix.vecMul y A ⬝ᵥ x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_isClosedEmbedding : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ClosedEmbeddingContinuousFunctionalCalculus R A p] {a : A}
  (ha : p a), Topology.IsClosedEmbedding ⇑(cfcHom ha)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_div_iff_left : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {b c : α} (a : α),
  a / b ≤ a / c ↔ c ≤ b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtDTreeMap.Const.ofList l cmp).getKey? k' = some k
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_toBilin' : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix n n R₁), LinearMap.BilinForm.toMatrix' (Matrix.toBilin' M) = M
-- Init.Data.UInt.Bitwise
UInt16.toFin_shiftRight : ∀ (a b : UInt16), b < 16 → (a >>> b).toFin = a.toFin >>> b.toFin
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffVAdd.continuousVAdd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M] (n : WithTop ℕ∞)
  [ContMDiffVAdd I I' n G M], ContinuousVAdd G M
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_comp : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [inst : AddZeroClass α]
  [inst_1 : AddZeroClass β] [inst_2 : AddZeroClass γ] (f : β →+ γ) (g : α →+ β),
  f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix
-- Mathlib.Data.FunLike.Ring
/-- A `FunLike` type with `(f + g) x = f x + g x` and `(f * g) x = f (g x)` is a `MonoidWithZero`
if `α` is a `MonoidWithZero`.  -/
FunLike.monoidWithZero : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α α] →
      [inst_1 : Zero F] →
        [inst_2 : One F] →
          [inst_3 : Mul F] →
            [inst_4 : Zero α] →
              [IsZeroApply F α α] →
                [IsOneApplyEqSelf F α] → [IsMulApplyEqComp F α] → [ZeroHomClass F α α] → MonoidWithZero F
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumUniformlyOn_iff_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α],
  HasSumUniformlyOn f g s ↔ TendstoUniformlyOn (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop s
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_monomial_one : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ),
  (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) 1) = (MvPolynomial.monomial d) 1
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.homEquiv_apply_apply : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (c : A →ₗ[R] CharacterModule B)
  (x : (addConGen (TensorProduct.Eqv R A B)).Quotient),
  (CharacterModule.homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun mn => (c.toAddMonoidHom mn.1) mn.2) ⋯
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_def : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (n : ℕ)
  (x : PreTilt O p), (PreTilt.coeff n) x = (Perfection.coeff (ModP O p) p n) x
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.AddSaturated.sInf : ∀ {M : Type u_1} [inst : AddZeroClass M] {f : Set (AddSubmonoid M)}, (∀ s ∈ f, s.AddSaturated) → (sInf f).AddSaturated
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.orderOf_one_add_four_mul : ∀ (a : ℤ), Odd a → ∀ (n : ℕ), orderOf (1 + 4 * ↑a) = 2 ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instFiniteToSSetOfSimplex : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })), (SSet.Subcomplex.ofSimplex x).toSSet.Finite
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
/-- Given a family of points `p : ι' → P` and an affine basis `b`, if the matrix whose rows are the
coordinates of `p` with respect `b` has a right inverse, then `p` is affine independent.  -/
AffineBasis.affineIndependent_of_toMatrix_right_inv : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [inst_4 : Fintype ι] [Finite ι']
  [inst_6 : DecidableEq ι'] (p : ι' → P) {A : Matrix ι ι' k}, b.toMatrix p * A = 1 → AffineIndependent k p
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtHashSet.ofList l).getD k' fallback = k
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).p =
    CategoryTheory.Limits.Cofork.π c
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE_comp_ofLE_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X Y : CategoryTheory.Subobject B) (h₁ : CategoryTheory.Subobject.mk f ≤ X) (h₂ : X ≤ Y) {Z : C}
  (h : CategoryTheory.Subobject.underlying.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁)
      (CategoryTheory.CategoryStruct.comp (X.ofLE Y h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f Y ⋯) h
-- Lean.Elab.ParseImportsFast
_private.Lean.Elab.ParseImportsFast.0.Lean.ParseImports.finishCommentBlock.eoi : Lean.ParseImports.State → Lean.ParseImports.State
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- `ordinaryHypergeometric (a b c : 𝕂) : 𝔸 → 𝔸`, denoted `₂F₁`, is the ordinary hypergeometric map,
defined as the sum of the `FormalMultilinearSeries` `ordinaryHypergeometricSeries 𝔸 a b c`.

Note that this takes the junk value `0` outside the radius of convergence.
 -/
term₂F₁ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Opposite
AddOpposite.addSemiconjBy_unop : ∀ {α : Type u_1} [inst : Add α] {a x y : αᵃᵒᵖ},
  AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop x) ↔ AddSemiconjBy a x y
-- Std.Data.ByteSlice
instSliceableByteSliceNat_4 : Std.Roo.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.Order.RelClasses
/-- Set notation form of `ge_of_eq` -/
superset_of_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a = b → b ⊆ a
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ChangeAnnotationSupport.groupsOnLabel? : Lean.Lsp.ChangeAnnotationSupport → Option Bool
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
/-- An object `X` in an abelian category has Injective dimension `≤ n` if
all `Ext X Y i` vanish when `n + 1 ≤ i`  -/
CategoryTheory.HasInjectiveDimensionLE : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → ℕ → Prop
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.IsRightKanExtension.nonempty_isUniversal : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} H} {inst_2 : CategoryTheory.Category.{v_4, u_4} D}
  {F' : CategoryTheory.Functor D H} {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  {α : L.comp F' ⟶ F} [self : F'.IsRightKanExtension α],
  Nonempty (CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk F' α))
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.addEquiv_symm_apply : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] (ofLp : V), (WithLp.addEquiv p V).symm ofLp = WithLp.toLp p ofLp
-- Mathlib.CategoryTheory.Quotient
/-- The functor from a category to its quotient.  -/
CategoryTheory.Quotient.functor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (r : HomRel C) → CategoryTheory.Functor C (CategoryTheory.Quotient r)
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprCertificateOracle : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Linarith.CertificateOracle
-- Init.Data.Array.Lemmas
Array.all_eq_not_any_not : ∀ {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : ℕ},
  as.all p start stop = !as.any (fun x => !p x) start stop
-- Mathlib.Order.Cover
covBy_irrefl : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬a ⋖ a
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vsub_cancel_left : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y z : P), dist (x -ᵥ y) (x -ᵥ z) = dist y z
-- Std.Data.DTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise panics.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DTreeMap.getEntry! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.Analysis.Convex.Segment
/-- Segments in a vector space. Denoted as `[x -[𝕜] y]` within the `Convex` namespace.  -/
segment : (𝕜 : Type u_1) → {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → E → E → Set E
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
dimension `> n`, one may extend the family by another vector while retaining linear independence.  -/
exists_linearIndependent_cons_of_lt_finrank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {n : ℕ} {v : Fin n → M},
  LinearIndependent R v → n < Module.finrank R M → ∃ x, LinearIndependent R (Fin.cons x v)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.le_comap_map : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {I : Ideal R} [inst_3 : RingHomClass F R S], I ≤ Ideal.comap f (Ideal.map f I)
-- Mathlib.GroupTheory.Index
AddSubgroup.inf_relIndex_left : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), (H ⊓ K).relIndex H = K.relIndex H
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {f : (a : α) → β a → γ a},
  (Std.DTreeMap.Internal.Impl.map f t).toListModel = List.map (fun x => ⟨x.fst, f x.fst x.snd⟩) t.toListModel
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_toArray_rco : ∀ {m n : ℤ}, (m<...=n).toArray = ((m + 1)...n + 1).toArray
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Category.{v, max u v} (CategoryTheory.Dial C)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_C_of_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {n : σ →₀ ℕ},
  n ≠ 0 → ∀ (a : R), (MvPowerSeries.coeff n) (MvPowerSeries.C a) = 0
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- **Alias** of `MvPolynomial.totalDegree_finsetSum`. -/
MvPolynomial.totalDegree_finset_sum : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R),
  (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding a multiple of the second vector passed to `oangle` to the first vector does not change
the sign of the angle.  -/
Orientation.oangle_sign_add_smul_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle (x + r • y) y).sign = (o.oangle x y).sign
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- Given `φ : a ≅ b` and `f : R ≅ S`, such that `φ.hom` lifts `f.hom`, then `φ.inv` lifts
`f.inv`.  -/
CategoryTheory.IsHomLift.inv_lift_inv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ≅ S) (φ : a ≅ b) [p.IsHomLift f.hom φ.hom],
  p.IsHomLift f.inv φ.inv
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
cmp_mul_right' : ∀ {α : Type u_3} [inst : Mul α] [inst_1 : LinearOrder α] [MulRightStrictMono α] (a b c : α),
  cmp (a * c) (b * c) = cmp a b
-- Lean.Linter.MissingDocs
_private.Lean.Linter.MissingDocs.0.Lean.Linter.MissingDocs.lintDocStatus : Bool → Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationProps.mk.sizeOf_spec : ∀ (expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx), sizeOf { expr := expr } = 1 + sizeOf expr
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a finitely supported function.  -/
Finsupp.logHeight : {K : Type u_1} → [inst : Field K] → [Height.AdmissibleAbsValues K] → {α : Type u_4} → (α →₀ K) → ℝ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.Nil.nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.Nil
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_union_le_add_edist`.

---

The extended diameter of a union is controlled by the diameter of the sets,
and the edistance between two points in the sets.  -/
EMetric.diam_union : ∀ {X : Type u_2} {s t : Set X} {x y : X} [inst : PseudoEMetricSpace X],
  x ∈ s → y ∈ t → Metric.ediam (s ∪ t) ≤ Metric.ediam s + edist x y + Metric.ediam t
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {inst : CommSemiring R} {inst_1 : Semiring A}
  {inst_2 : TopologicalSpace A} {inst_3 : Semiring B} {inst_4 : TopologicalSpace B} {inst_5 : Algebra R A}
  {inst_6 : Algebra R B} {toAlgEquiv : A ≃ₐ[R] B}
  {continuous_toFun : autoParam (Continuous toAlgEquiv.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toAlgEquiv.invFun) Homeomorph.continuous_invFun._autoParam}
  {toAlgEquiv_1 : A ≃ₐ[R] B}
  {continuous_toFun_1 : autoParam (Continuous toAlgEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toAlgEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam},
  { toAlgEquiv := toAlgEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAlgEquiv := toAlgEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 } →
    toAlgEquiv = toAlgEquiv_1
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- The q term inside the product defining the eta function. It is defined as
`eta_q n z = e ^ (2 π i (n + 1) z)`.  -/
ModularForm.eta_q : ℕ → ℂ → ℂ
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.rel_graphFunctor_map : ∀ {X Y : Type u} (f : X ⟶ Y),
  (CategoryTheory.RelCat.graphFunctor.map f).rel = Function.graph ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_zero_eq_zero : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) (n : A),
  (CategoryTheory.shiftFunctor C n).map 0 = 0
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.mk : ∀ {α : Type u_4} [t : TopologicalSpace α] [inst : Preorder α], t = Topology.lowerSet α → Topology.IsLowerSet α
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_readThe_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ : Type u}
  {post : ρ → ρ → Pred} {epost : EPred},
  Std.Internal.Do.wp (readThe ρ) post epost = Std.Internal.Do.wp MonadReaderOf.read post epost
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Push forward the multiplication of `R` on `M` along a compatible surjective map `f : R → S`.

See also `Function.Surjective.distribMulActionLeft`.
 -/
Function.Surjective.smulZeroClassLeft : {R : Type u_12} →
  {S : Type u_13} →
    {M : Type u_14} →
      [inst : Zero M] →
        [inst_1 : SMulZeroClass R M] →
          [inst_2 : SMul S M] →
            (f : R → S) → Function.Surjective f → (∀ (c : R) (x : M), f c • x = c • x) → SMulZeroClass S M
-- Mathlib.Topology.UniformSpace.Defs
isRefl_of_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α}, s ∈ uniformity α → s.IsRefl
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- There exists a `HahnEmbedding.Partial` whose domain is the whole module.  -/
HahnEmbedding.Partial.exists_domain_eq_top : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) [IsOrderedAddMonoid R]
  [Archimedean R], ∃ f, (↑f).domain = ⊤
-- Mathlib.Order.Completion
DedekindCut.le_principal_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {c : DedekindCut α}, c ≤ DedekindCut.principal a ↔ a ∈ c.right
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.triangle_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (CochainComplex.mappingCocone.triangle φ).mor₂ = φ
-- Lean.Meta.Diagnostics
Lean.Meta.instInhabitedDiagSummary.default : Lean.Meta.DiagSummary
-- Mathlib.Data.Finset.Max
Finset.max_mem_insert_bot_image_coe : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.max ∈ insert ⊥ (Finset.image WithBot.some s)
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.add_mul_mul_invOf_mul_eq_one : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
  [inst_5 : Invertible A] [inst_6 : Invertible C] [inst_7 : Invertible (⅟C + V * ⅟A * U)],
  (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) = 1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree_eq_zero_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  G.minDegree = 0 ↔ ∃ v, G.IsIsolated v
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- A `2`-pretransitive action is pretransitive.  -/
MulAction.isPretransitive_of_is_two_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α]
  [h2 : MulAction.IsMultiplyPretransitive G α 2], MulAction.IsPretransitive G α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A cofork `t` on the parallelPair `f g : X ⟶ Y` consists of two morphisms
`t.ι.app zero : X ⟶ t.pt` and `t.ι.app one : Y ⟶ t.pt`. Of these, only the second one is
interesting, and we give it the shorter name `Cofork.π t`.  -/
CategoryTheory.Limits.Cofork.π : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] → {f g : X ⟶ Y} → (t : CategoryTheory.Limits.Cofork f g) → Y ⟶ t.pt
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_7 : {α : Type u} → Std.Rio.Sliceable (Subarray α) ℕ (Subarray α)
-- Init.Grind.Ordered.Int
Lean.Grind.instLawfulOrderLTInt : Std.LawfulOrderLT ℤ