mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.isoSpec.inv (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) = h
-- Mathlib.Data.FunLike.Group
FunLike.coeAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.ofDual.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ}
  (x : GaloisInsertion u l), x.ofDual = { choice := x.choice, gc := ⋯, u_l_le := ⋯, choice_eq := ⋯ }
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- If `S` is `R`-flat, `tensorProd R S` preserves the equalizer of `f` and `g`.  -/
CommRingCat.Under.tensorProdMapEqualizerForkIsLimit : {R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    [Module.Flat ↑R ↑S] →
      {A B : CategoryTheory.Under R} →
        (f g : A ⟶ B) → CategoryTheory.Limits.IsLimit ((R.tensorProd S).mapCone (CommRingCat.Under.equalizerFork f g))
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocInfo.mk : Lean.Elab.ElabInfo → Lean.Elab.DocInfo
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.aestronglyMeasurable_exp_mul_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ},
  MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X ω)) μ →
    MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * Y ω)) μ →
      MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * (X + Y) ω)) μ
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashMap.emptyWithCapacity c).isEmpty = true
-- Mathlib.NumberTheory.Divisors
Int.divisors.eq_1 : ∀ (z : ℤ),
  z.divisors =
    (Finset.map Nat.castEmbedding z.natAbs.divisors).disjUnion
      (Finset.map (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))) z.natAbs.divisors) ⋯
-- Mathlib.Data.List.Rotate
List.singleton_eq_rotate_iff : ∀ {α : Type u} {l : List α} {n : ℕ} {x : α}, [x] = l.rotate n ↔ [x] = l
-- Mathlib.Algebra.Algebra.Tower
/-- Given a commutative ring `R`, an `R`-algebra `S` and an `R`-module `M` with a scalar tower
`IsScalarTower R S M`, if the algebra map from `R` to `S` is surjective, then this induces an order
isomorphism `Submodule S M ≃o Submodule R M`.
 -/
Submodule.orderIsoOfAlgebraMapSurjective : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : Ring S] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Algebra R S] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [IsScalarTower R S M] → Function.Surjective ⇑(algebraMap R S) → Submodule S M ≃o Submodule R M
-- Std.Http.Data.Version
/-- `HTTP/3.0`
 -/
Std.Http.Version.v30 : Std.Http.Version
-- Mathlib.Tactic.WithoutCDot
/-- A set of parentheses, supporting type ascriptions, which does not process `·`.

Primarily, this is useful when quoting user-provided syntax inside parentheses, as it prevents `·`s
from the caller being interpreted in the context of `()`s from the macro.  -/
Lean.Elab.Term.elabWithoutCDot : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
Profinite.NobelingProof.GoodProducts.linearIndependentAux : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (μ : Ordinal.{u}), Profinite.NobelingProof.P I μ
-- Init.Internal.Order.Basic
Lean.Order.monotone_stateRefT'Run : ∀ {γ : Sort u_1} {m : Type → Type} {ω σ α : Type} [inst : Lean.Order.PartialOrder γ] [inst_1 : Monad m]
  [inst_2 : MonadLiftT (ST ω) m] [inst_3 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  (f : γ → StateRefT' ω σ m α), Lean.Order.monotone f → ∀ (s : σ), Lean.Order.monotone fun x => (f x).run s
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.eq_rightInverse : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g₁ g₂ : β → α},
  Function.LeftInverse g₁ f → Function.RightInverse g₂ f → g₁ = g₂
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The natural isomorphism `shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k`
when `c.prev j = i` and `c.next j = k`.  -/
HomologicalComplex.natIsoSc' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          (i j k : ι) →
            c.prev j = i →
              c.next j = k →
                (HomologicalComplex.shortComplexFunctor C c j ≅ HomologicalComplex.shortComplexFunctor' C c i j k)
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.instIsCyclicAlgEquivOfFinite : ∀ (K : Type u_4) (L : Type u_5) [Finite L] [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], IsCyclic Gal(L/K)
-- Lean.Widget.InteractiveCode
Lean.Widget.instToJsonDiffTag : Lean.ToJson Lean.Widget.DiffTag
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_interval_add_interval_comm : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c d : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable f μ c d →
      IntervalIntegrable f μ a c →
        ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..d, f x ∂μ + ∫ (x : ℝ) in c..b, f x ∂μ
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- An archimedean decidable linearly ordered `CommGroup` has a version of the floor: for
`a > 1`, any `g` in the group lies between some two consecutive powers of `a`.  -/
existsUnique_zpow_near_of_one_lt : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
  1 < a → ∀ (g : G), ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
-- Mathlib.Data.Finset.Density
Finset.dens_disjUnion : ∀ {α : Type u_2} [inst : Fintype α] (s t : Finset α) (h : Disjoint s t), (s.disjUnion t h).dens = s.dens + t.dens
-- Mathlib.Algebra.Quaternion
Quaternion.im_zero : ∀ {R : Type u_3} [inst : CommRing R], Quaternion.im 0 = 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso : Inhabited Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.FieldTheory.KrullTopology
/-- Given a field extension `L/K`, `fixedByFinite K L` is the set of
subsets `Gal(L/E)` of `Gal(L/K)`, where `E/K` is finite.  -/
fixedByFinite : (K : Type u_1) →
  (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → Set (Subgroup Gal(L/K))
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_bot_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⊥.IsComplement' H ↔ H = ⊤
-- Mathlib.Order.Hom.Lattice
/-- Copy of a `LatticeHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
LatticeHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] → [inst_1 : Lattice β] → (f : LatticeHom α β) → (f' : α → β) → f' = ⇑f → LatticeHom α β
-- Init.Data.Order.Ord
Std.OrientedCmp.gt_of_not_isGE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, ¬(cmp a b).isGE = true → cmp b a = Ordering.gt
-- Mathlib.Data.Sign.Defs
sign_pos : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] {a : α}, 0 < a → SignType.sign a = 1
-- Init.Data.UInt.Bitwise
USize.neg_one_or : ∀ {a : USize}, -1 ||| a = -1
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_le_one_of_eraseLead_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead = 0 → f.support.card ≤ 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` tends to `f x₀` uniformly (along `𝓝 x₀`) on the spectrum of `a`,
and each `f x` is continuous on the spectrum of `a`, then `fun x ↦ cfc (f x) a` is
continuous at `x₀`.  -/
continuousAt_cfc_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : 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]
  [inst_9 : ContinuousFunctionalCalculus R A p] [inst_10 : TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X},
  TendstoUniformlyOn f (f x₀) (nhds x₀) (spectrum R a) →
    (∀ᶠ (x : X) in nhds x₀, ContinuousOn (f x) (spectrum R a)) → ContinuousAt (fun x => cfc (f x) a) x₀
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.isFractionRing_iff_of_base_ringEquiv : ∀ {R : Type u_1} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommRing P] (h : R ≃+* P), IsFractionRing R S ↔ IsFractionRing P S
-- Mathlib.CategoryTheory.Limits.ColimitLimit
CategoryTheory.Limits.map_id_left_eq_curry_map : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) {j : J} {k k' : K}
  {f : k ⟶ k'},
  F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id j) f) =
    ((CategoryTheory.Functor.curry.obj F).obj j).map f
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal : {𝕜 : Type u_2} → [inst : RCLike 𝕜] → {ι : Type u_5} → Inhabited (HilbertBasis ι 𝕜 ↥(lp (fun x => 𝕜) 2))
-- Aesop.Util.UnionFind
Aesop.UnionFind.ofArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Aesop.UnionFind α
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The type of bundled `n`-times continuously differentiable maps which vanish outside of a fixed
compact set `K`.  -/
ContDiffMapSupportedIn : (E : Type u_2) →
  (F : Type u_3) →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [NormedSpace ℝ F] → ℕ∞ → TopologicalSpace.Compacts E → Type (max u_2 u_3)
-- Lean.Data.Options
Lean.Option.Decl.deprecation? : {α : Type} → Lean.Option.Decl α → Option Lean.OptionDeprecation
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_sum_monomial_coeff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  ∑ v ∈ p.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v p) = p
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_le : ∀ {w : ℕ} (x : BitVec w), x.cpop.toNat ≤ w
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α} {a : α},
  a ∈ s / t ↔ ∃ b ∈ s, ∃ c ∈ t, b / c = a
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.freeReflMap_map : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {W : Type u_2} [inst_1 : CategoryTheory.ReflQuiver W]
  (F : V ⥤rq W) {v w : V} (f : v ⟶ w),
  (CategoryTheory.Cat.freeReflMap F).map (CategoryTheory.Cat.FreeRefl.homMk f) =
    CategoryTheory.Cat.FreeRefl.homMk (F.map f)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCoeAddGrpCat.eq_1 : AddCommGrpCat.instCoeAddGrpCat = { coe := (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).obj }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ Std.DHashMap.Const.insertManyIfNewUnit m l},
  (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey k h = m.getKey k mem
-- Mathlib.Logic.Relation
swap_eq_iff : ∀ {α : Type u_1} {r : α → α → Prop}, Function.swap r = r ↔ Std.Symm r
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_4 : ∀ {α : Type u_1} (P Q : RegularExpression α), (P.plus Q).matchEpsilon = (P.matchEpsilon || Q.matchEpsilon)
-- Mathlib.Data.Num.Basic
/-- Divides a `Num` by `2`  -/
Num.div2 : Num → Num
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_mul_self : ∀ (n : ℤ), (n * n).negOnePow = n.negOnePow
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → γ} {k : α},
  (Std.TreeMap.map f t)[k]! = (Option.map (f k) t[k]?).get!
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instInhabited.eq_1 : ∀ {α : Type u} [inst : AddGroup α], AddGroupTopology.instInhabited = { default := ⊤ }
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instIsArtinianSubtypeMem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [IsArtinian R M] (N : LieSubmodule R L M), IsArtinian R ↥N
-- Init.Grind.Ring.Field
Lean.Grind.Field.eq_inv_of_mul_eq_one : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : α}, a * b = 1 → a = b⁻¹
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseMonthLong : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Month.Ordinal
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂Iso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g), (F.map₂Iso η).inv = F.map₂ η.inv
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.natCast_atTop : ∀ {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {R : Type u_17} [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : R → E} {g : R → F},
  f =o[Filter.atTop] g → (fun n => f ↑n) =o[Filter.atTop] fun n => g ↑n
-- Mathlib.Data.Finset.Erase
Finset.erase_right_comm : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Finset α}, (s.erase a).erase b = (s.erase b).erase a
-- Mathlib.Combinatorics.Graph.Delete
Graph.vertexSet_induce : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α), (G.induce X).vertexSet = X
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.not_cliqueFree : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [Nonempty α],
  G.FarFromTriangleFree ε → 0 < ε → ¬G.CliqueFree 3
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
LinearMap.coe_toAffineMap : ∀ {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module k V₂] (f : V₁ →ₗ[k] V₂), ⇑f.toAffineMap = ⇑f
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.subtypeVal_submodule_sConvexComb : ∀ {F : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : SetLike F M]
  [inst_6 : AddSubmonoidClass F M] [inst_7 : SMulMemClass F R M] [inst_8 : Convexity.ConvexSpace R M]
  [inst_9 : Convexity.IsModuleConvexSpace R M] (S : F) (w : Convexity.StdSimplex R ↥S),
  ↑(Convexity.sConvexComb w) = Convexity.iConvexComb w Subtype.val
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank.eq_def : ∀ (x : PSet.{u}),
  x.rank =
    match x with
    | PSet.mk α A => ⨆ a, Order.succ (A a).rank
-- Aesop.Forward.Substitution
Aesop.Substitution.mk.injEq : ∀ (premises : Array (Option Lean.Expr)) (levels : Array (Option Lean.Level)) (premises_1 : Array (Option Lean.Expr))
  (levels_1 : Array (Option Lean.Level)),
  ({ premises := premises, levels := levels } = { premises := premises_1, levels := levels_1 }) =
    (premises = premises_1 ∧ levels = levels_1)
-- Mathlib.Data.Int.NatPrime
Int.not_prime_of_int_mul : ∀ {a b : ℤ} {c : ℕ}, a.natAbs ≠ 1 → b.natAbs ≠ 1 → a * b = ↑c → ¬Nat.Prime c
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.min_le_mk_of_le_of_le : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {x y z : M},
  y ≤ x → x ≤ z → min (MulArchimedeanClass.mk y) (MulArchimedeanClass.mk z) ≤ MulArchimedeanClass.mk x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Compose a pre-`0`-hypercover with a morphism on the right.  -/
CategoryTheory.PreZeroHypercover.pushforward : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (X ⟶ Y) → CategoryTheory.PreZeroHypercover X → CategoryTheory.PreZeroHypercover Y
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- A finite set which represents a finite collection of cells on the `ℕ × ℕ` grid.  -/
YoungDiagram.cells : YoungDiagram → Finset (ℕ × ℕ)
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_eq_norm_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {x : E} (y : E), ‖x‖ = 0 → ‖x - y‖ = ‖y‖
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.comp_apply : ∀ {X : TopCat} {x : ↑X} {U V W : TopologicalSpace.OpenNhds x} (f : U ⟶ V) (g : V ⟶ W) (x_1 : ↥↑U),
  (CategoryTheory.CategoryStruct.comp f g) x_1 = g (f x_1)
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_isClosed_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed
-- Mathlib.CategoryTheory.Sites.Point.Over
CategoryTheory.GrothendieckTopology.Point.over_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (Φ : J.Point) {X : C} (x : Φ.fiber.obj X),
  (Φ.over x).fiber = CategoryTheory.FunctorToTypes.fromOverFunctor Φ.fiber x
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.id_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.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.src
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.mk_subset_mk_lt_cof : ∀ {α : Type u_1},
  (Cardinal.mk α).IsStrongPrelimit → Cardinal.mk { s // Cardinal.mk ↑s < (Cardinal.mk α).ord.cof } = Cardinal.mk α
-- Init.GetElem
instLawfulGetElem : ∀ {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [inst : GetElem coll idx elem valid]
  [inst_1 : (xs : coll) → (i : idx) → Decidable (valid xs i)], LawfulGetElem coll idx elem valid
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
StrictMono.pow_const : ∀ {β : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : Preorder β] [MulLeftStrictMono M]
  [MulRightStrictMono M] {f : β → M}, StrictMono f → ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x => f x ^ n
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.isOrderedCancelAddMonoid : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsOrderedCancelAddMonoid N], IsOrderedCancelAddMonoid (Lex (α →₀ N))
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.flip : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  ν ≤ n → (bernsteinPolynomial R n ν).comp (1 - Polynomial.X) = bernsteinPolynomial R n (n - ν)
-- Init.Data.SInt.Lemmas
Int16.le_minValue_iff : ∀ {a : Int16}, a ≤ Int16.minValue ↔ a = Int16.minValue
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul_of_le_of_lt`.  -/
Right.one_lt_mul_of_le_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b : α}, 1 ≤ a → 1 < b → 1 < a * b
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.sup_apply : ∀ {E : Type u_3} [inst : AddGroup E] (p q : NonarchAddGroupSeminorm E) (x : E), (p ⊔ q) x = max (p x) (q x)
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_eq_zero : ∀ {x : NNReal}, NNReal.sqrt x = 0 ↔ x = 0
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.mk.inj : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {toSlashInvariantForm : SlashInvariantForm Γ k}
  {holo' : MDiff ⇑toSlashInvariantForm}
  {zero_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm.toFun k}
  {toSlashInvariantForm_1 : SlashInvariantForm Γ k} {holo'_1 : MDiff ⇑toSlashInvariantForm_1}
  {zero_at_cusps'_1 : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm_1.toFun k},
  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := zero_at_cusps' } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := zero_at_cusps'_1 } →
    toSlashInvariantForm = toSlashInvariantForm_1
-- Lean.DocString.Parser
/-- Parses an image.  -/
Lean.Doc.Parser.image : Lean.Parser.ParserFn
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.homEquiv_apply_coe : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} (f : Monoid.PushoutI φ →* K),
  ↑(Monoid.PushoutI.homEquiv f) = (fun i => f.comp (Monoid.PushoutI.of i), f.comp (Monoid.PushoutI.base φ))
-- Init.Prelude
Lean.instInhabitedMacroScopesView : Inhabited Lean.MacroScopesView
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instNatCast : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → NatCast (FractionalIdeal S P)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow : ℤ →
  Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr →
    ℕ → Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Order.Nucleus
Nucleus.himp_apply : ∀ {X : Type u_1} [inst : Order.Frame X] (m n : Nucleus X) (x : X), (m ⇨ n) x = ⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_ne_one : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [Nontrivial R] (x : X), FreeAlgebra.ι R x ≠ 1
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- If `φ : a ⟶ b` lifts `f` and `ψ : b ⟶ c` lifts `𝟙 T`, then `φ ≫ ψ` lifts `f`  -/
CategoryTheory.IsHomLift.comp_lift_id_right' : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b c : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] (T : 𝒮) (ψ : b ⟶ c)
  [p.IsHomLift (CategoryTheory.CategoryStruct.id T) ψ], p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instZero : {𝕜 : Type u_2} → {α : Type u_5} → [inst : Zero 𝕜] → [inst_1 : LE α] → Zero (IncidenceAlgebra 𝕜 α)
-- Mathlib.Order.Heyting.Hom
BiheytingHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (f : BiheytingHom α β),
  f.comp (BiheytingHom.id α) = f
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β),
  (MeasureTheory.Measure.map (⇑f) μ).Regular ↔ μ.Regular
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- This lemma uses `∑ i in` instead of `∑ i :`.  -/
InnerProductSpace.gramSchmidt_def : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (n : ι),
  InnerProductSpace.gramSchmidt 𝕜 f n = f n - ∑ i < n, (𝕜 ∙ InnerProductSpace.gramSchmidt 𝕜 f i).starProjection (f n)
-- Mathlib.GroupTheory.OrderOfElement
isOfFinAddOrder_of_finite : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [Finite G] (x : G), IsOfFinAddOrder x