mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range is beyond the upper bound, the size is zero.  -/
Std.Rxo.LawfulHasSize.size_eq_zero_of_not_le : ∀ {α : Type u} {inst : LT α} {inst_1 : Std.PRange.UpwardEnumerable α} {inst_2 : Std.Rxo.HasSize α}
  [self : Std.Rxo.LawfulHasSize α] (lo hi : α), ¬lo < hi → Std.Rxo.HasSize.size lo hi = 0
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.postAdjunctionLeft_unit_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X : C} {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X_1 : CategoryTheory.Over ((CategoryTheory.Functor.id C).obj X)),
  ((CategoryTheory.Over.postAdjunctionLeft a).unit.app X_1).left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X_1.left) X_1.hom ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.lift
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp X_1.hom (a.unit.app X))
              (a.unit.app X))
            (a.unit.app X_1.left))
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp X_1.hom (a.unit.app X))
            (a.unit.app X))
          ⋯)
        (CategoryTheory.Limits.pullback.lift
          (CategoryTheory.Limits.pullback.fst
            (G.map
              (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp X_1.hom (a.unit.app X)))
                (a.counit.app (F.obj X))))
            (a.unit.app X))
          (CategoryTheory.Limits.pullback.snd
            (G.map
              (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp X_1.hom (a.unit.app X)))
                (a.counit.app (F.obj X))))
            (a.unit.app X))
          ⋯))
-- Init.Data.Array.Perm
Array.perm_comm : ∀ {α : Type u_1} {xs ys : Array α}, xs.Perm ys ↔ ys.Perm xs
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_swap_mul_of_contravariant_mul : ∀ (N : Type u_2) (r : N → N → Prop) [inst : CommSemigroup N] [ContravariantClass N N (fun x1 x2 => x1 * x2) r],
  ContravariantClass N N (Function.swap fun x1 x2 => x1 * x2) r
-- Init.Data.SInt.Bitwise
ISize.toBitVec_shiftRight : ∀ (a b : ISize), (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod ↑System.Platform.numBits)
-- Mathlib.Data.List.ReduceOption
List.reduceOption_cons_of_none : ∀ {α : Type u_1} (l : List (Option α)), (none :: l).reduceOption = l.reduceOption
-- Mathlib.Algebra.Ring.Int.Parity
Int.natAbs_odd : ∀ {n : ℤ}, Odd n.natAbs ↔ Odd n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instCartesianMonoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Grp C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → Q 2 ≠ 0 → W'.add P Q = (P 1 ^ 2 * Q 2) • Q
-- Mathlib.Topology.Constructions.SumProd
Topology.IsClosedEmbedding.inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding Sum.inl
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Determinant of 3x3 matrix  -/
Matrix.det_fin_three : ∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 3) (Fin 3) R),
  A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0
-- Mathlib.RingTheory.Ideal.Span
Ideal.factors_decreasing : ∀ {α : Type u} [inst : CommSemiring α] [IsDomain α] (b₁ b₂ : α),
  b₁ ≠ 0 → ¬IsUnit b₂ → Ideal.span {b₁ * b₂} < Ideal.span {b₁}
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [inst_5 : CategoryTheory.Limits.HasBinaryCoproduct A A]
  [inst_6 : CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [P.IsVeryGood],
  HomotopicalAlgebra.IsFibrant P.I
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_ne_nil : ∀ (n : ℕ), n.primeFactorsList ≠ [] ↔ 1 < n
-- Mathlib.RingTheory.Smooth.Locus
/-- An `R`-algebra `A` is smooth at a prime `p` of `A` if `Aₚ` is formally smooth over `R`.

This does not imply `Aₚ` is smooth over `R` under the mathlib definition
even if `A` is finitely presented,
but it can be shown that this is equivalent to the stacks project definition that `A` is smooth
at `p` if and only if there exists `f ∉ p` such that `A_f` is smooth over `R`.
See `Algebra.basicOpen_subset_smoothLocus_iff_smooth` and `Algebra.isOpen_smoothLocus`.
 -/
Algebra.IsSmoothAt : (R : Type u_1) →
  {A : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (p : Ideal A) → [p.IsPrime] → Prop
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_inv_interval : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] (s : NonemptyInterval α),
  ↑s⁻¹ = (↑s)⁻¹
-- Mathlib.Algebra.AddConstMap.Basic
/-- Coercion to functions as a monoid homomorphism to `Function.End G`.  -/
AddConstMap.toEnd : {G : Type u_1} → [inst : Add G] → {a : G} → AddConstMap G G a a →* Function.End G
-- Init.Guard
/-- Syntactic matching for `guard_hyp` types  -/
Lean.Parser.colonS : Lean.ParserDescr
-- Mathlib.CategoryTheory.Simple
CategoryTheory.Simple.not_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C)
  [CategoryTheory.Simple X], ¬CategoryTheory.Limits.IsZero X
-- Mathlib.Geometry.Euclidean.Volume.Measure
EuclideanGeometry.measurePreserving_vaddConst : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (p : P),
  MeasureTheory.MeasurePreserving (⇑(IsometryEquiv.vaddConst p)) MeasureTheory.volume
    (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V))
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.hyperfilter_le_cofinite : ∀ {α : Type u} [inst : Infinite α], ↑(Filter.hyperfilter α) ≤ Filter.cofinite
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpNatIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (e : F ≅ F')
  (X : CategoryTheory.AddGrp C), ((CategoryTheory.Functor.mapAddGrpNatIso e).inv.app X).hom.hom = e.inv.app X.X
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.unit_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map (F.map f)) =
    CategoryTheory.CategoryStruct.comp f (adj.unit.app Y)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangleIso.inv.hom₃ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₃
-- Mathlib.RingTheory.Valuation.Archimedean
Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v : ∀ {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O F] {v : Valuation F Γ₀},
  v.Integers O → (WfDvdMonoid O ↔ WellFounded (Function.onFun (fun x1 x2 => x1 > x2) (⇑v ∘ ⇑(algebraMap O F))))
-- Mathlib.Analysis.Calculus.LHopital
HasDerivAt.lhopital_zero_right_on_Ioo : ∀ {a b : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  a < b →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
        (∀ x ∈ Set.Ioo a b, g' x ≠ 0) →
          Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0) →
            Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0) →
              Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l →
                Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l
-- Init.Data.SInt.Bitwise
UInt64.toInt64_not : ∀ (a : UInt64), (~~~a).toInt64 = ~~~a.toInt64
-- Mathlib.FieldTheory.Minpoly.Basic
/-- The defining property of the minimal polynomial of an element `x`:
it is the monic polynomial with smallest degree that has `x` as its root.  -/
minpoly.min : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic → (Polynomial.aeval x) p = 0 → (minpoly A x).degree ≤ p.degree
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_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]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).inv.app X_1).snd.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj X_2)
-- Init.Data.BitVec.Bitblast
/-- Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
same as truncating `y` to `s` bits, then zero extending to the original length,
and performing the multiplication.  -/
BitVec.mulRec_eq_mul_signExtend_setWidth : ∀ {w : ℕ} (x y : BitVec w) (s : ℕ), x.mulRec y s = x * BitVec.setWidth w (BitVec.setWidth (s + 1) y)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Filter.BoundedAtFilter.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Norm β] (l : Filter α) (f : α → β), l.BoundedAtFilter f = f =O[l] 1
-- Init.Core
LawfulBEq.mk : ∀ {α : Type u} [inst : BEq α] [toReflBEq : ReflBEq α], (∀ {a b : α}, (a == b) = true → a = b) → LawfulBEq α
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.isOp? : Lean.Expr → Lean.Meta.Grind.AC.ACM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.sPolynomial_mem_sup_ideal : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [inst : CommRing R] {I J : Ideal (MvPolynomial σ R)}
  {p q : MvPolynomial σ R}, p ∈ I → q ∈ J → m.sPolynomial p q ∈ I ⊔ J
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.C_addPolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y ℓ : R),
  Polynomial.C (W'.addPolynomial x y ℓ) =
    (Polynomial.X - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y ℓ)) *
        (W'.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y ℓ)) +
      W'.polynomial
-- Mathlib.Topology.Hom.ContinuousEvalConst
Continuous.eval_const : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F},
  Continuous f → ∀ (x : α), Continuous fun x_1 => (f x_1) x
-- Std.Sat.CNF.Basic
Std.Sat.CNF.mk.inj : ∀ {α : Type u} {clauses clauses_1 : Array (Std.Sat.CNF.Clause α)},
  { clauses := clauses } = { clauses := clauses_1 } → clauses = clauses_1
-- Mathlib.Data.Set.Prod
Set.empty_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : (i : ι) → Set (α i)), ∅.pi s = Set.univ
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valuation_toVal : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : R), (WithVal.valuation v) (WithVal.toVal v x) = v x
-- Aesop.Rule
Aesop.instInhabitedRegularRule.default : Aesop.RegularRule
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.codisjoint_mk_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule),
  Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q
-- Mathlib.Data.Set.Lattice
Set.iUnion_congr_Prop : ∀ {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q),
  (∀ (x : q), f₁ ⋯ = f₂ x) → Set.iUnion f₁ = Set.iUnion f₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.brecOn.eq : ∀ {motive : Lean.Grind.CommRing.Expr → Sort u} (t : Lean.Grind.CommRing.Expr)
  (F_1 : (t : Lean.Grind.CommRing.Expr) → Lean.Grind.CommRing.Expr.below t → motive t),
  Lean.Grind.CommRing.Expr.brecOn t F_1 = F_1 t (Lean.Grind.CommRing.Expr.brecOn.go t F_1).2
-- Init.Data.UInt.Lemmas
UInt32.ofFin_sub : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a - b) = UInt32.ofFin a - UInt32.ofFin b
-- Mathlib.Order.Defs.PartialOrder
/-- Equality is decidable if `≤` is.  -/
decidableEqOfDecidableLE : {α : Type u_1} → [inst : PartialOrder α] → [DecidableLE α] → DecidableEq α
-- Mathlib.Tactic.TermCongr
/-- Eliminate all congruence holes from an expression by replacing them with their values.  -/
Mathlib.Tactic.TermCongr.removeCHoles : Lean.Expr → Lean.Expr
-- Init.Data.UInt.Bitwise
USize.not_ne_self : ∀ {a : USize}, ~~~a ≠ a
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toProd_injective : ∀ {α : Type u_1} [inst : LE α], Function.Injective NonemptyInterval.toProd
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑(m₁.union m₂)).isEmpty = ((↑m₁).isEmpty && (↑m₂).isEmpty)
-- Batteries.Data.List.Lemmas
List.filterMap.match_1.congr_eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (x : Option β) (h_1 : Unit → motive none)
  (h_2 : (b : β) → motive (some b)) (b : β),
  x = some b →
    (match x with
      | none => h_1 ()
      | some b => h_2 b) ≍
      h_2 b
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `A`, this is
`(k[H] ⊗[k] A)_G` equipped with the `H`-representation defined by sending `h : H` and `⟦h₁ ⊗ₜ a⟧`
to `⟦h₁h⁻¹ ⊗ₜ a⟧`.  -/
Rep.ind : {k : Type u} →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] → [inst_2 : Group H] → (G →* H) → Rep.{w, u, v} k G → Rep.{max (max u v') w, u, v'} k H
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAlt.isRefl : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsAlt → B.IsRefl
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.StackEntry.expr.injEq : ∀ (info info_1 : Lean.Meta.RefinedDiscrTree.ExprInfo),
  (Lean.Meta.RefinedDiscrTree.StackEntry.expr info = Lean.Meta.RefinedDiscrTree.StackEntry.expr info_1) =
    (info = info_1)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] (it : Std.IterM m β),
  it.toArray = Std.IterM.toArray.go it #[]
-- Init.Data.Int.Order
Int.add_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_natCast_cancel : ∀ {a b : WithBot ℕ∞} {c : ℕ}, a + ↑c = b + ↑c ↔ a = b
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_apply : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} (l : α →₀ R), (Finsupp.linearCombination R v) l = l.sum fun i a => a • v i
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The sum of two polynomial laws  -/
PolynomialLaw.add : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → (M →ₚₗ[R] N) → (M →ₚₗ[R] N) → M →ₚₗ[R] N
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- The finset of numerators after clearing the denominators of a finite set of fractions.  -/
IsLocalizedModule.finsetIntegerMultiple : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {M' : Type u_3} →
              [inst_3 : AddCommMonoid M'] →
                [inst_4 : Module R M'] →
                  (f : M →ₗ[R] M') → [IsLocalizedModule S f] → [DecidableEq M] → Finset M' → Finset M
-- Init.Data.Vector.Lemmas
Vector.toList_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α → β} {xs : Vector α n},
  (Vector.mapIdx f xs).toList = List.mapIdx f xs.toList
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.eq_iff_exists : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x y : M}, f x = f y ↔ ∃ c, ↑c * x = ↑c * y
-- Mathlib.Data.Nat.Size
Nat.shiftLeft'_ne_zero_left : ∀ (b : Bool) {m : ℕ}, m ≠ 0 → ∀ (n : ℕ), Nat.shiftLeft' b m n ≠ 0
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- An auxiliary lemma for
`Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`. This lemma assumes
`w ∉ s` while the main lemma drops this assumption.  -/
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E}
  {s : Set ℂ},
  s.Countable →
    w ∈ Metric.ball c R \ s →
      ContinuousOn f (Metric.closedBall c R) →
        (∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
          ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • f w
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_log_mul_rpow_nhdsGT_zero : ∀ {r : ℝ}, 0 < r → Filter.Tendsto (fun x => Real.log x * x ^ r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
ContinuousLinearMap.fpowerSeries_apply_one : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E),
  f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f
-- Mathlib.Algebra.Algebra.Tower
AlgHom.map_algebraMap : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) (r : R),
  f ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.addCommMonoid : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                [inst_4 : DecidableEq ι] → AddCommMonoid (Module.DirectLimit G f)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrable_rpow_mul_exp_neg_mul_sq : ∀ {b : ℝ},
  0 < b → ∀ {s : ℝ}, -1 < s → MeasureTheory.Integrable (fun x => x ^ s * Real.exp (-b * x ^ 2)) MeasureTheory.volume
-- Mathlib.Data.Nat.ModEq
Nat.add_modulus_mul_modEq_iff : ∀ {n a b c : ℕ}, a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]
-- Std.Data.ExtHashMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.ExtHashMap.modify : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → (β → β) → Std.ExtHashMap α β
-- Mathlib.GroupTheory.IsSubnormal
/-- The inverse image of a subnormal additive subgroup under an additive group
homomorphism is a subnormal additive subgroup.  -/
AddSubgroup.IsSubnormal.comap : ∀ {G : Type u_1} [inst : AddGroup G] {G' : Type u_2} [inst_1 : AddGroup G'] {H' : AddSubgroup G'} (f : G →+ G'),
  H'.IsSubnormal → (AddSubgroup.comap f H').IsSubnormal
-- Mathlib.Order.GaloisConnection.Defs
/-- Property of the choice function.  -/
GaloisCoinsertion.choice_eq : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self : GaloisCoinsertion l u) (a : β) (h : a ≤ l (u a)), self.choice a h = u a
-- Lean.EnvExtension
Lean.MapDeclarationExtension.toPersistentEnvExtension : {α : Type} →
  Lean.MapDeclarationExtension α → Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)
-- Mathlib.CategoryTheory.Limits.Cones
/-- A `c : Cone F` is:
* an object `c.pt` and
* a natural transformation `c.π : c.pt ⟶ F` from the constant `c.pt` functor to `F`.

Example: if `J` is a category coming from a poset then the data required to make
a term of type `Cone F` is morphisms `πⱼ : c.pt ⟶ F j` for all `j : J` and,
for all `i ≤ j` in `J`, morphisms `πᵢⱼ : F i ⟶ F j` such that `πᵢ ≫ πᵢⱼ = πⱼ`.

`Cone F` is equivalent, via `cone.equiv` below, to `Σ X, F.cones.obj X`.
 -/
CategoryTheory.Limits.Cone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] → CategoryTheory.Functor J C → Type (max (max u₁ u₃) v₃)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.mk.inj : ∀ {G : Type u_6} {inst : AddGroup G} {toZeroHom : ZeroHom G ℝ}
  {add_le_max' : ∀ (r s : G), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s)}
  {neg' : ∀ (r : G), toZeroHom.toFun (-r) = toZeroHom.toFun r} {toZeroHom_1 : ZeroHom G ℝ}
  {add_le_max'_1 : ∀ (r s : G), toZeroHom_1.toFun (r + s) ≤ max (toZeroHom_1.toFun r) (toZeroHom_1.toFun s)}
  {neg'_1 : ∀ (r : G), toZeroHom_1.toFun (-r) = toZeroHom_1.toFun r},
  { toZeroHom := toZeroHom, add_le_max' := add_le_max', neg' := neg' } =
      { toZeroHom := toZeroHom_1, add_le_max' := add_le_max'_1, neg' := neg'_1 } →
    toZeroHom = toZeroHom_1
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[2] ⟶ Λ[3, 2]` which avoids `0`.  -/
SSet.horn₃₂.ι₀ : SSet.stdSimplex.obj { len := 2 } ⟶ (SSet.horn 3 2).toSSet
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.modByMonic_repr_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (g : Polynomial R), h.repr (h.map g) %ₘ f = g %ₘ f
-- Mathlib.Algebra.Group.Action.Defs
instIsLeftCancelSMul : ∀ (G : Type u_9) (P : Type u_10) [inst : Group G] [inst_1 : MulAction G P], IsLeftCancelSMul G P
-- Mathlib.MeasureTheory.Function.EssSup
/-- Essential infimum of `f` with respect to measure `μ`: the greatest `c : β` such that
`c ≤ f x` a.e.  -/
essInf : {α : Type u_1} →
  {β : Type u_2} → [ConditionallyCompleteLattice β] → {x : MeasurableSpace α} → (α → β) → MeasureTheory.Measure α → β