mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_const_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
  Measurable f → ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Balanced.zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E},
  Balanced 𝕜 s → s.Nonempty → 0 ∈ s
-- Mathlib.Algebra.Ring.Equiv
/-- If a non-unital ring homomorphism has an inverse, it is a ring isomorphism.  -/
RingEquiv.ofNonUnitalRingHom : {R : Type u_4} →
  {S : Type u_5} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        (hom : R →ₙ+* S) →
          (inv : S →ₙ+* R) → inv.comp hom = NonUnitalRingHom.id R → hom.comp inv = NonUnitalRingHom.id S → R ≃+* S
-- Lean.Parser.Basic
Lean.Parser.unicodeSymbolInfo : String → String → Lean.Parser.ParserInfo
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_comp_balance : ∀ {K : Type u_1} [inst : RCLike K] {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → ℝ),
  RCLike.ofReal ∘ Fintype.balance f = Fintype.balance (RCLike.ofReal ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- A monoidal category acts on itself on the left through the tensor product.
 -/
CategoryTheory.MonoidalCategory.selfLeftAction : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategory.MonoidalLeftAction C C
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support has a global minimum.  -/
Continuous.exists_forall_le_of_hasCompactSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [Nonempty β] [inst_5 : Zero α] {f : β → α},
  Continuous f → HasCompactSupport f → ∃ x, ∀ (y : β), f x ≤ f y
-- Batteries.Data.AssocList
Batteries.AssocList.replace.eq_def : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (b : β) (x : Batteries.AssocList α β),
  Batteries.AssocList.replace a b x =
    match x with
    | Batteries.AssocList.nil => Batteries.AssocList.nil
    | Batteries.AssocList.cons k v es =>
      match k == a with
      | true => Batteries.AssocList.cons a b es
      | false => Batteries.AssocList.cons k v (Batteries.AssocList.replace a b es)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.below.matched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) →
        String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1 → Prop}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos}
  (a : String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos)
  (a_1 : String.Slice.Pattern.Model.IsValidRevSearchFrom pat startPos l),
  String.Slice.Pattern.Model.IsValidRevSearchFrom.below a_1 →
    motive startPos l a_1 → String.Slice.Pattern.Model.IsValidRevSearchFrom.below ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rio_eq_self : ∀ {n i : ℕ}, i < n → (*...n).toArray[i]! = i
-- Batteries.Tactic.PrintDependents
/-- If true, an axiom not in the initial list will be considered as marked.  -/
Batteries.Tactic.CollectDependents.State.otherAxiom : Batteries.Tactic.CollectDependents.State → Bool
-- Std.Http.Data.Headers
/-- A structure for managing HTTP headers as key-value pairs.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5
 -/
Std.Http.Headers : Type
-- Lean.Meta.ArgsPacker
/-- Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R₁[x,y]`
and `(z : C) → R₂[z]`, returns an expression of type
```
(x : (A ⊗ B) ⊕ C) → (match x with | .inl (x, y) => R₁[x,y] | .inr R₂[z]
```
 -/
Lean.Meta.ArgsPacker.uncurry : Lean.Meta.ArgsPacker → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.mk : Option Lean.Meta.AbstractMVarsResult →
  Array Lean.Meta.SynthInstance.GeneratorNode →
    Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer) →
      Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry → Lean.Meta.SynthInstance.State
-- Init.Data.Int.DivMod.Lemmas
Int.sign_tmod : ∀ (a b : ℤ), (a.tmod b).sign = if b ∣ a then 0 else a.sign
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed
embedding. Let `e` be a closed embedding of a nonempty topological space `X` into a normal
topological space `Y`. Let `f` be a continuous real-valued function on `X`. Let `t` be a nonempty
convex set of real numbers (we use `OrdConnected` instead of `Convex` to automatically deduce this
argument by typeclass search) such that `f x ∈ t` for all `x`. Then there exists a continuous
real-valued function `g : C(Y, ℝ)` such that `g y ∈ t` for all `y` and `g ∘ e = f`.  -/
ContinuousMap.exists_extension_forall_mem_of_isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y] (f : C(X, ℝ))
  {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected],
  (∀ (x : X), f x ∈ t) → t.Nonempty → Topology.IsClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l → k ∈ List.map Prod.fst l → (m.insertMany l).getKey! k' = k
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- Geck's construction of the Lie algebra associated to a root system with distinguished base.

Note that it is convenient to include `range h` in the Lie span, to make it elementary that it
contains `RootPairing.GeckConstruction.cartanSubalgebra`, and not depend on
`RootPairing.GeckConstruction.lie_e_f_same`.  -/
RootPairing.GeckConstruction.lieAlgebra : {ι : 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} →
                    [P.IsCrystallographic] →
                      (b : P.Base) →
                        [Finite ι] →
                          [IsDomain R] →
                            [CharZero R] →
                              [inst_9 : Fintype ι] →
                                [inst_10 : DecidableEq ι] → LieSubalgebra R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
-- Init.Data.String.Decode
String.toByteArray_utf8EncodeChar_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {c : Char},
  b.utf8DecodeChar? 0 = some c → (String.utf8EncodeChar c).toByteArray = b.extract 0 c.utf8Size
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.sub_modEq_zero : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]
-- Mathlib.RingTheory.Flat.Equalizer
/-- The bilinear map corresponding to `LinearMap.tensorKer`.  -/
LinearMap.tensorKerBil : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f : N →ₗ[R] P) →
                                  M →ₗ[S] ↥f.ker →ₗ[R] ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker
-- Lean.Parser.Term
Lean.Parser.Term.dbgTrace.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.charAlgHom.congr_simp : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e e_1 : AddChar ℝ Circle}
  (e_e : e = e_1) {L L_1 : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (e_L : L = L_1) (he : Continuous ⇑e)
  (hL : Continuous fun p => (L p.1) p.2),
  BoundedContinuousFunction.charAlgHom he hL = BoundedContinuousFunction.charAlgHom ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : C ⥤ᵣ D} (α : F ⟶ G), (CategoryTheory.RightExactFunctor.forget C D).map α = α.hom
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.sq_normThreshold_add_one_le : ∀ {a : ℝ} (n : ℕ), ProbabilityTheory.Fernique.normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)
-- Mathlib.Data.Sign.Defs
sign_nonneg_iff : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : α}, 0 ≤ SignType.sign a ↔ 0 ≤ a
-- Mathlib.Topology.VectorBundle.Constructions
instModulePullback : (R : Type u_1) →
  {B : Type u_3} →
    (E : B → Type u_5) →
      {B' : Type u_6} →
        (f : B' → B) →
          [inst : Semiring R] →
            [inst_1 : (x : B) → AddCommMonoid (E x)] → [i : (x : B) → Module R (E x)] → (x : B') → Module R ((f *ᵖ E) x)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.invariantsResMap_comp : ∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type u_1} {H : Type u_2} [inst_2 : Group G]
  [inst_3 : Group H] {X : TopRep k G} {Y Y' : TopRep k H} (φ : H →* G) (f : TopRep.res φ X ⟶ Y) (g : Y ⟶ Y'),
  TopRep.invariantsResMap φ (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap φ f) ((TopRep.invariantsFunctor k H).map g)
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.withProtectedMCtx.finalize : Lean.Grind.Config → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Ring.Identities
/-- Degen's eight squares identity, see <https://en.wikipedia.org/wiki/Degen%27s_eight-square_identity>.

This sign choice here corresponds to the signs obtained by multiplying two octonions.
 -/
sum_eight_sq_mul_sum_eight_sq : ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R},
  (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
                  (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
                (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
              (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
            (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
          (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
        (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocOLeanEntry.mk.injEq : ∀ (declName : Lean.Name) (post : Bool) (keys : Array Lean.Meta.SimpTheoremKey) (declName_1 : Lean.Name) (post_1 : Bool)
  (keys_1 : Array Lean.Meta.SimpTheoremKey),
  ({ declName := declName, post := post, keys := keys } = { declName := declName_1, post := post_1, keys := keys_1 }) =
    (declName = declName_1 ∧ post = post_1 ∧ keys = keys_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.addHom_ext' : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddZeroClass M] {f g : Polynomial R →+ M},
  (∀ (n : ℕ), f.comp (Polynomial.monomial n).toAddMonoidHom = g.comp (Polynomial.monomial n).toAddMonoidHom) → f = g
-- Plausible.Functions
Plausible.TotalFunction.withDefault.injEq : ∀ {α : Type u} {β : Type v} (a : List ((_ : α) × β)) (a_1 : β) (a_2 : List ((_ : α) × β)) (a_3 : β),
  (Plausible.TotalFunction.withDefault a a_1 = Plausible.TotalFunction.withDefault a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.Int.DivMod.Lemmas
Int.eq_tdiv_of_mul_eq_left : ∀ {a b c : ℤ}, b ≠ 0 → a * b = c → a = c.tdiv b
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.renameSymmetricSubalgebra_apply_coe : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (e : σ ≃ τ)
  (a : ↥(MvPolynomial.symmetricSubalgebra σ R)),
  ↑((MvPolynomial.renameSymmetricSubalgebra e) a) = (MvPolynomial.rename ⇑e) ↑a
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is
injective. Rather, we assume that the images of `f` are disjoint on `I`, and `g ⊥ = 1`. The
conclusion is the same as in `prod_image`.  -/
Finset.prod_image_of_disjoint : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] [inst_2 : PartialOrder ι]
  [inst_3 : OrderBot ι] {f : κ → ι} {g : ι → M},
  g ⊥ = 1 → ∀ {I : Finset κ}, (↑I).PairwiseDisjoint f → ∏ s ∈ Finset.image f I, g s = ∏ i ∈ I, g (f i)
-- Mathlib.Analysis.Distribution.TemperedDistribution
ContinuousLinearMap.toPointwiseConvergenceCLM.congr_simp : ∀ {𝕜₁ : Type u_4} (𝕜₂ : Type u_5) [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7)
  (F : Type u_8) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  [inst_9 : ContinuousSMul 𝕜₁ E] [inst_10 : ContinuousConstSMul 𝕜₂ F],
  ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜₂ σ E F = ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜₂ σ E F
-- Mathlib.Algebra.Algebra.Unitization
Unitization.isSelfAdjoint_inr : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] {a : A},
  IsSelfAdjoint ↑a ↔ IsSelfAdjoint a
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.iIndepSets' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.iIndep m μ → ProbabilityTheory.iIndepSets (fun x => {s | MeasurableSet s}) μ
-- Mathlib.Order.Heyting.Basic
sdiff_le_sdiff_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, b ≤ a → b \ c ≤ a \ c
-- Mathlib.Data.Sym.Sym2
Sym2.diag_isDiag : ∀ {α : Type u_1} (a : α), (Sym2.diag a).IsDiag
-- Mathlib.NumberTheory.Padics.ValuativeRel
Padic.valuation_p_lt_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {Γ₀ : Type u_1} [inst : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation ℚ_[p] Γ₀)
  [v.Compatible], v ↑p < 1
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.copy.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_mul' := ⋯ }
-- Mathlib.Tactic.NormNum.DivMod
/-- The `norm_num` extension which identifies expressions of the form `Int.ediv a b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalIntDiv : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The `k`-th derivative of the Fourier integral of `f`, multiplied by `(L v w) ^ n`, is the
Fourier integral of the `n`-th derivative of `(L v w) ^ k * f`.  -/
VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ) →
      ∀ {k n : ℕ},
        ↑k ≤ K →
          ↑n ≤ N →
            ∀ {w : W},
              VectorFourier.fourierPowSMulRight (-L.flip)
                  (iteratedFDeriv ℝ k
                    (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f))
                  w n =
                VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L)
                  (iteratedFDeriv ℝ n fun v => VectorFourier.fourierPowSMulRight L f v k) w
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.mul_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X X + CategoryTheory.SemiCartesianMonoidalCategory.snd X X
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.IsClosedUnderKernels.kernels_le : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsClosedUnderKernels],
  (CategoryTheory.MorphismProperty.ofObjectProperty P P).kernels ≤ P
-- Mathlib.Logic.Function.Basic
Function.instAsymmSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Asymm r], Std.Asymm (Function.swap r)
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `descPochhammer S n` is nonnegative on `[n-1, ∞)`.  -/
descPochhammer_nonneg : ∀ {S : Type u_1} [inst : Ring S] [inst_1 : PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S},
  ↑n - 1 ≤ s → 0 ≤ Polynomial.eval s (descPochhammer S n)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.linearEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_3) (E : Type u_4) [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E],
  ⇑(WithCStarModule.linearEquiv R A E).symm = ⇑(WithCStarModule.equiv A E).symm
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.collectParamsCore : List Lean.Meta.Grind.TGrind → Lean.CoreM (Bool × Array Lean.Meta.Grind.TParam × Array Lean.Meta.Grind.TParam)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_lt_iff_lt_add'`. -/
sub_left_lt_of_lt_add : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a < b + c → a - b < c
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.Hom.line : {J : Type w} →
  J →
    CategoryTheory.Limits.WalkingParallelFamily.Hom J CategoryTheory.Limits.WalkingParallelFamily.zero
      CategoryTheory.Limits.WalkingParallelFamily.one
-- Mathlib.Algebra.AffineMonoid.Embedding
/-- An arbitrary embedding of an affine monoid `M` into `ℤ ^ dim M`.  -/
AffineAddMonoid.embedding : (M : Type u_1) →
  [inst : AddCancelCommMonoid M] →
    [AddMonoid.FG M] → [IsAddTorsionFree M] → M →+ FreeAbelianGroup (Fin (AffineAddMonoid.dim M))
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsPathConnected (pathComponent x)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_intCast_eq_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ}, ‖↑z‖ = 1 ↔ IsCoprime z ↑p
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (B : C),
  ((CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone F).ι.app (Opposite.op A)).app B =
    TypeCat.ofHom fun f => (CategoryTheory.ConcreteCategory.hom (F.map f)) A.pt
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_dvd_cast : ∀ {α : Type u_3} [inst : Ring α] (m n : ℤ), m ∣ n → ↑m ∣ ↑n
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_limsup_self : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [inst : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.CondIndep m (Filter.limsup s f) (Filter.limsup s f) hm μ
-- Init.Meta.Defs
Lean.Syntax.instReprTSyntax : {ks : Lean.SyntaxNodeKinds} → Repr (Lean.TSyntax ks)
-- Mathlib.CategoryTheory.Pi.Basic
_private.Mathlib.CategoryTheory.Pi.Basic.0.CategoryTheory.Pi.optionEquivalence.match_1.eq_2 : ∀ {J : Type u_1} (motive : Option J → Sort u_2) (i : J) (h_1 : Unit → motive none) (h_2 : (i : J) → motive (some i)),
  (match some i with
    | none => h_1 ()
    | some i => h_2 i) =
    h_2 i
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- **Alias** of `Finset.prod_eq_prod_sdiff_singleton_mul`. -/
Finset.prod_eq_prod_diff_singleton_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M), ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i
-- Mathlib.Algebra.Algebra.Operations
Submodule.le_self_mul_one_div : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {I : Submodule R A}, I ≤ 1 → I ≤ I * (1 / I)
-- Mathlib.Topology.PartitionOfUnity
/-- the functions are each at most one  -/
BumpCovering.le_one' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s),
  self.toFun ≤ 1
-- Mathlib.Algebra.FreeMonoid.Basic
/-- An induction principle for free monoids which mirrors induction on lists, with cases analogous
to the empty list and cons  -/
FreeMonoid.inductionOn' : ∀ {α : Type u_1} {motive : FreeMonoid α → Prop} (a : FreeMonoid α),
  motive 1 → (∀ (b : α) (a : FreeMonoid α), motive a → motive (FreeMonoid.of b * a)) → motive a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t₁ \ t₂).getKeyD k fallback = if k ∈ t₂ then fallback else t₁.getKeyD k fallback
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_prod : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P), ↑(f.prod g) = (↑f).prod ↑g
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- Converts an element of `WithAbs v` to an element of `R`.  -/
WithAbs.ofAbs : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → {v : AbsoluteValue R S} → WithAbs v → R
-- Init.Data.List.ControlImpl
List.flatMapMTR.loop.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x : List (List β)),
  List.flatMapMTR.loop f [] x = pure x.reverse.flatten
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.injective : ∀ {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₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), Function.Injective ⇑e