mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mk0_mul : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (x y : G₀) (hxy : x * y ≠ 0),
  Units.mk0 (x * y) hxy = Units.mk0 x ⋯ * Units.mk0 y ⋯
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_fun_comp_smul_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} {E : Type u_5} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 E] {X : Ω → 𝓧} {Y : Ω → 𝓨}
  {f : 𝓧 → 𝕜} {g : 𝓨 → E},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ) →
            ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ = (∫ (ω : Ω), f (X ω) ∂μ) • ∫ (ω : Ω), g (Y ω) ∂μ
-- Mathlib.Data.Num.Bitwise
PosNum.instHShiftLeftNat : HShiftLeft PosNum ℕ PosNum
-- Mathlib.Data.WSeq.Basic
/-- auxiliary definition of `destruct_append` over weak sequences  -/
Stream'.WSeq.destruct_append.aux : {α : Type u} → Stream'.WSeq α → Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_hom_naturality_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} (n a a' : M) (ha' : n + a = a')
  (f : X ⟶ Y) {Z : A} (h : (F.shift a').obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f))
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app X)
      (CategoryTheory.CategoryStruct.comp ((F.shift a').map f) h)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_tsum_le_of_forall_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] [Nonempty ι] {f : ι → M}
  {C : ℝ}, (∀ (i : ι), ‖f i‖ ≤ C) → ‖∑' (i : ι), f i‖ ≤ C
-- Mathlib.Combinatorics.Pigeonhole
/-- A version of the pigeonhole principle for set-valued functions.

Given a family of sets `f : α → Finset β` and a choice of indices `s : Finset α`.
Let `k` denote the minimum cardinality of the `f j`s.
If the cardinality of the union `s.biUnion f` is less than `s.card`, then
there exists an element `x ∈ s.biUnion f` which is covered by more than `k` of the sets
`f j` (i.e., `k < #{j ∈ s | x ∈ f j}`).

This is a double-counting variant of the pigeonhole principle.
Unlike the classical pigeonhole principle (see
`Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to`),
this formulation handles a *set-valued* assignment where elements may belong to
multiple sets simultaneously.  -/
Finset.exists_mem_exists_mem_inf'_card_lt : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} [inst_1 : DecidableEq α] [inst_2 : Fintype α]
  {f : α → Finset β} (h₁ : s.Nonempty),
  (∀ j ∈ s, 0 < (f j).card) →
    (s.biUnion f).card < s.card → ∃ a ∈ s, ∃ x ∈ f a, (s.inf' h₁ fun j => (f j).card) < {j | j ∈ s ∧ x ∈ f j}.card
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {x : M},
  ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' (f x)) ∘ f) x
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
  CategoryTheory.eHomWhiskerRight C f Y = (CategoryTheory.MonoidalClosed.pre f).app Y
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_smul : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] {x : HahnSeries Γ R}
  {s : HahnSeries.SummableFamily Γ R α}, (x • s).hsum = x * s.hsum
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.toCompl : {α : Type u_1} → [self : Order.Frame α] → Compl α
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₁₀_comp_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom
        (ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A))
          (fun n => groupHomology.inhomogeneousChains.d A n) 1 0))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A)) x)
-- Mathlib.CategoryTheory.PUnit
/-- A category being equivalent to `PUnit` is equivalent to it having a unique morphism between
any two objects. (In fact, such a category is also a groupoid;
see `CategoryTheory.Groupoid.ofHomUnique`)  -/
CategoryTheory.equiv_punit_iff_unique : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  Nonempty (C ≌ CategoryTheory.Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommGroupOfAddMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddCommGroup (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddCommGroup (DirectLimit G f)
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.ErrorFormat.github.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.ErrorFormat.github = 1
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.of_isNoetherian_rng : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] [IsNoetherian K V₂] {f : V →ₗ[K] V₂}, f.HasNoetherianRange
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonCreateFile : Lean.FromJson Lean.Lsp.CreateFile
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Functional equation for the even Hurwitz zeta function with poles removed (alternative form).  -/
HurwitzZeta.completedCosZeta₀_one_sub : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedCosZeta₀ a (1 - s) = HurwitzZeta.completedHurwitzZetaEven₀ a s
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than the given key.
 -/
Std.DTreeMap.getEntryGT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → (a : α) × β a
-- Mathlib.Topology.Sheaves.MayerVietoris
Opens.mayerVietorisSquare_X₃ : ∀ {T : Type u} [inst : TopologicalSpace T] (U V : TopologicalSpace.Opens T), (Opens.mayerVietorisSquare U V).X₃ = V
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The Jacobian point class underlying a nonsingular Jacobian point on `W`.  -/
WeierstrassCurve.Jacobian.Point.point : {R : Type r} →
  [inst : CommRing R] → {W' : WeierstrassCurve.Jacobian R} → W'.Point → WeierstrassCurve.Jacobian.PointClass R
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.univ : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s : Set α}, Absorbs G₀ Set.univ s
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.collectedBasis.congr_simp : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2}
  (v v_1 : (i : ι) → Module.Basis (α i) R ↥(A i)), v = v_1 → h.collectedBasis v = h.collectedBasis v_1
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- The (bundled) type of `X`-continuous maps `Y → Z`.  -/
Topology.ContinuousMapGeneratedBy : {ι : Type t} →
  (X : ι → Type u) →
    [(i : ι) → TopologicalSpace (X i)] →
      (Y : Type v) → [TopologicalSpace Y] → (Z : Type v') → [TopologicalSpace Z] → Type (max v v')
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.commonSuffix.loop.eq_def : ∀ (s t : Substring.Raw) (spos tpos : String.Pos.Raw),
  Substring.Raw.commonSuffix.loop✝ s t spos tpos =
    if h : s.startPos < spos ∧ t.startPos < tpos then
      let spos' := String.Pos.Raw.prev s.str spos;
      have tpos' := String.Pos.Raw.prev t.str tpos;
      if (String.Pos.Raw.get s.str spos' == String.Pos.Raw.get t.str tpos') = true then
        have this := ⋯;
        Substring.Raw.commonSuffix.loop✝ s t spos' tpos'
      else spos
    else spos
-- Init.Prelude
/-- Non-strict inequality is reflexive: `n ≤ n`  -/
Nat.le.refl : ∀ {n : ℕ}, n.le n
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.iInter₂ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {ι : Sort u_3} {κ : ι → Sort u_4} {f : (i : ι) → κ i → Set E},
  (∀ (i : ι) (j : κ i), AbsConvex 𝕜 (f i j)) → AbsConvex 𝕜 (⋂ i, ⋂ j, f i j)
-- Mathlib.Combinatorics.Optimization.ValuedCSP
Function.HasMaxCutPropertyAt.rows_lt_aux : ∀ {D : Type u_1} {C : Type u_3} [inst : PartialOrder C] {f : (Fin 2 → D) → C} {a b : D},
  Function.HasMaxCutPropertyAt f a b →
    a ≠ b →
      ∀ {ω : FractionalOperation D 2}, ω.IsSymmetric → ∀ {r : Fin 2 → D}, r ∈ ω.tt ![![a, b], ![b, a]] → f ![a, b] < f r
-- Std.Data.ExtTreeMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtTreeMap.getKey : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (a : α) → a ∈ t → α
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eq : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} {n : ℕ},
  f.support.card = n ↔
    ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, Polynomial.C (x i) * Polynomial.X ^ k i
-- Mathlib.Topology.Specialization
Specialization.ofEquiv_symm : ∀ {α : Type u_1}, Specialization.ofEquiv.symm = Specialization.toEquiv
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.id_apply : ∀ {α : Type u_2} [inst : CompleteLattice α] (a : α), (CompleteLatticeHom.id α) a = a
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.pos : ∀ {c : Cardinal.{u_1}}, c.IsRegular → 0 < c
-- Mathlib.CategoryTheory.Limits.Final
/-- A prefunctor mapping structured arrows on `G` to structured arrows on `pre F G` with their
action on fibers being the identity.  -/
CategoryTheory.Grothendieck.structuredArrowToStructuredArrowPre : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D CategoryTheory.Cat) →
          (G : CategoryTheory.Functor C D) →
            (d : D) →
              (f : ↑(F.obj d)) →
                CategoryTheory.StructuredArrow d G ⥤q
                  CategoryTheory.StructuredArrow { base := d, fiber := f } (CategoryTheory.Grothendieck.pre F G)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coeff : ℕ → Lean.Meta.Grind.Arith.Linear.EqCnstr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Mathlib.Data.Vector3
Fin2.add.eq_1 : ∀ {n : ℕ} (i : Fin2 n), i.add 0 = i
-- Mathlib.CategoryTheory.Action.Concrete
Action.FintypeCat.quotientToEndHom_mk : ∀ {G : Type u_1} [inst : Group G] (H N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : N.Normal] (x : ↥H) (g : G),
  (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.quotientToEndHom H N) ⟦x⟧).hom) ⟦g⟧ = ⟦g * ↑x⁻¹⟧
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- A `2 × 2` matrix is *elliptic* if its discriminant is strictly negative.  -/
Matrix.IsElliptic : {R : Type u_1} → [CommRing R] → [Preorder R] → Matrix (Fin 2) (Fin 2) R → Prop
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.epi_map_0_of_epi : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) [CategoryTheory.Epi f],
  CategoryTheory.Epi (groupHomology.map (MonoidHom.id G) f 0)
-- Mathlib.Order.Basic
eq_iff_ge_not_gt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a = b ↔ b ≤ a ∧ ¬b < a
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The simplicial `G`-set sending `[n]` to `Gⁿ⁺¹` equipped with the diagonal action of `G`.  -/
classifyingSpaceUniversalCover : (G : Type u) → [inst : Monoid G] → CategoryTheory.SimplicialObject (Action (Type u) G)
-- Mathlib.Data.Set.Prod
Set.snd_image_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (t : Set β), Prod.snd '' s ×ˢ t = t
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.compIso_hom_comp_image_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.IsIso g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom
      (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g
-- Mathlib.Data.Nat.Factorial.SuperFactorial
/-- `sf` notation for superfactorial  -/
Nat.termSf_ : Lean.ParserDescr
-- Mathlib.Algebra.Opposites
AddOpposite.op_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : α), AddOpposite.op (a * b) = AddOpposite.op a * AddOpposite.op b
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_le_iff_le : ∀ {a b : BitVec 8}, { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.TreeMap.maxEntryD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α × β → α × β
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.comp_hom_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom.base = CategoryTheory.CategoryStruct.comp f.hom.base g.hom.base
-- Mathlib.Computability.Partrec
Computable.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : γ → σ} {g : α → β → γ},
  Computable f → Computable₂ g → Computable₂ fun a b => f (g a b)
-- Lean.Meta.Tactic.Grind.Action
/-- Given `[t₁, ..., tₙ]`, returns
```
· t₁
  ...
  tₙ
```
If the list is empty, it returns `· done`.
 -/
Lean.Meta.Grind.Action.mkGrindNext : List Lean.Meta.Grind.TGrind → Lean.CoreM Lean.Meta.Grind.TGrind
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- `p.occursInAt x g` means that the finite pattern `p` appears in the configuration `x`
at position `g`.

Formally: for every position `h` in the support of `p`, the value of the configuration
at `g + h` coincides with the value of `p.config` at `h`.

Intuitively, if you shift the configuration `x` by `g` (using `shift g`),
then on the support of `p` you exactly recover the pattern `p`. This is the basic
notion of "pattern occurrence" used to define subshifts via forbidden patterns.  -/
SymbolicDynamics.FullShift.Pattern.occursInAt : {A : Type u_1} →
  {G : Type u_2} → [inst : Inhabited A] → [AddMonoid G] → SymbolicDynamics.FullShift.Pattern A G → (G → A) → G → Prop
-- Mathlib.Data.Finsupp.Basic
Finsupp.restrictSupportEquiv.eq_1 : ∀ {α : Type u_1} (s : Set α) (M : Type u_12) [inst : AddCommMonoid M],
  Finsupp.restrictSupportEquiv s M =
    { toFun := fun f => Finsupp.subtypeDomain (fun x => x ∈ s) ↑f, invFun := fun f => ⟨f.extendDomain, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instMulSemiringAction : (K : Type u_1) →
  [inst : Field K] →
    {G : Type u_3} → [inst_1 : Group G] → [MulSemiringAction G K] → MulSemiringAction G (NumberField.RingOfIntegers K)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafifyLift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η η_1 : P ⟶ Q), η = η_1 → ∀ (hQ : CategoryTheory.Presheaf.IsSheaf J Q), J.sheafifyLift η hQ = J.sheafifyLift η_1 hQ
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.getIOTypeArg : Lean.Expr → Option Lean.Expr
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.not_rankInfinite : ∀ {α : Type u_1} (M : Matroid α) [M.RankFinite], ¬M.RankInfinite
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- On topological spaces where indicators of closed sets have decreasing approximating sequences of
continuous functions (`HasOuterApproxClosed`), the topology of weak convergence of finite Borel
measures is Hausdorff (`T2Space`).  -/
MeasureTheory.FiniteMeasure.t2Space : ∀ (Ω : Type u_1) [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [inst_3 : BorelSpace Ω], T2Space (MeasureTheory.FiniteMeasure Ω)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExceptSummand_of_notMem : ∀ (L : PeriodPair), ∀ l₀ ∉ L.lattice, L.weierstrassPExceptSummand l₀ = L.weierstrassPSummand
-- Init.Internal.Order.Basic
Lean.Order.PProd.chain.fst : {α : Sort u} → {β : Sort v} → [Lean.Order.CCPO α] → [Lean.Order.CCPO β] → (α ×' β → Prop) → α → Prop
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- Sets of the family "centered" at a given point.  -/
VitaliFamily.setsAt : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → X → Set (Set X)
-- Batteries.Data.BinomialHeap.Basic
/-- The well formedness predicate for a heap node.
It asserts that:
* If `a` is added at the top to make the forest into a tree, the resulting tree
  is a `le`-min-heap (if `le` is well-behaved)
* When interpreting `child` and `sibling` as left and right children of a binary tree,
  it is a perfect binary tree with depth `r`
 -/
Batteries.BinomialHeap.Imp.HeapNode.WF : {α : Type u_1} → (α → α → Bool) → α → Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Prop
-- Lean.Meta.CollectFVars
Lean.Expr.collectFVars : Lean.Expr → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_zpow_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 1 < a → (a ^ m < a ^ n ↔ m < n)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F F_1 : CategoryTheory.Functor C FintypeCat),
  F = F_1 →
    CategoryTheory.PreGaloisCategory.PointedGaloisObject F = CategoryTheory.PreGaloisCategory.PointedGaloisObject F_1
-- Mathlib.Logic.Basic
/-- Wrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.Prime` into an instance implicit assumption.

On the other hand, making `Nat.Prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.Prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.Prime]` to `ZMod.instField`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  -/
Fact : Prop → Prop
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_id_f_hom_eq_compLeft : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) (i : ℕ),
  ModuleCat.Hom.hom ((groupCohomology.cochainsMap (MonoidHom.id G) f).f i) = (Rep.Hom.hom f).compLeft (Fin i → G)
-- Mathlib.Data.Set.Card
Set.encard_strictMono : ∀ {α : Type u_1} [Finite α], StrictMono Set.encard
-- Init.Omega.IntList
Lean.Omega.IntList.add_get : ∀ (xs ys : Lean.Omega.IntList) (i : ℕ), (xs + ys).get i = xs.get i + ys.get i
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_set_MonadState_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {post : PUnit.{u + 1} → Pred} {epost : EPred} [inst_4 : MonadStateOf σ m] (x : σ),
  Std.Internal.Do.wp (MonadState.set x) post epost = Std.Internal.Do.wp (set x) post epost
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Obj.mk.injEq : ∀ (e? e?_1 : Option Lean.Expr), ({ e? := e? } = { e? := e?_1 }) = (e? = e?_1)
-- Mathlib.Algebra.MvPolynomial.Eval
/-- A map `σ → S₁` where `S₁` is an algebra over `R` generates an `R`-algebra homomorphism
from multivariate polynomials over `σ` to `S₁`.  -/
MvPolynomial.aeval : {R : Type u} →
  {S₁ : Type v} →
    {σ : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S₁] → [inst_2 : Algebra R S₁] → (σ → S₁) → MvPolynomial σ R →ₐ[R] S₁
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.hasSum_coe_one : ∀ {α : Type u_1} (p : PMF α), HasSum (⇑p) 1
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.injOn_of_disjoint_ker : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} {s : Set M}, s ⊆ ↑p → Disjoint p f.ker → Set.InjOn (⇑f) s
-- Lean.Data.Lsp.Internal
/-- Namespaces that are open at the position of `identifier`.
Used for accurately matching declarations against `identifier` in context.
 -/
Lean.Lsp.LeanModuleQuery.openNamespaces : Lean.Lsp.LeanModuleQuery → Array Lean.Lsp.OpenNamespace