mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_comp : ∀ {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 : CategoryTheory.Functor C D)
  {G H K : CategoryTheory.Functor D E} (α : G ⟶ H) (β : H ⟶ K),
  F.whiskerLeft (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (F.whiskerLeft α) (F.whiskerLeft β)
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.State.mk.inj : ∀ {items items_1 : Array Lean.Lsp.ResolvableCompletionItem}, { items := items } = { items := items_1 } → items = items_1
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (G : Type u)
  [inst_9 : TopologicalSpace G] [inst_10 : ChartedSpace H G] [inst_11 : Group G] [inst_12 : LieGroup I (↑⊤) G],
  smoothSheafGroup IM I M G = { obj := smoothPresheafGroup IM I M G, property := ⋯ }
-- Mathlib.Topology.Sets.VietorisTopology
/-- When `Set` is equipped with the Vietoris topology, taking the image under an inducing map is
inducing.  -/
Topology.IsInducing.image_vietoris : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsInducing f → Topology.IsInducing fun x => f '' x
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_norm_pow_of_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {p q : ℕ},
      p ≤ q → MeasureTheory.Integrable (fun x => ‖f x‖ ^ q) μ → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ
-- Mathlib.Algebra.Order.Field.Basic
le_inv_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a ≤ b⁻¹ ↔ b ≤ a⁻¹)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.mk : List Lean.Name →
  Bool →
    Array Lean.Expr →
      Array Lean.Expr →
        Lean.FVarIdMap ℕ →
          Array Lean.Expr → Array Lean.Name → Array Lean.Name → Array Lean.Name → Lean.Meta.IndPredBelow.Context✝
-- Mathlib.MeasureTheory.VectorMeasure.AddContent
/-- Consider an additive content `m ` on a semi-ring of sets `C`, which is dominated by a finite
measure `μ`. Assume that `C` generates the sigma-algebra.
Then `m` extends to a countably additive vector measure which is dominated by `μ`.  -/
MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom : ∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)} {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetSemiring C →
    (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) →
      hα = MeasurableSpace.generateFrom C → ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.instIsManifoldtransContinuousLinearEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) [IsManifold I n M],
  IsManifold (I.transContinuousLinearEquiv e) n M
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_iff_monotone_get`. -/
Monotone.sortedLE : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], Monotone l.get → l.SortedLE
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_one : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddZeroClass G] [inst_2 : One G]
  [inst_3 : Add H] [AddConstMapClass F G H 1 b] (f : F), f 1 = f 0 + b
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt32.beq_eq_decide_eq : ∀ {a b : UInt32}, (a == b) = decide (a = b)
-- Batteries.Data.Stream
/-- Read up to `n` values from the stream `s` as a list from first to last.  -/
Std.Stream.take : {σ : Type u_1} → {α : Type u_2} → [Std.Stream σ α] → σ → ℕ → List α × σ
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map'_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {lc : Filter γ} (F : (α → β) → γ → δ)
  (hF : Relator.LiftFun l.EventuallyEq lc.EventuallyEq F F) (f : α → β), Filter.Germ.map' F hF ↑f = ↑(F f)
-- Mathlib.FieldTheory.IsPerfectClosure
sub_mem_pNilradical_iff_pow_expChar_pow_eq : ∀ {R : Type u_1} [inst : CommRing R] {p : ℕ} [ExpChar R p] {x y : R},
  x - y ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = y ^ p ^ n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.whiskering_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D),
  (CategoryTheory.SimplicialObject.Augmented.whiskering C D).obj F =
    CategoryTheory.SimplicialObject.Augmented.whiskeringObj C D F
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.OrderedFinpartition.extend.match_1.eq_2 : ∀ {n : ℕ} (c : OrderedFinpartition n) (motive : Option (Fin c.length) → Sort u_1) (i : Fin c.length)
  (h_1 : Unit → motive none) (h_2 : (i : Fin c.length) → motive (some i)),
  (match some i with
    | none => h_1 ()
    | some i => h_2 i) =
    h_2 i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_inter_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₂.contains k = false → Std.DHashMap.Internal.Raw₀.Const.getD (m₁.inter m₂) k fallback = fallback
-- Mathlib.Data.EReal.Operations
EReal.add_lt_add_of_lt_of_le' : ∀ {x y z t : EReal}, x < y → z ≤ t → t ≠ ⊥ → (t = ⊤ → z = ⊤ → x = ⊥) → x + z < y + t
-- Std.Http.Protocol.H1.Parser
/-- Checks if a byte may appear inside a field value.

This parser enforces strict ASCII-only field values and allows only `field-content`
(`HTAB / SP / VCHAR`).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.isFieldVChar : UInt8 → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Summable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α)
  (L : SummationFilter β), Summable f L = ∃ a, HasSum f a L
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- **Parseval's identity** for inner products: for `L²` functions `f, g` on `UnitAddTorus d`, the
inner product of the Fourier coefficients of `f` and `g` is the inner product of `f` and `g`.  -/
UnitAddTorus.hasSum_prod_mFourierCoeff : ∀ {d : Type u_1} [inst : Fintype d] (f g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)),
  HasSum (fun i => (starRingEnd ℂ) (UnitAddTorus.mFourierCoeff (↑↑f) i) * UnitAddTorus.mFourierCoeff (↑↑g) i)
    (∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑f t) * ↑↑g t)
-- Std.Sat.AIG.Basic
/-- The circuit itself as an `Array Decl` whose members have indices into said array.
 -/
Std.Sat.AIG.decls : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG α → Array (Std.Sat.AIG.Decl α)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map.congr_simp : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] (f f_1 : Γ₀ →*₀ Γ'₀) (e_f : f = f_1) (hf : Monotone ⇑f)
  (v v_1 : Valuation R Γ₀), v = v_1 → Valuation.map f hf v = Valuation.map f_1 ⋯ v_1
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_int64ToBitVec : ∀ (x : Int64), ISize.ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.cechNerve_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (f : CategoryTheory.Arrow C), CategoryTheory.SimplicialObject.cechNerve.obj f = f.cechNerve
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_or`. -/
Set.setOf_or : ∀ {α : Type u} {p q : α → Prop}, {a | p a ∨ q a} = {a | p a} ∪ {a | q a}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_volume : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ),
  MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) =
    ↑(NumberField.mixedEmbedding.convexBodySumFactor K) * ENNReal.ofReal B ^ Module.finrank ℚ K
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
/-- A morphism of schemes is surjective if the underlying map is.  -/
AlgebraicGeometry.Surjective : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_indicator_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Zero β] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    (MeasureTheory.AEStronglyMeasurable (s.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.card_filter : ∀ {ι : Type u_1} (p : ι → Prop) [inst : DecidablePred p] (s : Finset ι),
  {i ∈ s | p i}.card = ∑ i ∈ s, if p i then 1 else 0
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.braiding_hom_apply : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (m : ↑M) (n : ↑N),
  (CategoryTheory.ConcreteCategory.hom (β_ M N).hom) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLEQuarter : LE Std.Time.Month.Quarter
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.id_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  (a : Y), Topology.ContinuousMapGeneratedBy.id a = id a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P 2 = 0 → W'.addX P Q = (P 0 * Q 2) ^ 2 * Q 0
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensorFreeToFinsupp.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (α : Type u) [inst_2 : DecidableEq α],
  A.coinvariantsTensorFreeToFinsupp α =
    ↑(((A.ρ.tprod (Representation.leftRegular k G)).coinvariantsFinsuppLEquiv α).trans
          (Finsupp.lcongr (Equiv.refl α) A.ρ.coinvariantsTprodLeftRegularLEquiv)) ∘ₗ
      Representation.Coinvariants.map (CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.free k G α)).ρ
        ((A.ρ.tprod (Representation.leftRegular k G)).finsupp α)
        ↑(A.ρ.finsuppTensorRight (Representation.leftRegular k G) α)
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectOutput.below.indirect : ∀ {α β : Type w} [inst : Std.Iterator α Id β]
  {motive : (a : Std.Iter β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} {it it' : Std.Iter β} {out : β}
  (a : it'.IsPlausibleSuccessorOf it) (a_1 : it'.IsPlausibleIndirectOutput out),
  Std.Iter.IsPlausibleIndirectOutput.below a_1 → motive it' out a_1 → Std.Iter.IsPlausibleIndirectOutput.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_μ_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.LaxMonoidal] [inst_9 : G.LaxMonoidal] (X Y : C × E),
  (CategoryTheory.Functor.LaxMonoidal.μ (F.prod G) X Y).1 = CategoryTheory.Functor.LaxMonoidal.μ F X.1 Y.1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_lt_of_lt_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulStrictMono α],
  0 < a → b < 1 → a * b < a
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instMonoidalForget : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) → [inst_1 : Monoid G] → [inst_2 : CategoryTheory.MonoidalCategory V] → (Action.forget V G).Monoidal
-- Init.System.FilePath
/-- Normalizes a path, returning an equivalent path that may better follow platform conventions.

In particular:
* On Windows, drive letters are made uppercase.
* On platforms that support multiple path separators (that is, where
  `System.FilePath.pathSeparators` has length greater than one), alternative path separators are
  replaced with the preferred path separator.

There is no guarantee that two equivalent paths normalize to the same path.
 -/
System.FilePath.normalize : System.FilePath → System.FilePath
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- a family of functors `C ⥤ D` indexed by the elements of the additive monoid `A`  -/
CategoryTheory.SingleFunctors.functor : {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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              CategoryTheory.SingleFunctors C D A → A → CategoryTheory.Functor C D
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- Specialization of `ContinuousLinearMap.postcomp_uniformConvergenceCLM` to compact
convergence.  -/
ContinuousLinearMap.postcompCompactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    (E : Type u_4) →
                      {F : Type u_5} →
                        {G : Type u_6} →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            [inst_13 : IsTopologicalAddGroup F] →
                                              [inst_14 : IsTopologicalAddGroup G] →
                                                [inst_15 : ContinuousConstSMul 𝕜₃ G] →
                                                  [inst_16 : ContinuousConstSMul 𝕜₂ F] →
                                                    (F →SL[τ] G) →
                                                      CompactConvergenceCLM σ E F →SL[τ] CompactConvergenceCLM ρ E G
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.instLineDerivLeftSMulReal : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E], LineDerivLeftSMul ℝ E (SchwartzMap E F) (SchwartzMap E F)
-- Mathlib.Logic.Function.Basic
Function.Surjective.forall₂ : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
  Function.Surjective f → ∀ {p : β → β → Prop}, (∀ (y₁ y₂ : β), p y₁ y₂) ↔ ∀ (x₁ x₂ : α), p (f x₁) (f x₂)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanPrepareModuleHierarchyParams : Lean.ToJson Lean.Lsp.LeanPrepareModuleHierarchyParams
-- Lean.Elab.Tactic.Config
/-- Interprets the `config` as an array of option/value pairs.  -/
Lean.Elab.Tactic.mkConfigItemViews : Lean.TSyntaxArray `Lean.Parser.Tactic.configItem → Array Lean.Elab.Tactic.ConfigItemView
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.ext_of_isThin_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {n : SimplexCategoryᵒᵖ}
  {x y : (CategoryTheory.nerve C).obj n}, x = y ↔ x.obj = y.obj
-- Init.Data.Repr
Bool.repr : Bool → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.nonsingular_mul_iff : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] [IsCancelAdd R]
  {A B : Matrix n n R}, (A * B).Nonsingular ↔ A.Nonsingular ∧ B.Nonsingular
-- Mathlib.Order.Filter.Pointwise
Filter.add_pure : ∀ {α : Type u_2} [inst : Add α] {f : Filter α} {b : α}, f + pure b = Filter.map (fun x => x + b) f
-- Mathlib.Data.Quot
/-- Recursion/induction principle for `Trunc`.  -/
Trunc.rec : {α : Sort u_1} →
  {C : Trunc α → Sort u_3} → (f : (a : α) → C (Trunc.mk a)) → (∀ (a b : α), ⋯ ▸ f a = f b) → (q : Trunc α) → C q
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In a canonically-ordered monoid, a product bounds each of its terms.

See also `Finset.single_le_prod'`.  -/
Finset.single_le_prod_of_canonicallyOrdered : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedMul M] {f : ι → M}
  {s : Finset ι} {i : ι}, i ∈ s → f i ≤ ∏ j ∈ s, f j
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂_coe_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithOne α) (b : β),
  WithOne.map₂ f a ↑b = WithOne.map (fun x => f x b) a
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `f : α → β` sends the measure `μa` to `μb` and `g : γ → δ` sends the measure `μc` to `μd`,
then `Prod.map f g` sends `μa.prod μc` to `μb.prod μd`.  -/
MeasureTheory.MeasurePreserving.prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {δ : Type u_4} [inst_3 : MeasurableSpace δ] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ}
  [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : α → β} {g : γ → δ},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasureTheory.MeasurePreserving g μc μd → MeasureTheory.MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_restrict : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  v.IsEquiv v.restrict
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_top : ∀ {V : Type u} {G : SimpleGraph V}, ⊤.spanningCoe = G
-- Lean.Parser.Do
Lean.Parser.Term.termUnless.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.limit.lift_π_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
  (j : J) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F_1]
  (x : carrier c.pt),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift F c)) x) =
    (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_singleton_zero : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.zeroLocus 𝒜 {0} = Set.univ
-- Batteries.Data.UInt
UInt32.le_iff_toNat_le_toNat : ∀ {x y : UInt32}, x ≤ y ↔ x.toNat ≤ y.toNat
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight.mk.injEq : ∀ (range : Lean.Lsp.Range) (kind? : Option Lean.Lsp.DocumentHighlightKind) (range_1 : Lean.Lsp.Range)
  (kind?_1 : Option Lean.Lsp.DocumentHighlightKind),
  ({ range := range, kind? := kind? } = { range := range_1, kind? := kind?_1 }) = (range = range_1 ∧ kind? = kind?_1)
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.coe_pow : ∀ {M : Type u_5} [inst : Monoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] {S : A} (x : ↥S)
  (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Lean.LoadDynlib
Lean.instNonemptyDynlib : Nonempty Lean.Dynlib
-- Mathlib.Topology.Algebra.Monoid
continuousMul_induced : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] [inst_4 : TopologicalSpace N] [ContinuousMul N] (f : F), ContinuousMul M
-- Mathlib.FieldTheory.JacobsonNoether
/-- If `D` is a purely inseparable extension of `k` of characteristic `p`,
then for every element `a` of `D \ k`, there exists a natural number `m`
greater than 0 such that `(a * x - x * a) ^ n = 0` (as linear maps) for
every `n` greater than `(p ^ m)`.  -/
JacobsonNoether.exist_pow_eq_zero_of_le : ∀ {D : Type u_1} [inst : DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [hchar : ExpChar D p]
  {a : D},
  a ∉ Subring.center D →
    (∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) →
      ∃ m, 1 ≤ m ∧ ∀ (n : ℕ), p ^ m ≤ n → (⇑((LieAlgebra.ad (↥(Subring.center D)) D) a))^[n] = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimit_iff_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  {F G : CategoryTheory.Functor C D} (h : F ≅ G),
  CategoryTheory.Limits.PreservesColimit K F ↔ CategoryTheory.Limits.PreservesColimit K G
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination.eq_1 : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : α → M), Finsupp.linearCombination R v = (Finsupp.lsum ℕ) fun i => LinearMap.id.smulRight (v i)
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.toPermHom_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) (k : ↥(Subgroup.centralizer {g}))
  (c : ↥g.cycleFactorsFinset), ((Equiv.Perm.OnCycleFactors.toPermHom g) k) c = k • c
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.mem_extremePoints_measure_univ_eq : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ],
  Ergodic f μ → μ ∈ Set.extremePoints ENNReal {ν | MeasureTheory.MeasurePreserving f ν ν ∧ ν Set.univ = μ Set.univ}
-- Lean.Level
_private.Lean.Level.0.Lean.Level.accMax : Lean.Level → Lean.Level → ℕ → Lean.Level
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.instInhabitedGrwKey.default : Mathlib.Tactic.ClickSuggestions.GrwKey