mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Instances
Lean.Meta.Instances.mk.sizeOf_spec : ∀ (discrTree : Lean.Meta.InstanceTree) (instanceNames : Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry)
  (erased : Lean.PHashSet Lean.Name),
  sizeOf { discrTree := discrTree, instanceNames := instanceNames, erased := erased } =
    1 + sizeOf discrTree + sizeOf instanceNames + sizeOf erased
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.below.sInter : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {motive : (a : Set α) → Filter.CardinalGenerateSets g a → Prop}
  {S : Set (Set α)} (a : Cardinal.mk ↑S < c) (a_1 : ∀ s ∈ S, Filter.CardinalGenerateSets g s),
  (∀ (s : Set α) (a : s ∈ S), Filter.CardinalGenerateSets.below ⋯) →
    (∀ (s : Set α) (a : s ∈ S), motive s ⋯) → Filter.CardinalGenerateSets.below ⋯
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.hom_left_inv_left_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (e : f ≅ g) {Z : T}
  (h : f.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.inv) h) =
    h
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.ι_π_of_ne_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] {b c : β},
  b ≠ c →
    ∀ {Z : C} (h : f c ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.π f c) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.DTreeMap.ofList l cmp).getKeyD k' fallback = k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toArray_toList_eq_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β), (↑m).toList.toArray = (↑m).toArray
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_or : ∀ (a b : BitVec 64), { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The fundamental property of the operator norm of a continuous multilinear map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`, `nnnorm` version.  -/
ContinuousMultilinearMap.le_opNNNorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i), ‖f m‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊
-- Init.Data.Vector.Erase
Vector.mem_eraseIdx_iff_getElem? : ∀ {α : Type u_1} {n : ℕ} {x : α} {xs : Vector α n} {k : ℕ} {h : k < n},
  x ∈ xs.eraseIdx k h ↔ ∃ i, i ≠ k ∧ xs[i]? = some x
-- Init.Data.UInt.Lemmas
UInt64.ofNat_mul : ∀ (a b : ℕ), UInt64.ofNat (a * b) = UInt64.ofNat a * UInt64.ofNat b
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  [inst_3 : DecidableEq G] (f g : SkewMonoidAlgebra k G) (x : G),
  (f * g).coeff x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
-- Aesop.BaseM
/-- State of the `BaseM` monad.  -/
Aesop.BaseM.State : Type
-- Mathlib.Data.PFunctor.Univariate.M
/-- Relation between two approximations of the cofix of a pfunctor
that state they both contain the same data until one of them is truncated  -/
PFunctor.Approx.Agree : {F : PFunctor.{uA, uB}} → {n : ℕ} → PFunctor.Approx.CofixA F n → PFunctor.Approx.CofixA F (n + 1) → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_toArray_roc : ∀ {a b : ℕ}, (a<...=b).toArray.size = b - a
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instVAddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass Mᵒᵈ N α
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.inhabitedImageMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        Inhabited (CategoryTheory.Limits.ImageMap (CategoryTheory.CategoryStruct.id f))
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.ext_iff : ∀ {X : Type u} {inst : PartialOrder X} {x y : PartialOrder.NonemptyFiniteChains X}, x = y ↔ x.finset = y.finset
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff_integrable_smul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → ENNReal},
  Measurable f →
    (∀ᵐ (x : α) ∂μ, f x < ⊤) →
      ∀ {g : α → E},
        MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun x => (f x).toReal • g x) μ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.filterMap! : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {x : Ord α} {t : Std.DTreeMap.Internal.Impl α β}
  {f : (a : α) → β a → Option (γ a)}, t.WF → (Std.DTreeMap.Internal.Impl.filterMap! f t).WF
-- Mathlib.NumberTheory.MulChar.Basic
/-- The inverse of a multiplicative character `χ`, applied to `a`, is the inverse of `χ a`.
Variant when the target is a field  -/
MulChar.inv_apply_eq_inv' : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_3} [inst_1 : CommGroupWithZero R'] (χ : MulChar R R') (a : R),
  χ⁻¹ a = (χ a)⁻¹
-- Mathlib.Geometry.Euclidean.Projection
/-- Orthogonal projection is idempotent.  -/
EuclideanGeometry.orthogonalProjection_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.orthogonalProjection s) ↑((EuclideanGeometry.orthogonalProjection s) p) =
    (EuclideanGeometry.orthogonalProjection s) p
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- `of` is the canonical map from `α` to a presented additive monoid with generators `x : α`. The
term `x` is mapped to the equivalence class of the image of `x` in `FreeAddMonoid α`.  -/
PresentedAddMonoid.of : {α : Type u_1} → (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) → α → PresentedAddMonoid rels
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_comp_coinvariantsMk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ A) ((Rep.coinvariantsMk k G).app A) = 0
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.toProd : {V : Type u_1} → {G : SimpleGraph V} → G.Dart → V × V
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_congr_enorm_ae : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ) → MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
-- Mathlib.ModelTheory.Algebra.Field.Basic
/-- A model for the theory of fields is a field. To introduced locally on Types that don't
already have instances for ring operations.

When this is used, it is almost always useful to also add locally the instance
`compatibleFieldOfModelField` afterwards.  -/
FirstOrder.Field.fieldOfModelField : (K : Type u_2) → [inst : FirstOrder.Language.ring.Structure K] → [K ⊨ FirstOrder.Language.Theory.field] → Field K
-- Mathlib.Condensed.TopCatAdjunction
_private.Mathlib.Condensed.TopCatAdjunction.0.CondensedSet.coinducingCoprod.match_1.eq_1 : ∀ (X : CondensedSet) (motive : (i : (S : CompHaus) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop → Sort u_2)
  (fst : CompHaus) (i : X.obj.obj (Opposite.op fst)) (s : ↑⟨fst, i⟩.fst.toTop)
  (h_1 : (fst : CompHaus) → (i : X.obj.obj (Opposite.op fst)) → (s : ↑⟨fst, i⟩.fst.toTop) → motive ⟨⟨fst, i⟩, s⟩),
  (match ⟨⟨fst, i⟩, s⟩ with
    | ⟨⟨fst, i⟩, s⟩ => h_1 fst i s) =
    h_1 fst i s
-- Init.Data.UInt.Basic
instPowUInt16Nat : Pow UInt16 ℕ
-- Init.Data.BitVec.Basic
BitVec.cast_eq : ∀ {n : ℕ} (h : n = n) (x : BitVec n), BitVec.cast h x = x
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_eq_toENNReal : ∀ {x y : EReal}, 0 ≤ x → 0 ≤ y → (x.toENNReal = y.toENNReal ↔ x = y)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : C} (e : G ≅ H) [inst_3 : CategoryTheory.GrpObj G]
  [inst_4 : CategoryTheory.IsCommMonObj G] [inst_5 : CategoryTheory.GrpObj H] [inst_6 : CategoryTheory.IsCommMonObj H]
  [inst_7 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.CommGrp.mkIso' e).inv.hom.hom.hom = e.inv
-- Lean.Data.DeclarationRange
Lean.instInhabitedDeclarationLocation : Inhabited Lean.DeclarationLocation
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_mem : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
-- Mathlib.CategoryTheory.Localization.Quotient
/-- Given `homRel : HomRel C` and `W : MorphismProperty C`, this is the property
that whenever `homRel f g`, then the morphisms `f` and `g` are sent to the
same morphism in the localization category with respect to `W`.  -/
HomRel.FactorsThroughLocalization : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → HomRel C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {V W : CoalgCat R} {x y : V.Hom W}, x.toCoalgHom' = y.toCoalgHom' → x = y
-- Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Finset.sum_preimage_of_bij : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [inst : AddCommMonoid β] (f : ι → κ) (s : Finset κ)
  (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β), ∑ x ∈ s.preimage f ⋯, g (f x) = ∑ x ∈ s, g x
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- Every positive `x` is between two successive integer powers of
another `y` greater than one. This is the same as `exists_mem_Ioc_zpow`,
but with ≤ and < the other way around.  -/
exists_mem_Ico_zpow : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K}
  [ExistsAddOfLE K], 0 < x → 1 < y → ∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.instIsFiniteMeasureElemSphereOfNatRealToSphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  MeasureTheory.IsFiniteMeasure μ.toSphere
-- Mathlib.GroupTheory.Index
Subgroup.index_map_subtype : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (K : Subgroup ↥H),
  (Subgroup.map H.subtype K).index = K.index * H.index
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
mem_subalgebraOfSubring : ∀ {R : Type u_1} [inst : Ring R] {x : R} {S : Subring R}, x ∈ subalgebraOfSubring S ↔ x ∈ S
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.residue_smul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (G : Type u_4) [inst_2 : Group G]
  [inst_3 : MulSemiringAction G R] (g : G) (r : R), (IsLocalRing.residue R) (g • r) = g • (IsLocalRing.residue R) r
-- Aesop.Stats.Extension
Aesop.StatsArray : Type
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.insert_toList_zoom_node : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {c' : RBTree.RBColor} {l : RBTree.RBNode α}
  {v' : α} {r : RBTree.RBNode α} {p : RBTree.RBNode.Path α} {v : α} {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.zoom (cmp v) t = (RBTree.RBNode.node c' l v' r, p) →
      (RBTree.RBNode.insert cmp t v).toList = p.withList (RBTree.RBNode.node c l v r).toList
-- Mathlib.GroupTheory.Sylow
/-- If `f : H →* G` is injective, then `Finite (Sylow p G)` implies `Finite (Sylow p H)`.  -/
Sylow.finite_of_injective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] {f : H →* G},
  Function.Injective ⇑f → ∀ [Finite (Sylow p G)], Finite (Sylow p H)
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Two continuous linear maps from `lp E p` agree if they agree on `lp.single`.

See note [partially-applied ext lemmas].  -/
lp.ext_continuousLinearMap : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_4 : DecidableEq α] {F : Type u_5} [inst_5 : AddCommMonoid F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F]
  [T2Space F] [inst_9 : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ ⦃f g : ↥(lp E p) →L[𝕜] F⦄,
      (∀ (i : α), f ∘SL lp.singleContinuousLinearMap 𝕜 E p i = g ∘SL lp.singleContinuousLinearMap 𝕜 E p i) → f = g
-- Mathlib.NumberTheory.MulChar.Basic
/-- We can post-compose a multiplicative character with a ring homomorphism.  -/
MulChar.ringHomComp : {R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} →
      [inst_1 : CommRing R'] → {R'' : Type u_3} → [inst_2 : CommRing R''] → MulChar R R' → (R' →+* R'') → MulChar R R''
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.ext' : ∀ {α : Type u_1} [inst : UniformSpace α] {Y : Type u_4} [inst_1 : TopologicalSpace Y] [T2Space Y]
  {f g : UniformSpace.Completion α → Y},
  Continuous f → Continuous g → (∀ (a : α), f ↑a = g ↑a) → ∀ (a : UniformSpace.Completion α), f a = g a
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
/-- Quick filter to decide whether it is worth applying `eval` or not.  -/
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isApplicable : Lean.Expr → Bool
-- Init.Data.String.Search
String.revFindAux : String → (Char → Bool) → String.Pos.Raw → Option String.Pos.Raw
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicative_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : AddZeroClass H] (f : G ≃+ H) (a : Multiplicative H),
  (AddEquiv.toMultiplicative f).symm a = (AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom) a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.subset_zero_iff : ∀ {α : Type u_2} [inst : Zero α] {s : Finset α}, s.Nonempty → (s ⊆ 0 ↔ s = 0)
-- Init.PropLemmas
or_iff_left : ∀ {b a : Prop}, ¬b → (a ∨ b ↔ a)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.firstDart_eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (h₁ : ¬p.Nil) (h₂ : 0 < p.darts.length),
  p.firstDart h₁ = p.darts[0]
-- Mathlib.Data.Nat.Factorial.Basic
Nat.succ_ascFactorial : ∀ (n k : ℕ), n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
-- Mathlib.Algebra.Ring.Basic
div_neg : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] {b : R} (a : R), a / -b = -(a / b)
-- Mathlib.Data.Sign.Defs
SignType.pos_iff : ∀ {a : SignType}, 0 < a ↔ a = 1
-- Mathlib.Order.UpperLower.Closure
LowerSet.coe_sdiff : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (t : Set α), ↑(s.sdiff t) = ↑s \ ↑(upperClosure t)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprodEquiv_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R]
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁]
  [inst_9 : AddCommMonoid M₂] [inst_10 : Module R M₂] [inst_11 : ContinuousAdd M₁] [inst_12 : ContinuousAdd M₂]
  [inst_13 : Semiring S] [inst_14 : Module S M] [inst_15 : ContinuousConstSMul S M] [inst_16 : SMulCommClass R S M]
  (f : (M₁ →L[R] M) × (M₂ →L[R] M)), ContinuousLinearMap.coprodEquiv f = f.1.coprod f.2
-- Std.Time.Zoned.TimeZone
Std.Time.instInhabitedTimeZone.default : Std.Time.TimeZone
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.evalAddMonoidHom.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} (j : ι) [inst_1 : (i : ι) → AddMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)],
  RestrictedProduct.evalAddMonoidHom R j = { toFun := fun x => x j, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The vertices in distinct parts are adjacent.  -/
SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (self : G.CompleteEquipartiteSubgraph r t),
  (↑self.parts).Pairwise fun x1 x2 => G.IsCompleteBetween ↑x1 ↑x2
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.nsmul_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] (g : G) (k : ℕ), k • g ∈ AddSubgroup.zmultiples g
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore numerator of a fraction.  -/
OreLocalization.OreSet.oreNum : {R : Type u_1} → {inst : Monoid R} → {S : Submonoid R} → [self : OreLocalization.OreSet S] → R → ↥S → R
-- Mathlib.NumberTheory.AlmostPrime
/-- `IsAlmostPrime k n` means that `n` is `k`-almost prime: it has exactly `k`
prime factors, counted with multiplicity. The side condition excludes `0`, so `1` is
`0`-almost prime.  -/
Nat.IsAlmostPrime : ℕ → ℕ → Prop
-- Mathlib.Geometry.Diffeology.Basic
ContDiff.isPlot : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace ℝ X]
  [Diffeology.IsContDiffCompatible X] {p : EuclideanSpace ℝ (Fin n) → X}, ContDiff ℝ (↑⊤) p → Diffeology.IsPlot p
-- Mathlib.Topology.MetricSpace.Bounded
/-- The **Heine–Borel theorem**:
In a proper metric space, a set is compact if and only if it is closed and bounded.  -/
Metric.isCompact_iff_isClosed_bounded : ∀ {α : Type u_3} {s : Set α} [inst : MetricSpace α] [ProperSpace α], IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F), Differentiable 𝕜 ⇑f
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry : Type
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_sphere_closedBall_closedBall : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.Topology.Covering.Basic
/-- **Alias** of `IsCoveringMapOn.of_isLocalHomeomorphOn`.

---

If `f : E → X` is a continuous map between Hausdorff spaces with `E` compact, `s` is a subset
of `X` such that `f` restricts to a homeomorphism on a neighborhood of every point of `f ⁻¹' s`,
then `f` is a covering map on `s`.

For example, `s` can be taken to be the set of regular values of a C¹ map `f : E → X`
where `E` and `X` are manifolds of the same dimension with `E` compact, according to
the inverse function theorem (see `ContDiffAt.toOpenPartialHomeomorph`).  -/
IsCoveringMapOn.of_openPartialHomeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  [T2Space E] [T2Space X] [CompactSpace E], Continuous f → IsLocalHomeomorphOn f (f ⁻¹' s) → IsCoveringMapOn f s
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_meet_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l} [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.himp P Q) P) Q
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.mk.injEq : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)}
  (spineToSimplex :
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
        X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h }))
  (spine_spineToSimplex : ∀ (m : ℕ) (h : m ≤ n + 1), X.spine m h ∘ spineToSimplex m ⋯ = id)
  (spineToSimplex_spine : ∀ (m : ℕ) (h : m ≤ n + 1), spineToSimplex m ⋯ ∘ X.spine m h = id)
  (spineToSimplex_1 :
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
        X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h }))
  (spine_spineToSimplex_1 : ∀ (m : ℕ) (h : m ≤ n + 1), X.spine m h ∘ spineToSimplex_1 m ⋯ = id)
  (spineToSimplex_spine_1 : ∀ (m : ℕ) (h : m ≤ n + 1), spineToSimplex_1 m ⋯ ∘ X.spine m h = id),
  ({ spineToSimplex := spineToSimplex, spine_spineToSimplex := spine_spineToSimplex,
        spineToSimplex_spine := spineToSimplex_spine } =
      { spineToSimplex := spineToSimplex_1, spine_spineToSimplex := spine_spineToSimplex_1,
        spineToSimplex_spine := spineToSimplex_spine_1 }) =
    (spineToSimplex = spineToSimplex_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙ_nnreal_subset : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : Module ℝ A] [inst_3 : IsScalarTower ℝ A A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : TopologicalSpace A] [inst_6 : IsTopologicalRing A] [T2Space A]
  [inst_8 : PartialOrder A] [inst_9 : NonnegSpectrumClass ℝ A] [inst_10 : StarOrderedRing A] [inst_11 : StarModule ℝ A]
  [inst_12 : ContinuousStar A] [inst_13 : ContinuousConstSMul ℝ A]
  [inst_14 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (0 ≤ a) range_cfcₙ_nnreal_subset._auto_1 →
    (Set.range fun x => cfcₙ x a) ⊆ {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}
-- Batteries.Data.PairingHeap
/-- `O(1)`. Make a new empty pairing heap.  -/
Batteries.mkPairingHeap : (α : Type u) → (le : α → α → Bool) → Batteries.PairingHeap α le
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_sub_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ ν : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → ν.Integrable f → ∫ᵛ (x : X), f x ∂[B; μ - ν] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[B; ν]
-- Mathlib.RingTheory.Polynomial.Basic
/-- The span of every finite set of polynomials is contained in a `degreeLT n` for some `n`.  -/
Polynomial.span_of_finite_le_degreeLT : ∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)},
  s.Finite → ∃ n, Submodule.span R s ≤ Polynomial.degreeLT R n
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The restriction of `lift` to the source and base set of `T`, as a bundled continuous map.  -/
Bundle.Trivialization.liftCM : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] → (T : Bundle.Trivialization F proj) → C(↑T.source × ↑T.baseSet, ↑T.source)