mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.DiscrTree.Util
/-- Apply a function to the array of values at each node in a `DiscrTree`.  -/
Lean.Meta.DiscrTree.mapArrays : {α β : Type} → Lean.Meta.DiscrTree α → (Array α → Array β) → Lean.Meta.DiscrTree β
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_neg_copy : ∀ {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (neg : α) (hi : neg = ↑(-u)),
  ↑(-u.copy val hv neg hi) = neg
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.card_orderOf_eq_totient : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α] [inst_2 : Fintype α] {d : ℕ},
  d ∣ Fintype.card α → {a | orderOf a = d}.card = d.totient
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_toSubmonoid : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), H.op.toSubmonoid = H.op
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.equivalence_join_red : ∀ {α : Type u}, Equivalence (Relation.Join FreeAddGroup.Red)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Finset.measurableSet_biUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β),
  (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋃ b ∈ s, f b)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- If the kernel comparison map for `G` at `f` is an isomorphism, then `G` preserves the
kernel of `f`.
 -/
CategoryTheory.Limits.PreservesKernel.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.kernelComparison f G)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G
-- Mathlib.Geometry.Manifold.Submersion
/-- A choice of complement of the model normed space `E` of `M` in the model normed space
`E'` of `N`  -/
Manifold.IsSubmersion.complement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} → {f : M → N} → Manifold.IsSubmersion I J n f → Type u
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullback_obj_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (A : P.Over Q Y),
  ((CategoryTheory.MorphismProperty.Over.pullback P Q f).obj A).hom = CategoryTheory.Limits.pullback.snd A.hom f
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instMonad : Monad FreeGroup
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.diff m₂).get? k = m₁.get? k
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_trans_self : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂),
  e.symm.trans e = ContinuousLinearEquiv.refl R₂ M₂
-- Batteries.Data.Array.Scan
Array.getElem_scanl : ∀ {β : Type u_1} {α : Type u_2} {i : ℕ} {init : β} {f : β → α → β} {as : Array α}
  (h : i < (Array.scanl f init as).size), (Array.scanl f init as)[i] = Array.foldl f init (as.take i)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Semigroup M] → Semigroup (l.Germ M)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {L₁ L₂ : Filter (E × E)},
  HasFDerivAtFilter f f' L₂ → L₁ ≤ L₂ → HasFDerivAtFilter f f' L₁
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.Topology.Category.TopCat.Basic
_private.Mathlib.Topology.Category.TopCat.Basic.0.TopCat.Hom.mk.sizeOf_spec : ∀ {X Y : TopCat} (hom' : C(↑X, ↑Y)), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Batteries.Tactic.Congr
/-- Repeatedly apply `congr` and `ext`, using the given patterns as arguments for `ext`.

There are two ways this tactic stops:
* `congr` fails (makes no progress), after having already applied `ext`.
* `congr` canceled out the last usage of `ext`. In this case, the state is reverted to before
  the `congr` was applied.

For example, when the goal is
```
⊢ (fun x => f x + 3) '' s = (fun x => g x + 3) '' s
```
then `rcongr x` produces the goal
```
x : α ⊢ f x = g x
```
This gives the same result as `congr; ext x; congr`.

In contrast, `congr` would produce
```
⊢ (fun x => f x + 3) = (fun x => g x + 3)
```
and `congr with x` (or `congr; ext x`) would produce
```
x : α ⊢ f x + 3 = g x + 3
```
 -/
Batteries.Tactic.rcongr : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H`, a morphism of `G`-representations `f : A ⟶ B` induces
a morphism of `H`-representations `(k[H] ⊗[k] A)_G ⟶ (k[H] ⊗[k] B)_G`.  -/
Rep.indMap : {k : Type u} →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] → (φ : G →* H) → {A B : Rep.{u_1, u, v} k G} → (A ⟶ B) → (Rep.ind φ A ⟶ Rep.ind φ B)
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto_eq_prod_pow_floor : ∀ (n : ℕ), n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.coe_inv : ∀ {M : Type u_8} {N : Type u_9} [inst : One M] [inst_1 : InvOneClass N] (f : OneHom M N), ⇑f⁻¹ = (⇑f)⁻¹
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSMulCommClass_1 : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Mul (G i)]
  [inst_5 : (i : ι) → SMul R (G i)] [∀ (i : ι), SMulCommClass (G i) R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)],
  SMulCommClass (DirectLimit G f) R (DirectLimit G f)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.lipschitz : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), LipschitzWith 1 ⇑f
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (d : D), CategoryTheory.IsConnected (CategoryTheory.StructuredArrow d F)) → F.Final
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffAt_zeroSection : ∀ {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {x : B},
  ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.zeroSection F E) x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompLinearEquiv.eq_1 : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : IsTopologicalAddGroup W],
  ContinuousAffineMap.decompLinearEquiv R S V W =
    { toFun := (ContinuousAffineMap.decompEquiv R V W).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := (ContinuousAffineMap.decompEquiv R V W).invFun, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Geometry.Manifold.Submersion
/-- The local property of being a submersion at a point: `f : M → N` is a submersion at `x` if
there exist charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively, such that in these
charts, `f` looks like the projection `(u, v) ↦ u`.
This definition has a fixed parameter `F`, which is a choice of complement of `E''` in the model
normed space `E` of `M`: being a submersion at `x` includes a choice of linear isomorphism
between `E'' × F` and `E`.  -/
Manifold.SubmersionAtProp : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    (F : Type u_5) →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              ModelWithCorners 𝕜 E H →
                                ModelWithCorners 𝕜 E'' G →
                                  (M : Type u_11) →
                                    (N : Type u_13) →
                                      [inst : TopologicalSpace M] →
                                        [inst_9 : TopologicalSpace N] →
                                          (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableOn.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G}, DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun y => ‖f y‖ ^ 2) s
-- Mathlib.CategoryTheory.Localization.Predicate
/-- the isomorphism relating the localization functor and the two other given functors  -/
CategoryTheory.Localization.Lifting.iso : {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} →
        {E : Type u_3} →
          {inst_2 : CategoryTheory.Category.{v_3, u_3} E} →
            (L : CategoryTheory.Functor C D) →
              (W : CategoryTheory.MorphismProperty C) →
                (F : CategoryTheory.Functor C E) →
                  (F' : CategoryTheory.Functor D E) →
                    [self : CategoryTheory.Localization.Lifting L W F F'] → L.comp F' ≅ F
-- Mathlib.Probability.Moments.Basic
/-- **Chernoff bound** on the upper tail of a real random variable.  -/
ProbabilityTheory.measure_ge_le_exp_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ),
  0 ≤ t →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      μ.real {ω | ε ≤ X ω} ≤ Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.mapAlgHom_coe_ringHom : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : Algebra R S₁] [inst_4 : Algebra R S₂] (f : S₁ →ₐ[R] S₂),
  ↑(MvPolynomial.mapAlgHom f) = MvPolynomial.map ↑f
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A Noetherian scheme has a Noetherian underlying topological space.  -/
AlgebraicGeometry.IsNoetherian.noetherianSpace : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X], TopologicalSpace.NoetherianSpace ↥X
-- Lean.Level
Lean.Level.normLtAux : Lean.Level → ℕ → Lean.Level → ℕ → Bool
-- Mathlib.Algebra.Free
FreeSemigroup.length_of : ∀ {α : Type u} (x : α), (FreeSemigroup.of x).length = 1
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.comap_exp_atTop : Filter.comap Real.exp Filter.atTop = Filter.atTop
-- Init.Data.String.Defs
/-- The slice is not degenerate (but it may be empty).  -/
String.Slice.startInclusive_le_endExclusive : ∀ (self : String.Slice), self.startInclusive ≤ self.endExclusive
-- Std.Do.WP.Sound
Std.Do.instWPSoundIdPure : Std.Do.WPSound Id Std.Do.PostShape.pure
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.ediam_range : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕),
  Metric.ediam (Set.range ⇑f) = Metric.ediam Set.univ
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.reflectsLimit_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.ReflectsLimit (F.comp G) H],
  CategoryTheory.Limits.ReflectsLimit G H
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mapsTo_coreflection_coroot : ∀ {ι : 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 : ι),
  Set.MapsTo (⇑(P.coreflection i)) (Set.range ⇑P.coroot) (Set.range ⇑P.coroot)
-- Mathlib.Order.CompleteLattice.Basic
le_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α}, (∀ (i : ι), a ≤ f i) → a ≤ iInf f
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_def : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p : MvPolynomial σ R),
  p.degrees = p.support.sup fun s => Finsupp.toMultiset s
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_map : ∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : NonUnitalNonAssocRing T] (s : NonUnitalSubring R) (g : S →ₙ+* T) (f : R →ₙ+* S),
  NonUnitalSubring.map g (NonUnitalSubring.map f s) = NonUnitalSubring.map (g.comp f) s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forM_eq_forM_toList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'], m.WF → ∀ {f : α × β → m' PUnit.{w + 1}}, forM m f = forM m.toList f
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃L[𝕜] F), HasStrictFDerivAt (⇑iso) (↑iso) x
-- Mathlib.Algebra.Category.Ring.Limits
/-- The flat sections of a functor into `SemiRingCat` form a subsemiring of all sections.  -/
SemiRingCat.sectionsSubsemiring : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) → Subsemiring ((j : J) → ↑(F.obj j))
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.dite : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : (x : α) → Decidable (x ∈ s)] {f : ↑s → β},
  Measurable f →
    ∀ {g : ↑sᶜ → β}, Measurable g → MeasurableSet s → Measurable fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩
-- Mathlib.Algebra.Order.Group.Synonym
toLex_smul' : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α), toLex b • a = b • a
-- Lean.Environment
/-- Enables/disables kernel diagnostics.  -/
Lean.Kernel.Environment.enableDiag : Lean.Kernel.Environment → Bool → Lean.Kernel.Environment
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.piIsoPi_inv_kernel_ι_apply : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : CategoryTheory.Limits.HasProduct Z] (i : ι)
  (x : (i : ι) → ↑(Z i)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i))
      ((CategoryTheory.ConcreteCategory.hom (ModuleCat.piIsoPi Z).inv) x) =
    x i
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.funLike : {M : Type u_4} → {N : Type u_5} → [inst : One M] → [inst_1 : One N] → FunLike (OneHom M N) M N
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {ι : Type u_8} {β : ι → Type u_9} (m : (x : ι) → MeasurableSpace (β x))
  (f : (i : ι) → Ω → β i),
  ProbabilityTheory.Kernel.iIndepFun f κ μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme), AlgebraicGeometry.IsAffineHom (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.root'In.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S N] [inst_8 : IsScalarTower S R N]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S] (i : ι),
  P.root'In S i = (P.corootSpan S).subtype.restrictScalarsRange (Algebra.linearMap S R) ⋯ (P.root' i) ⋯
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_one : ONote.fastGrowing 1 = fun n => 2 * n
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domain_supSpanSingleton : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f : E →ₛₗ.[σ] F) (x : E) (y : F) (hx : x ∉ f.domain), (f.supSpanSingleton x y hx).domain = f.domain ⊔ K ∙ x
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s : Finset β} (b : β),
  s -ᵥ {b} = Finset.image (fun x => x -ᵥ b) s
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.embed_def : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (DividedPowerAlgebra.embed R M) m = DividedPowerAlgebra.dp R 1 m
-- Mathlib.RingTheory.Polynomial.ScaleRoots
/-- **Alias** of `Polynomial.scaleRoots_dvd`. -/
Dvd.dvd.scaleRoots : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R} [NoZeroDivisors R],
  p ∣ q → p.scaleRoots r ∣ q.scaleRoots r
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.IsSheaf.isSeparated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presieve.IsSheaf J P → CategoryTheory.Presieve.IsSeparated J P
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.of_dvd_two : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : M →ₗ[R] M →ₗ[R] R) {x : M} [IsCancelMulZero R] [NeZero 2], (B x) x ∣ 2 → B.IsReflective x
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.isTriangulated : ∀ {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] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions]
  [inst_11 : CategoryTheory.Limits.HasZeroObject D] [inst_12 : CategoryTheory.Preadditive D]
  [inst_13 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_14 : CategoryTheory.Pretriangulated D]
  [L.IsTriangulated] [CategoryTheory.IsTriangulated C], CategoryTheory.IsTriangulated D
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.mk.inj : ∀ {visitedExpr : Lean.ExprSet} {fvarSet : Lean.FVarIdSet} {fvarIds : Array Lean.FVarId} {visitedExpr_1 : Lean.ExprSet}
  {fvarSet_1 : Lean.FVarIdSet} {fvarIds_1 : Array Lean.FVarId},
  { visitedExpr := visitedExpr, fvarSet := fvarSet, fvarIds := fvarIds } =
      { visitedExpr := visitedExpr_1, fvarSet := fvarSet_1, fvarIds := fvarIds_1 } →
    visitedExpr = visitedExpr_1 ∧ fvarSet = fvarSet_1 ∧ fvarIds = fvarIds_1
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.ext_iff : ∀ {R : Type u_1} [inst : NonAssocRing R] {p q : MulRingSeminorm R}, p = q ↔ ∀ (x : R), p x = q x
-- Lean.Elab.Util
Lean.Elab.checkSyntaxNodeKind : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.Name
-- Init.Data.String.PosRaw
String.Pos.Raw.decreaseBy_zero : ∀ {p : String.Pos.Raw}, p.decreaseBy 0 = p
-- Mathlib.Algebra.Order.Star.Basic
mul_star_self_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  (r : R), 0 ≤ r * star r