mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Cover
/-- In a dense order, nothing covers anything.  -/
not_covBy : ∀ {α : Type u_1} [inst : LT α] {a b : α} [DenselyOrdered α], ¬a ⋖ b
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- Constructor for objects in the étale site of a scheme `X`: it takes
an étale morphism `f : Y ⟶ X` as an input.  -/
AlgebraicGeometry.Scheme.Etale.mk : {X Y : AlgebraicGeometry.Scheme} → (f : Y ⟶ X) → [AlgebraicGeometry.Etale f] → X.Etale
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_eq_pi_single : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i : ι} {b : β i},
  (⇑fun₀ | i => b) = Pi.single i b
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F)
  {x : (i : ι) → Em i} {s : Set ((i : ι) → Em i)}, AnalyticWithinAt 𝕜 (⇑f) s x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_neg : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P →
    WeierstrassCurve.Projective.Point.toAffine W (W.neg P) = -WeierstrassCurve.Projective.Point.toAffine W P
-- Lean.Parser.Term.Basic
Lean.Parser.Term.instBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- The Cartesian product of two nonarchimedean groups is nonarchimedean.  -/
NonarchimedeanGroup.Prod.instNonarchimedeanGroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3}
  [inst_3 : Group K] [inst_4 : TopologicalSpace K] [NonarchimedeanGroup K], NonarchimedeanGroup (G × K)
-- Mathlib.Algebra.Group.Conj
ConjClasses.map_surjective : ∀ {α : Type u} {β : Type v} [inst : Monoid α] [inst_1 : Monoid β] {f : α →* β},
  Function.Surjective ⇑f → Function.Surjective (ConjClasses.map f)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMap.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)],
  PiTensorProduct.piTensorHomMap =
    ↑PiTensorProduct.lift ∘ₗ PiTensorProduct.lift (MultilinearMap.piLinearMap (PiTensorProduct.tprod R))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If `F` preserves the pullback of `f, g`, it also preserves the pullback of `g, f`.  -/
CategoryTheory.Limits.preservesPullback_symmetry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) G
-- Mathlib.Data.List.Nodup
List.nodup_iff_count_eq_one : ∀ {α : Type u} {l : List α} [inst : BEq α] [LawfulBEq α], l.Nodup ↔ ∀ a ∈ l, List.count a l = 1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.ext_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f g : X ⟶ Y},
  AlgebraicGeometry.Scheme.Hom.appTop f = AlgebraicGeometry.Scheme.Hom.appTop g → f = g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α} {h' : a ∈ t}, t.get a h' = t.get! a
-- Batteries.Data.UInt
UInt8.min_def : ∀ (x y : UInt8), x ⊓ y = if x ≤ y then x else y
-- Lean.Setup
Lean.instToJsonImportArtifacts : Lean.ToJson Lean.ImportArtifacts
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_append : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l₁ l₂ : List ((a : α) × β a)}, m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.induction_on : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M] {motive : AddMonoidAlgebra R M → Prop}
  (x : AddMonoidAlgebra R M),
  (∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))) →
    (∀ (x y : AddMonoidAlgebra R M), motive x → motive y → motive (x + y)) →
      (∀ (r : R) (x : AddMonoidAlgebra R M), motive x → motive (r • x)) → motive x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_zero : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α}, MeasureTheory.IntegrableAtFilter 0 l μ
-- Init.Data.List.Lemmas
List.getLast_filter_of_pos : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.getLast w) = true),
  (List.filter p l).getLast ⋯ = l.getLast w
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonSlice : Lean.ToJson String.Slice
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instCoeWFWFUnitInner : {α : Type u} → {cmp : α → α → Ordering} → {t : Std.TreeSet.Raw α cmp} → Coe t.WF t.inner.WF
-- Mathlib.Order.Hom.Bounded
BotHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] (f : BotHom α β), f.comp (BotHom.id α) = f
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.List.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_inv : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), |a⁻¹|ₘ = |a|ₘ
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instQuasiIsoIntπTruncGEOfIsGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsGE n], QuasiIso (K.πTruncGE n)
-- Mathlib.Algebra.Order.Group.Multiset
/-- `Multiset.card` bundled as a group hom.  -/
Multiset.cardHom : {α : Type u_1} → Multiset α →+ ℕ
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_univ_eq_finrank : ∀ (E : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  dimH Set.univ = ↑(Module.finrank ℝ E)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- A non-trivial `cons` walk is representable as a `concat` walk.  -/
SimpleGraph.Walk.exists_cons_eq_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  ∃ x q, ∃ (h' : G.Adj x w), SimpleGraph.Walk.cons h p = q.concat h'
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.instIsNormalEpiCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.IsNormalEpiCategory (CategoryTheory.ShortComplex C)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instDecidableEqQuotientOfDecidableCoeForallProp.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) [inst_1 : (a b : M) → Decidable (c a b)],
  c.instDecidableEqQuotientOfDecidableCoeForallProp = AddCon.instDecidableEqQuotientOfDecidableCoeForallProp._aux_1 c
-- Mathlib.NumberTheory.Padics.Complex
/-- `ℂ_[p]` is algebraically closed.  -/
PadicComplex.isAlgClosed : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsAlgClosed ℂ_[p]
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry!_eq_getEntry!ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Inhabited ((a : α) × β a)] (k : α)
  (l : Std.DTreeMap.Internal.Impl α β), l.getEntry! k = l.getEntry!ₘ k
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instTop : {α : Type u_1} → [inst : TopologicalSpace α] → [CompactSpace α] → Top (TopologicalSpace.CompactOpens α)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.truncLT_mem_range_extendFun : ∀ {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} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain)
  (y : ↥(f.extendFun hx).domain) (c : FiniteArchimedeanClass M),
  toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) y))) ∈ (f.extendFun hx).toFun.range
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instOne : {X : AlgebraicGeometry.Scheme} → One X.IdealSheafData
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.toSubgraph.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} (H H_1 : SimpleGraph V) (e_H : H = H_1) (h : H ≤ G),
  SimpleGraph.toSubgraph H h = SimpleGraph.toSubgraph H_1 ⋯
-- Mathlib.ModelTheory.Basic
/-- Composition of first-order homomorphisms is associative.  -/
FirstOrder.Language.Hom.comp_assoc : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Hom M N) (g : L.Hom N P) (h : L.Hom P Q),
  (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Logic.ExistsUnique
ExistsUnique.elim₂ : ∀ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} {b : Prop},
  (∃! x, ∃! h, q x h) → (∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) → b
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse],
  (CategoryTheory.Equivalence.sheafCongr J K e A).counitIso = CategoryTheory.Equivalence.sheafCongr.counitIso J K e A
-- Mathlib.Util.Qq
/-- If `e` has type `Type u` for some level `u`, return `u` and `e : Q(Type u)`.  -/
Qq.getLevelQ' : Lean.Expr → Lean.MetaM ((u : Lean.Level) × Q(Type u))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coeSubgraph_restrict_eq : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (H' : G.Subgraph),
  SimpleGraph.Subgraph.coeSubgraph (SimpleGraph.Subgraph.restrict H') = H ⊓ H'
-- Mathlib.Order.SuccPred.Tree
instCoeOutSubRootedTreeRootedTree : (t : RootedTree) → CoeOut (SubRootedTree t) RootedTree
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_id : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.id f) =
    CategoryTheory.CategoryStruct.id f
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition with a linear isometry on the right preserves the norm of the iterated derivative
within a set.  -/
LinearIsometryEquiv.norm_iteratedFDeriv_comp_right : ∀ {𝕜 : 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 : G ≃ₗᵢ[𝕜] E) (f : E → F) (x : G) (i : ℕ),
  ‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖
-- Mathlib.Data.List.Permutation
List.Perm.permutations : ∀ {α : Type u_1} {s t : List α}, s.Perm t → s.permutations.Perm t.permutations
-- Mathlib.Analysis.Analytic.Binomial
Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero : ∀ {r : ℝ},
  r ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (r - x) ^ 2)
      (FormalMultilinearSeries.ofScalars ℝ fun n => (r ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖r‖ₑ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq.eq_1 : ∀ (a : Bool) (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.instBEqPolyCnstr.beq { eq := a, lhs := a_1, rhs := a_2 } { eq := b, lhs := b_1, rhs := b_2 } =
    (a == b && (a_1 == b_1 && a_2 == b_2))
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_sUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} (S : Set (Set α)),
  (∀ s ∈ S, IsOpen s) → (∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) → TendstoLocallyUniformlyOn F f p (⋃₀ S)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.of_op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.op.ContainsIdentities], W.ContainsIdentities
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.comp_def : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ),
  f.comp g = ((Representation.IntertwiningMap.llcomp ρ σ τ) f) g
-- Init.Data.SInt.Lemmas
Int16.toInt64_neg_of_ne : ∀ {x : Int16}, x ≠ -32768 → (-x).toInt64 = -x.toInt64
-- Init.Syntax
/-- Updates the `i`'th argument of the syntax.
Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
 -/
Lean.Syntax.setArg : Lean.Syntax → ℕ → Lean.Syntax → Lean.Syntax
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Ordering.then.match_1.splitter : (motive : Ordering → Sort u_1) →
  (a : Ordering) → (Unit → motive Ordering.eq) → ((a : Ordering) → (a = Ordering.eq → False) → motive a) → motive a
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.mk.sizeOf_spec : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : SizeOf k] [inst_5 : SizeOf V] [inst_6 : SizeOf P]
  (points : Fin (n + 1) → P) (independent : AffineIndependent k points),
  sizeOf { points := points, independent := independent } = 1
-- Mathlib.GroupTheory.FiniteAbelian.Basic
Submodule.fg_toAddSubgroup : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [Module.Finite ℤ R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  {A : Submodule R M}, A.FG → A.toAddSubgroup.FG
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldl.match_1.splitter : {σ : Sort u_3} →
  {α : Type u_1} →
    (motive : σ → RBTree.RBNode α → Sort u_2) →
      (x : σ) →
        (x_1 : RBTree.RBNode α) →
          ((b : σ) → motive b RBTree.RBNode.nil) →
            ((b : σ) →
                (c : RBTree.RBColor) →
                  (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive b (RBTree.RBNode.node c l v r)) →
              motive x x_1
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_iUnion : ∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_1} (s : ι → Set R),
  PrimeSpectrum.zeroLocus (⋃ i, s i) = ⋂ i, PrimeSpectrum.zeroLocus (s i)
-- Mathlib.Data.List.Cycle
List.prev_eq_getElem?_idxOf_pred_of_ne_head : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α} (ha : a ∈ l),
  a ≠ l.head ⋯ → some (l.prev a ha) = l[List.idxOf a l - 1]?
-- Mathlib.Analysis.Normed.Operator.Basic
LinearIsometry.norm_toContinuousLinearMap_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗᵢ[σ₁₂] F),
  ‖f.toContinuousLinearMap‖ ≤ 1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_add_add : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Add β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i + f j) (f k + f l) μ
-- Mathlib.FieldTheory.CardinalEmb
/-- Extend the family `X i := E⟮<i⟯ →ₐ[F] Ē` from `ι` to `WithTop ι`.  -/
Field.Emb.Cardinal.factor : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [Algebra.IsAlgebraic F E] → WithTop (Module.rank F E).ord.ToType → Type v
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Range of an `NonUnitalAlgHom` as a non-unital subalgebra.  -/
NonUnitalAlgHom.range : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] → [NonUnitalAlgHomClass F R A B] → F → NonUnitalSubalgebra R B
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.inhabited_FGEquiv_of_IsEmpty_Constants_and_Relations : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → [IsEmpty L.Constants] → [IsEmpty (L.Relations 0)] → Inhabited (L.FGEquiv M N)
-- Lean.Server.Rpc.Basic
/-- Version `0` uses JSON.
Serialized RPC data is stored directly in `RpcCallParams.params` and in `JsonRpc.Response.result`
(as opposed to being wrapped in additional metadata).
General types (except RPC references) are (de)serialized via `ToJson/FromJson`.
RPC references are serialized as `{"p": n}`.  -/
Lean.Lsp.RpcWireFormat.v0 : Lean.Lsp.RpcWireFormat
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Use the axiom of choice to extract explicit `LimitCone F` from `HasLimit F`.  -/
CategoryTheory.Limits.getLimitCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasLimit F] → CategoryTheory.Limits.LimitCone F
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Copy of an additive subgroup with a new `carrier` equal to the old one.
Useful to fix definitional equalities  -/
AddSubgroup.copy : {G : Type u_1} → [inst : AddGroup G] → (K : AddSubgroup G) → (s : Set G) → s = ↑K → AddSubgroup G
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.lit : Lean.IR.LitVal → Lean.IR.Expr
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F)
  (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x
-- Mathlib.Order.Filter.IsBounded
Antitone.isCoboundedUnder_le_of_isCobounded : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Antitone f →
    ∀ [F.NeBot], Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) F → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.add_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousAdd α] {s t : Set β},
  Disjoint s t → HasSum (f ∘ Subtype.val) a → HasSum (f ∘ Subtype.val) b → HasSum (f ∘ Subtype.val) (a + b)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.ennreal_toReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).toReal) μ
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_eq_of_degree_eq_card : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {S : Finset R},
  (∀ x ∈ S, Polynomial.eval x p = 0) → ↑S.card = p.degree → p.roots = S.val
-- Init.Data.Vector.Lemmas
Vector.cast_mk : ∀ {α : Type u_1} {n m : ℕ} {xs : Array α} {h : xs.size = n} {h' : n = m},
  Vector.cast h' (Vector.mk xs h) = Vector.mk xs ⋯
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- The connected component of `v` in `G.induce Kᶜ`.  -/
SimpleGraph.componentComplMk : {V : Type u} → {K : Set V} → (G : SimpleGraph V) → {v : V} → v ∉ K → G.ComponentCompl K
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.simpTheorems : Lean.Meta.Simp.Context → Lean.Meta.SimpTheoremsArray
-- Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
/-- The pushforward of algebraic cycles with respect to a quasicompact morphism of schemes. The
arguments `wx` and `wy` are certain weight functions used to calculate how the weights of the
algebraic cycle should be adjusted to make the pushforward operation functorial. Typically in
applications these will be some notions of dimension or codimension. The most common notion of
dimension is `Order.height`, and the most common notion of codimension is `Order.coheight`, though
more sophisticated notions exist in the literature which are useful when sufficient
equidimensionality hypotheses cannot be assumed.
 -/
AlgebraicGeometry.AlgebraicCycle.map : {X Y : AlgebraicGeometry.Scheme} →
  {R : Type u_1} →
    (f : X ⟶ Y) →
      [inst : Semiring R] →
        [AlgebraicGeometry.QuasiCompact f] →
          {N : Type u_2} →
            [DecidableEq N] →
              (↥X → N) → (↥Y → N) → AlgebraicGeometry.AlgebraicCycle X R → AlgebraicGeometry.AlgebraicCycle Y R
-- Mathlib.Algebra.BigOperators.Group.List.Basic
AddCommute.list_sum_left : ∀ {M : Type u_4} [inst : AddMonoid M] (l : List M) (y : M), (∀ x ∈ l, AddCommute x y) → AddCommute l.sum y
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `isPGroup_iff_card_dvd_pow`. -/
IsPGroup.exists_card_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G], IsPGroup p G → ∃ n, Nat.card G ∣ p ^ n
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- In a compactly coherent space `X`, a set `s` is open iff `f ⁻¹' s` is open for every continuous
map from a compact space.  -/
CompactlyCoherentSpace.isOpen_iff_forall_compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyCoherentSpace X] (s : Set X),
  IsOpen s ↔ ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- If an element `a` divides another element `b` in a ring, `a` divides the difference of `b` and
another element `c` iff `a` divides `c`.  -/
dvd_sub_right : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → (a ∣ b - c ↔ a ∣ c)
-- Mathlib.Probability.Distributions.Pareto
/-- The Pareto pdf is nonnegative.  -/
ProbabilityTheory.paretoPDFReal_nonneg : ∀ {t r : ℝ}, 0 ≤ t → 0 ≤ r → ∀ (x : ℝ), 0 ≤ ProbabilityTheory.paretoPDFReal t r x
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabForall : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.isEqSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → α → Sort u_2) (a b : α) (h_1 : (a b : α) → motive (some a) b)
  (h_2 : (x : α) → motive none x),
  (match some a, b with
    | some a, b => h_1 a b
    | none, x => h_2 x) =
    h_1 a b