mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.Classes
/-- This typeclass bundles `MinEqOr α` and `LawfulOrderInf α`. It characterizes when a `Min α`
instance reasonably computes minima in some type `α` that has an `LE α` instance.

As long as `α` is a preorder (see `IsPreorder α`), this typeclass implies that the order on
`α` is total and that `Min.min a b` returns either `a` or `b`, whichever is less or equal to
the other.
 -/
Std.LawfulOrderMin : (α : Type u) → [Min α] → [LE α] → Prop
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_lift_OptionT_apply_eq : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (x : m α),
  Std.Internal.Do.wp (OptionT.lift x) post epost = Std.Internal.Do.wp (MonadLift.monadLift x) post epost
-- Mathlib.Geometry.Diffeology.Basic
NormedSpace.isContDiffCompatible_iff_eq_toDiffeology : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] [inst_2 : FiniteDimensional ℝ X]
  [d : DiffeologicalSpace X], Diffeology.IsContDiffCompatible X ↔ d = NormedSpace.toDiffeology X
-- Lean.Hygiene
Lean.Unhygienic.Context.scope : Lean.Unhygienic.Context → Lean.MacroScope
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.ref : Lean.Elab.DerivingClassView → Lean.Syntax
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_add : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ + o₂).repr = o₁.repr + o₂.repr
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcConnected : Lean.FromJson Lean.Lsp.RpcConnected
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_congr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ γ' : ℝ → M},
  Set.EqOn γ γ' (Set.Icc a b) → Manifold.pathELength I γ a b = Manifold.pathELength I γ' a b
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.smul_apply : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ) (r : R) (f : AdicCompletion.AdicCauchySequence I M), ↑(r • f) n = r • ↑f n
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_norm_sub' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u - v‖
-- Mathlib.Data.Set.Function
Set.bijOn_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Set.BijOn f Set.univ Set.univ ↔ Function.Bijective f
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulL.injEq : ∀ (k : ℤ) (a : Int.Internal.Linear.Expr) (k_1 : ℤ) (a_1 : Int.Internal.Linear.Expr),
  (Int.Internal.Linear.Expr.mulL k a = Int.Internal.Linear.Expr.mulL k_1 a_1) = (k = k_1 ∧ a = a_1)
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalParen : Lean.Elab.Tactic.Tactic
-- Batteries.Data.Fin.Lemmas
Fin.map_findSome? : ∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : Fin n → Option α) (g : α → β),
  Option.map g (Fin.findSome? f) = Fin.findSome? fun x => Option.map g (f x)
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.IsLocalIso.instIsZariskiLocalAtSource : AlgebraicGeometry.IsZariskiLocalAtSource @AlgebraicGeometry.IsLocalIso
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Pointed.mono : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C₁ C₂ : ConvexCone R M}, C₁ ≤ C₂ → C₁.Pointed → C₂.Pointed
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.hull.eq_1 : ∀ (R : Type u_2) {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (s : Set M), ConvexCone.hull R s = sInf {C | s ⊆ ↑C}
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.isoImage_ι_inv_morphismRestrict_homOfLE : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : TopologicalSpace.Opens ↥↑V),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage U.ι ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W)).inv
      (X.homOfLE e ∣_ W) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) (AlgebraicGeometry.Scheme.Hom.isoImage V.ι W).inv
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.encodeList.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.CategoryTheory.Limits.Cones
/-- For `F : J ⥤ C`, given a cocone `c : Cocone F`, and a natural isomorphism `α : H ≅ H'` for functors
`H H' : C ⥤ D`, the precomposition of the cocone `H.mapCocone` using the isomorphism `α` is
isomorphic to the cocone `H'.mapCocone`.
 -/
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J C} →
              {H H' : CategoryTheory.Functor C D} →
                (α : H ≅ H') →
                  (c : CategoryTheory.Limits.Cocone F) →
                    (CategoryTheory.Limits.Cocone.precompose (F.whiskerLeft α.inv)).obj (H.mapCocone c) ≅ H'.mapCocone c
-- Batteries.CodeAction.Attr
/-- The list of tactic code actions to apply on any tactic.  -/
Batteries.CodeAction.TacticCodeActions.onAnyTactic : Batteries.CodeAction.TacticCodeActions → Array Batteries.CodeAction.TacticCodeAction
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.dvd_comp_X_add_C_iff : ∀ {R : Type u} [inst : CommRing R] (p q : Polynomial R) (a : R),
  p ∣ q.comp (Polynomial.X + Polynomial.C a) ↔ p.comp (Polynomial.X - Polynomial.C a) ∣ q
-- Lean.Elab.PreDefinition.Main
Lean.Elab.addPreDefinitions : Lean.LocalContext × Lean.LocalInstances → Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfMulEquiv.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  (k : T.LocalizationMap Q) {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T),
  f.mulEquivOfMulEquiv k H = f.mulEquivOfLocalizations (k.ofMulEquivOfDom H)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_right_iff : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α],
  IsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.pow_inj_mod : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {x : G} {n m : ℕ}, x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x
-- Batteries.Data.Nat.Lemmas
Nat.recDiag_succ_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (m n : ℕ),
  Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) (n + 1) =
    succ_succ m n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n)
-- Mathlib.Algebra.Algebra.Hom
/-- If a `RingHom` is `R`-linear, then it is an `AlgHom`.  -/
AlgHom.mk' : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → (f : A →+* B) → (∀ (c : R) (x : A), f (c • x) = c • f x) → A →ₐ[R] B
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_toContinuousMultilinearMap : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F), ‖f.toContinuousMultilinearMap‖ = ‖f‖
-- Mathlib.Algebra.Order.Ring.Abs
sq_lt_one_iff_abs_lt_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), a ^ 2 < 1 ↔ |a| < 1
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.Iso.inv_hom_id_apply`. -/
CategoryTheory.inv_hom_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier Y),
  (CategoryTheory.ConcreteCategory.hom self.hom) ((CategoryTheory.ConcreteCategory.hom self.inv) x) = x
-- Mathlib.Data.ENNReal.Basic
ENNReal.instUniqueAddUnits : Unique (AddUnits ENNReal)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Auxiliary definition to avoid looping in `dsimp`
with `Bundle.Trivialization.preimageHomeomorph_symm_apply`.  -/
Bundle.Trivialization.preimageHomeomorph_symm_apply.aux : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e : Bundle.Trivialization F proj) → {s : Set B} → s ⊆ e.baseSet → ↑s × F ≃ₜ ↑(proj ⁻¹' s)
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAway`
if whenever `P` holds for `f` it also holds for the composition with
localization maps on the target.  -/
RingHom.StableUnderCompositionWithLocalizationAwayTarget : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.getFirstCtor : Lean.Name → Lean.MetaM (Option Lean.Name)
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.prodMk'.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : LocallyCompactSpace X]
  [inst_6 : LocallyCompactSpace Y], AbstractMeasure.prodMk' = AbstractMeasure.prodMk'
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instGetElem?Mem : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → GetElem? (Std.HashMap.Raw α β) α β fun m a => a ∈ m
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_alter_of_beq_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β}, (k == k') = false → (m.alter k f).contains k' = m.contains k'
-- Std.Data.Internal.List.Associative
Std.Internal.List.beqModel_eq_constBeqModel : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : BEq β] {l₁ l₂ : List ((_ : α) × β)},
  Std.Internal.List.beqModel l₁ l₂ = Std.Internal.List.Const.beqModel l₁ l₂
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Set.principalSegIioIicOfLE.congr_simp : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (h : i ≤ j), Set.principalSegIioIicOfLE h = Set.principalSegIioIicOfLE h
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.app.sizeOf_spec : ∀ (arr : Array Mathlib.Tactic.ClickSuggestions.ApplyLemma),
  sizeOf (Mathlib.Tactic.ClickSuggestions.Candidates.app✝ arr) = 1 + sizeOf arr
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_omega0 : Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) Ordinal.omega0
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_const_eq_top_of_ne_zero : ∀ {α : Type u_4} [Infinite α] {c : ENNReal}, c ≠ 0 → ∑' (x : α), c = ⊤
-- Mathlib.Data.ENat.Basic
ENat.pow_lt_top_iff : ∀ {a : ℕ∞} {n : ℕ}, a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0
-- Init.Data.Rat.Basic
instInhabitedRat : Inhabited ℚ
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D D_1 : ℝ),
  D = D_1 → ∀ (a a_1 : E), a = a_1 → ExistsContDiffBumpBase.y D a = ExistsContDiffBumpBase.y D_1 a_1
-- Mathlib.Tactic.Module
/-- The main algorithm behind the `match_scalars` and `module` tactics: partially-normalizing an
expression in an additive commutative monoid `M` into the form c1 • x1 + c2 • x2 + ... c_k • x_k,
where x1, x2, ... are distinct atoms in `M`, and c1, c2, ... are scalars. The scalar type of the
expression is not pre-determined: instead it starts as `ℕ` (when each atom is initially given a
scalar `(1:ℕ)`) and gets bumped up into bigger semirings when such semirings are encountered.

It is assumed that there is a "linear order" on all the semirings which appear in the expression:
for any two semirings `R` and `S` which occur, we have either `Algebra R S` or `Algebra S R`.

TODO: implement a variant in which a semiring `R` is provided by the user, and the assumption is
instead that for any semiring `S` which occurs, we have `Algebra S R`. The PR https://github.com/leanprover-community/mathlib4/pull/16984 provides a
proof-of-concept implementation of this variant, but it would need some polishing before joining
Mathlib.

Possible TODO, if poor performance on large problems is witnessed: switch the implementation from
`AtomM` to `CanonM`, per the discussion
https://github.com/leanprover-community/mathlib4/pull/16593/files#r1749623191  -/
Mathlib.Tactic.Module.parse : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(AddCommMonoid «$M»)) →
      (x : Q(«$M»)) →
        Mathlib.Tactic.AtomM
          ((u : Lean.Level) ×
            (R : Q(Type u)) ×
              (iR : Q(Semiring «$R»)) ×
                (x_1 : Q(Module «$R» «$M»)) ×
                  (l : Mathlib.Tactic.Module.qNF R M) ×
                    have a := l.toNF;
                    Q(«$x» = «$a».eval))
-- Init.Data.UInt.Lemmas
USize.lt_add_one : ∀ {c : USize}, c ≠ -1 → c < c + 1
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.IsMultiplicative.pdiv : ∀ {R : Type u_1} [inst : CommGroupWithZero R] {f g : ArithmeticFunction R},
  f.IsMultiplicative → g.IsMultiplicative → (f.pdiv g).IsMultiplicative
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.isInstImplicit : Lean.Meta.ParamInfo → Bool
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.triangleIndices.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] (s : Finset α),
  triangleIndices✝ s =
    Finset.map { toFun := fun xa => (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2), inj' := ⋯ } (Finset.univ ×ˢ s)
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.unitsComplexConj_torsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (ζ : ↥(NumberField.Units.torsion K)), (NumberField.IsCMField.unitsComplexConj K) ↑ζ = ↑ζ⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).inv.app X_1).snd.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj X_2)
-- Mathlib.RingTheory.Bialgebra.Hom
Bialgebra.counitBialgHom_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  ↑(Bialgebra.counitBialgHom R A) = Coalgebra.counitCoalgHom R A
-- Mathlib.Data.Set.Sigma
Set.sigma_preimage_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ι → Type u_6}
  {f : ι' → ι} {g : (i : ι) → β i → α i},
  ((f ⁻¹' s).sigma fun i => g (f i) ⁻¹' t (f i)) = (fun p => ⟨f p.fst, g (f p.fst) p.snd⟩) ⁻¹' s.sigma t
-- Init.Data.List.Impl
List.filterMap_eq_filterMapTR : @List.filterMap = @List.filterMapTR
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.symm : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =o[l] g → (fun x => f₂ x - f₁ x) =o[l] g
-- Mathlib.CategoryTheory.Triangulated.WeakKernels
/-- A pretriangulated category has weak kernels.  -/
CategoryTheory.Pretriangulated.instHasWeakKernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C],
  CategoryTheory.Limits.HasWeakKernels C
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.smul_sum : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} {T : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : DistribSMul T S]
  (p : Polynomial R) (b : T) (f : ℕ → R → S), b • p.sum f = p.sum fun n a => b • f n a
-- Init.Data.ByteArray.Lemmas
ByteArray.set.eq_1 : ∀ (x : ℕ) (x_1 : UInt8) (bs : Array UInt8) (x_2 : x < { data := bs }.size),
  { data := bs }.set x x_1 x_2 = { data := bs.set x x_1 x_2 }
-- Init.Grind.Lemmas
Lean.Grind.Bool.ne_of_eq_true_of_eq_false : ∀ {a b : Bool}, a = true → b = false → (a = b) = False
-- Mathlib.Data.Multiset.ZeroCons
Multiset.zero_ssubset : ∀ {α : Type u_1} {s : Multiset α}, 0 ⊂ s ↔ s ≠ 0
-- Mathlib.Order.UpperLower.Closure
LowerSet.coe_erase : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (a : α), ↑(s.erase a) = ↑s \ ↑(UpperSet.Ici a)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.singletonSubgraph_snd_le_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {h : G.Adj u v}, G.singletonSubgraph v ≤ G.subgraphOfAdj h
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
Polynomial.mem_iff_annIdealGenerator_dvd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {p : Polynomial 𝕜} {a : A},
  p ∈ Polynomial.annIdeal 𝕜 a ↔ Polynomial.annIdealGenerator 𝕜 a ∣ p
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.diag_obj : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] (a : C), (CategoryTheory.Functor.diag C).obj a = (a, a)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instMulAction : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_3} → {A : Type u_5} → [inst : Monoid R] → [MulAction R A] → MulAction R (CStarMatrix m n A)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instAddLeftReflectLE : AddLeftReflectLE Ordinal.{u}
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_le_pow_right : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {m n : ℕ}, m ≤ n → I ^ n ≤ I ^ m
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapAddEquiv_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S)
  (r : R) (m : M), (MonoidAlgebra.mapAddEquiv M e) (MonoidAlgebra.single m r) = MonoidAlgebra.single m (e r)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasColimitsOfSize : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} A]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} B]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} L],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {fallback : β} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.alter t k f) k' fallback =
    if cmp k k' = Ordering.eq then (f (Std.ExtDTreeMap.Const.get? t k)).getD fallback
    else Std.ExtDTreeMap.Const.getD t k' fallback
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.warning.simp.varHead : Lean.Option Bool
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.mul_inv_rev : ∀ {k : Type u_2} [inst : Field k] (φ ψ : PowerSeries k), (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instConcreteCategoryLinearMapIdCarrier : (R : Type u) → [inst : Ring R] → CategoryTheory.ConcreteCategory (ModuleCat R) fun x1 x2 => ↑x1 →ₗ[R] ↑x2
-- Std.Internal.Do.WP.Lemmas
EStateM.throw.eq_1 : ∀ {ε σ α : Type u} (e : ε) (s : σ), EStateM.throw e s = EStateM.Result.error e s
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.proj_recompose : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜]
  (a : DirectSum ι fun i => ↥(𝒜 i)) (i : ι),
  (GradedRing.proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) =
    (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun i => ↥(𝒜 i)) i) (a i))
-- Lean.Parser.Extension
/-- convenience function for testing  -/
Lean.Parser.runParserCategory : Lean.Environment → Lean.Name → String → optParam String "<input>" → Except String Lean.Syntax
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Post-composition with the preimage of an inducing function whose range is closed preserves
upper hemicontinuity.  -/
UpperHemicontinuousWithinAt.isInducing_comp : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α}
  {x : α} {γ : Type u_5} [inst_2 : TopologicalSpace γ] {i : γ → β},
  UpperHemicontinuousWithinAt f s x →
    Topology.IsInducing i → IsClosed (Set.range i) → UpperHemicontinuousWithinAt (fun x => i ⁻¹' f x) s x
-- Mathlib.Algebra.BigOperators.Fin
/-- For `f = (a₁, ..., aₙ)` in `αⁿ`, `partialProd f` is `(1, a₁, a₁a₂, ..., a₁...aₙ)` in `αⁿ⁺¹`.  -/
Fin.partialProd : {M : Type u_2} → [Monoid M] → {n : ℕ} → (Fin n → M) → Fin (n + 1) → M
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C], (CategoryTheory.Idempotents.toKaroubiEquivalence C).functor.Additive
-- Mathlib.Order.Monotone.Monovary
Subsingleton.monovary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton ι] (f : ι → α)
  (g : ι → β), Monovary f g
-- Mathlib.Algebra.Lie.Basic
lie_sub : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m n : M),
  ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆
-- Mathlib.Order.Basic
update_lt_update_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x : (i : ι) → π i}
  {i : ι} {a b : π i}, Function.update x i a < Function.update x i b ↔ a < b
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.inverseCompIso_inv_app : ∀ {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 E}
  {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D),
  i.inverseCompIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))