mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.ihom_map : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F : CategoryTheory.Functor D C) {G H : CategoryTheory.Functor D C} (f : G ⟶ H),
  (CategoryTheory.ihom F).map f = F.closedIhom.map f
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mk.sizeOf_spec : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : SizeOf C] [inst_8 : SizeOf ι] (ω₁ : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C)
  (δ' :
    (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_2
            CategoryTheory.Triangulated.SpectralObject._proof_4).comp
        ω₁ ⟶
      (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6
            CategoryTheory.Triangulated.SpectralObject._proof_2).comp
        (ω₁.comp (CategoryTheory.shiftFunctor C 1)))
  (distinguished' :
    ∀ (D : CategoryTheory.ComposableArrows ι 2),
      CategoryTheory.Pretriangulated.Triangle.mk
          (ω₁.map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Triangulated.SpectralObject._proof_6
                  CategoryTheory.Triangulated.SpectralObject._proof_8
                  CategoryTheory.Triangulated.SpectralObject._proof_10
                  CategoryTheory.Triangulated.SpectralObject._proof_2
                  CategoryTheory.Triangulated.SpectralObject._proof_4).app
              D))
          (ω₁.map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Triangulated.SpectralObject._proof_8
                  CategoryTheory.Triangulated.SpectralObject._proof_2
                  CategoryTheory.Triangulated.SpectralObject._proof_6
                  CategoryTheory.Triangulated.SpectralObject._proof_4
                  CategoryTheory.Triangulated.SpectralObject._proof_4).app
              D))
          (δ'.app D) ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles),
  sizeOf { ω₁ := ω₁, δ' := δ', distinguished' := distinguished' } = 1 + sizeOf ω₁ + sizeOf δ'
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearMap_refl : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {ρ : ContRepresentation R G V},
  ↑(ContRepresentation.Equiv.refl ρ).toContinuousLinearEquiv = ContinuousLinearMap.id R V
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A family of continuous linear maps is continuous at a point iff all its applications are.  -/
continuousAt_clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {X : Type u_1} [inst_6 : TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} {x : X},
  ContinuousAt f x ↔ ∀ (y : E), ContinuousAt (fun q => (f q) y) x
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- Constant functions are torus integrable  -/
TorusIntegrable.torusIntegrable_const : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] (a : E) (c : Fin n → ℂ) (R : Fin n → ℝ),
  TorusIntegrable (fun x => a) c R
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_neg : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.ΨSq (-n) = W.ΨSq n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Inhabited ((a : α) × β a)] (t : Std.DTreeMap.Internal.Impl α β)
  (k : α),
  t.getEntry! k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.getEntry!" 147 13
        "Key is not present in map"
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => l.getEntry! k
      | Ordering.gt => r.getEntry! k
      | Ordering.eq => ⟨k', v'⟩
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instLawfulBackwardPatternModelChar : ∀ {c : Char}, String.Slice.Pattern.Model.LawfulBackwardPatternModel c
-- Mathlib.Data.Nat.Prime.Defs
/-- The square of the smallest prime factor of a composite number `n` is at most `n`.
 -/
Nat.minFac_sq_le_self : ∀ {n : ℕ}, 0 < n → ¬Nat.Prime n → n.minFac ^ 2 ≤ n
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {t : Set γ},
  LowerHemicontinuousOn f s → ContinuousOn g t → Set.MapsTo g t s → LowerHemicontinuousOn (f ∘ g) t
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `m` and `n` are finite and lie in the same universe as `R`, the rank of `m × n` matrices
is `# m * # n`.  -/
rank_matrix'' : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (m n : Type u) [Finite m] [Finite n],
  Module.rank R (Matrix m n R) = Cardinal.mk m * Cardinal.mk n
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top map in the left unitality square.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (F.comp (CategoryTheory.MonoidalCategory.tensorUnitLeft D) ⟶
                  (CategoryTheory.MonoidalCategory.curriedTensorPre F).obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Data.Set.Card
Set.ncard_powerset : ∀ {α : Type u_1} (s : Set α), autoParam s.Finite Set.ncard_powerset._auto_1 → (𝒫 s).ncard = 2 ^ s.ncard
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.χ`.

---

returns the characteristic morphism of the subobject `(m : U ⟶ X) [Mono m]`  -/
CategoryTheory.HasClassifier.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasSubobjectClassifier C] →
      {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ CategoryTheory.HasSubobjectClassifier.Ω C
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.below.empty : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop},
  Std.Sat.AIG.RelabelNat.State.Inv2.below ⋯
-- Std.Do.Triple.Basic
/-- Conjunction for two Hoare triple specifications of a program `x`.
This theorem is useful for decomposing proofs, because unrelated facts about `x` can be proven
separately and then combined with this theorem.
 -/
Std.Do.Triple.and : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {P₁ : Std.Do.Assertion ps} {Q₁ : Std.Do.PostCond α ps}
  {P₂ : Std.Do.Assertion ps} {Q₂ : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps] (x : m α),
  ⦃P₁⦄ x ⦃Q₁⦄ → ⦃P₂⦄ x ⦃Q₂⦄ → ⦃P₁ ∧ P₂⦄ x ⦃Q₁.and Q₂⦄
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_ne_mul_pi_div_two : ∀ {x : ℝ} (k : ℤ), Real.arctan x ≠ (2 * ↑k + 1) * Real.pi / 2
-- Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
SeparableClosure.hasEnoughRootsOfUnity : ∀ (F : Type u_1) [inst : Field F] (n : ℕ) [NeZero ↑n], HasEnoughRootsOfUnity (SeparableClosure F) n
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A weight `k` modular form is bounded in norm by a constant multiple of
`max 1 (1 / (τ.im) ^ k)`.  -/
ModularFormClass.exists_bound : ∀ {k : ℤ},
  0 ≤ k →
    ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
      [ModularFormClass F Γ k] (f : F), ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Representation.FiniteCyclicGroup.coinvariantsKer_eq_range : ∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Group G] {V : Type u_4} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) [Finite G],
  (∀ (x : G), x ∈ Subgroup.zpowers g) → Representation.Coinvariants.ker ρ = (ρ g - LinearMap.id).range
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0π_comp_H0Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A)) x) =
    (Representation.Coinvariants.mk A.ρ) x
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_univ : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E], Balanced 𝕜 Set.univ
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.instIsGaussianMapHSub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (c : E),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (fun x => x - c) μ)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Type u_4} {γ : Type u_5}
  [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ]
  [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x) → UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the right respects higher differentiability at a
point.  -/
ContinuousLinearEquiv.contDiffAt_comp_iff : ∀ {𝕜 : 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] {f : E → F} {x : E} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E),
  ContDiffAt 𝕜 n (f ∘ ⇑e) (e.symm x) ↔ ContDiffAt 𝕜 n f x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.mono_Δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {A : C},
  CategoryTheory.Mono (CategoryTheory.Limits.diag A)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J J' : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} (F_1 : J ⟶ J') (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).map F_1).fst.app X_1 = (F_1.app X_1).fst
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_of_lift_eq : ∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β') →
    Cardinal.mk (α ≃ β') = 2 ^ Cardinal.lift.{v, u} (Cardinal.mk α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Data.PNat.Prime
Nat.Primes.coe_pnat_nat : ∀ (p : Nat.Primes), ↑↑p = ↑p
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.pos_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun a => max (f a) 0) μ
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_rio : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_rio._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (cmp e.fst bound).isLT) t.toList
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_iterate_symm_powMulEquiv : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n m : ℕ),
  (Perfection.coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) =
    (Perfection.coeffMonoidHom M p (n + m)) f
-- Mathlib.CategoryTheory.CommSq
/-- Equivalences of `LiftStruct` for a square in the opposite category and
the corresponding square in the original category.  -/
CategoryTheory.CommSq.LiftStruct.unopEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : Cᵒᵖ} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → (sq : CategoryTheory.CommSq f i p g) → sq.LiftStruct ≃ ⋯.LiftStruct
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforwardEq_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f g : X ⟶ Y} (h : f = g)
  (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  (TopCat.Presheaf.pushforwardEq h ℱ).hom.app U = ℱ.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangle_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangle φ).mor₁ = φ
-- Init.Data.List.Lemmas
List.decide_forall_mem : ∀ {α : Type u_1} {l : List α} {p : α → Prop} [inst : DecidablePred p],
  decide (∀ x ∈ l, p x) = l.all fun b => decide (p b)
-- Mathlib.Data.Matrix.Mul
RingHom.map_mulVec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [inst : Fintype n] [inst_1 : NonAssocSemiring R]
  [inst_2 : NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : n → R) (i : m),
  f (M.mulVec v i) = (M.map ⇑f).mulVec (⇑f ∘ v) i
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_im_objs_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (d : D),
  d ∈ (CategoryTheory.Subgroupoid.im φ hφ).objs ↔ ∃ c, φ.obj c = d
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.throwDeltaDeriveFailure : {α : Type} →
  Lean.Name →
    Lean.Name →
      Option Lean.MessageData → optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "") → Lean.MetaM α
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Constructor for morphisms from `(t.truncGE n).obj X`.  -/
CategoryTheory.Triangulated.TStructure.descTruncGE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                {X Y : C} → (X ⟶ Y) → (n : ℤ) → [t.IsGE Y n] → (t.truncGE n).obj X ⟶ Y
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- Presheaf categories on an essentially small domain have a subobject classifier.  -/
CategoryTheory.instHasSubobjectClassifierFunctorOppositeTypeOfEssentiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C],
  CategoryTheory.HasSubobjectClassifier (CategoryTheory.Functor Cᵒᵖ (Type w))
-- Mathlib.Order.InitialSeg
PrincipalSeg.mem_range_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} {b : β} [inst_1 : LT α] (f : α <i β),
  b ≤ f.toRelEmbedding a → b ∈ Set.range ⇑f.toRelEmbedding
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- a polynomial is `Monic` if its leading coefficient is 1  -/
Polynomial.Monic : {R : Type u} → [inst : Semiring R] → Polynomial R → Prop
-- Mathlib.Analysis.Normed.Module.Connected
/-- **Alias** of `Metric.contractibleSpace_eball`. -/
Metric.eball_contractible : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  0 < r → ContractibleSpace ↑(Metric.eball x r)
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, `C ≠ ∞`, `r < 1`,
then `f` is a Cauchy sequence.  -/
cauchySeq_of_edist_le_geometric : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal),
  r < 1 → C ≠ ⊤ → ∀ {f : ℕ → α}, (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) → CauchySeq f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.equiv_iff_toList_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {v : α → M}, ⊤.Realize v ↔ True
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing.injEq : ∀ (h : Lean.Expr) (x : Int.Internal.Linear.Var) (e' : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly)
  (re : Lean.Meta.Grind.Arith.CommRing.RingExpr) (rp : Lean.Grind.CommRing.Poly) (p' : Int.Internal.Linear.Poly)
  (h_1 : Lean.Expr) (x_1 : Int.Internal.Linear.Var) (e'_1 : Int.Internal.Linear.Expr) (p_1 : Int.Internal.Linear.Poly)
  (re_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (rp_1 : Lean.Grind.CommRing.Poly) (p'_1 : Int.Internal.Linear.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h x e' p re rp p' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h_1 x_1 e'_1 p_1 re_1 rp_1 p'_1) =
    (h = h_1 ∧ x = x_1 ∧ e' = e'_1 ∧ p = p_1 ∧ re = re_1 ∧ rp = rp_1 ∧ p' = p'_1)
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An inequality of subobjects is witnessed by some morphism between the corresponding objects.  -/
CategoryTheory.Subobject.ofLE : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B : C} →
      (X Y : CategoryTheory.Subobject B) →
        X ≤ Y → (CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build an `AddEquiv` from an isomorphism in the category `AddSemigroup`.  -/
CategoryTheory.Iso.addSemigrpIsoToAddEquiv : {X Y : AddSemigrp} → (X ≅ Y) → ↑X ≃+ ↑Y
-- Lean.Meta.Basic
/-- Return `true` if `indVal` is an inductive predicate. That is, `inductive` type in `Prop`.
 -/
Lean.Meta.isInductivePredicateVal : Lean.InductiveVal → Lean.MetaM Bool
-- Lean.Parser.Basic
Lean.Parser.isQuotableCharDefault : Char → Bool
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.inhabitedOfEmpty : {α : Type u_1} → {β : Type u_2} → [IsEmpty α] → [IsEmpty β] → Inhabited (PartialEquiv α β)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_nonempty : ∀ {α : Type u_2} [inst : Zero α], Finset.Nonempty 0
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_one : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], ⇑1 = id
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app' : ∀ (R : Type u) [inst : CommRing R],
  AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app (Opposite.op (CommRingCat.of R)) =
    (CommRingCat.ofHom
        (algebraMap R
          ((AlgebraicGeometry.structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))
                  ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj
            (Opposite.op ⊤)))).op
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `get_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.get_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α}
  {h : k ∈ Std.DTreeMap.filterMap f t},
  Std.DTreeMap.Const.get (Std.DTreeMap.filterMap f t) k h = (f k (Std.DTreeMap.Const.get t k ⋯)).get ⋯
-- Mathlib.RingTheory.Congruence.Defs
RingCon.comap_rel : ∀ {R : Type u_2} {R' : Type u_3} {F : Type u_4} [inst : Add R] [inst_1 : Add R'] [inst_2 : FunLike F R R']
  [inst_3 : AddHomClass F R R'] [inst_4 : Mul R] [inst_5 : Mul R'] [inst_6 : MulHomClass F R R'] {J : RingCon R'}
  {f : F} {x y : R}, (J.comap f) x y ↔ J (f x) (f y)
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.smul_mem_iff : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E}
  {x : E} {a b : 𝕜}, Balanced 𝕜 s → ‖a‖ = ‖b‖ → (a • x ∈ s ↔ b • x ∈ s)
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.mk : Lean.LevelSet → Lean.ExprSet → Array Lean.LMVarId → Lean.CollectLevelMVars.State
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The **valuative criterion** for separated morphisms.  -/
AlgebraicGeometry.IsSeparated.of_valuativeCriterion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.ValuativeCriterion.Uniqueness f → AlgebraicGeometry.IsSeparated f
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ Action V G` preserves the colimit of some `K : J ⥤ C` if
it does after postcomposing with the forgetful functor `Action V G ⥤ V`.  -/
Action.preservesColimit_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} J] (K : CategoryTheory.Functor J C),
  CategoryTheory.Limits.PreservesColimit K (F.comp (Action.forget V G)) → CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.multiplicativeClosure_eq_strictMap_paths : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C),
  W.multiplicativeClosure = W.paths.strictMap (CategoryTheory.pathComposition C)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withExpectedType : Option Lean.Expr → (Lean.Expr → Lean.Elab.TermElabM Lean.Expr) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.insert_of_notMem : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  a ∉ s → s.Pairwise r → (∀ b ∈ s, r a b ∧ r b a) → (insert a s).Pairwise r
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.toEnd_pow_apply_mem : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] {M : Type u_3} [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] {χ₁ χ₂ : ↥H → R} {x : L} {m : M},
  x ∈ LieAlgebra.rootSpace H χ₁ →
    m ∈ LieModule.genWeightSpace M χ₂ →
      ∀ (n : ℕ), ((LieModule.toEnd R L M) x ^ n) m ∈ LieModule.genWeightSpace M (n • χ₁ + χ₂)