mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_apply_eq_cov : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (x y : E),
      ((ProbabilityTheory.covarianceBilin μ) x) y =
        ProbabilityTheory.covariance (fun u => inner ℝ x u) (fun u => inner ℝ y u) μ
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum.eq_1 : ∀ {α : Type u_3} [inst : AddMonoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise AddCommute),
  s.noncommSum comm = Multiset.noncommFold (fun x1 x2 => x1 + x2) s comm 0
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_ne_top : ∀ {r : ℝ}, ENNReal.ofReal r ≠ ⊤
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), ProbabilityTheory.cgf X (κ ω') t ≤ ↑c * t ^ 2 / 2
-- Mathlib.RingTheory.TensorProduct.Basic
/-- An auxiliary definition, used for constructing the `Module (A ⊗[R] B) M` in
`TensorProduct.Algebra.module` below.  -/
TensorProduct.Algebra.moduleAux : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Module A M] →
                    [inst_6 : Module B M] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [IsScalarTower R A M] → [IsScalarTower R B M] → TensorProduct R A B →ₗ[R] M →ₗ[R] M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q),
  c.toCocone.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = c.inl
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_gradedMul : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (x y : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ)),
  (TensorProduct.gradedComm R 𝒜 ℬ) (((TensorProduct.gradedMul R 𝒜 ℬ) x) y) =
    ((TensorProduct.gradedMul R ℬ 𝒜) ((TensorProduct.gradedComm R 𝒜 ℬ) x)) ((TensorProduct.gradedComm R 𝒜 ℬ) y)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X)
      ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.category_comp_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  {X Y Z : CategoryTheory.Cokleisli U} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).of =
    CategoryTheory.CategoryStruct.comp (U.δ.app X.of) (CategoryTheory.CategoryStruct.comp (U.map f.of) g.of)
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- The ring of `p`-adic integers.  -/
«termℤ_[_]» : Lean.ParserDescr
-- Lean.SubExpr
Lean.SubExpr.instFromJsonGoalLocation : Lean.FromJson Lean.SubExpr.GoalLocation
-- Lean.Language.Basic
/-- Arbitrary snapshot type, used for extensibility.  -/
Lean.Language.DynamicSnapshot : Type
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_coe : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M), ↑(Submodule.map f p) = ⇑f '' ↑p
-- Mathlib.LinearAlgebra.Span.Basic
/-- The span of a finite subset is compact in the lattice of submodules.  -/
Submodule.finset_span_isCompactElement : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Finset M),
  IsCompactElement (Submodule.span R ↑S)
-- Mathlib.Analysis.Normed.Group.HomCompletion
/-- The map from a normed group to its completion, as a normed group hom.  -/
NormedAddCommGroup.toCompl : {G : Type u_1} → [inst : SeminormedAddCommGroup G] → NormedAddGroupHom G (UniformSpace.Completion G)
-- Mathlib.Analysis.CStarAlgebra.Basic
nndist_star_star : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x y : E),
  nndist (star x) (star y) = nndist x y
-- Init.MetaTypes
Lean.Meta.LiftLetsConfig.toExtractLetsConfig : Lean.Meta.LiftLetsConfig → Lean.Meta.ExtractLetsConfig
-- Mathlib.Analysis.Calculus.Deriv.Inv
differentiableAt_inv_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔ x ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A morphism between the two vertex objects of the bicones  -/
CategoryTheory.Limits.BiconeMorphism.hom : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → {A B : CategoryTheory.Limits.Bicone F} → CategoryTheory.Limits.BiconeMorphism A B → (A.pt ⟶ B.pt)
-- Mathlib.NumberTheory.NumberField.Basic
/-- A finite extension of a number field is a number field.  -/
NumberField.of_module_finite : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [NumberField K] [inst_3 : Algebra K L]
  [Module.Finite K L], NumberField L
-- Std.Internal.Do.Order.PreservesSup
/-- The **frame closure** of a post-transformer `k` with respect to a family of `Sup`-preserving
operators `op r`: the meet over all resources `r` of the `r`-upper-adjoint of `k` framed by `r`. It
internalizes the frame rule into any `k` (see `frameClosure_frames`), with no assumption on `k`. A
weakest precondition built as `frameClosure op (fun Q => bwp x Q E)` satisfies the `op`-frame rule by
construction.  -/
Lean.Order.PreservesSup.frameClosure : {α : Type u} → [Lean.Order.CompleteLattice α] → {R : Type v} → {β : Type w} → (R → α → α) → ((β → α) → α) → (β → α) → α
-- Init.Data.String.Substring
/-- If `suff` is a suffix of `s`, returns the remainder. Returns `none` otherwise.

The substring `suff` is a suffix of `s` if there exists a `t : Substring` such that
`s.toString = t.toString ++ suff.toString`. If so, the result the substring of `s` without the
suffix.
 -/
Substring.Raw.dropSuffix? : Substring.Raw → Substring.Raw → Option Substring.Raw
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Refl.rel_of_ne_imp`.

---

To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
it suffices to show it holds when `x ≠ y`.  -/
Reflexive.rel_of_ne_imp : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {x y : α}, (x ≠ y → r x y) → r x y
-- Mathlib.Order.Monotone.Monovary
antivaryOn_iff_antivary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s ↔ Antivary (fun i => f ↑i) fun i => g ↑i
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toNormedCommRing : {A : Type u_1} → [self : CommCStarAlgebra A] → NormedCommRing A
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.eqOn_of_comp_eqOn : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f →
    ∀ {A : Type u_3} [inst_2 : TopologicalSpace A] {s : Set A} {g₁ g₂ : A → E},
      IsPreconnected s →
        ContinuousOn g₁ s →
          ContinuousOn g₂ s → Set.EqOn (f ∘ g₁) (f ∘ g₂) s → ∀ {a : A}, a ∈ s → g₁ a = g₂ a → Set.EqOn g₁ g₂ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_ΨSq : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ},
  ↑n ≠ 0 → (W.ΨSq n).natDegree = n.natAbs ^ 2 - 1
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image2_image_left_anticomm`.  -/
Set.image_image2_antidistrib_left : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α} {t : Set β}
  {g : γ → δ} {f' : β' → α → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' b) a) → g '' Set.image2 f s t = Set.image2 f' (g' '' t) s
-- Mathlib.Order.Hom.Set
/-- Order isomorphism between two equal sets.  -/
OrderIso.setCongr : {α : Type u_1} → [inst : Preorder α] → (s t : Set α) → s = t → ↑s ≃o ↑t
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ μ' : MeasureTheory.Measure α}
  {ν ν' : MeasureTheory.Measure β} [MeasureTheory.SFinite ν'], μ ≤ μ' → ν ≤ ν' → μ.prod ν ≤ μ'.prod ν'
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddCommMonoid β]
  (f g : α →+ β), (f + g).mapMatrix = f.mapMatrix + g.mapMatrix
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_pos : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0}, 0 < ↑q ↔ 0 < q
-- Lean.Parser.Extra
Lean.Parser.ppHardSpace.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.instInhabited : Inhabited UpperHalfPlane
-- Lean.Parser.Extension
/-- Whether arguments should be wrapped in `group(·)` if they do not produce exactly one syntax node.  -/
Lean.Parser.ParserAliasInfo.autoGroupArgs : Lean.Parser.ParserAliasInfo → Bool
-- Init.Data.String.Basic
ByteArray.isSome_utf8Decode?Go_eq_validateUTF8Go : ∀ {b : ByteArray} {i : ℕ} {acc : Array Char} {hi : i ≤ b.size},
  (ByteArray.utf8Decode?.go b i acc hi).isSome = ByteArray.validateUTF8.go b i hi
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instAddLeftReflectLT : AddLeftReflectLT Ordinal.{u}
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurable_memPartitionSet_subtype : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ)
  (m_1 : MeasurableSpace ↑(memPartition t n)), Measurable fun a => ⟨memPartitionSet t n a, ⋯⟩
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet.eq_1 : ∀ (x : List ℕ), Turing.ToPartrec.stepRet Turing.ToPartrec.Cont.halt x = Turing.ToPartrec.Cfg.halt x
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.coe_mapAddHom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C},
  ⇑F.mapAddHom = F.map
-- Mathlib.CategoryTheory.Localization.OfQuotient
/-- Auxiliary definition for `Quotient.isLocalization_functor`.  -/
_private.Mathlib.CategoryTheory.Localization.OfQuotient.0.CategoryTheory.Quotient.isLocalization_functor.strictUniversalPropertyFixedTarget : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {r : HomRel C} →
      {W : CategoryTheory.MorphismProperty C} →
        W.IsInvertedBy (CategoryTheory.Quotient.functor r) →
          (∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π) →
            (E : Type u_3) →
              [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
                CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.Quotient.functor r) W E
-- Mathlib.Logic.Function.Basic
Function.Surjective.of_comp_iff : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
  Function.Surjective g → (Function.Surjective (f ∘ g) ↔ Function.Surjective f)
-- Mathlib.Geometry.Manifold.Bordism
/-- If `(N, f)` is a singular manifold on `X` and `M` another `C^k` manifold,
a continuous map `φ : M → N` induces a singular manifold structure `(M, f ∘ φ)` on `X`.  -/
SingularManifold.comap : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_4} →
        {H : Type u_5} →
          {M : Type u_6} →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace ℝ E] →
                [inst_3 : FiniteDimensional ℝ E] →
                  [inst_4 : TopologicalSpace H] →
                    {I : ModelWithCorners ℝ E H} →
                      [inst_5 : TopologicalSpace M] →
                        [inst_6 : ChartedSpace H M] →
                          [IsManifold I k M] →
                            [CompactSpace M] →
                              [BoundarylessManifold I M] →
                                (s : SingularManifold X k I) → {φ : M → s.M} → Continuous φ → SingularManifold X k I
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.mono : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {m n : ℕ}, m ≤ n → IsMulFreimanHom n A B f → IsMulFreimanHom m A B f
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C} (a : X ⟶ Y),
  CategoryTheory.Groupoid.invEquiv a = CategoryTheory.Groupoid.inv a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.left : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Bool
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaPairing_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
  (α : P ⟶ Q),
  (CategoryTheory.yonedaPairing C).map α =
    TypeCat.ofHom fun β =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.1.unop) (CategoryTheory.CategoryStruct.comp β α.2)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_eq_singleton : ∀ {R : Type u} [inst : CommSemiring R] (m : Ideal R) [inst_1 : m.IsMaximal],
  PrimeSpectrum.zeroLocus ↑m = {{ asIdeal := m, isPrime := ⋯ }}
-- Init.Grind.Offset
Lean.Grind.Nat.ro_lo_2 : ∀ (u w v k₁ k₂ : ℕ), Lean.Grind.isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqCongrTheoremCacheKey : BEq Lean.Meta.Grind.CongrTheoremCacheKey
-- Mathlib.Order.Comparable
/-- The incomparability relation `IncompRel r a b` means `¬ r a b` and `¬ r b a`.  -/
IncompRel : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- Complex-valued characters of a finite abelian group `α` form a basis of `α → ℂ`.  -/
AddChar.complexBasis : (α : Type u_1) → [inst : AddCommGroup α] → [Finite α] → Module.Basis (AddChar α ℂ) ℂ (α → ℂ)
-- Mathlib.Topology.UniformSpace.Closeds
/-- In the Hausdorff uniformity, the powerset of a totally bounded set is totally bounded.  -/
TotallyBounded.powerset_hausdorff : ∀ {α : Type u_1} [inst : UniformSpace α] {t : Set α}, TotallyBounded t → TotallyBounded (𝒫 t)
-- Std.Sync.Broadcast
/-- Creates a new broadcast channel.
 -/
Std.Broadcast.new : {α : Type} → (capacity : optParam ℕ 16) → autoParam (capacity > 0) Std.Broadcast.new._auto_1 → BaseIO (Std.Broadcast α)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.LazyEntry.mk : Option Lean.Meta.RefinedDiscrTree.ExprInfo →
  List Lean.Meta.RefinedDiscrTree.StackEntry →
    Lean.MetavarContext →
      Option (Array Lean.MVarId) → List Lean.Meta.RefinedDiscrTree.Key → Lean.Meta.RefinedDiscrTree.LazyEntry
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- The maximum cardinality of a `1`-separated set in the ball of radius `2`. This is also the
optimal number of families in the Besicovitch covering theorem.  -/
Besicovitch.multiplicity : (E : Type u_2) → [NormedAddCommGroup E] → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h =
    (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono (CategoryTheory.ShortComplex.opMap φ) h.op).unop
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.exists_inv_mem_iff_exists_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {P : G → Prop}, (∃ x ∈ K, P x⁻¹) ↔ ∃ x ∈ K, P x
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_of_right_eq_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v y = 0 → v (x + y) = v x
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_inv : ∀ {R : Type u_1} [inst : CommRing R] (f : (PowerSeries R)ˣ),
  (PowerSeries.derivative R) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (PowerSeries.derivative R) ↑f
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Handlers for which this trie position's key is a strict prefix.  -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.children : Lean.Elab.ConfigEval.HandlerTrie✝ → Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)
-- Lean.Meta.Tactic.Grind.Types
/-- Modification time  -/
Lean.Meta.Grind.ENode.mt : Lean.Meta.Grind.ENode → ℕ
-- Init.Data.String.Basic
/-- Given a valid position on `s.str` which is within the bounds of the slice `s`, obtains the
corresponding valid position on `s`.
 -/
String.Slice.Pos.ofStr : {s : String.Slice} → (pos : s.str.Pos) → s.startInclusive ≤ pos → pos ≤ s.endExclusive → s.Pos
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppModule : Lean.TSyntax `Lean.Parser.Module.module → Lean.CoreM Std.Format
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_zero`. -/
EMetric.ball_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, Metric.eball x 0 = ∅
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_mul_lt_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightMono α] {a b c d : α}, a * b < c → d ≤ a → d * b < c
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.mono : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, RightOrdContinuous f → Monotone f
-- Init.Data.List.Zip
List.drop_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {i : ℕ},
  List.drop i (List.zipWith f l l') = List.zipWith f (List.drop i l) (List.drop i l')
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Ideal.map_mk_comap_factor : ∀ {R : Type u_1} [inst : Ring R] {I J K : Ideal R} [inst_1 : J.IsTwoSided] [inst_2 : K.IsTwoSided],
  J ≤ I →
    ∀ (hJK : K ≤ J),
      Ideal.comap (Ideal.Quotient.factor hJK) (Ideal.map (Ideal.Quotient.mk J) I) = Ideal.map (Ideal.Quotient.mk K) I
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_iff_hasSum_of_ne_zero_bij : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → α} (i : ↑(Function.support g) → β),
  Function.Injective i →
    Function.support f ⊆ Set.range i → (∀ (x : ↑(Function.support g)), f (i x) = g ↑x) → (HasSum f a ↔ HasSum g a)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The family of 2-morphisms out of the left Kan lift `f₊ g`.  -/
CategoryTheory.Bicategory.lanLiftDesc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            (s : CategoryTheory.Bicategory.LeftLift f g) → CategoryTheory.Bicategory.lanLift f g ⟶ s.lift
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.getHeadInfo : Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.HeadInfo
-- Mathlib.Topology.Order.LiminfLimsup
/-- A monotone function between (conditionally) complete linear ordered spaces sends a
`Filter.limsSup` to the `Filter.limsup` of the image if the function is continuous at the `limsSup`
(and the filter is bounded from above and frequently bounded from below).  -/
Monotone.map_limsSup_of_continuousAt : ∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [OrderTopology S]
  {F : Filter R} [F.NeBot] {f : R → S},
  Monotone f →
    ContinuousAt f F.limsSup →
      autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) F) Monotone.map_limsSup_of_continuousAt._auto_1 →
        autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F) Monotone.map_limsSup_of_continuousAt._auto_3 →
          f F.limsSup = Filter.limsup f F
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- Given a submersive presentation of `S` as `R`-algebra, the images of `dxᵢ`
for `i` in the complement of `σ` in `ι` form a basis of `Ω[S⁄R]`.  -/
Algebra.SubmersivePresentation.basisKaehler : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) → Module.Basis (↑(Set.range P.map)ᶜ) S Ω[S⁄R]
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapRangeAlgHom_comp : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : Monoid M] (f : A →ₐ[R] B) (g : B →ₐ[R] C),
  MonoidAlgebra.mapAlgHom M (g.comp f) = (MonoidAlgebra.mapAlgHom M g).comp (MonoidAlgebra.mapAlgHom M f)
-- Mathlib.CategoryTheory.Products.Bifunctor
CategoryTheory.Bifunctor.map_id_comp : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor (C × D) E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
  F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id W) f))
      (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id W) g))