mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωSup_bind : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type v} (c : OmegaCompletePartialOrder.Chain α)
  (f : α →o Part β) (g : α →o β → Part γ),
  OmegaCompletePartialOrder.ωSup (c.map (f.partBind g)) =
    OmegaCompletePartialOrder.ωSup (c.map f) >>= OmegaCompletePartialOrder.ωSup (c.map g)
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.isGreatest_u : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {a : α}, IsGreatest {b | l b ≤ a} (u a)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.addMonoidHom.eq_1 : @Pi.addMonoidHom = @AddMonoidHom.pi
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- If `A` is a non-unital `R`-algebra, the `R`-quasispectrum of `a : A` consists of those `r : R`
such that if `r` is invertible (in `R`), then `-(r⁻¹ • a)` is not quasiregular.

The quasispectrum is precisely the spectrum in the unitization when `R` is a commutative ring.
See `Unitization.quasispectrum_eq_spectrum_inr`.  -/
quasispectrum : (R : Type u_1) → {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : NonUnitalRing A] → [Module R A] → A → Set R
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.DTreeMap.Raw.containsThenInsert : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → (a : α) → β a → Bool × Std.DTreeMap.Raw α β cmp
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- A version of `tendsto_card_div_pow_atTop_volume` for a real variable.  -/
tendsto_card_div_pow_atTop_volume' : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Fintype ι],
  Bornology.IsBounded s →
    MeasurableSet s →
      MeasureTheory.volume (frontier s) = 0 →
        (∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) →
          Filter.Tendsto
            (fun x => ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι)
            Filter.atTop (nhds (MeasureTheory.volume.real s))
-- Mathlib.Logic.Equiv.Fin.Basic
/-- Equivalence between `Fin m × Fin n` and `Fin (m * n)`  -/
finProdFinEquiv : {m n : ℕ} → Fin m × Fin n ≃ Fin (m * n)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The range of a morphism of non-unital semirings is finite if the domain is finite.  -/
NonUnitalRingHom.finite_srange : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] [Finite R] (f : F),
  Finite ↥(NonUnitalRingHom.srange f)
-- Mathlib.Data.SetLike.Basic
instIsConcreteLE : ∀ (A : Type u_1) (B : Type u_2) [inst : SetLike A B], IsConcreteLE A B
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (szl : ℕ) (k' : α) (v' : β k') (l' r' l'' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    Std.DTreeMap.Internal.Impl.Tree α β ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
      Sort u_3)
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
  (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_eq_prod_even : ∀ (n : ℕ), (2 * n).doubleFactorial = ∏ i ∈ Finset.range n, 2 * (i + 1)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_eq_top_iff_finite : ∀ {α : Type u} [inst : Semiring α] (s : Set α), Ideal.span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ Ideal.span ↑s' = ⊤
-- Init.Data.Vector.Count
Vector.count_flatten : ∀ {α : Type u_1} [inst : BEq α] {m n : ℕ} {a : α} {xss : Vector (Vector α m) n},
  Vector.count a xss.flatten = (Vector.map (Vector.count a) xss).sum
-- Lean.Meta.Sym.Offset
_private.Lean.Meta.Sym.Offset.0.Lean.Meta.Sym.isOffset?.get : Lean.Expr → Lean.Meta.Sym.Offset
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset_4 : HAdd Std.Time.PlainDateTime Std.Time.Millisecond.Offset Std.Time.PlainDateTime
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- If the derivatives of `g` at `f x` are bounded by `C`, and the `i`-th derivative
of `f` at `x` is bounded by `D^i` for all `1 ≤ i ≤ n`, then the `n`-th derivative
of `g ∘ f` is bounded by `n! * C * D^n`.  -/
norm_iteratedFDeriv_comp_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {N : WithTop ℕ∞},
  ContDiff 𝕜 N g →
    ContDiff 𝕜 N f →
      ↑n ≤ N →
        ∀ (x : E) {C D : ℝ},
          (∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) →
              ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n.factorial * C * D ^ n
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitUpper_eq_bot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a continuous multilinear map is constructed from a multilinear map via the constructor
`mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative.  -/
MultilinearMap.mkContinuous_norm_le' : ∀ {𝕜 : 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 : MultilinearMap 𝕜 E G) {C : ℝ}
  (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖), ‖f.mkContinuous C H‖ ≤ max C 0
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_μ_inv_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  (m₁ m₂ m₃ : M) (X : C) [inst_3 : F.Monoidal] {Z : C}
  (h : (F.obj m₃).obj ((CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj m₁) (F.obj m₂)).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.Functor.OplaxMonoidal.δ F m₁ m₂).app X)) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (CategoryTheory.MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Functor.OplaxMonoidal.δ F m₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X))
            h)))
-- Batteries.Recycling.RBTree.Basic
RBTree.instEmptyCollectionRBMap : (α : Type u) → (β : Type v) → (cmp : α → α → Ordering) → EmptyCollection (RBTree.RBMap α β cmp)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_filter_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  m.WF → ((Std.DHashMap.Raw.filter (fun a x => f a) m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.getKey k h) = true)
-- Mathlib.Topology.Homotopy.TopCat.Basic
/-- A homotopy between morphisms in `TopCat` is a homotopy between
the corresponding continuous maps.  -/
TopCat.Homotopy : {X Y : TopCat} → (X ⟶ Y) → (X ⟶ Y) → Type u
-- Init.Data.Array.Lemmas
Array.map_eq_replicate_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} {b : β},
  Array.map f xs = Array.replicate xs.size b ↔ ∀ x ∈ xs, f x = b
-- Mathlib.Algebra.Order.Quantale
Quantale.bot_mul : ∀ {α : Type u_3} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α] {x : α}, ⊥ * x = ⊥
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.parentD_linkAux : ∀ {i : ℕ} {self : Array Batteries.UFNode} {x y : Fin self.size},
  Batteries.UnionFind.parentD (Batteries.UnionFind.linkAux self x y) i =
    if ↑x = ↑y then Batteries.UnionFind.parentD self i
    else
      if self[↑y].rank < self[↑x].rank then if ↑y = i then ↑x else Batteries.UnionFind.parentD self i
      else if ↑x = i then ↑y else Batteries.UnionFind.parentD self i
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.toMul_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : Additive α}, Additive.toMul a < Additive.toMul b ↔ a < b
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierInvModule` is a function space on which the Fourier transform is a linear map.  -/
FourierInvModule : (R : Type u_5) →
  (E : Type u_6) → (F : outParam (Type u_7)) → [Add E] → [Add F] → [SMul R E] → [SMul R F] → Type (max u_6 u_7)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.SimplicialObject.Split C},
  x.X = y.X → x.s ≍ y.s → x = y
-- Mathlib.CategoryTheory.Category.Pointed
typeToPointed_map_toFun : ∀ {X Y : Type u} (f : X ⟶ Y) (a : Option X),
  (typeToPointed.map f).toFun a = Option.map (⇑(CategoryTheory.ConcreteCategory.hom f)) a
-- Init.Sym.Lemmas
Lean.Sym.ne_self : ∀ {α : Sort u_1} (a : α), (a ≠ a) = False
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β}, StrictConcaveOn 𝕜 s f → ConcaveOn 𝕜 s f
-- Lean.Environment
/-- Applies the given function to the extension state. See `AsyncMode` for details on how modifications
from different environment branches are reconciled.

Note that in modes `sync` and `async`, `f` will be called twice, on the local and on the `checked`
state.
 -/
Lean.EnvExtension.modifyState : {σ : Type} →
  (ext : Lean.EnvExtension σ) →
    Lean.Environment →
      (σ → σ) →
        optParam Lean.EnvExtension.AsyncMode ext.asyncMode → optParam Lean.Name Lean.Name.anonymous → Lean.Environment
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instAddMonoidHomClass : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N],
  AddMonoidHomClass (S.LocalizationMap N) M N
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_log_of_rpow_le : ∀ {x y z : ℝ}, 0 < x → x ^ z ≤ y → z * Real.log x ≤ Real.log y
-- Init.Data.SInt.Lemmas
Int64.ofInt_neg : ∀ (a : ℤ), Int64.ofInt (-a) = -Int64.ofInt a
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.id_toAlgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A], ↑(BialgHom.id R A) = AlgHom.id R A
-- Mathlib.RingTheory.Prime
/-- If `x * y = a * p ^ n` where `p` is prime, then `x` and `y` can both be written
as the product of a power of `p` and a divisor of `a`.  -/
mul_eq_mul_prime_pow : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y a p : R} {n : ℕ},
  Prime p → x * y = a * p ^ n → ∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_add : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : AddMonoid M] {k : κ} (f g : ι k →₀ M),
  (f + g).embSigma = f.embSigma + g.embSigma
-- Init.Data.List.Erase
List.Pairwise.eraseP : ∀ {α : Type u_1} {p : α → α → Prop} {l : List α} (q : α → Bool), List.Pairwise p l → List.Pairwise p (List.eraseP q l)
-- Batteries.Data.AssocList
Batteries.AssocList.beq.eq_4 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] (a : α) (b : β) (t : Batteries.AssocList α β) (a' : α)
  (b' : β) (t' : Batteries.AssocList α β),
  (Batteries.AssocList.cons a b t).beq (Batteries.AssocList.cons a' b' t') = (a == a' && b == b' && t.beq t')
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_comp_mul_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨] {X : Ω → 𝓧} {Y : Ω → 𝓨} {f : 𝓧 → 𝕜}
  {g : 𝓨 → 𝕜},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ) →
            ∫ (x : Ω), (f ∘ X * g ∘ Y) x ∂μ = (∫ (x : Ω), (f ∘ X) x ∂μ) * ∫ (x : Ω), (g ∘ Y) x ∂μ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.limitsOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (X₁ X₂ : CategoryTheory.Functor J C)
  (c₁ : CategoryTheory.Limits.Cone X₁) (c₂ : CategoryTheory.Limits.Cone X₂) (x : CategoryTheory.Limits.IsLimit c₁)
  (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂),
  W.functorCategory J f → W.limitsOfShape J (h₂.lift { pt := c₁.pt, π := CategoryTheory.CategoryStruct.comp c₁.π f })
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)),
  PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t) = closure t
-- Lean.Parser.Term
Lean.Parser.Term.trailing_parser : Lean.Parser.Parser
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.identNoAntiquot.parenthesizer : Lean.PrettyPrinter.ParenthesizerM Unit
-- Mathlib.Analysis.Normed.Group.Basic
ne_one_of_nnnorm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E}, ‖a‖₊ ≠ 0 → a ≠ 1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M] (a b : M),
  SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b
-- Lean.Environment
Lean.ReplayFn : Type → Type
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_3),
  (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁ =
    ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⊞ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃))
-- Mathlib.Analysis.Meromorphic.RCLike
/-- If `f` is meromorphic function on `ℝ` or `ℂ`, then there exists a point where a meromorphic function
`f` has finite order iff `f` has finite order at every point.
 -/
Meromorphic.exists_meromorphicOrderAt_ne_top_iff_forall : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {f : 𝕜 → E}, Meromorphic f → ((∃ u, meromorphicOrderAt f u ≠ ⊤) ↔ ∀ (u : 𝕜), meromorphicOrderAt f u ≠ ⊤)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Composition of polynomial maps.  -/
PolynomialLaw.comp : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {P : Type u_3} →
                  [inst_5 : AddCommMonoid P] → [inst_6 : Module R P] → (N →ₚₗ[R] P) → (M →ₚₗ[R] N) → M →ₚₗ[R] P
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_surjOn : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.SurjOn (Set.projIci a) (Set.Ici a) Set.univ
-- Mathlib.Data.Nat.Log
_private.Mathlib.Data.Nat.Log.0.Nat.log.go.match_1.eq_1 : ∀ (motive : ℕ × ℕ → Sort u_1) (q e : ℕ) (h_1 : (q e : ℕ) → motive (q, e)),
  (match (q, e) with
    | (q, e) => h_1 q e) =
    h_1 q e
-- Mathlib.Topology.Algebra.Monoid
isClosed_setOfPred_map_mul : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Mul M₁] [inst_3 : Mul M₂]
  [ContinuousMul M₂], IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.ker_eq_bot_of_mono : ∀ {A B : AddCommGrpCat} (f : A ⟶ B) [CategoryTheory.Mono f], (AddCommGrpCat.Hom.hom f).ker = ⊥
-- Std.Time.Format.Modifier
Std.Time.Modifier.n.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.n presentation = Std.Time.Modifier.n presentation_1 → presentation = presentation_1
-- Mathlib.Algebra.Star.Basic
StarMul.toInvolutiveStar : {R : Type u} → {inst : Mul R} → [self : StarMul R] → InvolutiveStar R
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₂_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ),
  (X.sc₂ f g fg h n₀).X₃ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Mathlib.CategoryTheory.Comma.CardinalArrow
/-- The bijection `Arrow Cᵒᵖ ≃ Arrow C`.  -/
CategoryTheory.Arrow.opEquiv : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Arrow Cᵒᵖ ≃ CategoryTheory.Arrow C
-- Mathlib.Control.Traversable.Instances
Sum.naturality : ∀ {σ : Type u} {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G]
  [LawfulApplicative F] (η : ApplicativeTransformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : σ ⊕ α),
  (fun {α} => η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} => η.app α) ∘ f) x
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.eval.eq_2 : Std.Tactic.BVDecide.Gate.xor.eval = fun x1 x2 => x1 ^^ x2
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → ℕ → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options) (annotationId? : Option String)
  (uri_1 : Lean.Lsp.DocumentUri) (options?_1 : Option Lean.Lsp.CreateFile.Options) (annotationId?_1 : Option String),
  ({ uri := uri, options? := options?, annotationId? := annotationId? } =
      { uri := uri_1, options? := options?_1, annotationId? := annotationId?_1 }) =
    (uri = uri_1 ∧ options? = options?_1 ∧ annotationId? = annotationId?_1)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ico_right_eq_Ico_add_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α} [NoMaxOrder α], a ≤ b → insert b (Finset.Ico a b) = Finset.Ico a (b + 1)
-- Aesop.Tree.Traversal
Aesop.TreeRef.rapp.injEq : ∀ (rref rref_1 : Aesop.RappRef), (Aesop.TreeRef.rapp rref = Aesop.TreeRef.rapp rref_1) = (rref = rref_1)
-- Init.Data.List.Basic
List.intersperse.eq_2 : ∀ {α : Type u} (sep head : α), List.intersperse sep [head] = [head]
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_succ_le : ∀ {a b : Ordinal.{u}} {s : Set Ordinal.{u}},
  ¬BddAbove s → a ∈ s → Ordinal.enumOrd s b < a → Ordinal.enumOrd s (Order.succ b) ≤ a
-- Mathlib.Geometry.Manifold.ConformalGroupoid
/-- The groupoid of conformal maps.  -/
conformalGroupoid : {X : Type u_1} → [inst : NormedAddCommGroup X] → [NormedSpace ℝ X] → StructureGroupoid X
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.Linter.mk.inj : ∀ {test : Lean.Name → Lean.MetaM (Option Lean.MessageData)} {noErrorsFound errorsFound : Lean.MessageData}
  {isFast : Bool} {test_1 : Lean.Name → Lean.MetaM (Option Lean.MessageData)}
  {noErrorsFound_1 errorsFound_1 : Lean.MessageData} {isFast_1 : Bool},
  { test := test, noErrorsFound := noErrorsFound, errorsFound := errorsFound, isFast := isFast } =
      { test := test_1, noErrorsFound := noErrorsFound_1, errorsFound := errorsFound_1, isFast := isFast_1 } →
    test = test_1 ∧ noErrorsFound = noErrorsFound_1 ∧ errorsFound = errorsFound_1 ∧ isFast = isFast_1
-- Init.Data.List.Nat.Erase
List.getElem_eraseIdx : ∀ {α : Type u_1} {l : List α} {i j : ℕ} (h : j < (l.eraseIdx i).length),
  (l.eraseIdx i)[j] = if h' : j < i then l[j] else l[j + 1]
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.commShiftIso_inv_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] {X Y : C}
  (f : X ⟶ Y) (a : A) {Z : D} (h : F.obj ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) h)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_of_not_integrable : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ → InformationTheory.klDiv μ ν = ⊤
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_eq_add_of_root_eq_smul_add_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j k l : ι}
  {x y : R}, P.root k = x • P.root i + y • P.root l → P.pairing k j = x • P.pairing i j + y • P.pairing l j
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.pi_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {γ : Type w} [inst_1 : Add γ] (g : (i : I) → γ →ₙ+ f i)
  (x : γ) (i : I), (AddHom.pi g) x i = (g i) x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)],
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).H =
    CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toAddMonoidHom_eq_coe : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α), f.toAddMonoidHom = ↑f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ofList_eq_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List ((a : α) × β a)},
  Std.ExtDTreeMap.ofList l cmp = List.foldl (fun acc p => acc.insert p.fst p.snd) ∅ l