mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- Coefficients of the truncation of a multivariate power series.  -/
MvPowerSeries.coeff_trunc' : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R),
  MvPolynomial.coeff m ((MvPowerSeries.trunc' R n) φ) = if m ≤ n then (MvPowerSeries.coeff m) φ else 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulZeroOneClass : {M₀ : Type u_1} →
  [inst : TopologicalSpace M₀] →
    [inst_1 : MulZeroOneClass M₀] → [ContinuousMul M₀] → MulZeroOneClass (SeparationQuotient M₀)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- Whiskering commutes with the enriched composition.  -/
CategoryTheory.eComp_eHomWhiskerLeft : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C)
  {Z Z' : C} (g : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.eHomWhiskerLeft V X g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerLeft V Y g))
      (CategoryTheory.eComp V X Y Z')
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (d' : ℕ) (h_1 : Unit → motive 0) (h_2 : (d d' : ℕ) → d = d' + 1 → motive (Int.ofNat d'.succ))
  (h_3 : (d : ℕ) → motive (Int.negSucc d)),
  (match Int.ofNat d'.succ with
    | 0 => h_1 ()
    | Int.ofNat d@hd:d'.succ => h_2 d d' hd
    | Int.negSucc d => h_3 d) =
    h_2 (d' + 1) d' ⋯
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context : Type
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppCasesTrace : Lean.Meta.Grind.M✝ Unit
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have sums `a`, `b` respectively, then
the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has
sum `a + b`.  -/
HasSum.int_rec : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousAdd M] {f g : ℕ → M},
  HasSum f m → HasSum g m' → HasSum (fun t => Int.rec f g t) (m + m')
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Scalar multiplication is smooth (as a function of the scalar variable).  -/
contDiff_smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : Type u_4} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] (v : F), ContDiff 𝕜 n fun a => a • v
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instIsMonoidalForallPi' : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor D ((i : I) → C i)} [inst_4 : F.LaxMonoidal] [inst_5 : G.LaxMonoidal]
  (τ : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ⟶ G.comp (CategoryTheory.Pi.eval C i))
  [∀ (i : I), CategoryTheory.NatTrans.IsMonoidal (τ i)],
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.NatTrans.pi' τ)
-- Lean.Declaration
Lean.ReducibilityHints.isRegular : Lean.ReducibilityHints → Bool
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.essentiallySmallSelf : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.EssentiallySmall.{max w v u, v, u} C
-- Mathlib.NumberTheory.Real.Irrational
irrational_ratCast_sub_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (↑q - x) ↔ Irrational x
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.apply_one : ∀ (R : Type u_1) [inst : NonAssocRing R] [inst_1 : DecidableEq R] [inst_2 : NoZeroDivisors R] [inst_3 : Nontrivial R]
  (x : R), 1 x = if x = 0 then 0 else 1
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.iSupLift.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {ι : Type u_4} [inst_5 : Nonempty ι] (K : ι → Subalgebra R A)
  (dir : Directed (fun x1 x2 => x1 ≤ x2) K) (f f_1 : (i : ι) → ↥(K i) →ₐ[R] B) (e_f : f = f_1)
  (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)) (T : Subalgebra R A) (hT : T ≤ iSup K),
  Subalgebra.iSupLift K dir f hf T hT = Subalgebra.iSupLift K dir f_1 ⋯ T hT
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.retracts_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [Q.IsStableUnderRetracts], P.retracts ≤ Q ↔ P ≤ Q
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.instDiscreteUniformity : ∀ {α : Type u_1} [inst : UniformSpace α] [DiscreteUniformity α], DiscreteUniformity (TopologicalSpace.Compacts α)
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.newLocalDecls : Lean.Elab.Term.MutualClosure.ClosureState → Array Lean.LocalDecl
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ n` is integrable for all `n : ℕ`.  -/
ProbabilityTheory.integrable_pow_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) → ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => X ω ^ n) μ
-- Std.Http.Protocol.H1
/-- Convenience helper for the common malformed-message failure path.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.failBadMessage : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Computability.StateTransition
/-- A variation on `Reaches`. `Reaches₀ f a b` holds if whenever `Reaches₁ f b c` then
`Reaches₁ f a c`. This is a weaker property than `Reaches` and is useful for replacing states with
equivalent states without taking a step.  -/
StateTransition.Reaches₀ : {σ : Type u_1} → (σ → Option σ) → σ → σ → Prop
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_ne_zero : ∀ {α : Type u} [inst : Preorder α] [h : Nonempty α], Order.cof α ≠ 0
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordMonoidHom.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R],
  Ring.ordMonoidHom = Ring.ordMonoidHom
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.lift_ι_apply : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : X → A) (x : X), ((FreeAlgebra.lift R) f) (FreeAlgebra.ι R x) = f x
-- Init.Data.SInt.Lemmas
ISize.toBitVec_toInt16 : ∀ (x : ISize), x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
-- Lean.Declaration
Lean.DefinitionSafety.partial.sizeOf_spec : sizeOf Lean.DefinitionSafety.partial = 1
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.congrLeft_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y)
  (g : LocallyConstant Y Z), (LocallyConstant.congrLeft e).symm g = LocallyConstant.comap (↑e) g
-- Lean.Parser.Syntax
Lean.Parser.Syntax.nonReserved.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofInv.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s s_1 : Y ⟶ X) (e_s : s = s_1) (hs : W s),
  CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs = CategoryTheory.MorphismProperty.LeftFraction.ofInv s_1 ⋯
-- Mathlib.Data.Finsupp.Single
Finsupp.support_eq_singleton' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, f.support = {a} ↔ ∃ b, b ≠ 0 ∧ f = fun₀ | a => b
-- Init.Data.List.Basic
/-- Checks whether the first list is a prefix of the second.

The relation `List.IsPrefixOf` expresses this property with respect to logical equality.

Examples:
* `[1, 2].isPrefixOf [1, 2, 3] = true`
* `[1, 2].isPrefixOf [1, 2] = true`
* `[1, 2].isPrefixOf [1] = false`
* `[1, 2].isPrefixOf [1, 1, 2, 3] = false`
 -/
List.isPrefixOf : {α : Type u} → [BEq α] → List α → List α → Bool
-- Mathlib.Topology.Constructions
isClosed_range_sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, IsClosed (Set.range (Sigma.mk i))
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.hom₂_ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x y : a ⟶ b}
  {f g : x ⟶ y}, f = g ↔ f.iso.hom = g.iso.hom
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.MatchResult.push.loop : {α : Type} → ℕ → Array α → Array (Array (Array α)) → Lean.Meta.LazyDiscrTree.MatchResult α
-- Init.Data.Repr
/-- Converts a natural number less than `10` to the corresponding Unicode subscript digit character.
Returns `'*'` for other numbers.

Examples:
* `Nat.subDigitChar 3 = '₃'`
* `Nat.subDigitChar 7 = '₇'`
* `Nat.subDigitChar 10 = '*'`
 -/
Nat.subDigitChar : ℕ → Char
-- Mathlib.Algebra.Quandle
Quandle.instDihedral : (n : ℕ) → Quandle (Quandle.Dihedral n)
-- Lean.Data.Lsp.Internal
/-- Version of the file these imports are from.  -/
Lean.Lsp.LeanILeanHeaderSetupInfoParams.version : Lean.Lsp.LeanILeanHeaderSetupInfoParams → ℕ
-- Init.Data.Slice.Array.Iterator
Array.instAppendSubarray : {α : Type u} → Append (Subarray α)
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- For every `W` with a morphism `e : Y ⟶ W` that coequalizes every pair of morphisms
`g₁ g₂ : Z ⟶ Y` which `f` coequalizes, `desc e h` is a morphism `X ⟶ W`...
 -/
CategoryTheory.EffectiveEpiStruct.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f : Y ⟶ X} →
        CategoryTheory.EffectiveEpiStruct f →
          {W : C} →
            (e : Y ⟶ W) →
              (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
                  CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
                    CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
                (X ⟶ W)
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.coe_mem_cutMap_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : DivisionRing β] {a : α} {q : ℚ}
  [CharZero β], ↑q ∈ LinearOrderedField.cutMap β a ↔ ↑q < a
-- Mathlib.Algebra.Homology.CochainComplexOpposite
ComplexShape.embeddingUpIntDownInt_f : ∀ (n : ℤ), ComplexShape.embeddingUpIntDownInt.f n = -n
-- Mathlib.Computability.Partrec
Computable.sumCasesOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ},
  Computable f → Computable₂ g → Computable₂ h → Computable fun a => Sum.casesOn (f a) (g a) (h a)
-- Mathlib.CategoryTheory.Comma.Arrow
/-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories.  -/
CategoryTheory.Functor.mapArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow D)
-- Mathlib.Algebra.Lie.TraceForm
LieIdeal.coe_killingCompl_top : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (LieIdeal.toLieSubalgebra R L (LieIdeal.killingCompl R L ⊤)).toSubmodule = LinearMap.ker (killingForm R L)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] (X : B),
  P.fullsubcategory.mapId X = CategoryTheory.Cat.Hom.isoMk (P.mapId X)
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.continuous_lift : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
  {f : X → Y} (hf : Continuous f), Continuous (T2Quotient.lift hf)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.empty : ∀ {𝕜 : 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} {x : E}, HasFDerivWithinAt f f' ∅ x
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
/-- **Alias** of `CategoryTheory.FunctorToTypes.rightAdj`.

---

A right adjoint of `tensorLeft F`.  -/
CategoryTheory.FunctorToTypes.rightAdj_map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor C (Type (max w v u)) →
      CategoryTheory.Functor (CategoryTheory.Functor C (Type (max w v u))) (CategoryTheory.Functor C (Type (max w v u)))
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkPatternFromType : List Lean.Name → Lean.Expr → Option ℕ → Lean.MetaM Lean.Meta.Sym.Pattern
-- Mathlib.Topology.Separation.Basic
IsCompact.closure_eq_biUnion_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K : Set X},
  IsCompact K → closure K = ⋃ x ∈ K, {y | Inseparable x y}
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.zero_zeroAtFilter : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero β] [inst_1 : TopologicalSpace β] (l : Filter α), l.ZeroAtFilter 0
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.mk.injEq : ∀ (name : String) (type? docString? doc_url? kind? : Option String) (name_1 : String)
  (type?_1 docString?_1 doc_url?_1 kind?_1 : Option String),
  ({ name := name, type? := type?, docString? := docString?, doc_url? := doc_url?, kind? := kind? } =
      { name := name_1, type? := type?_1, docString? := docString?_1, doc_url? := doc_url?_1, kind? := kind?_1 }) =
    (name = name_1 ∧ type? = type?_1 ∧ docString? = docString?_1 ∧ doc_url? = doc_url?_1 ∧ kind? = kind?_1)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.commGroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : CommGroup β],
  e.commGroup = Function.Injective.commGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Lean.Parser.Command
Lean.Parser.Command.synth.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Gives the connected component containing a particular vertex.  -/
SimpleGraph.connectedComponentMk : {V : Type u} → (G : SimpleGraph V) → V → G.ConnectedComponent
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km → t.getKey? km = some km
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- An oracle that uses Fourier-Motzkin elimination.  -/
Mathlib.Tactic.Linarith.CertificateOracle.fourierMotzkin : Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe.eq_1 : ∀ {α : Type u}, WithOne.coe = some
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Extract the left and right-hand sides of an equality or iff statement.  -/
Mathlib.Tactic.LibraryRewrite.eqOrIff? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t[k]? = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ t.toArray
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.closedCounit_app_app : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F G : CategoryTheory.Functor D C) (X : D),
  (F.closedCounit.app G).app X = (CategoryTheory.ihom.ev (F.obj X)).app (G.obj X)
-- Init.Data.SInt.Bitwise
Int64.not_ne_self : ∀ {a : Int64}, ~~~a ≠ a
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.UnusedSimpArgsInfo.mk.injEq : ∀ (mask mask_1 : Array Bool), ({ mask := mask } = { mask := mask_1 }) = (mask = mask_1)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
CategoryTheory.Under.instHasFiniteColimitsOfHasFiniteWidePushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasFiniteWidePushouts C],
  CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Under B)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.decidableNonneg : {d : ℕ} → (a : ℤ√↑d) → Decidable a.Nonneg
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
abs_dist_sub_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), |dist x z - dist y z| ≤ dist x y
-- Mathlib.Algebra.Ring.Parity
Odd.one_add : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd a → Even (1 + a)
-- Init.Data.Array.Lemmas
Array.map_flatten : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xss : Array (Array α)},
  Array.map f xss.flatten = (Array.map (Array.map f) xss).flatten
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.instMonoidalCategory : CategoryTheory.MonoidalCategory AugmentedSimplexCategory
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.id_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (X : CategoryTheory.Grothendieck F), (CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom ⋯
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Alias** of `intervalIntegral.integral_deriv_smul_comp`.

---

Change of variables, most common version. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous, then we can substitute `u = f x` to get
`∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_comp_smul_deriv : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) → Continuous g → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.comp_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom₁ = CategoryTheory.CategoryStruct.comp f.hom₁ g.hom₁
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- `cfc` is continuous in the variable `a : A` when `s : Set 𝕜` is compact and `a` varies over
elements whose spectrum is contained in `s`, all of which satisfy the predicate `p`, and the
function `f` is continuous on the spectrum of `a`.  -/
Continuous.cfc' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [inst_6 : TopologicalSpace X] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A},
      Continuous a →
        (∀ (x : X), spectrum 𝕜 (a x) ⊆ s) →
          autoParam (ContinuousOn f s) Continuous.cfc'._auto_1 →
            autoParam (∀ (x : X), p (a x)) Continuous.cfc'._auto_3 → Continuous fun x => cfc f (a x)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R),
  (p * q).support ⊆ p.support + q.support
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCone.inr φ = HomologicalComplex.homotopyCofiber.inr φ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_iff_forall_mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.BalancedSz.symm : ∀ {l r : ℕ}, Ordnode.BalancedSz l r → Ordnode.BalancedSz r l
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instCore : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Presentation R S ι σ} → Algebra P.Core R
-- Mathlib.Algebra.Group.Units.Equiv
/-- Right multiplication in a `Group` is a permutation of the underlying type.  -/
Equiv.mulRight : {G : Type u_5} → [Group G] → G → Equiv.Perm G
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_sInf : ∀ {α : Type u_1} [inst : LE α] (S : Set (UpperSet α)), (sInf S).compl = ⨅ s ∈ S, s.compl
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_False : Set.Ioi False = {True}
-- Init.Data.Array.Lex.Lemmas
Array.le_iff_exists : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs ys : Array α},
  xs ≤ ys ↔
    xs = ys.take xs.size ∨
      ∃ i, ∃ (h₁ : i < xs.size) (h₂ : i < ys.size), (∀ (j : ℕ) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_π_zero : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨0, SSet.horn₃₁.desc.multicofork_π_zero._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 0).inv f₀
-- Mathlib.Data.Rat.Floor
Rat.isNat_intFloor : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat ⌊r⌋ m
-- Mathlib.LinearAlgebra.Span.Defs
/-- A variant of `span_induction` that combines `∀ x ∈ s, p x` and `∀ r x, p x → p (r • x)`
into a single condition `∀ r, ∀ x ∈ s, p (r • x)`, which can be easier to verify.  -/
Submodule.closure_induction : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {p : (x : M) → x ∈ Submodule.span R s → Prop},
  p 0 ⋯ →
    (∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) →
      (∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯) → ∀ {x : M} (hx : x ∈ Submodule.span R s), p x hx