mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.measurable_lmarginalPartialTraj : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (a b : ℕ)
  {f : ((n : ℕ) → X n) → ENNReal}, Measurable f → Measurable (ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b f)
-- Mathlib.Algebra.Group.Conj
isConj_iff : ∀ {α : Type u} [inst : Group α] {a b : α}, IsConj a b ↔ ∃ c, c * a * c⁻¹ = b
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
MultilinearMap.codRestrict.congr_simp : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f f_1 : MultilinearMap R M₁ M₂) (e_f : f = f_1) (p : Submodule R M₂)
  (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p), f.codRestrict p h = f_1.codRestrict p ⋯
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transportIso_hom_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c), (x.transportIso α).hom.base = α.inv
-- Init.Data.SInt.Lemmas
ISize.sub_zero : ∀ (a : ISize), a - 0 = a
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The right adjoint mate `fᘁ : Xᘁ ⟶ Yᘁ` of a morphism `f : X ⟶ Y`.  -/
CategoryTheory.«term_ᘁ_1» : Lean.TrailingParserDescr
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIocDiv` is eventually constant on the left at every point.  -/
eventuallyEq_toIocDiv_nhdsLE : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  toIocDiv hp a =ᶠ[nhdsWithin x (Set.Iic x)] fun x_1 => toIocDiv hp a x
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsSeparator.of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : C}, CategoryTheory.IsSeparator G → ∀ (α : C ≌ D), CategoryTheory.IsSeparator (α.functor.obj G)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.algebraMap_eq_one_iff : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] (x : R), (algebraMap R (FreeAlgebra R X)) x = 1 ↔ x = 1
-- Init.Data.Int.DivMod.Lemmas
Int.neg_tdiv_neg : ∀ (a b : ℤ), (-a).tdiv (-b) = a.tdiv b
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.norm_eval_le_projectiveSeminorm : ∀ {ι : 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)] {G : Type u_4}
  [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
  (x : PiTensorProduct 𝕜 fun i => E i), ‖(PiTensorProduct.lift f.toMultilinearMap) x‖ ≤ ‖f‖ * ‖x‖
-- Lean.Meta.Basic
/-- Similar to `forallTelescopeReducing`, stops constructing the telescope when
it reaches size `maxFVars`.

If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.

If `whnfType` is `true`, we give `k` the `whnf` of the resulting type.
This is a free operation unless `maxFVars? == some 0`, in which case it computes the `whnf`.
 -/
Lean.Meta.forallBoundedTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        Lean.Expr → Option ℕ → (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → optParam Bool false → n α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_bijective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N], Function.Bijective ContinuousAddEquiv.symm
-- Init.Data.Int.Gcd
Int.dvd_lcm_left : ∀ (a b : ℤ), a ∣ ↑(a.lcm b)
-- Mathlib.Algebra.Group.Units.Basic
eq_zero_of_add_right : ∀ {α : Type u} [inst : AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → a = 0
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) (ι : Type u_5) [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F]
  [inst_8 : ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G] [inst_11 : TopologicalSpace G]
  [inst_12 : IsTopologicalAddGroup G] [inst_13 : ContinuousConstSMul 𝕜 G] (g : F →L[𝕜] G) (f : E [⋀^ι]→L[𝕜] F),
  ((ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 E F G ι) g) f = g.compContinuousAlternatingMap f
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S.eq_1 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R 0 = 1
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- A primitive subgroup of `Equiv.Perm α` that contains a 3-cycle
contains the alternating group (Jordan).  -/
Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem : ∀ {α : Type u_1} {G : Subgroup (Equiv.Perm α)} [inst : Fintype α] [inst_1 : DecidableEq α],
  MulAction.IsPreprimitive (↥G) α → ∀ {g : Equiv.Perm α}, g.IsThreeCycle → g ∈ G → alternatingGroup α ≤ G
-- Lean.Elab.Util
Lean.Elab.pp.macroStack : Lean.Option Bool
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the left by a uniformly continuous function preserves
uniform convergence on a set  -/
UniformContinuous.comp_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
  {s : Set α} {p : Filter ι} [inst_1 : UniformSpace γ] {g : β → γ},
  UniformContinuous g → TendstoUniformlyOn F f p s → TendstoUniformlyOn (fun i => g ∘ F i) (g ∘ f) p s
-- Mathlib.Data.Set.Sigma
Set.sigma_eq_biUnion : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)}, s.sigma t = ⋃ i ∈ s, Sigma.mk i '' t i
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
/-- Giving a precoverage on a category is the same as giving a predicate
on every pre-`0`-hypercover that is stable under deduplication.  -/
CategoryTheory.Precoverage.equivPreZeroHypercoverFamily : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C ≃ CategoryTheory.PreZeroHypercoverFamily C
-- Mathlib.NumberTheory.FermatPsp
Nat.frequently_atTop_fermatPsp : ∀ {b : ℕ}, 1 ≤ b → ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.llcomp_apply' : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {M : Type u_17} {N : Type u_18}
  {P : Type u_19} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃] [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R₂ N]
  [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (f : N →ₛₗ[σ₂₃] P) (g : M →ₛₗ[σ₁₂] N), ((LinearMap.llcomp R₃ M N P) f) g = f ∘ₛₗ g
-- Mathlib.Algebra.Group.Hom.Defs
/-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a left inverse,
then `f x` has a left inverse too. For elements invertible on both sides see `IsUnit.map`.  -/
MonoidHom.map_exists_left_inv : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) {x : M}, (∃ y, y * x = 1) → ∃ y, y * f x = 1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.injective_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N), Function.Injective ⇑f ↔ ∀ ⦃x : M⦄, x ∈ S → IsRegular x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} [inst_2 : Inhabited β] {f : Option β → Option β},
  (m.alter k f)[k']! = if (k == k') = true then (f m[k]?).get! else m[k']!
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- `@[simp]`-normal form of `toSheafify_app_apply`.  -/
PresheafOfModules.toSheafify_app_apply' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  (X : Cᵒᵖ) (x : ↑(M₀.obj X)),
  (ModuleCat.Hom.hom ((PresheafOfModules.toSheafify α φ).app X)) x = (CategoryTheory.ConcreteCategory.hom (φ.app X)) x
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.mk : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      (stratum : FiniteArchimedeanClass M → Submodule K M) →
                        (∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum c)) →
                          (∀ (c : FiniteArchimedeanClass M),
                              FiniteArchimedeanClass.ball K c ⊔ stratum c = FiniteArchimedeanClass.closedBall K c) →
                            HahnEmbedding.ArchimedeanStrata K M
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
lift_rank_lt_rank_dual : ∀ {K : Type u} {V : Type v} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Cardinal.aleph0 ≤ Module.rank K V → Cardinal.lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.MorphismProperty.shift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {A : Type w}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] {X Y : C} {f : X ⟶ Y},
  W f → ∀ (a : A), W ((CategoryTheory.shiftFunctor C a).map f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} [inst_1 : Inhabited (β k')] {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).get! k' =
        if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).get! else t.get! k'
-- Mathlib.Data.Rat.Lemmas
Rat.div_int_inj : ∀ {a b c d : ℤ},
  0 < b → 0 < d → a.natAbs.Coprime b.natAbs → c.natAbs.Coprime d.natAbs → ↑a / ↑b = ↑c / ↑d → a = c ∧ b = d
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} {x : α × γ} [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η] {s : Set (β × δ)},
  MeasurableSet s → ((κ.parallelComp η) x) s = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.Algebra.Group.Basic
div_one : ∀ {G : Type u_3} [inst : DivInvOneMonoid G] (a : G), a / 1 = a
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roi.count_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {r : Std.Roi α},
  r.iter.length = r.size
-- Mathlib.Analysis.ODE.DiscreteGronwall
/-- Discrete Grönwall inequality, uniform bound: a single bound holding for all `n ∈ [n₀, n₁)`.  -/
discrete_gronwall_Ico : ∀ {u b c : ℕ → ℝ} {n₀ n₁ : ℕ},
  0 ≤ u n₀ →
    (∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) →
      (∀ n ≥ n₀, 0 ≤ c n) →
        (∀ n ≥ n₀, 0 ≤ b n) →
          ∀ ⦃n : ℕ⦄,
            n ∈ Finset.Ico n₀ n₁ → u n ≤ (u n₀ + ∑ k ∈ Finset.Ico n₀ n₁, b k) * Real.exp (∑ i ∈ Finset.Ico n₀ n₁, c i)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.mismatched_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos endPos' : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidRevSearchFrom pat startPos l →
    startPos < endPos' →
      (∀ (pos : s.Pos), startPos < pos → pos ≤ endPos' → ¬String.Slice.Pattern.Model.RevMatchesAt pat pos) →
        endPos = endPos' →
          String.Slice.Pattern.Model.IsValidRevSearchFrom pat endPos'
            (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The adjunction between `withModuleTopology` and the forgetful functor.  -/
TopModuleCat.withModuleTopologyAdj : (R : Type u) →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      TopModuleCat.withModuleTopology R ⊣ CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)
-- Mathlib.Data.List.Sort
List.Perm.eq_of_sortedGE : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁.SortedGE → l₂.SortedGE → l₁.Perm l₂ → l₁ = l₂
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_zero_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β), κ.parallelComp 0 = 0
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.postcomp_map_heq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D} {X Y : C} {f : X ⟶ Y}
  (H : CategoryTheory.Functor D E),
  F.obj X = G.obj X → F.obj Y = G.obj Y → F.map f ≍ G.map f → (F.comp H).map f ≍ (G.comp H).map f
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_le_one : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, ↑n ≤ 1 ↔ n ≤ 1
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyLE_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsStrictlyLE n], L.IsStrictlyLE n
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to negative infinity along a filter, then `f` multiplied by
a positive constant (on the left) also tends to negative infinity.  -/
Filter.Tendsto.const_mul_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => r * f x) l Filter.atBot
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_three_near_10 : |Real.log 3 - 109861228867 / 100000000000| ≤ 1 / 10 ^ 10
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The indexing category of the filtered colimit presentation  -/
CategoryTheory.Limits.IndObjectPresentation.I : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} → CategoryTheory.Limits.IndObjectPresentation A → Type v
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {f : PowerSeries R},
  PowerSeries.constantCoeff f = 0 → Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
-- Mathlib.Data.Set.Countable
/-- Restate `Set.Countable` as a `Countable` instance.  -/
Countable.to_set : ∀ {α : Type u} {s : Set α}, Countable ↑s → s.Countable
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatRestrictScalarsPseudofunctor_map : ∀ {X Y : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (f : X ⟶ Y),
  CommRingCat.moduleCatRestrictScalarsPseudofunctor.map f =
    (ModuleCat.restrictScalars (CommRingCat.Hom.hom f.as.unop)).toCatHom
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- The determinant of a Hadamard matrix is regular, provided the order is regular in `R`.  -/
Matrix.IsHadamard.isRegular_det : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → IsRegular ↑(Fintype.card n) → IsRegular A.det
-- Lean.Message
Lean.instToMessageDataOptionExpr : Lean.ToMessageData (Option Lean.Expr)
-- Mathlib.Data.List.Infix
List.singleton_infix_iff : ∀ {α : Type u_1} (x : α) (xs : List α), [x] <:+: xs ↔ x ∈ xs
-- Mathlib.CategoryTheory.Sites.Sieves
/-- the intermediate object  -/
CategoryTheory.Presieve.BindStruct.Y : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Presieve X} →
        {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} → {Z : C} → {h : Z ⟶ X} → S.BindStruct R h → C
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f = g` and `f` is an immersion, so is `g`.  -/
Manifold.IsImmersionOfComplement.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N},
  Manifold.IsImmersionOfComplement F I J n f → f = g → Manifold.IsImmersionOfComplement F I J n g
-- Init.Data.SInt.Lemmas
Int32.sub_le : ∀ {a b : Int32}, 0 ≤ b → b ≤ a → a - b ≤ a
-- Mathlib.Algebra.Algebra.Hom
/-- Ring homomorphisms are the same as `ℤ`-algebra homomorphisms.  -/
RingHom.equivIntAlgHom : (R : Type u_1) → (S : Type u_2) → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) ≃ (R →ₐ[ℤ] S)
-- Mathlib.Util.CompileInductive
/-- Returns the names of the recursors for a nested or mutual inductive,
using the `all` and `numMotives` arguments from `RecursorVal`.  -/
Mathlib.Util.mkRecNames : List Lean.Name → ℕ → List Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q (CategoryTheory.Limits.pushout f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g)) h)
-- Mathlib.LinearAlgebra.AffineSpace.Ceva
/-- **Ceva's theorem** for a triangle, expressed in terms of multiplying weights.  -/
Affine.Triangle.prod_eq_prod_one_sub_of_mem_line_point_lineMap : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : CommRing k] [NoZeroDivisors k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] {t : Affine.Triangle k P} {r : Fin 3 → k} {p' : P},
  (∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]) →
    ∏ i, r i = ∏ i, (1 - r i)
-- Mathlib.Tactic.Widget.Conv
/-- Rpc function for the conv widget.  -/
Mathlib.Tactic.Conv.SelectionPanel.rpc : SelectInsertParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_add_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ : ProbabilityTheory.Kernel α β) (κ η : ProbabilityTheory.Kernel (α × β) γ)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  μ.compProd (κ + η) = μ.compProd κ + μ.compProd η
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.inter_eq_of_subset_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → I ⊆ J → M.Indep J → J ∩ X = I
-- Lean.Server.FileWorker.Utils
/-- `EditableDocumentCore` with reporter task.  -/
Lean.Server.FileWorker.EditableDocument : Type
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.match_1.congr_eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (x : Option s.Pos)
  (h_1 : (pos : s.Pos) → x = some pos → motive (some pos)) (h_2 : x = none → motive none) (pos : s.Pos)
  (heq_1 : x = some pos),
  (match hd : x with
    | some pos => h_1 pos hd
    | none => h_2 hd) ≍
    h_1 pos heq_1
-- Init.Meta.Defs
Lean.isNumericSubscript : Char → Bool
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.size.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Zipper.size✝ Std.DTreeMap.Internal.Zipper.done = 0
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.FG.map : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} (f : A →ₐ[R] B), S.FG → (Subalgebra.map f S).FG
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α} {hc : t.contains km = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.prodEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)),
  StarAlgHom.prodEquiv f = f.1.prod f.2
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R],
  AlgebraicIndependent R x → (IsTranscendenceBasis R x ↔ Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instSingletonProdOfBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Singleton (α × β) (Std.HashMap.Raw α β)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffsIn_le : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {N : Submodule R (MvPolynomial σ S)},
  MvPolynomial.coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ (i : σ →₀ ℕ), (MvPolynomial.monomial i) m ∈ N