mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.mk.sizeOf_spec : ∀ {X : SSet} {n : ℕ}
  (concat :
    (x : X.obj (Opposite.op { len := 1 })) →
      (s : X.obj (Opposite.op { len := n })) →
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
            (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s →
          X.obj (Opposite.op { len := n + 1 }))
  (map_mkOfSucc_zero_concat :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) (concat x s h) = x)
  (δ₀_concat :
    ∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
      (h :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) (concat x s h) = s)
  (injective :
    ∀ {x y : X.obj (Opposite.op { len := n + 1 })},
      (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) x =
          (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) y →
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) y →
          x = y),
  sizeOf
      { concat := concat, map_mkOfSucc_zero_concat := map_mkOfSucc_zero_concat, δ₀_concat := δ₀_concat,
        injective := injective } =
    1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instAddCommMonoid : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → AddCommMonoid (Derivation R A M)
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.ge_lower0 : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i],
  (i.lo? == some 0) = true → ∀ (a : α), -1 * ↑a ≤ 0
-- Mathlib.GroupTheory.OrderOfElement
Units.isOfFinOrder_val : ∀ {G : Type u_1} [inst : Monoid G] {u : Gˣ}, IsOfFinOrder ↑u ↔ IsOfFinOrder u
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
CategoryTheory.Nerve.isStrictSegal : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.nerve C).IsStrictSegal
-- Mathlib.Analysis.Analytic.Composition
Composition.sigmaCompositionAux.eq_1 : ∀ {n : ℕ} (a : Composition n) (b : Composition a.length) (i : Fin (a.gather b).length),
  a.sigmaCompositionAux b i = { blocks := (a.blocks.splitWrtComposition b)[↑i], blocks_pos := ⋯, blocks_sum := ⋯ }
-- Mathlib.CategoryTheory.Monad.Products
/-- The forward direction of the equivalence from algebras for the coproduct monad to the under
category.
 -/
CategoryTheory.algebraToUnder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        CategoryTheory.Functor (CategoryTheory.coprodMonad X).Algebra (CategoryTheory.Under X)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeAdjunction_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (G : PresheafOfModules R),
  (PresheafOfModules.freeAdjunction R).homEquiv F G = PresheafOfModules.freeHomEquiv
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.toProd_add : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s t : NonemptyInterval α), (s + t).toProd = s.toProd + t.toProd
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.mk.injEq : ∀ {α : Type} (root root_1 : Lean.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α)),
  ({ root := root } = { root := root_1 }) = (root = root_1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insert_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).size ≤ t.size + 1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.one_lt_of_isSuccLimit : ∀ {o : Ordinal.{u_4}}, Order.IsSuccLimit o → 1 < o
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The (noncomputable) `ωSup` definition for the `ω`-CPO structure on `Part α`.  -/
Part.ωSup : {α : Type u_2} → OmegaCompletePartialOrder.Chain (Part α) → Part α
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens : ∀ {R : Type u} [inst : CommRing R] (e : { e // IsIdempotentElem e }),
  (PrimeSpectrum.isIdempotentElemEquivClopens e).toOpens = PrimeSpectrum.basicOpen ↑e
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.trans : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b c p : M}, a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p]
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_sub_inv_eq_inv : ∀ {p q r : NNReal}, p.HolderTriple q r → r⁻¹ - q⁻¹ = p⁻¹
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
smul_finsum_mem : ∀ {M : Type u_1} {N : Type u_2} {γ : Type u_3} [inst : AddCommMonoid N] [inst_1 : DistribSMul M N] {r : M} {f : γ → N}
  {s : Set γ}, s.Finite → r • ∑ᶠ (x : γ) (_ : x ∈ s), f x = ∑ᶠ (x : γ) (_ : x ∈ s), r • f x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function `f : P.RankFunction ι` for a proper pairing `P`
of a subcomplex of a simplicial set, this is the induced morphism
`f.sigmaHorn j ⟶ f.filtration j` for any `j : ι`.  -/
SSet.Subcomplex.Pairing.RankFunction.t : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) → [inst_1 : P.IsProper] → (j : ι) → f.sigmaHorn j ⟶ (f.filtration j).toSSet
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.evalFinsetIccNat.match_1.eq_1 : ∀ (en em' : Q(ℕ)) (motive : (s : Q(Finset ℕ)) × Q(Finset.Icc «$em'» «$en» = «$s») → Sort u_1) (s : Q(Finset ℕ))
  (hs : Q(Finset.Icc «$em'» «$en» = «$s»))
  (h_1 : (s : Q(Finset ℕ)) → (hs : Q(Finset.Icc «$em'» «$en» = «$s»)) → motive ⟨s, hs⟩),
  (match ⟨s, hs⟩ with
    | ⟨s, hs⟩ => h_1 s hs) =
    h_1 s hs
-- Init.Data.List.Perm
List.Perm.countP_eq : ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Perm l₂ → List.countP p l₁ = List.countP p l₂
-- Std.Data.TreeMap.Basic
/-- Folds the given function over the mappings in the map in descending order.  -/
Std.TreeMap.foldr : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → {δ : Type w} → (α → β → δ → δ) → δ → Std.TreeMap α β cmp → δ
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toImage_app_hom_apply_coe : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) (U : SimplexCategoryᵒᵖ) (x : A.toSSet.obj U),
  ↑((CategoryTheory.ConcreteCategory.hom ((A.toImage f).app U)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom fun x => ↑x) (f.app U))) x
-- Mathlib.RingTheory.LocalRing.Length
/-- If `B/A` is a flat extension of local rings, and if `M` is an `A`-module, then
`ℓ_B(B ⊗[A] M) = ℓ_A(M) * ℓ_B(B ⧸ m_A)`.  -/
IsLocalRing.length_baseChange : ∀ (A : Type u_1) (B : Type u_2) (M : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsLocalRing A]
  [IsLocalRing B] [inst_4 : Algebra A B] [IsLocalHom (algebraMap A B)] [inst_6 : AddCommGroup M] [inst_7 : Module A M]
  [Module.Flat A B],
  Module.length B (TensorProduct A B M) =
    Module.length A M * Module.length B (B ⧸ Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A))
-- Mathlib.Analysis.BoxIntegral.Basic
/-- A function is integrable if there exists a vector that satisfies the `HasIntegral`
predicate.  -/
BoxIntegral.Integrable : {ι : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [Fintype ι] →
                BoxIntegral.Box ι →
                  BoxIntegral.IntegrationParams → ((ι → ℝ) → E) → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤ → Prop
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Separation.Basic
continuousWithinAt_update_of_ne : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] [inst_2 : DecidableEq X]
  [inst_3 : TopologicalSpace Y] {f : X → Y} {s : Set X} {x x' : X} {y : Y},
  x' ≠ x → (ContinuousWithinAt (Function.update f x y) s x' ↔ ContinuousWithinAt f s x')
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `SeminormedCommGroup` structure from a `GroupSeminormClass` on a `CommGroup`.  -/
GroupSeminormClass.toSeminormedCommGroup : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α ℝ] → [inst_1 : CommGroup α] → [GroupSeminormClass F α ℝ] → F → SeminormedCommGroup α
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelOpOp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.kernelOpOp f).hom =
    (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯).op
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiable.comp : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {g : M' → M''}, MDiff g → MDiff f → MDiff (g ∘ f)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.MutualMeasure.func.inj : ∀ {a a_1 : ℕ}, Lean.Elab.WF.GuessLex.MutualMeasure.func a = Lean.Elab.WF.GuessLex.MutualMeasure.func a_1 → a = a_1
-- Mathlib.Algebra.Star.Free
/-- Note that `star_one` is already a global simp lemma, but this one works with dsimp too  -/
FreeMonoid.star_one : ∀ {α : Type u_1}, star 1 = 1
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.disjoint_path_image_Ioc : ∀ {x y : Circle}, x ≠ y → Disjoint (⇑(x.path y) '' Set.Ioc 0 1) (⇑(y.path x) '' Set.Ioc 0 1)
-- Mathlib.Data.List.Cycle
Cycle.coe_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), (↑l).toFinset = l.toFinset
-- Mathlib.Data.Part
/-- `Part α` is the type of "partial values" of type `α`. It
is similar to `Option α` except the domain condition can be an
arbitrary proposition, not necessarily decidable.  -/
Part : Type u → Type u
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A `C^n` local diffeomorphism at `x` is `C^n` differentiable at `x`.  -/
IsLocalDiffeomorphAt.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  IsLocalDiffeomorphAt I J n f x → ContMDiffAt I J n f x
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_mul : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), toBoolAlg (a * b) = toBoolAlg a ⊓ toBoolAlg b
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.constantCoeff_inv : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k),
  MvPowerSeries.constantCoeff φ⁻¹ = (MvPowerSeries.constantCoeff φ)⁻¹
-- Mathlib.Data.Fin.Basic
Fin.coe_int_sub_eq_ite : ∀ {n : ℕ} (u v : Fin n), ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n
-- Mathlib.Data.FunLike.Basic
DFunLike.mk : {F : Sort u_1} →
  {α : outParam (Sort u_2)} →
    {β : outParam (α → Sort u_3)} → (coe : F → (a : α) → β a) → Function.Injective coe → DFunLike F α β
-- Mathlib.RingTheory.HopfAlgebra.Convolution
/-- The antipode of a commutative Hopf algebra as an anti-algebra hom.  -/
HopfAlgebra.antipodeAlgHomOp : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : HopfAlgebra R A] → A →ₐ[R] Aᵐᵒᵖ
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.composableArrows₃Functor_obj : ∀ (C : Type u_1) {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (i j : ι) [inst_2 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c),
  (HomologicalComplex.HomologySequence.composableArrows₃Functor C i j).obj K =
    HomologicalComplex.HomologySequence.composableArrows₃ K i j
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.submoduleMap_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M), Function.Surjective ⇑(f.submoduleMap p)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.update_eq_erase_add_single : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type u_1} [inst_1 : (i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i)
  (i : ι) (b : β i), f.update i b = DFinsupp.erase i f + fun₀ | i => b
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_integral_norm_bounded : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : ℝ),
      (∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) →
        (∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I) → MeasureTheory.Integrable f μ
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_fun_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 d s x →
      derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Length of a row of a Young diagram  -/
YoungDiagram.rowLen : YoungDiagram → ℕ → ℕ
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_ofNat : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NatCast R] (n : ℕ) [inst_2 : n.AtLeastTwo],
  SeparationQuotient.mk (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.corepresentableBy_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) {Y : D},
  (adj.corepresentableBy X).homEquiv = adj.homEquiv X Y
-- Mathlib.Analysis.Complex.Basic
/-- **Alias** of `Complex.uniformContinuous_im`. -/
Complex.uniformlyContinuous_im : UniformContinuous Complex.im
-- Mathlib.Control.Monad.Writer
MonadWriterAdapter.mk : {ω : outParam (Type u)} → {m : Type u → Type v} → ({α : Type u} → (ω → ω) → m α → m α) → MonadWriterAdapter ω m
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan.eq_1 : ∀ {𝕜 : 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] {n : ℕ}
  (s : Affine.Simplex 𝕜 P n),
  s.orthogonalProjectionSpan = EuclideanGeometry.orthogonalProjection (affineSpan 𝕜 (Set.range s.points))
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_injective : ∀ {α : Type u}, Function.Injective FreeAddGroup.negRev
-- Mathlib.Order.Defs.LinearOrder
/-- Default definition of `min`.  -/
minDefault : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → α → α
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.fieldRange_comp_val : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_6}
  [inst_3 : Field K] [inst_4 : Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K),
  (f.comp L.val).fieldRange = IntermediateField.map f L
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableConstVAdd.measurable_const_vadd : ∀ {M : Type u_2} {α : Type u_3} {inst : VAdd M α} {inst_1 : MeasurableSpace α} [self : MeasurableConstVAdd M α] (c : M),
  Measurable fun x => c +ᵥ x
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piUnique.eq_1 : ∀ {ι : Type u_16} (M : ι → Type u_17) [inst : (j : ι) → Mul (M j)] [inst_1 : Unique ι],
  MulEquiv.piUnique M = { toEquiv := Equiv.piUnique M, map_mul' := ⋯ }
-- Mathlib.Topology.ClusterPt
/-- **Alias** of `isClosed_setOfPred_clusterPt`.

---

The set of cluster points of a filter is closed. In particular, the set of limit points
of a sequence is closed.  -/
isClosed_setOf_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {f : Filter X}, IsClosed {x | ClusterPt x f}
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι_map_tensorHom_eq : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D]
  [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  {d₁ d₁' d₂ d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
  (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f f') =
    CategoryTheory.MonoidalCategory.DayConvolution.map
      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f)
      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f')
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α},
  Array.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Const.toArray t) = none ↔ k ∉ t
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- For any measure `ξ` dominating `μ` and `ν`, the Radon-Nikodym derivative of `μ` with respect to
`ν` is `ν`-almost everywhere equal to the ratio of the Radon-Nikodym derivatives of `μ` and `ν` with
respect to `ξ`.  -/
MeasureTheory.Measure.rnDeriv_eq_div : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ξ],
  μ.AbsolutelyContinuous ξ → ν.AbsolutelyContinuous ξ → μ.rnDeriv ν =ᵐ[ν] fun x => μ.rnDeriv ξ x / ν.rnDeriv ξ x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.insert : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → σ → β → σ
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- The identity partial equivalence on a set `s`  -/
OpenPartialHomeomorph.ofSet : {X : Type u_1} → [inst : TopologicalSpace X] → (s : Set X) → IsOpen s → OpenPartialHomeomorph X X
-- Aesop.Forward.State
/-- Metavariables for level parameters appearing in the rule's premises.  -/
Aesop.ClusterState.AddM.Context.premiseLMVars : Aesop.ClusterState.AddM.Context → Array Lean.LMVarId
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.instContinuousMul : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α],
  ContinuousMul (UniformSpace.Completion α)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenterWeights_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∀ (i : Fin (n + 1)), s.excenterWeights signs i ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coconeOfDiagramInitial_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C)
  [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] (x : J),
  (CategoryTheory.Limits.coconeOfDiagramInitial hX F).ι.app x = CategoryTheory.inv (F.map (hX.to x))
-- Mathlib.Data.Fintype.Order
Finite.map_iInf_of_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β},
  AntitoneOn g s → (∀ (i : ι), f i ∈ s) → g (⨅ i, f i) = ⨆ i, g (f i)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.sublist_getBasis : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {ex : Tactic.ComputeAsymptotics.BasisExtension basis},
  List.Sublist basis ex.getBasis
-- Mathlib.Data.Set.Basic
Set.subset_union_left : ∀ {α : Type u} {s t : Set α}, s ⊆ s ∪ t
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsFiltered.filteredClosure f a → Prop} {a : C}
  (t : CategoryTheory.IsFiltered.filteredClosure f a),
  (∀ (a : C) (t : CategoryTheory.IsFiltered.filteredClosure f a),
      CategoryTheory.IsFiltered.filteredClosure.below t → motive a t) →
    motive a t