mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.LocalContext
Lean.LocalContext.pop : Lean.LocalContext → Lean.LocalContext
-- Mathlib.FieldTheory.SeparableClosure
/-- The same-universe version of `Field.lift_sepDegree_eq_of_equiv`.  -/
Field.sepDegree_eq_of_equiv : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K), Field.sepDegree F E = Field.sepDegree F K
-- Init.Internal.Order.Lemmas
_private.Init.Data.Array.Basic.0.Array.findSomeRevM?.find.induct : ∀ {α : Type u} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Prop),
  (∀ (x : 0 ≤ as.size), motive 0 x) →
    (∀ (i : ℕ) (h : i + 1 ≤ as.size) (this : i < as.size),
        (have this := ⋯;
          motive i this) →
          motive i.succ h) →
      ∀ (i : ℕ) (a : i ≤ as.size), motive i a
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) {Z : A}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η Φ.presheafFiber) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) h
-- Init.Data.Queue
/-- `O(1)` amortized, `O(n)` worst case. Pop an element from the back of the queue,
returning the element and the new queue.
 -/
Std.Queue.dequeue? : {α : Type u} → Std.Queue α → Option (α × Std.Queue α)
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).whiskerLeft AlgebraicTopology.DoldKan.N₂Γ₂.hom =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom AlgebraicTopology.DoldKan.N₁Γ₀.hom
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.grpObj_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.GrpObj (F.obj X)],
  CategoryTheory.MonObj.one =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one)
-- Mathlib.Algebra.Group.Basic
add_neg_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + -b = 0 ↔ a = b
-- Mathlib.Analysis.Convolution
MeasureTheory.zero_convolution : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {g : G → E'} [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F}
  [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G],
  MeasureTheory.convolution 0 g L μ = 0
-- Mathlib.Data.Finsupp.Antidiagonal
/-- The `Finsupp` counterpart of `Multiset.antidiagonal`: the antidiagonal of
`s : α →₀ ℕ` consists of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
The finitely supported function `antidiagonal s` is equal to the multiplicities of these pairs.  -/
Finsupp.antidiagonal' : {α : Type u} → [DecidableEq α] → (α →₀ ℕ) → (α →₀ ℕ) × (α →₀ ℕ) →₀ ℕ
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If the (product-like) biproduct comparison for `F`, `X` and `Y` is a monomorphism, then
`F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`.  -/
CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : C} [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)]
  [CategoryTheory.Mono (F.biprodComparison X Y)], CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : M) (y : ↥S),
  (f.addEquivOfAddEquiv k H) (f.mk' x y) = k.mk' (j x) ⟨j ↑y, ⋯⟩
-- Mathlib.Data.List.Lattice
List.bagInter.eq_3 : ∀ {α : Type u_1} [inst : BEq α] (x : List α) (a : α) (l₁ : List α),
  (x = [] → False) → (a :: l₁).bagInter x = if List.elem a x = true then a :: l₁.bagInter (x.erase a) else l₁.bagInter x
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_of_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set R},
  s ⊆ t → Module.IsTorsionBySet R M t → Module.IsTorsionBySet R M s
-- Mathlib.Algebra.Group.Defs
/-- A Prop stating that the multiplication is commutative.  -/
IsMulCommutative : (M : Type u_2) → [Mul M] → Prop
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.endsWith_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.copy.endsWith pat = s.endsWith pat
-- Mathlib.RingTheory.IsGaloisGroup.Defs
/-- If `B/A` and `B/A'` are Galois with the same Galois group, then `A ≃+* A'`.  -/
IsGaloisGroup.ringEquiv : (G : Type u_1) →
  (A : Type u_2) →
    (A' : Type u_3) →
      (B : Type u_4) →
        [inst : Group G] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra A B] →
                [inst_4 : MulSemiringAction G B] →
                  [hA : IsGaloisGroup G A B] →
                    [FaithfulSMul A B] →
                      [inst_6 : CommSemiring A'] →
                        [inst_7 : Algebra A' B] → [FaithfulSMul A' B] → [hA' : IsGaloisGroup G A' B] → A ≃+* A'
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.TreeMap.unitOfList l cmp).isEmpty = l.isEmpty
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Mon : Type
-- Mathlib.Data.Analysis.Filter
CFilter.instCoeFunForall : {α : Type u_1} → {σ : Type u_3} → [inst : PartialOrder α] → CoeFun (CFilter α σ) fun x => σ → α
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} {A : C} (x₂ : A ⟶ S.X₂) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ S.g = 0),
  CategoryTheory.CategoryStruct.comp (S.liftCycles x₂ hx₂) S.homologyπ = 0 ↔
    ∃ A' π,
      ∃ (_ : CategoryTheory.Epi π),
        ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S.f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Mathlib.Data.Finsupp.Single
Finsupp.erase.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) (f : α →₀ M),
  Finsupp.erase a f =
    { support := f.support.erase a, toFun := fun a' => if a' = a then 0 else f a', mem_support_toFun := ⋯ }
-- Mathlib.Computability.TuringDegree
/-- Turing degrees are the equivalence classes of partial functions under Turing equivalence.
 -/
TuringDegree : Type
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.smul_add : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : Zero R]
  [inst_6 : DistribSMul R V] (x : HahnSeries Γ R) (y z : HahnModule Γ' R V), x • (y + z) = x • y + x • z
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_intCast : ∀ {R : Type u_1} [inst : Ring R] (x y : R) (n : ℤ), Polynomial.evalEval x y ↑n = ↑n
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.cuspFunction_add`. -/
ModularFormClass.cuspFunction_add : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.cuspFunction h (⇑f + ⇑g) = UpperHalfPlane.cuspFunction h ⇑f + UpperHalfPlane.cuspFunction h ⇑g
-- Init.Data.List.Nat.Modify
List.modifyTailIdx_modifyTailIdx_self : ∀ {α : Type u_1} {f g : List α → List α} (i : ℕ) (l : List α),
  (l.modifyTailIdx i f).modifyTailIdx i g = l.modifyTailIdx i (g ∘ f)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_const : ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (a : Ordinal.{max u v}), (o.blsub fun x x_1 => a) = Order.succ a
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
ContinuousLinearMap.compLeftContinuousBounded_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} {𝕜 : Type u_1} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 β] [inst_4 : SeminormedAddCommGroup γ]
  [inst_5 : NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) (f : BoundedContinuousFunction α β) (x : α),
  ((ContinuousLinearMap.compLeftContinuousBounded α g) f) x = g (f x)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.fiberEquivGroup.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})),
  hf.fiberEquivGroup e = (Equiv.ofBijective (fun g => ⟨g • ↑e, ⋯⟩) ⋯).symm
-- Mathlib.Algebra.BigOperators.Ring.List
Commute.list_sum_left : ∀ {R : Type u_5} [inst : NonUnitalNonAssocSemiring R] (b : R) (l : List R), (∀ a ∈ l, Commute a b) → Commute l.sum b
-- Mathlib.Order.Heyting.Basic
fst_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : Compl α] [inst_1 : Compl β] (a : α × β), aᶜ.1 = a.1ᶜ
-- Mathlib.RingTheory.LocalProperties.Basic
/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is included in
the localization of `J` at `P`, then `I ≤ J`.  -/
Ideal.le_of_localization_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] {I J : Ideal R},
  (∀ (P : Ideal R) (x : P.IsMaximal),
      Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ Ideal.map (algebraMap R (Localization.AtPrime P)) J) →
    I ≤ J
-- Mathlib.Analysis.InnerProductSpace.Basic
innerₗ_apply_apply : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (v w : F),
  ((innerₗ F) v) w = inner ℝ v w
-- Mathlib.Geometry.Manifold.HasGroupoid
Structomorph.mk.sizeOf_spec : ∀ {H : Type u} [inst : TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6}
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H M] [inst_4 : ChartedSpace H M']
  [inst_5 : SizeOf H] [inst_6 : SizeOf M] [inst_7 : SizeOf M'] (toHomeomorph : M ≃ₜ M')
  (mem_groupoid :
    ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
      c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G),
  sizeOf { toHomeomorph := toHomeomorph, mem_groupoid := mem_groupoid } = 1 + sizeOf toHomeomorph
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong : ∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [P.RespectsIso],
  (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q') →
    (∀ {R S : CommRingCat} {f : R ⟶ S}, P' (AlgebraicGeometry.Spec.map f) → Q' (CommRingCat.Hom.hom f)) →
      (∀ {R S : CommRingCat} {f : R ⟶ S}, P (AlgebraicGeometry.Spec.map f) ↔ Q (CommRingCat.Hom.hom f)) →
        ∀ {R S T : CommRingCat} {f : AlgebraicGeometry.Spec T ⟶ AlgebraicGeometry.Spec R}
          {g : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R},
          P' f → P (CategoryTheory.Limits.pullback.fst f g) → P g
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- The `RingHom.ker` of `φ : characterSpace 𝕜 A` is maximal.  -/
WeakDual.ker_isMaximal : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Field 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : Ring A] [inst_5 : TopologicalSpace A] [inst_6 : Algebra 𝕜 A]
  (φ : ↑(WeakDual.characterSpace 𝕜 A)), (RingHom.ker φ).IsMaximal
-- Std.Async.DNS
Std.Async.DNS.NameInfo.mk.inj : ∀ {host service host_1 service_1 : String},
  { host := host, service := service } = { host := host_1, service := service_1 } → host = host_1 ∧ service = service_1
-- Mathlib.Analysis.Normed.Group.Rat
Rat.norm_cast_real : ∀ (r : ℚ), ‖↑r‖ = ‖r‖
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {s : ℕ → Set α},
  Monotone s → (∀ (i : ℕ), MeasurableSet (s i)) → Filter.Tendsto (fun n => v (s n)) Filter.atTop (nhds (v (⋃ n, s n)))
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- A functor between two categories `C` and `D` can be lifted to an oplax functor between the
corresponding locally discrete bicategories.

This is just an abbreviation of `Functor.toPseudofunctor.toOplax`.
 -/
CategoryTheory.Functor.toOplaxFunctor : {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] →
        CategoryTheory.Functor C D →
          CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete C) (CategoryTheory.LocallyDiscrete D)
-- Mathlib.Topology.LocallyClosed
Topology.IsInducing.isLocallyClosed_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Topology.IsInducing f → (IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s)
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- The underlying presheaf of `sheafHom F G`. It is isomorphic to `presheafHom F.1 G.1`
(see `sheafHom'Iso`), but has better definitional properties.  -/
CategoryTheory.sheafHom' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          CategoryTheory.Sheaf J A → CategoryTheory.Sheaf J A → CategoryTheory.Functor Cᵒᵖ (Type (max (max u v) v'))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.mem_maximalRealSubfield_iff : ∀ {K : Type u_2} [inst : Field K] (x : K), x ∈ NumberField.maximalRealSubfield K ↔ ∀ (φ : K →+* ℂ), star (φ x) = φ x
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.J_transpose : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R], (Matrix.J l R).transpose = -Matrix.J l R
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_finsupp_sum_index : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {α : Type u_2} {β : Type u_3} [inst_1 : Zero β] (f : α →₀ β)
  (g : α → β → σ →₀ ℕ) (a : R),
  (MvPolynomial.monomial (f.sum g)) a = MvPolynomial.C a * f.prod fun a b => (MvPolynomial.monomial (g a b)) 1
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_le_opow_left : ∀ {a b : Ordinal.{u_1}} (c : Ordinal.{u_1}), a ≤ b → a ^ c ≤ b ^ c
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- The left derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `derivWithin` in that case is 0.  -/
InformationTheory.leftDeriv_klFun : ∀ {x : ℝ}, derivWithin InformationTheory.klFun (Set.Iio x) x = Real.log x
-- Aesop.Tree.RunMetaM
Aesop.RappRef.runMetaMModifying : {m : Type → Type} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.RappRef → m α
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.prod.injEq : ∀ (fst snd : Lean.Expr.ProdTree) (lfst lsnd : Lean.Level) (fst_1 snd_1 : Lean.Expr.ProdTree)
  (lfst_1 lsnd_1 : Lean.Level),
  (fst.prod snd lfst lsnd = fst_1.prod snd_1 lfst_1 lsnd_1) =
    (fst = fst_1 ∧ snd = snd_1 ∧ lfst = lfst_1 ∧ lsnd = lsnd_1)
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A scheme is disjoint if the children of each set of pairwise disjoint.  -/
CantorScheme.Disjoint : {β : Type u_1} → {α : Type u_2} → (List β → Set α) → Prop
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instMonoFShortComplexOpcyclesThreeδ₂Toδ₁ : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Mono (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for a Submonoid `S`, we get an isomorphism between
the Localization of `M` at `S` as a quotient type and `N`.  -/
AddLocalization.addEquivOfQuotient : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → AddLocalization S ≃+ N
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_intCast : ∀ {R : Type u} [inst : Ring R] (n : ℤ), (↑n).natDegree = 0
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- The natural isomorphism
`F.mapShortComplex ⋙ homologyFunctor D ≅ homologyFunctor C ⋙ F`
for a functor `F : C ⥤ D` which preserves homology.  -/
CategoryTheory.ShortComplex.homologyFunctorIso : {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] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.CategoryWithHomology C] →
                  [inst_6 : CategoryTheory.CategoryWithHomology D] →
                    [F.PreservesHomology] →
                      F.mapShortComplex.comp (CategoryTheory.ShortComplex.homologyFunctor D) ≅
                        (CategoryTheory.ShortComplex.homologyFunctor C).comp F
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_inl_inr : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N],
  (MonoidHom.inl M N).noncommCoprod (MonoidHom.inr M N) ⋯ = MonoidHom.id (M × N)
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Result.mk.inj : ∀ {status : Lean.Util.ParamMinimizer.Status} {paramMask : Array Bool} {numCalls : ℕ}
  {status_1 : Lean.Util.ParamMinimizer.Status} {paramMask_1 : Array Bool} {numCalls_1 : ℕ},
  { status := status, paramMask := paramMask, numCalls := numCalls } =
      { status := status_1, paramMask := paramMask_1, numCalls := numCalls_1 } →
    status = status_1 ∧ paramMask = paramMask_1 ∧ numCalls = numCalls_1
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- A quick attempt to prove that `⦋m⦌` is `n`-truncated (`⦋m⦌.len ≤ n`).  -/
SimplexCategory.Truncated.tacticTrunc : Lean.ParserDescr
-- Lean.Data.Lsp.Basic
/-- A textual edit applicable to a text document.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textEdit)  -/
Lean.Lsp.TextEdit : Type
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.mk.injEq : ∀ (name : String) (uri : Lean.Lsp.DocumentUri) (data? : Option Lean.Json) (name_1 : String)
  (uri_1 : Lean.Lsp.DocumentUri) (data?_1 : Option Lean.Json),
  ({ name := name, uri := uri, data? := data? } = { name := name_1, uri := uri_1, data? := data?_1 }) =
    (name = name_1 ∧ uri = uri_1 ∧ data? = data?_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.top_add : ∀ {α : Type u} [inst : Add α] (x : WithTop α), ⊤ + x = ⊤
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ProbabilityTheory.Kernel.iIndepSet s κ μ →
      ∀ (n : ℕ),
        ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s (n + 1)})
          (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) κ μ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.lift_comp_zero_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddMonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  (g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddMonObj.zero) g)
      CategoryTheory.AddMonObj.add =
    g
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- The submodule of `Dual K H` spanned by the roots associated to a Lie ideal.  -/
LieIdeal.rootSpan : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            {H : LieSubalgebra K L} →
              [H.IsCartanSubalgebra] →
                [CharZero K] →
                  [LieAlgebra.IsKilling K L] →
                    [LieModule.IsTriangularizable K (↥H) L] → LieIdeal K L → Submodule K (Module.Dual K ↥H)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.isBase_of_isBasis_superset : ∀ {α : Type u_1} {M : Matroid α} {B I X : Set α}, M.IsBase B → B ⊆ X → M.IsBasis I X → M.IsBase I
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebraClass.subtype_apply : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SetLike S A] [inst_4 : NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A]
  {s : S} (x : ↥s), (NonUnitalSubalgebraClass.subtype s) x = ↑x