mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → Std.Internal.List.getKey? (Std.Internal.List.minKey! l) l = some (Std.Internal.List.minKey! l)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.noSibling_merge : ∀ {α : Type u_1} (le : α → α → Bool) (s₁ s₂ : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.merge le s₁ s₂).NoSibling
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.equivOfEquiv.congr_simp : ∀ {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field L]
  [inst_3 : Field M] [inst_4 : Algebra R M] [inst_5 : Module.IsTorsionFree R M] [inst_6 : IsAlgClosure R M]
  [inst_7 : Algebra S L] [inst_8 : Module.IsTorsionFree S L] [inst_9 : IsAlgClosure S L] [inst_10 : IsDomain R]
  [inst_11 : IsDomain S] (hSR hSR_1 : S ≃+* R),
  hSR = hSR_1 → IsAlgClosure.equivOfEquiv L M hSR = IsAlgClosure.equivOfEquiv L M hSR_1
-- Mathlib.Topology.NhdsWithin
mem_closure_ne_iff_frequently_within : ∀ {α : Type u_1} [inst : TopologicalSpace α] {z : α} {s : Set α},
  z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in nhdsWithin z {z}ᶜ, x ∈ s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_empty : ∀ {α : Type u}, FreeAddGroup.negRev [] = []
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.of_one : ∀ (α : Type u) [inst : One α], FreeAbelianGroup.of 1 = 1
-- Mathlib.Analysis.Normed.Module.FiniteDimension
LinearIsometry.toLinearIsometryEquiv_apply : ∀ {F : Type u_1} {E₁ : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedAddCommGroup E₁] {R₁ : Type u_3}
  [inst_2 : Field R₁] [inst_3 : Module R₁ E₁] [inst_4 : Module R₁ F] [inst_5 : FiniteDimensional R₁ E₁]
  [inst_6 : FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : Module.finrank R₁ E₁ = Module.finrank R₁ F) (x : E₁),
  (li.toLinearIsometryEquiv h) x = li x
-- Init.Data.List.Lemmas
/-- Variant of `getElem_append_right` useful for rewriting from the small list to the big list.  -/
List.getElem_append_right' : ∀ {α : Type u_1} (l₁ : List α) {l₂ : List α} {i : ℕ} (hi : i < l₂.length), l₂[i] = (l₁ ++ l₂)[i + l₁.length]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.count_support_takeUntil_eq_one : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
  List.count u (p.takeUntil u h).support = 1
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
MeasureTheory.FiniteMeasure.pi_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.FiniteMeasure (α i)) (s : (i : ι) → Set (α i)),
  (MeasureTheory.FiniteMeasure.pi μ) (Set.univ.pi s) = ∏ i, (μ i) (s i)
-- Mathlib.Algebra.Category.BialgCat.Basic
CategoryTheory.Iso.toBialgEquiv_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : BialgCat R} (e : X ≅ Y), e.symm.toBialgEquiv = e.toBialgEquiv.symm
-- Init.Data.List.Find
List.findIdx?_eq_none_iff_findIdx_eq : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.findIdx? p xs = none ↔ List.findIdx p xs = xs.length
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- Given submodules `pᵢ ⊆ Eᵢ`, this is the natural map: `⨂[𝕜] i, pᵢ → ⨂[𝕜] i, Eᵢ`.
This is the continuous version of `PiTensorProduct.mapIncl`.  -/
PiTensorProduct.mapLIncl : {ι : Type u_1} →
  [inst : Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              (p : (i : ι) → Submodule 𝕜 (E i)) →
                (PiTensorProduct 𝕜 fun i => ↥(p i)) →L[𝕜] PiTensorProduct 𝕜 fun i => E i
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.support_spanningCoe : ∀ {V : Type u_1} {s : Set V} (G : SimpleGraph ↑s), G.spanningCoe.support = Subtype.val '' G.support
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.coe_sInf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S : Set (IntermediateField F E)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.PostponeBehavior.yes.sizeOf_spec : sizeOf Lean.Elab.Term.PostponeBehavior.yes = 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.leftKanExtensionUnit F) G)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.leftKanExtension F) G).hom
        (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom)) =
    L.leftKanExtensionUnit (F.comp G)
-- Mathlib.Probability.UniformOn
ProbabilityTheory.isProbabilityMeasure_uniformOn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω},
  s.Finite → s.Nonempty → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn s)
-- Init.Data.SInt.Lemmas
Int64.ofInt_iSizeToInt : ∀ (x : ISize), Int64.ofInt x.toInt = x.toInt64
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
NumberField.RingOfIntegers.equiv.eq_1 : ∀ {K : Type u_1} [inst : Field K] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsIntegralClosure R ℤ K],
  NumberField.RingOfIntegers.equiv R = (IsIntegralClosure.equiv ℤ R K (NumberField.RingOfIntegers K)).symm.toRingEquiv
-- Mathlib.Algebra.Group.End
MulAutMultiplicative_apply_apply : ∀ (G : Type u_3) [inst : AddGroup G] (a : Multiplicative G ≃* Multiplicative G) (a_1 : G),
  ((MulAutMultiplicative G) a) a_1 = Multiplicative.toAdd (a (Multiplicative.ofAdd a_1))
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.freeGroupoidFunctor_comp : ∀ {V : Type u} [inst : Quiver V] {V' : Type u'} [inst_1 : Quiver V'] {V'' : Type u''} [inst_2 : Quiver V'']
  (φ : V ⥤q V') (φ' : V' ⥤q V''),
  Quiver.freeGroupoidFunctor (φ ⋙q φ') = (Quiver.freeGroupoidFunctor φ).comp (Quiver.freeGroupoidFunctor φ')
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_add_le_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R}, x.orderTop + y.orderTop ≤ (x * y).orderTop
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- `Real.cosh` as an `OpenPartialHomeomorph` from $(0, ∞)$ to $(1, ∞)$.  -/
Real.coshOpenPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
-- Mathlib.Topology.Algebra.Group.Defs
/-- A topological group is a group in which the multiplication and inversion operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformGroup` using
`IsTopologicalGroup.rightUniformSpace` and `isUniformGroup_of_commGroup`.  -/
IsTopologicalGroup : (G : Type u_4) → [TopologicalSpace G] → [Group G] → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β} {g : β → γ},
  MeasurableEmbedding g → MeasurableEmbedding f → MeasurableEmbedding (g ∘ f)
-- Lean.Elab.App
/-- Resolves `(.$id:ident)` using the expected type to infer the namespace for `id`.

To infer a namespace from the expected type, we do the following operations:
- put it into WHNF using `whnfCore`, while consuming annotations
- enter the bodies of pi types
- if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
  and if that doesn't work, try unfolding the expression and continuing.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveDottedIdentFn : Lean.Syntax →
  Lean.Name →
    List Lean.Level →
      Option Lean.Expr → Lean.Elab.TermElabM (List (Lean.Expr × Lean.Syntax × List Lean.Syntax × List Lean.Level))
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The set of vectors in the direction of a nonempty affine subspace is given by `vsub_set`.  -/
AffineSubspace.coe_direction_eq_vsub_set : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P}, (↑s).Nonempty → ↑s.direction = ↑s -ᵥ ↑s
-- Mathlib.Tactic.TFAE
/-- Accesses the propositions at indices `i` and `j` of `tfaeList`, and constructs the expression
`Pi <arr> Pj`, which will be the type of our `tfae_have` hypothesis  -/
Mathlib.Tactic.TFAE.elabTFAEType : List Q(Prop) → Lean.TSyntax `Mathlib.Tactic.TFAE.Parser.tfaeType → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Order.Completion
/-- The **Dedekind-MacNeille completion** of a partial order is the smallest complete lattice that
contains it. We define here the type of Dedekind cuts of `α` as the `Concept` lattice of the `≤`
relation of `α`.

For `A : DedekindCut α`, the sets `A.left` and `A.right` are related by
`upperBounds A.left = A.right` and `lowerBounds A.right = A.left`.

The theorem `DedekindCut.principalEmbedding_trans_factorEmbedding` proves that if `α` is a partial
order and `β` is a complete lattice, any embedding `α ↪o β` factors through `DedekindCut α`.  -/
DedekindCut : (α : Type u_1) → [Preorder α] → Type u_1
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_multiset_prod_of_monic : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)) [Nontrivial R],
  (∀ f ∈ t, f.Monic) → t.prod.degree = (Multiset.map Polynomial.degree t).sum
-- Mathlib.Order.Monotone.Basic
antitoneOn_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn (⇑OrderDual.toDual ∘ f) s ↔ MonotoneOn f s
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_mul_int : ∀ (x y : ℂ) (n : ℤ), x ^ (y * ↑n) = (x ^ y) ^ n
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- The flexible linter makes sure that "rigid" tactics do not follow "flexible" tactics.  -/
Mathlib.Linter.linter.flexible : Lean.Option Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.isShared.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_25),
  sizeOf (Lean.Compiler.LCNF.LetValue.isShared fvarId h) = 1 + sizeOf fvarId + sizeOf h
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.instIsSmallGeneratingMonomorphismsOfSmallSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : C) [Small.{w, max u v} (CategoryTheory.Subobject G)],
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥A) (x : ↥A)
  (i : ι), (algebraMap (↥B) S) (((H.basisOfBasisLeft H' b).repr ↑x) i) = (algebraMap R S) ((b.repr x) i)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  SaturatedSubmonoid.instPartialOrder = PartialOrder.ofSetLike (SaturatedSubmonoid M) M
-- Mathlib.Data.Finset.Insert
Finset.singleton_subset_singleton : ∀ {α : Type u_1} {a b : α}, {a} ⊆ {b} ↔ a = b
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_zero : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], F⟮0⟯ = ⊥
-- Mathlib.Algebra.Central.End
LinearEquiv.conjAlgEquiv_ext_iff' : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {S : Type u_4} {M₂ : Type u_5} [inst_4 : CommRing S] [IsCancelMulZero S] [inst_6 : Module S M]
  [inst_7 : SMulCommClass R S M] [inst_8 : Algebra S R] [inst_9 : IsScalarTower S R M] [inst_10 : AddCommGroup M₂]
  [inst_11 : Module R M₂] [inst_12 : Module S M₂] [inst_13 : SMulCommClass R S M₂] [inst_14 : IsScalarTower S R M₂]
  [Algebra.IsCentral S R] [Module.IsTorsionFree S M₂] (f g : M ≃ₗ[R] M₂),
  LinearEquiv.conjAlgEquiv S f = LinearEquiv.conjAlgEquiv S g ↔ ∃ α, f = α • g
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
measurableSet_lineDifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {v : E},
  Continuous f → MeasurableSet {x | LineDifferentiableAt 𝕜 f x v}
-- Mathlib.AlgebraicGeometry.Restrict
/-- The restriction of a morphism `X ⟶ Y` onto `X |_{f ⁻¹ U} ⟶ Y |_ U`.  -/
AlgebraicGeometry.morphismRestrict : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (U : Y.Opens) → ↑((TopologicalSpace.Opens.map f.base).obj U) ⟶ ↑U
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_pow : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℕ), Dilation.ratio (e ^ n) = Dilation.ratio e ^ n
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
UniqueFactorizationMonoid.moebius_of_not_squarefree : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  ¬Squarefree a → UniqueFactorizationMonoid.moebius a = 0
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.adj_counit_app : ∀ (A : Type u), CategoryTheory.Codiscrete.adj.counit.app A = TypeCat.ofHom (CategoryTheory.Codiscrete.counitApp A)
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_lt_of_lt_coe : ∀ {a : ENNReal} {p : NNReal}, a < ↑p → a.toNNReal < p
-- Mathlib.Algebra.Order.Monovary
antivaryOn_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn (-f) g s ↔ MonovaryOn f g s
-- Std.Data.TreeSet.Basic
Std.TreeSet.instMembership : {α : Type u} → {cmp : α → α → Ordering} → Membership α (Std.TreeSet α cmp)
-- Lean.Data.Lsp.Basic
Lean.Lsp.Location.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {range : Lean.Lsp.Range} {uri_1 : Lean.Lsp.DocumentUri} {range_1 : Lean.Lsp.Range},
  { uri := uri, range := range } = { uri := uri_1, range := range_1 } → uri = uri_1 ∧ range = range_1
-- Std.Sync.StreamMap
/-- Get all registered stream names
 -/
Std.StreamMap.keys : {α β : Type} → Std.StreamMap α β → Array α
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A map from the codomain of `f` to `Z`  -/
CategoryTheory.RegularMono.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.RegularMono f) → Y ⟶ self.Z
-- Init.Data.List.Basic
/-- Returns `true` if `p` returns `true` for every element of `l`.

`O(|l|)`. Short-circuits upon encountering the first `false`.

Examples:
* `[a, b, c].all p = (p a && (p b && p c))`
* `[2, 4, 6].all (· % 2 = 0) = true`
* `[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
List.all : {α : Type u} → List α → (α → Bool) → Bool
-- Init.Prelude
/-- A version of `HEq.refl` with an implicit argument.  -/
HEq.rfl : ∀ {α : Sort u} {a : α}, a ≍ a
-- Mathlib.Order.FixedPoints
fixedPoints.instSemilatticeSupElemFixedPointsCoeOrderHom : {α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → SemilatticeSup ↑(Function.fixedPoints ⇑f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.hasStrictDerivAt_sin : ∀ (x : ℝ), HasStrictDerivAt Real.sin (Real.cos x) x
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.IsCoskeletal.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SimplicialObject C} {n : ℕ},
  CategoryTheory.Functor.IsRightKanExtension X
      (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X)) →
    X.IsCoskeletal n
-- Mathlib.Order.Minimal
maximal_gt_iff : ∀ {α : Type u_2} {x y : α} [inst : Preorder α], Maximal (fun x => y < x) x ↔ y < x ∧ IsMax x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_sub_vadd_comm : ∀ {α : Type u_2} [inst : AddCommGroup α] (a : α) (s : Set α) (b : α) (t : Set α), (a +ᵥ s) - (b +ᵥ t) = (a - b) +ᵥ s - t
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.IsSeparable.exists_countable_measureDense : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [self : MeasureTheory.IsSeparable μ],
  ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.bot_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], ↑⊥ = ⊥
-- Mathlib.Analysis.Normed.Group.Continuity
controlled_sum_of_mem_closure_range : ∀ {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {j : E →+ F}
  {b : F},
  b ∈ closure ↑j.range →
    ∀ {f : ℕ → ℝ},
      (∀ (n : ℕ), 0 < f n) →
        ∃ a,
          Filter.Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧
            ‖-j (a 0) + b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.forget C = { obj := fun A => A.X, map := fun {X Y} f => f.hom, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.Oscillation
ContinuousAt.oscillation_eq_zero : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] {f : E → F} {x : E},
  ContinuousAt f x → oscillation f x = 0
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.map_smul : ∀ {M' : Type u_1} {X : Type u_5} [inst : SMul M' X] {Y : Type u_6} [inst_1 : SMul M' Y] (f : X →ₑ[id] Y) (m : M')
  (x : X), f (m • x) = m • f x
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instAddActionSubtypeMem.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : AddMonoid M']
  [inst_2 : AddSubmonoidClass S' M'] [inst_3 : AddAction M' α],
  AddSubmonoid.instAddActionSubtypeMem s =
    { toVAdd := AddSubmonoid.instVAddSubtypeMem s, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.sUnion_edgeSet_subset_vertexSet : ∀ {α : Type u_1} {H : Hypergraph α}, ⋃₀ H.edgeSet ⊆ H.vertexSet
-- Mathlib.Computability.Primrec.Basic
Primrec.pred : Primrec Nat.pred
-- Mathlib.Data.Finset.Fold
Finset.fold_empty : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
  {b : β}, Finset.fold op b f ∅ = b
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.eq.inj : ∀ {solverId : ℕ} {lhs rhs : Lean.Expr} {rest : Lean.Meta.Grind.PendingSolverPropagationsData✝} {solverId_1 : ℕ}
  {lhs_1 rhs_1 : Lean.Expr} {rest_1 : Lean.Meta.Grind.PendingSolverPropagationsData✝},
  Lean.Meta.Grind.PendingSolverPropagationsData.eq✝ solverId lhs rhs rest =
      Lean.Meta.Grind.PendingSolverPropagationsData.eq✝ solverId_1 lhs_1 rhs_1 rest_1 →
    solverId = solverId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1 ∧ rest = rest_1
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.instUniqueOfIsEmpty : {α : Sort u_1} → {β : Sort u_2} → [IsEmpty α] → Unique (α ↪ β)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.default_asIdeal : ∀ {K : Type u_1} [inst : Field K], default.asIdeal = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
_private.Mathlib.Combinatorics.SimpleGraph.Acyclic.0.SimpleGraph.Walk.length.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2)
  (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h q)),
  (match u, SimpleGraph.Walk.nil with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h q => h_2 v v_1 h q) =
    h_1 ()
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.cechNerveEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve),
  (CategoryTheory.SimplicialObject.cechNerveEquiv X F).symm G =
    CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.symm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (f₁ - f₂) =o[𝕜; l] g → (f₂ - f₁) =o[𝕜; l] g
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.ofDual_eq_top : ∀ (α : Type u) [inst : Top α] {a : αᵒᵈ}, OrderDual.ofDual a = ⊤ ↔ a = ⊥
-- Mathlib.MeasureTheory.SetAlgebra
/-- `generateSetAlgebra 𝒜` is the smallest algebra of sets containing `𝒜`.  -/
MeasureTheory.generateSetAlgebra : {α : Type u_2} → Set (Set α) → Set (Set α)
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.toPiLocalization_not_surjective_of_infinite : ∀ {ι : Type u_5} (R : ι → Type u_4) [inst : (i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] [Infinite ι],
  ¬Function.Surjective ⇑(PrimeSpectrum.toPiLocalization ((i : ι) → R i))
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mono : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
  ↑K₁ ⊆ ↑K₂ → μ K₁ ≤ μ K₂
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) [inst_4 : MulSemiringAction Gal(L/K) B] [IsGalois K L],
  IsDecompositionField K L P ↥(FixedPoints.intermediateField ↥(MulAction.stabilizer Gal(L/K) P))
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_coe : ∀ {α : Type u_3} [inst : Monoid α] (l : List α) (comm : {x | x ∈ ↑l}.Pairwise Commute), (↑l).noncommProd comm = l.prod
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.mkParamName : Lean.MetavarContext.LevelMVarToParam.M Lean.Name
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.instEpiFromTerminalIsTerminal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A : C) [inst_1 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Epi (CategoryTheory.Limits.terminalIsTerminal.from A)
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquivLast_symm_some : ∀ {n : ℕ} (i : Fin n), finSuccEquivLast.symm (some i) = i.castSucc
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instPartialOrder : {E : Type u_3} → [inst : AddGroup E] → PartialOrder (AddGroupNorm E)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_dvd : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S),
  p ∣ q → Polynomial.eval₂ f x p ∣ Polynomial.eval₂ f x q