mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsUnit.cfcNNRpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (y : NNReal),
  IsUnit a → y ≠ 0 → autoParam (0 ≤ a) IsUnit.cfcNNRpow._auto_1 → IsUnit (a ^ y)
-- Init.Data.Nat.Lemmas
Nat.lt_mul_div_self_add : ∀ {x k : ℕ}, 0 < k → x < k * (x / k) + k
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Fintype J] (X : C) (f : J → C),
  (CategoryTheory.leftDistributor X f).hom =
    ∑ j,
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j))
        (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j)
-- Init.Prelude
Char.ne_of_val_ne : ∀ {c d : Char}, ¬c.val = d.val → ¬c = d
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.trivialOn_vertexSet : ∀ {α : Type u_1} (f : Set α), (Hypergraph.trivialOn f).vertexSet = f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg.sizeOf_spec : sizeOf Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg = 1
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteLimits C] (k : K),
  CategoryTheory.Limits.PreservesFiniteLimits ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul : ∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) → MeasureTheory.eLpNormEssSup f μ ≤ c • MeasureTheory.eLpNormEssSup g μ
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_injective : ∀ {R : Type u_2} [inst : NonAssocRing R], Function.Injective Subring.op
-- Mathlib.Analysis.ConstantSpeed
hasConstantSpeedOnWith_iff_ordered : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal},
  HasConstantSpeedOnWith f s l ↔
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Set.Icc x y) = ENNReal.ofReal (↑l * (y - x))
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- The dirac outer measure.  -/
MeasureTheory.OuterMeasure.dirac : {α : Type u_1} → α → MeasureTheory.OuterMeasure α
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly.map : ∀ {p : ℕ} {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  {f : ⦃R : Type u⦄ → [CommRing R] → WittVector p R → WittVector p R},
  WittVector.IsPoly p f → ∀ (g : R →+* S) (x : WittVector p R), (WittVector.map g) (f x) = f ((WittVector.map g) x)
-- Mathlib.Data.PFun
/-- `PFun α β`, or `α →. β`, is the type of partial functions from
`α` to `β`. It is defined as `α → Part β`.  -/
PFun : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalNonAssocCommSemiringQuotient : {R : Type u_1} → [inst : NonUnitalNonAssocCommSemiring R] → (c : RingCon R) → NonUnitalNonAssocCommSemiring c.Quotient
-- Init.Data.List.TakeDrop
List.rotateLeft.eq_1 : ∀ {α : Type u} (xs : List α) (i : ℕ),
  xs.rotateLeft i =
    if xs.length ≤ 1 then xs
    else
      have i := i % xs.length;
      have ys := List.take i xs;
      have zs := List.drop i xs;
      zs ++ ys
-- Mathlib.Condensed.TopComparison
topCatToSheafCompHausLike_obj : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X : TopCat), (topCatToSheafCompHausLike P hs).obj X = TopCat.toSheafCompHausLike P X hs
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_eq_of_le : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} {g : Γ},
  g ∈ x.support → (∀ g' ∈ x.support, g ≤ g') → x.orderTop = ↑g
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.sInter : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] {s : Set (Set α)},
  (∀ x ∈ s, DirSupClosedOn D x) → DirSupClosedOn D (⋂₀ s)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_pure_elim_cons : ∀ {σs : List (Type u)} {σ : Type u} [Inhabited σ] (P Q : Prop), ⌜P⌝ ⊢ₛ ⌜Q⌝ ↔ ⌜P⌝ ⊢ₛ ⌜Q⌝
-- Mathlib.Order.SuccPred.WithBot
WithBot.lt_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] [NoMaxOrder α] (x : WithBot α),
  x < ↑x.succ
-- Mathlib.Tactic.Linter.Whitespace
/-- The kind of formatting error. For example: `extra space`, `remove line break` or
`missing space`.

Strings starting with `Oh no` indicate an internal error.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.msg : Mathlib.Linter.FormatError✝ → String
-- Mathlib.Data.Set.Prod
Set.prod_subset_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {P : Set (α × β)}, s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.ExprVisited.mk.inj : ∀ {e e_1 : Lean.Expr}, { e := e } = { e := e_1 } → e = e_1
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.leftComm_toLinearEquiv : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C],
  ↑(Algebra.TensorProduct.leftComm R A B C) = TensorProduct.leftComm R A B C
-- Mathlib.Control.LawfulFix
Part.fix_le : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {X : (a : α) → Part (β a)},
  f X ≤ X → Part.fix ⇑f ≤ X
-- Init.Data.List.Zip
List.zipWith_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : List α} {bs : List β},
  List.zipWith f as bs = List.zipWith (fun b a => f a b) bs as
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_eq_zero_of_not_inj : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  {v : Fin n → M}, ¬Function.Injective v → (ExteriorAlgebra.ιMulti R n) v = 0
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜), iteratedDeriv n (-f) a = -iteratedDeriv n f a
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (optionName declName : Lean.Name),
  sizeOf { stx := stx, optionName := optionName, declName := declName } =
    1 + sizeOf stx + sizeOf optionName + sizeOf declName
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.instNonempty : ∀ {α : Type u} [inst : UniformSpace α] [h : Nonempty α], Nonempty (CauchyFilter α)
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabTypeAscription : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.equivLike_neg_eq_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ+ N), EquivLike.inv f = ⇑f.symm
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_mulSingle_mulSingle : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : DecidableEq α]
  [inst_1 : (a : α) → DecidableEq (β a)] [inst_2 : (a : α) → (b : β a) → One (γ a b)] (a : α) (b : β a) (x : γ a b),
  Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin_toMatrix : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁), (Matrix.toBilin b) ((LinearMap.BilinForm.toMatrix b) B) = B
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyGeneralizingMap : AlgebraicGeometry.IsZariskiLocalAtSource
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => GeneralizingMap)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.monotone_restrict : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, Monotone fun π => π.restrict J
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- `R ⟶ S` induces `S-Alg ⥤ R-Alg`. Not an instance because `S` cannot be inferred.  -/
Algebra.restrictScalars : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_4) →
      [inst : Semiring A] →
        [inst_1 : CommSemiring S] → [Algebra S A] → [inst_3 : CommSemiring R] → [Algebra R S] → Algebra R A
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.fill.eq_2 : ∀ {α : Type u_1} (x : RBTree.RBNode α) (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (y : α)
  (b : RBTree.RBNode α), (RBTree.RBNode.Path.left c parent y b).fill x = parent.fill (RBTree.RBNode.node c x y b)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.exists_s_b_of_partDen : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ} {b : α},
  g.partDens.get? n = some b → ∃ gp, g.s.get? n = some gp ∧ gp.b = b
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence on some family `𝔖` of subsets of `α`. We denote it `α →ᵤ[𝔖] β`.  -/
UniformConvergence.«term_→ᵤ[_]_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
/-- Map `AddMonoid.Coprod M N` to `AddMonoid.Coprod M' N'`
by applying `Sum.map f g` to each element of the underlying list.  -/
AddMonoid.Coprod.map : {M : Type u_1} →
  {N : Type u_2} →
    {M' : Type u_3} →
      {N' : Type u_4} →
        [inst : AddZeroClass M] →
          [inst_1 : AddZeroClass N] →
            [inst_2 : AddZeroClass M'] →
              [inst_3 : AddZeroClass N'] → (M →+ M') → (N →+ N') → AddMonoid.Coprod M N →+ AddMonoid.Coprod M' N'
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- If `X ⟶ Y` is an open immersion, and `Y` is a scheme, then so is `X`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme : {X : AlgebraicGeometry.PresheafedSpace CommRingCat} →
  (Y : AlgebraicGeometry.Scheme) →
    (f : X ⟶ Y.toPresheafedSpace) → [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → AlgebraicGeometry.Scheme
-- Lean.Util.PtrSet
Lean.Ptr.mk.injEq : ∀ {α : Type u} (value value_1 : α), ({ value := value } = { value := value_1 }) = (value = value_1)
-- Init.Data.Nat.Basic
Nat.sub_one_add_one : ∀ {a : ℕ}, a ≠ 0 → a - 1 + 1 = a
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
Finsupp.toFreeAbelianGroup_comp_singleAddHom : ∀ {X : Type u_1} (x : X),
  Finsupp.toFreeAbelianGroup.comp (Finsupp.singleAddHom x) =
    (smulAddHom ℤ (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)
-- Mathlib.NumberTheory.ClassNumber.FunctionField
/-- The class number of a function field is `1` iff the ring of integers is a PID.  -/
FunctionField.classNumber_eq_one_iff : ∀ (Fq : Type u_1) (F : Type u_2) [inst : Field Fq] [inst_1 : Fintype Fq] [inst_2 : Field F]
  [inst_3 : Algebra (Polynomial Fq) F] [inst_4 : Algebra (RatFunc Fq) F]
  [inst_5 : IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [inst_6 : FunctionField Fq F]
  [inst_7 : Algebra.IsSeparable (RatFunc Fq) F],
  FunctionField.classNumber Fq F = 1 ↔ IsPrincipalIdealRing ↥(FunctionField.ringOfIntegers Fq F)
-- Mathlib.Algebra.Polynomial.Basis
Polynomial.coe_basisMonomials : ∀ (R : Type u) [inst : Semiring R], ⇑(Polynomial.basisMonomials R) = fun s => (Polynomial.monomial s) 1
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.mk : {J : Type u_1} → [inst : LinearOrder J] → J → CategoryTheory.SimplicialThickening J
-- Mathlib.Data.Nat.Squarefree
Nat.Squarefree.ext_iff : ∀ {n m : ℕ}, Squarefree n → Squarefree m → (n = m ↔ ∀ (p : ℕ), Nat.Prime p → (p ∣ n ↔ p ∣ m))
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_neg : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f : MvPolynomial σ R),
  m.withBotDegree (-f) = m.withBotDegree f
-- Mathlib.LinearAlgebra.RootSystem.Base
Finsupp.linearEquivFunOnFinite.eq_1 : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M],
  Finsupp.linearEquivFunOnFinite R M α =
    { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯, invFun := Finsupp.equivFunOnFinite.invFun, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Probability.Process.Filtration
MeasureTheory.instCoeFunFiltrationForallMeasurableSpace : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} → [inst : Preorder ι] → CoeFun (MeasureTheory.Filtration ι m) fun x => ι → MeasurableSpace Ω
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instIsLeftCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsLeftCancelAdd α], IsLeftCancelAdd (Colex α)
-- Mathlib.Probability.UniformOn
ProbabilityTheory.isProbabilityMeasure_uniformOn' : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s : Set Ω},
  s.Finite → s.Nonempty → MeasurableSet s → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn s)
-- Mathlib.Topology.Order.Monotone
/-- If a monotone function sending `bot` to `bot` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition.  -/
Monotone.map_iSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β}
  {g : ι → α}, ContinuousAt f (iSup g) → Monotone f → f ⊥ = ⊥ → f (⨆ i, g i) = ⨆ i, f (g i)
-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- the isomorphism `((((whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj F' ≅ F` expressing
that `F` is induced by `F'` up to an isomorphism  -/
CategoryTheory.Localization.Lifting₃.iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
                {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} →
                  {inst_2 : CategoryTheory.Category.{v_3, u_3} C₃} →
                    {inst_3 : CategoryTheory.Category.{v_4, u_6} D₁} →
                      {inst_4 : CategoryTheory.Category.{v_5, u_7} D₂} →
                        {inst_5 : CategoryTheory.Category.{v_6, u_8} D₃} →
                          {inst_6 : CategoryTheory.Category.{v_13, u_13} E} →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                (L₃ : CategoryTheory.Functor C₃ D₃) →
                                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                                    (W₂ : CategoryTheory.MorphismProperty C₂) →
                                      (W₃ : CategoryTheory.MorphismProperty C₃) →
                                        (F :
                                            CategoryTheory.Functor C₁
                                              (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) →
                                          (F' :
                                              CategoryTheory.Functor D₁
                                                (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) →
                                            [self : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F'] →
                                              ((((CategoryTheory.Functor.whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj
                                                  F' ≅
                                                F
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons_tail_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), u :: p.support.tail = p.support
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- Construction of the pushout in the category of types, as a quotient of `X₁ ⊕ X₂`.  -/
CategoryTheory.Limits.Types.Pushout : {S X₁ X₂ : Type u} → (S ⟶ X₁) → (S ⟶ X₂) → Type u
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addCommSemigroup : {M : Type u_3} →
  [inst : AddCommMonoid M] → [inst_1 : Preorder M] → [AddLeftStrictMono M] → AddCommSemigroup { x // 0 < x }
-- Mathlib.Data.Set.Lattice
Set.sUnion_inter_sUnion : ∀ {α : Type u_1} {s t : Set (Set α)}, ⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, p.1 ∩ p.2
-- Mathlib.Data.DFinsupp.Defs
/-- Note the general `SMul` instance doesn't apply as `ℕ` is not distributive
unless `β i`'s addition is commutative.  -/
DFinsupp.hasNatScalar : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddMonoid (β i)] → SMul ℕ (Π₀ (i : ι), β i)
-- Mathlib.Algebra.BigOperators.Module
/-- **Summation by parts** for ranges  -/
Finset.sum_range_by_parts : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : ℕ → R) (g : ℕ → M)
  (n : ℕ),
  ∑ i ∈ Finset.range n, f i • g i =
    f (n - 1) • ∑ i ∈ Finset.range n, g i -
      ∑ i ∈ Finset.range (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i
-- Mathlib.GroupTheory.Complement
Subgroup.smul_apply_eq_smul_apply_inv_smul : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {F : Type u_2} [inst_1 : Group F] [inst_2 : MulAction F G]
  [inst_3 : MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H),
  ↑(⋯.leftQuotientEquiv q) = f • ↑(⋯.leftQuotientEquiv (f⁻¹ • q))
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.not_isField : ∀ {A : Type u_2} [inst : CommRing A], ¬IsField (PowerSeries A)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instFaithfulMonadFunctorMonadToFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.monadToFunctor C).Faithful
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.instMul : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → Mul (GroupLike R A)
-- Init.Data.BitVec.Lemmas
BitVec.not_le : ∀ {n : ℕ} {x y : BitVec n}, ¬x ≤ y ↔ y < x
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context.targets : Lean.Elab.Tactic.ElimApp.Context✝ → Array Lean.Expr
-- Mathlib.Topology.UniformSpace.Basic
/-- Uniform continuity for functions of two variables.  -/
UniformContinuous₂ : {α : Type ua} →
  {β : Type ub} → {γ : Type uc} → [UniformSpace α] → [UniformSpace β] → [UniformSpace γ] → (α → β → γ) → Prop
-- Mathlib.RingTheory.Ideal.Span
IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span : ∀ {R : Type u_1} [inst : CommRing R] {e : R},
  IsIdempotentElem e → (LinearMap.toSpanSingleton R R (1 - e)).ker = Ideal.span {e}
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.toLinearPreorderOfOrdArgs : {α : Type u} → Std.Packages.LinearOrderOfOrdArgs α → Std.Packages.LinearPreorderOfOrdArgs α
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.isEmpty_pullback : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  Disjoint (Set.range ⇑f) (Set.range ⇑g) → IsEmpty ↥(CategoryTheory.Limits.pullback f g)
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : ↥s),
  (Subgroup.quotientSubgroupOfEmbeddingOfLE H h) ↑g = ↑((Subgroup.inclusion h) g)
-- Mathlib.Algebra.Group.Action.Defs
SMulCommClass.of_commMonoid : ∀ (A : Type u_9) (B : Type u_10) (G : Type u_11) [inst : CommMonoid G] [inst_1 : SMul A G] [inst_2 : SMul B G]
  [IsScalarTower A G G] [IsScalarTower B G G], SMulCommClass A B G
-- Init.Control.Lawful.Instances
OptionT.run_controlAt : ∀ {m : Type u → Type u_1} {α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)),
  (controlAt m f).run = f fun {β} x => x.run
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank : ∀ (R : Type u_1) {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] (x : L) [Nontrivial R],
  LieAlgebra.IsRegular R x ↔ (LinearMap.charpoly ((LieAlgebra.ad R L) x)).natTrailingDegree = LieAlgebra.rank R L
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- `f1` is unsat iff `f2` is unsat  -/
Std.Tactic.BVDecide.LRAT.Internal.Equisat : (α : Type u) →
  {σ1 : Type v} →
    {σ2 : Type w} →
      [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] →
        [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] → σ1 → σ2 → Prop
-- Init.Data.Int.Lemmas
Int.add_zero : ∀ (a : ℤ), a + 0 = a
-- Lean.Language.Basic
/-- Maximum number of errors to report.  -/
Lean.Language.maxErrors : Lean.Option ℕ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vadd_of_tower_mem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : VAdd S R]
  [inst_3 : VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) (s : S) {x : M}, x ∈ p → s +ᵥ x ∈ p
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.mk'_apply_Adj : ∀ {V : Type u_1} (x : V → V → Bool) (v w : V), (Digraph.mk' x).Adj v w = (x v w = true)
-- Lean.Elab.Tactic.Basic
/-- Registers a tactic elaborator for the given syntax node kind.

A tactic elaborator should have type `Lean.Elab.Tactic.Tactic` (which is
`Lean.Syntax → Lean.Elab.Tactic.TacticM Unit`), i.e. should take syntax of the given syntax
node kind as a parameter and alter the tactic state.

The `elab_rules` and `elab` commands should usually be preferred over using this attribute
directly.
 -/
Lean.Elab.Tactic.tacticElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Tactic
-- Mathlib.Geometry.Manifold.Submersion
/-- A `C^n` submersion is `C^n`  -/
Manifold.IsSubmersion.contMDiff : ∀ {𝕜 : 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 → ContMDiff I J n f
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.gc_map_comap : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M'),
  GaloisConnection (LieSubmodule.map f) (LieSubmodule.comap f)
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.modifyNth.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (f : Γ → Γ) (x : Turing.ListBlank Γ) (n : ℕ),
  Turing.ListBlank.modifyNth f n.succ x = Turing.ListBlank.cons x.head (Turing.ListBlank.modifyNth f n x.tail)