mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_smul : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedSpace ℝ E] [inst_2 : DistribSMul 𝕜 E] [SMulCommClass ℝ 𝕜 E] (c : 𝕜)
  {f : MeasureTheory.SimpleFunc α E},
  MeasureTheory.Integrable (⇑f) μ →
    MeasureTheory.SimpleFunc.integral μ (c • f) = c • MeasureTheory.SimpleFunc.integral μ f
-- Mathlib.Topology.Algebra.UniformConvergence
instAddGroupUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : AddGroup β],
  instAddGroupUniformOnFun =
    { toAddMonoid := instAddMonoidUniformOnFun, toNeg := instNegUniformOnFun, toSub := instSubUniformOnFun,
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯ }
-- Mathlib.Order.Partition.Finpartition
/-- Transfer a finpartition over an order isomorphism.  -/
Finpartition.map : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      {β : Type u_2} →
        [inst_2 : Lattice β] → [inst_3 : OrderBot β] → {a : α} → (e : α ≃o β) → Finpartition a → Finpartition (e a)
-- Mathlib.Combinatorics.Graph.Basic
Graph.not_isLink_of_notMem_edgeSet : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, e ∉ G.edgeSet → ¬G.IsLink e x y
-- Mathlib.RingTheory.Ideal.IsPrimary
/-- **Alias** of `Ideal.isPrimary_finsetInf`. -/
Ideal.isPrimary_finset_inf : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → Ideal R} {i : ι},
  i ∈ s →
    (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
-- Mathlib.Topology.Homotopy.Equiv
/-- A homotopy equivalence between topological spaces `X` and `Y` are a pair of functions
`toFun : C(X, Y)` and `invFun : C(Y, X)` such that `toFun.comp invFun` and `invFun.comp toFun`
are both homotopic to corresponding identity maps.
 -/
ContinuousMap.HomotopyEquiv : (X : Type u) → (Y : Type v) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u v)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.Context : Type
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.of'_mul_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (a : G)
  (x : AddMonoidAlgebra k G), (AddMonoidAlgebra.of' k G a * x).divOf a = x
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Global sections of sheaves are naturally isomorphic to the limits of the underlying presheaves.
Note that while `HasLimitsOfShape Cᵒᵖ A` is needed here to talk about `lim` as a functor, global
sections are still limits without it - see `Sheaf.isLimitConeΓ`.  -/
CategoryTheory.Sheaf.ΓNatIsoLim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Cᵒᵖ A] →
              CategoryTheory.Sheaf.Γ J A ≅ (CategoryTheory.sheafToPresheaf J A).comp CategoryTheory.Limits.lim
-- Init.Data.SInt.Lemmas
ISize.add_assoc : ∀ (a b c : ISize), a + b + c = a + (b + c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey?_modify_eq_minKey? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey? = t.minKey?
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.eval_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Polynomial R)
  (q : PolynomialModule R M) (r : R),
  (PolynomialModule.eval r) (p • q) = Polynomial.eval r p • (PolynomialModule.eval r) q
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedTZif : Inhabited Std.Time.TimeZone.TZif.TZif
-- Lean.Elab.PreDefinition.Basic
/-- Collects all the level parameters in sorted order from the types and values of each predefinition.
Throws an "unused universe parameter" error if there is an unused `.{...}` parameter.

See `Lean.collectLevelParams`.
 -/
_private.Lean.Elab.PreDefinition.Basic.0.Lean.Elab.getLevelParamsPreDecls : Array Lean.Elab.PreDefinition → List Lean.Name → List Lean.Name → Lean.Elab.TermElabM (List Lean.Name)
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.θ_natDegree_le : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.θ✝ E).natDegree ≤ RatFunc.Luroth.m✝ E
-- Init.Data.Nat.Basic
Nat.pos_of_neZero : ∀ (n : ℕ) [NeZero n], 0 < n
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Lean.Compiler.LCNF.Types
/-- `isClass? type` return `some ClsName` if the LCNF `type` is an instance of the class `ClsName`.
 -/
Lean.Compiler.LCNF.isClass? : Lean.Expr → Lean.CoreM (Option Lean.Name)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Scalar multiplication is smooth (as a function of the vector variable).  -/
contDiff_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [inst_3 : DistribSMul R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F] (c : R), ContDiff 𝕜 n fun p => c • p
-- Lean.Data.RArray
Lean.RArray.toExpr : {α : Type u_1} → Lean.Expr → (α → Lean.Expr) → Lean.RArray α → Lean.MetaM Lean.Expr
-- Std.Sync.Mutex
Std.Mutex.mutex : {α : Type} → Std.Mutex α → Std.BaseMutex
-- Init.Data.Vector.Basic
/-- Insert an element into a vector using a `Nat` index and a tactic provided proof.  -/
Vector.insertIdx : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → α → autoParam (i ≤ n) Vector.insertIdx._auto_1 → Vector α (n + 1)
-- Mathlib.Algebra.Opposites
MulOpposite.op_ne_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : α), MulOpposite.op a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
two_nsmul_inf_eq_add_sub_abs_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), 2 • (a ⊓ b) = a + b - |b - a|
-- Batteries.Data.List.Lemmas
List.isSome_isPrefixOf?_eq_isPrefixOf : ∀ {α : Type u_1} [inst : BEq α] (xs ys : List α), (xs.isPrefixOf? ys).isSome = xs.isPrefixOf ys
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentEdit.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier) (edits : Lean.Lsp.TextEditBatch),
  sizeOf { textDocument := textDocument, edits := edits } = 1 + sizeOf textDocument + sizeOf edits
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.Composition.recOnSingleAppend.match_3.eq_1 : ∀ (motive : (n : ℕ) → Composition n → Sort u_1) (blocks : List ℕ) (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i)
  (h_1 :
    (blocks : List ℕ) →
      (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) →
        motive blocks.sum { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := ⋯ }),
  (match blocks.sum, { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := ⋯ } with
    | .(blocks.sum), { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := ⋯ } => h_1 blocks blocks_pos) =
    h_1 blocks blocks_pos
-- Mathlib.Dynamics.Transitive
MulAction.isTopologicallyTransitive_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α],
  MulAction.IsTopologicallyTransitive M α ↔
    ∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, (m • U ∩ V).Nonempty
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Given a point on a sphere and a point not outside it, the inner product between the
difference of those points and the radius vector is positive unless the points are equal.  -/
EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → dist p₂ s.center ≤ s.radius → 0 < inner ℝ (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) ∨ p₁ = p₂
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.exponentialPDF_of_nonneg : ∀ {r x : ℝ}, 0 ≤ x → ProbabilityTheory.exponentialPDF r x = ENNReal.ofReal (r * Real.exp (-(r * x)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?!_snd : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β},
      (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! t k v).2 = Std.DTreeMap.Internal.Impl.insertIfNew! k v t
-- Mathlib.Lean.Linter
/-- Processes `set_option ... in`s that wrap the input `stx`, then acts on the inner syntax with
`x` after checking that the provided linter option is `true`.

If `breakOnError` is `true` (the default), avoids running the linter when errors are present.

This is typically used to start off linter code:
```
def myLinter : Linter where
  run := whenLinterActivated linter.myLinter fun stx ↦ do
    ...
```

Note: this definition is marked as `@[macro_inline]`, so it is okay to supply it with a linter
option which has been registered in the same module.
 -/
Lean.Linter.whenLinterActivated : Lean.Option Bool → Lean.Elab.Command.CommandElab → optParam Bool true → Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E},
  HasFPowerSeriesAt f p x → HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- `SL(2, ℤ)` is generated by `S` and `T`.  -/
SpecialLinearGroup.SL2Z_generators : Subgroup.closure {ModularGroup.S, ModularGroup.T} = ⊤
-- Init.Data.SInt.Lemmas
Int64.toUInt64_neg : ∀ (a : Int64), (-a).toUInt64 = -a.toUInt64
-- Mathlib.Data.Finset.Insert
Finset.cons.congr_simp : ∀ {α : Type u_1} (a a_1 : α) (e_a : a = a_1) (s s_1 : Finset α) (e_s : s = s_1) (h : a ∉ s),
  Finset.cons a s h = Finset.cons a_1 s_1 ⋯
-- Mathlib.Data.Fintype.Card
Fintype.card_lt_of_injective_of_notMem : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Injective f → ∀ {b : β}, b ∉ Set.range f → Fintype.card α < Fintype.card β
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.tprod_subtype_mul_tprod_subtype_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] [CompleteSpace α]
  [T2Space α] {f : β → α}, Multipliable f → ∀ (s : Set β), (∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.comp_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7}
  [inst_9 : AddCommGroup W₂] [inst_10 : Module R W₂] [inst_11 : TopologicalSpace Q₂] [inst_12 : AddTorsor W₂ Q₂]
  [inst_13 : TopologicalSpace V] [inst_14 : IsTopologicalAddTorsor P] [inst_15 : TopologicalSpace W]
  [inst_16 : IsTopologicalAddTorsor Q] [inst_17 : TopologicalSpace W₂] [inst_18 : IsTopologicalAddTorsor Q₂]
  (f : P →ᴬ[R] Q) (g : Q →ᴬ[R] Q₂), (g.comp f).contLinear = g.contLinear ∘SL f.contLinear
-- Std.Do.PredTrans
/-- The predicate transformer that always returns the same precondition `P`; `(const P).apply Q = P`.
 -/
Std.Do.PredTrans.const : {ps : Std.Do.PostShape} → {α : Type u} → Std.Do.Assertion ps → Std.Do.PredTrans ps α
-- Mathlib.Data.Nat.Choose.Multinomial
Sym.countPerms_coe_fill_of_notMem : ∀ {n : ℕ} {α : Type u_1} [inst : DecidableEq α] {m : Fin (n + 1)} {s : Sym α (n - ↑m)} {x : α},
  x ∉ s → (↑(Sym.fill x m s)).countPerms = n.choose ↑m * (↑s).countPerms
-- Init.Data.SInt.Bitwise
Int64.shiftLeft_zero : ∀ {a : Int64}, a <<< 0 = a
-- Init.Data.Iterators.Basic
Std.IterM.toIter_mk : ∀ {α β : Type u_1} {it : α}, { internalState := it }.toIter = { internalState := it }
-- Mathlib.Topology.Order
/-- The Galois coinsertion between `TopologicalSpace α` and `(Set (Set α))ᵒᵈ` whose lower part sends
a topology to its collection of open subsets, and whose upper part sends a collection of subsets
of `α` to the topology they generate.  -/
TopologicalSpace.gciGenerateFrom : (α : Type u_1) →
  GaloisCoinsertion (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_finite : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Finite M],
  IsArtinian R M
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRocSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRocSlice._auto_1) →
    Std.Roc.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RocSlice α)
-- Init.Data.Vector.FinRange
Vector.finRange_zero : Vector.finRange 0 = #v[]
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n),
  CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h =
    CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.exists_mk'_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S), ∃ x y, IsLocalization.mk' S x y = z
-- Lean.Elab.Level
Lean.Elab.Level.Context.mk : Lean.Options → Lean.Syntax → Bool → Lean.Elab.Level.Context
-- Batteries.Data.List.Lemmas
/-- List.prod satisfies a specification of cartesian product on lists.  -/
List.pair_mem_product : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {x : α} {y : β}, (x, y) ∈ xs.product ys ↔ x ∈ xs ∧ y ∈ ys
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.pushInstPending : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Unit
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.mk_mem_ramifiedPlacesOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {φ : L →+* ℂ},
  φ ∈ NumberField.ComplexEmbedding.mixedEmbeddingsOver L v.embedding →
    NumberField.InfinitePlace.mk φ ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v
-- Mathlib.Tactic.Push
/-- Elaborator for the argument passed to `push`. It accepts a constant, or a function  -/
Mathlib.Tactic.Push.elabHead : Lean.Term → Lean.Elab.TermElabM Mathlib.Tactic.Push.Head
-- Batteries.Data.Char.AsciiCasing
Char.toUpper_toUpper_eq_toUpper : ∀ (c : Char), c.toUpper.toUpper = c.toUpper
-- Mathlib.RingTheory.PolynomialAlgebra
/-- If `A` is an `R`-algebra, then `A[X]` is an `R[X]` algebra.
This gives a diamond for `Algebra R[X] R[X][X]`, so this is not a global instance.  -/
Polynomial.algebra : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra (Polynomial R) (Polynomial A)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.trans.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {L : Type u_3} [inst_4 : Mul L] [inst_5 : TopologicalSpace L] (cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L),
  cme1.trans cme2 = { toMulEquiv := cme1.trans cme2.toMulEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).obj Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.obj X).map g)) f =
    CategoryTheory.shrinkYonedaObjObjEquiv.symm
      (CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.shrinkYonedaObjObjEquiv f))
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.covering.congr_simp : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v v_1 : VitaliFamily μ} (e_v : v = v_1) {f f_1 : X → Set (Set X)} (e_f : f = f_1) {s s_1 : Set X} (e_s : s = s_1)
  (_h : v.FineSubfamilyOn f s) (a a_1 : X × Set X),
  a = a_1 → ∀ (a_2 a_3 : X), a_2 = a_3 → _h.covering a a_2 = ⋯.covering a_1 a_3
-- Init.Data.Range.Polymorphic.PRange
/-- The lower bound of the range. `lower` is not included in the range.
   -/
Std.Roc.lower : {α : Type u} → Std.Roc α → α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.liesOver_embedding_of_mem_ramifiedPlacesOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
  w ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v → NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding
-- Std.Data.DTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.toList : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → List ((a : α) × β a)
-- Init.Data.List.Lemmas
List.filterMap_flatten : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {L : List (List α)},
  List.filterMap f L.flatten = (List.map (List.filterMap f) L).flatten
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.instEquivLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β],
  OrderMonoidIso.instEquivLike =
    { coe := fun f => f.toFun, inv := fun f => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
-- Mathlib.Topology.Ultrafilter
isOpen_iff_ultrafilter : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ nhds x → s ∈ l
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos : ∀ {x y : ℝ*}, ¬x.Infinitesimal → 0 < x → y.InfinitePos → (x * y).InfinitePos
-- Init.Grind.ToInt
Lean.Grind.IntInterval.isFinite.eq_4 : Lean.Grind.IntInterval.ii.isFinite = false
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorph.preimage_boundary : ∀ {𝕜 : 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'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ {f : M → N}, IsLocalDiffeomorph I I' n f → f ⁻¹' ModelWithCorners.boundary N = ModelWithCorners.boundary M
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mono_map : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀' i₀ i₁ i₂ i₃ : ι}
  (f₁ : i₀ ⟶ i₁) (f₁' : i₀' ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂ f₃) (n₀ n₁ n₂ n₃ : ℤ),
  autoParam (α.app 1 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 1))
      CategoryTheory.Abelian.SpectralObject.mono_map._auto_1 →
    autoParam (α.app 2 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 2))
        CategoryTheory.Abelian.SpectralObject.mono_map._auto_3 →
      autoParam (α.app 3 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 3))
          CategoryTheory.Abelian.SpectralObject.mono_map._auto_5 →
        ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mono_map._auto_7)
          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mono_map._auto_9),
          autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.mono_map._auto_11 →
            CategoryTheory.Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.next?.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Stream α → Sort u_2) →
    (x : RBTree.RBNode.Stream α) →
      (Unit → motive RBTree.RBNode.Stream.nil) →
        ((v : α) →
            (r : RBTree.RBNode α) → (tail : RBTree.RBNode.Stream α) → motive (RBTree.RBNode.Stream.cons v r tail)) →
          motive x
-- Mathlib.Analysis.Fourier.AddCircle
/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series converges
uniformly to `f`.  -/
hasSum_fourier_series_of_summable : ∀ {T : ℝ} [hT : Fact (0 < T)] {f : C(AddCircle T, ℂ)},
  Summable (fourierCoeff ⇑f) → HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate' : ∀ {K : Type u_3} {V : Type u_8} [inst : Field K] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] (Q : QuadraticForm K V),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q) →
    ∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul : Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.card_cycleType_pos : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, 0 < σ.cycleType.card ↔ σ ≠ 1
-- Lean.Meta.Offset
_private.Lean.Meta.Offset.0.Lean.Meta.isNatZero : Lean.Expr → Lean.MetaM Bool
-- Std.Sync.Channel
/-- Try to receive a value from the channel, if this can be completed right away without blocking return
`some value`, otherwise return `none`.
 -/
Std.CloseableChannel.tryRecv : {α : Type} → Std.CloseableChannel α → BaseIO (Option α)
-- Mathlib.Data.Finset.Image
/-- **Alias** of the forward direction of `Finset.image_nonempty`. -/
Finset.Nonempty.of_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
  (Finset.image f s).Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.surjective_up_to_refinements_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Epi f] {A : C} (y : A ⟶ Y),
  ∃ A' π,
    ∃ (_ : CategoryTheory.Epi π), ∃ x, CategoryTheory.CategoryStruct.comp π y = CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Every graph homomorphism from a complete graph is injective.  -/
SimpleGraph.Hom.injective_of_top_hom : ∀ {V : Type u_1} {W : Type u_2} {G' : SimpleGraph W} (f : ⊤ →g G'), Function.Injective ⇑f
-- Mathlib.Data.Sigma.Lex
Sigma.instIsTransLex : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrans ι r]
  [∀ (i : ι), IsTrans (α i) (s i)], IsTrans ((i : ι) × α i) (Sigma.Lex r s)