mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₂.X₃ = Z
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- Formula for orthogonal projection onto a single unit vector.  -/
Submodule.starProjection_unit_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : E}, ‖v‖ = 1 → ∀ (w : E), (𝕜 ∙ v).starProjection w = inner 𝕜 v w • v
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.mkRecursorInfoCore : Lean.Name → Option ℕ → Lean.MetaM Lean.Meta.RecursorInfo
-- Mathlib.Order.Heyting.Basic
/-- Transfer `CoheytingAlgebra` across an `Equiv`.  -/
Equiv.coheytingAlgebra : {α : Type u_2} → {β : Type u_3} → α ≃ β → [CoheytingAlgebra β] → CoheytingAlgebra α
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- the underlying additive map `R.obj X →+ M.obj X` of a derivation  -/
PresheafOfModules.Derivation.d : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} → M.Derivation φ → {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X)
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.TreeMap.Raw.keyAtIdxD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → ℕ → α → α
-- Init.Data.SInt.Bitwise
ISize.toInt8_or : ∀ (a b : ISize), (a ||| b).toInt8 = a.toInt8 ||| b.toInt8
-- Mathlib.Analysis.Normed.Group.Uniform
/-- A seminormed group is a uniform group, i.e., multiplication and division are uniformly
continuous.  -/
SeminormedCommGroup.to_isUniformGroup : ∀ {E : Type u_2} [inst : SeminormedCommGroup E], IsUniformGroup E
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasSubgaussianMGF X 0 μ → X =ᵐ[μ] 0
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.congr_arg : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) {x_2 y : α},
  x_2 = y → f x_2 = f y
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.trans_homotopyInvHomId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  (f.trans g).homotopyInvHomId =
    ⋯.mpr (⋯.mp (((f.homotopyInvHomId.compRightId g.hom).compLeft g.inv).trans g.homotopyInvHomId))
-- Std.Http.Protocol.H1
/-- Utility result for body parser branches that exceed configured body limits.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.bodyTooLarge : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.Data.Finset.Sym
Finset.sym_eq_empty : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ}, s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasInitial C]
  {P Q : CategoryTheory.ObjectProperty C} [Q.IsClosedUnderBinaryCoproducts]
  [Q.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})], P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- If two mul homomorphisms are equal on a set, then they are equal on its subsemigroup closure.  -/
MulHom.eqOn_closure : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N} {s : Set M},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subsemigroup.closure s)
-- Mathlib.Data.Setoid.Basic
Setoid.prodQuotientEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} (r : Setoid α) (s : Setoid β) (x : Quotient r × Quotient s),
  (r.prodQuotientEquiv s) x =
    match x with
    | (x, y) => Quotient.map₂ Prod.mk ⋯ x y
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.eq_mk'_of_mul_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} {y : ↥M} {z : R},
  z * ↑y = x → (algebraMap R S) z = IsLocalization.mk' S x y
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instFunLike : (M : Type u_4) → [inst : AddZero M] → FunLike (AddMonoid.End M) M M
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_le_iff_le : ∀ {a b : BitVec 32}, { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The number of square roots of `a` modulo `p` is determined by the Legendre symbol.  -/
legendreSym.card_sqrts : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], p ≠ 2 → ∀ (a : ℤ), ↑{x | x ^ 2 = ↑a}.toFinset.card = legendreSym p a + 1
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.instIsCentralScalar : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} [inst : AddZeroClass A] [inst_1 : AddZeroClass B]
  [inst_2 : DistribSMul M B] [inst_3 : DistribSMul Mᵐᵒᵖ B] [IsCentralScalar M B], IsCentralScalar M (A →+ B)
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.ofFn_eq_sum_monomial : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ} (v : Fin n → R),
  (Polynomial.ofFn n) v = ∑ i, (Polynomial.monomial ↑i) (v i)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
summable_jacobiTheta₂_term_fderiv_iff : ∀ (z τ : ℂ), (Summable fun x => jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im
-- Init.System.FilePath
System.instReprFilePath : Repr System.FilePath
-- Mathlib.Analysis.Complex.JensenFormula
/-- **Jensen's Formula** specialized to the case that `f` is analytic and `f c ≠ 0`.  -/
AnalyticOnNhd.circleAverage_log_norm : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℂ},
  R ≠ 0 →
    AnalyticOnNhd ℂ f (Metric.closedBall c |R|) →
      f c ≠ 0 →
        Real.circleAverage (fun x => Real.log ‖f x‖) c R =
          ∑ᶠ (u : ℂ), ↑((MeromorphicOn.divisor f (Metric.closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
            Real.log ‖f c‖
-- Mathlib.Topology.UniformSpace.Cauchy
TotallyBounded.isCompact_of_isComplete : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, TotallyBounded s → IsComplete s → IsCompact s
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.toRat.match_1.eq_2 : ∀ (motive : Dyadic → Sort u_1) (n : ℤ) (k : ℕ) (hn : n % 2 = 1) (h_1 : Unit → motive Dyadic.zero)
  (h_2 : (n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.ofNat k) hn))
  (h_3 : (n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.negSucc k) hn)),
  (match Dyadic.ofOdd n (Int.ofNat k) hn with
    | Dyadic.zero => h_1 ()
    | Dyadic.ofOdd n (Int.ofNat k) hn => h_2 n k hn
    | Dyadic.ofOdd n (Int.negSucc k) hn => h_3 n k hn) =
    h_2 n k hn
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfMotives : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Init.Data.Float.Float32
instReprAtomFloat32 : ReprAtom Float32
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_symmGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen (Relation.SymmGen r) = Relation.EqvGen r
-- Init.Data.UInt.Lemmas
USize.size_sub_one_mod_uint32Size : (USize.size - 1) % UInt32.size = UInt32.size - 1
-- Mathlib.RingTheory.IsTensorProduct
Algebra.lift_algHom_comp_left : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [inst_11 : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_12 : Semiring A] [inst_13 : Algebra R A] (f : S →ₐ[R] A)
  (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x),
  (Algebra.pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R S S') = f
-- Mathlib.RingTheory.RingHom.Flat
CommRingCat.flat_iff : ∀ {R S : CommRingCat} (f : R ⟶ S), CommRingCat.flat f ↔ (CommRingCat.Hom.hom f).Flat
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lint : Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.StdSimplex.join_single : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (x : Convexity.StdSimplex R M), (Convexity.StdSimplex.single x).join = x
-- Mathlib.NumberTheory.Primorial
primorial_succ : ∀ {n : ℕ}, n ≠ 1 → Odd n → primorial (n + 1) = primorial n
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_real_apply_of_mem_of_mem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∈ s → y ∈ s → (ProbabilityTheory.bernoulliMeasure x y p).real s = 1
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Filter.EventuallyConst.of_not_isCofinal_rangeSplitting : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β} [Nonempty α],
  Monotone f → ¬IsCofinal (Set.range (Set.rangeSplitting f)) → Filter.EventuallyConst f Filter.atTop
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.re_zero : Complex.UnitClosedDisc.re 0 = 0
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_shiftConcat : ∀ {w : ℕ} (x : BitVec w) (b : Bool) (i : ℕ),
  (x.shiftConcat b).getLsbD i = (decide (i < w) && if i = 0 then b else x.getLsbD (i - 1))
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_le_smul : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} {U : X.Opens} [inst_2 : Nonempty ↥↑U],
  x ∈ U →
    ∀ {a : ↑(X.presheaf.obj (Opposite.op U))},
      a ≠ 0 → ∀ (f : ↑X.functionField), AlgebraicGeometry.Scheme.ord f x ≤ AlgebraicGeometry.Scheme.ord (a • f) x
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const.opObjUnop_inv_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : Cᵒᵖ) (j : Jᵒᵖ),
  (CategoryTheory.Functor.const.opObjUnop X).inv.app j =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).leftOp.obj j)
-- Mathlib.Algebra.Order.Group.Synonym
toLex_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : α), toLex (a * b) = toLex a * toLex b
-- Mathlib.Data.Multiset.UnionInter
Multiset.cons_inter_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α), a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqCompletionItem : BEq Lean.Lsp.CompletionItem
-- Mathlib.Data.Set.Image
Set.range_inr : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inr = {x | x.isRight = true}
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.age.eq_1 : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M],
  L.age M = {N | FirstOrder.Language.Structure.FG L ↑N ∧ Nonempty (L.Embedding (↑N) M)}
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousOn.enorm : ∀ {E : Type u_7} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {X : Type u_8} [inst_2 : TopologicalSpace X]
  {f : X → E} {s : Set X}, ContinuousOn f s → ContinuousOn (fun x => ‖f x‖ₑ) s
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalAddMonoidHom_apply : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → AddZeroClass (f i)] (i : I) (g : (i : I) → f i),
  (Pi.evalAddMonoidHom f i) g = g i
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_5.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : Std.IterM Id s.Subslice → Sort u_1) (currPos : s.Pos)
  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitIterator.operating currPos searcher })
  (h_2 : Unit → motive { internalState := String.Slice.SplitIterator.atEnd }),
  (match { internalState := String.Slice.SplitIterator.operating currPos searcher } with
    | { internalState := String.Slice.SplitIterator.operating currPos searcher } => h_1 currPos searcher
    | { internalState := String.Slice.SplitIterator.atEnd } => h_2 ()) =
    h_1 currPos searcher
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult : Type
-- Lean.Elab.DeclModifiers
/-- Declaration visibility modifier. That is, whether a declaration is public or private or inherits its visibility from the outer scope.  -/
Lean.Elab.Visibility : Type
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
/-- The class of morphisms in an abelian category that are epimorphisms
and have an injective kernel.  -/
CategoryTheory.Abelian.epiWithInjectiveKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Abelian C] → CategoryTheory.MorphismProperty C
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.t3_quotient_of_isClosed : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M] [IsClosed ↑S], T3Space (M ⧸ S)
-- Mathlib.Order.UpperLower.Closure
UpperSet.erase_inf_Ici : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {a : α},
  a ∈ s → (∀ b ∈ s, b ≤ a → b = a) → s.erase a ⊓ UpperSet.Ici a = s
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.zero_snd : ∀ {q : ℕ}, 0.2 = 0
-- Lean.Data.PersistentArray
Lean.PersistentArray.foldl : {α : Type u} → {β : Type u_1} → Lean.PersistentArray α → (β → α → β) → β → optParam ℕ 0 → β
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSMul : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_3} →
      {M : Type u_5} → [inst_1 : TopologicalSpace M] → [inst_2 : SMul R M] → [ContinuousConstSMul R M] → SMul R C(α, M)
-- Mathlib.Data.List.Map2
List.zipRight_nil_cons : ∀ {α : Type u} {β : Type v} (b : β) (bs : List β), [].zipRight (b :: bs) = (none, b) :: List.map (fun b => (none, b)) bs
-- Mathlib.Probability.Kernel.Disintegration.Density
/-- Auxiliary lemma for `setIntegral_density`.  -/
ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β},
      MeasurableSet s → ∀ {A : Set γ}, MeasurableSet A → ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor sending an object `X` in the comma category to `X.left`.  -/
CategoryTheory.Comma.fst : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) → CategoryTheory.Functor (CategoryTheory.Comma L R) A
-- Mathlib.Geometry.Euclidean.Projection
/-- The distance between a point and its orthogonal projection to a subspace equals the distance
to that subspace as given by `Metric.infDist`. This is not a `simp` lemma since the simplest form
depends on the context (if any calculations are to be done with the distance, the version with
the orthogonal projection gives access to more lemmas about orthogonal projections that may be
useful).  -/
EuclideanGeometry.dist_orthogonalProjection_eq_infDist : ∀ {𝕜 : 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] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  dist p ↑((EuclideanGeometry.orthogonalProjection s) p) = Metric.infDist p ↑s
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_smul : ∀ {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K),
  a ≠ 0 → Submodule.map (a • f) p = Submodule.map f p
-- Mathlib.RingTheory.NormalClosure
/-- We register this specific instance as a local instance rather than making
`FractionRing.liftAlgebra` a local instance because the latter causes timeouts since
it is too general.
 -/
Ring.instAlgebraFractionRing : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain R] →
          [IsDomain S] → [inst_4 : Algebra R S] → [Module.IsTorsionFree R S] → Algebra (FractionRing R) (FractionRing S)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- The kernel of the norm map on `QuadraticAlgebra R a b` equals
the submonoid of unitary elements.  -/
QuadraticAlgebra.mker_norm_eq_unitary : ∀ {R : Type u_2} {a b : R} [inst : CommRing R], MonoidHom.mker QuadraticAlgebra.norm = unitary (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.nonneg.hasMemOrNegMem : ∀ {H : Type u_2} [inst : AddCommGroup H] [inst_1 : LinearOrder H] [inst_2 : IsOrderedAddMonoid H],
  HasMemOrNegMem (AddGroupCone.nonneg H)
-- Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
/-- For `u : ℤ × ℤ`, this is the complex shape on `ℕ × ℕ`, which
connects `a` to `b` when the equality `a + u = b` holds in `ℤ × ℤ`.  -/
ComplexShape.spectralSequenceNat : ℤ × ℤ → ComplexShape (ℕ × ℕ)
-- Batteries.CodeAction.Misc
/-- Similar to `getElimExprInfo`, but returns the names of binders instead of just the numbers;
intended for code actions which need to name the binders.
 -/
Batteries.CodeAction.getElimExprNames : Lean.Expr → Lean.MetaM (Array (Lean.Name × Array Lean.Name))
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.smul_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ {c : ENNReal}, c ≠ 0 → μ.AbsolutelyContinuous (c • ν)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.State.column : Std.Format.State✝ → ℕ
-- Mathlib.Probability.Independence.Conditional
/-- Two random variables are conditionally independent iff they satisfy the almost sure equality
of conditional expectations `μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧`
for all measurable sets `s` and `t` (see `condIndepFun_iff_condExp_inter_preimage_eq_mul`).
Here, this is phrased with Markov kernels associated to the conditional expectations, and the
almost sure equality is expressed as equality of the composition-product with the measure, which is
equivalent to a.e. equality. See `condIndepFun_iff_map_prod_eq_prod_map_map` for the a.e. equality
version with kernels.

For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`.  -/
ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        (μ.trim hm').compProd ((ProbabilityTheory.condExpKernel μ m').map fun ω => (f ω, g ω)) =
          (μ.trim hm').compProd
            (((ProbabilityTheory.condExpKernel μ m').map f).prod ((ProbabilityTheory.condExpKernel μ m').map g)))
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.compLeft.eq_1 : ∀ {α : Type u_5} {β : Type u_6} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (I : Type u_7),
  f.compLeft I = { toFun := fun h => ⇑f ∘ h, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The graph homomorphism from a smaller graph to a bigger one.  -/
SimpleGraph.Hom.ofLE : {V : Type u_1} → {G₁ G₂ : SimpleGraph V} → G₁ ≤ G₂ → G₁ →g G₂
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisHole : Lean.Options → Bool
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.epsilon_lt_of_neg : ∀ {r : ℝ}, r < 0 → ↑r < Hyperreal.epsilon
-- Mathlib.Topology.Algebra.Valued.WithZeroMulInt
/-- In a `ℤᵐ⁰`-valued ring, powers of `x` tend to zero if `v x ≤ exp (-1)`.  -/
Valued.tendsto_zero_pow_of_le_exp_neg_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Valued R (WithZero (Multiplicative ℤ))] {x : R},
  Valued.v x ≤ WithZero.exp (-1) → Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0)
-- Init.Data.Range.Polymorphic.Fin
Fin.instIsAlwaysFinite_1 : ∀ {n : ℕ}, Std.Rxo.IsAlwaysFinite (Fin n)
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffineHom.isAffine_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsAffineHom f] (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
-- Lean.Expr
/-- Return `true` if `e` contains the specified loose bound variable with index `bvarIdx`.

This operation traverses the expression tree.
 -/
Lean.Expr.hasLooseBVar : Lean.Expr → ℕ → Bool
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_one`. -/
ContinuousLinearMap.coe_one : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ↑1 = 1
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : D} {d d' : C} (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g.mop =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g f
-- Init.Data.SInt.Lemmas
Int8.toInt16_mod : ∀ (a b : Int8), (a % b).toInt16 = a.toInt16 % b.toInt16
-- Lean.Parser.Basic
Lean.Parser.instBEqRecoveryContext : BEq Lean.Parser.RecoveryContext
-- Mathlib.Order.WithBot
WithBot.map₂_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithBot α} {b : WithBot β},
  WithBot.map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
-- Init.Prelude
/-- Apply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.

Examples:
 * `(none : Option Nat).map (· + 1) = none`
 * `(some 3).map (· + 1) = some 4`
 -/
Option.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Option α → Option β
-- Mathlib.Tactic.Ring.Common
/-- If `value` is not an integer, then `hyp` should be a proof of `(value.den : α) ≠ 0`.  -/
Mathlib.Tactic.Ring.RatCoeff.hyp : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.RatCoeff e → Option Lean.Expr