mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Mul
dotProduct_assoc : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : NonUnitalSemiring α]
  (u : m → α) (w : n → α) (v : Matrix m n α), (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_eq_zero_iff_support_subset_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R}, p.degrees = 0 ↔ p.support ⊆ {0}
-- Mathlib.Topology.Category.Stonean.Adjunctions
/-- The Stone-Cech compactification functor is left adjoint to the forgetful functor.  -/
Stonean.stoneCechAdjunction : typeToStonean ⊣ CategoryTheory.forget Stonean
-- Mathlib.Data.Complex.Basic
/-- This defines the complex conjugate as the `star` operation of the `StarRing ℂ`. It
is recommended to use the ring endomorphism version `starRingEnd`, available under the
notation `conj` in the scope `ComplexConjugate`.  -/
Complex.instStarRing : StarRing ℂ
-- Mathlib.CategoryTheory.Limits.Cones
/-- `functoriality F _ ⋙ postcompose (whisker_left F _)` simplifies to `functoriality F _`.  -/
CategoryTheory.Functor.functorialityCompPostcompose : {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') →
                  (CategoryTheory.Limits.Cone.functoriality F H).comp
                      (CategoryTheory.Limits.Cone.postcompose (F.whiskerLeft α.hom)) ≅
                    CategoryTheory.Limits.Cone.functoriality F H'
-- Mathlib.Data.Nat.Init
/-- Two natural numbers are equal if and only if they have the same multiples.  -/
Nat.dvd_right_iff_eq : ∀ {m n : ℕ}, (∀ (a : ℕ), m ∣ a ↔ n ∣ a) ↔ m = n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.instSubsingletonSymmetricCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  Subsingleton (CategoryTheory.SymmetricCategory C)
-- Mathlib.SetTheory.Lists
/-- Prelists, helper type to define `Lists`. `Lists' α false` are the "atoms", a copy of `α`.
`Lists' α true` are the "proper" ZFA prelists, inductively defined from the empty ZFA prelist and
from appending a ZFA prelist to a proper ZFA prelist. It is made so that you can't append anything
to an atom while having only one appending function for appending both atoms and proper ZFA prelists
to a proper ZFA prelist.  -/
Lists' : Type u → Bool → Type u
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k k' : α} {f : β k → β k},
  (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator.eq_1 : ∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (W : Submodule R M), W.dualAnnihilator = W.dualRestrict.ker
-- Init.SimpLemmas
Lean.arrow_true : ∀ (α : Sort u), Lean.Arrow α True = True
-- Mathlib.Analysis.Convex.Independent
/-- A family with at most one point is convex independent.  -/
Subsingleton.convexIndependent : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [Subsingleton ι] (p : ι → E), ConvexIndependent 𝕜 p
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- Series divergence test: if `f` is unconditionally summable, then `f x` tends to
zero along `cofinite`.  -/
Summable.tendsto_cofinite_zero : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  {f : α → G}, Summable f → Filter.Tendsto f Filter.cofinite (nhds 0)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonAssocCommSemiringOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonAssocCommSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → NonAssocCommSemiring (DirectLimit G f)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_support : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [inst : TopologicalSpace E]
  [TopologicalSpace.MetrizableSpace E] [inst_2 : Zero E] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.NullMeasurableSet (Function.support f) μ
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- **Steinhaus Theorem** for finite mass sets.

In any locally compact group `G` with a Haar measure `μ` that's inner regular on finite measure
sets, for any measurable set `E` of finite positive measure, the set `E / E` is a neighbourhood of
`1`.  -/
MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegularCompactLTTop]
  (E : Set G), MeasurableSet E → 0 < μ E → μ E ≠ ⊤ → E / E ∈ nhds 1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_bind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} (Z : ι → C) (g : (i : ι) → Z i ⟶ X)
  (j : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Presieve.ofArrows Z g f → Type u_2)
  (W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → j f H → C)
  (k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y),
  ((CategoryTheory.Presieve.ofArrows Z g).bind fun x f H => CategoryTheory.Presieve.ofArrows (W f H) (k f H)) =
    CategoryTheory.Presieve.ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij =>
      CategoryTheory.CategoryStruct.comp (k (g ij.fst) ⋯ ij.snd) (g ij.fst)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.trans_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsFibrant A] (P P' : HomotopicalAlgebra.PathObject A) [inst_3 : P'.IsGood],
  (P.trans P').p₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd P.p₁ P'.p₀) P'.p₁
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Hom.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.OplaxTrans.Hom η θ},
  x = y ↔ x.as = y.as
-- Mathlib.Data.Set.Disjoint
Set.disjoint_left : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
isUniformGroup_inf : ∀ {G : Type u_1} [inst : Group G] {u₁ u₂ : UniformSpace G}, IsUniformGroup G → IsUniformGroup G → IsUniformGroup G
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.mk_of_exists_colimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (X : C), ∃ J x, P.colimitsOfShape J X) → P.IsStrongGenerator
-- Mathlib.Order.Hom.Lattice
/-- `LatticeHomClass F α β` states that `F` is a type of lattice morphisms.

You should extend this class when you extend `LatticeHom`.  -/
LatticeHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [Lattice α] → [Lattice β] → [FunLike F α β] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.isType₂_δ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ),
  SSet.prodStdSimplex.pairingCore.IsType₂ hl.δ
-- Mathlib.RingTheory.Flat.Stability
/-- A base change of a flat module is flat.  -/
Module.Flat.isBaseChange : ∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Flat R M] (N : Type t) [inst_6 : AddCommMonoid N]
  [inst_7 : Module R N] [inst_8 : Module S N] [inst_9 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f → Module.Flat S N
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (f : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {𝒢' : CategoryTheory.Sheaf K A} (g : ℱ' ⟶ 𝒢') {Z : CategoryTheory.Functor Dᵒᵖ A}
  (h : 𝒢'.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom
        (CategoryTheory.CategoryStruct.comp f (G.op.whiskerLeft g.hom)))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom f)
      (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_apply_eq_zero_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0] [Nontrivial Γ₀] {x : R}, 1 x = 0 ↔ x = 0
-- Mathlib.Order.Preorder.Chain
IsMaxChain.isEmpty_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxChain r s → (IsEmpty α ↔ s = ∅)
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.cotangentCompAwaySec.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  (x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent),
  Algebra.Generators.cotangentCompAwaySec g P x = ((Algebra.Generators.basisCotangentAway T g).constr T) fun x_1 => x
-- Mathlib.CategoryTheory.NatIso
/-- The application of a natural isomorphism to an object. We put this definition in a different
namespace, so that we can use `α.app`  -/
CategoryTheory.Iso.app : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  (ih ih_1 : (i : ι) → F i), ih = ih_1 → DirectLimit.map₀ f ih = DirectLimit.map₀ f ih_1
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context.mk.sizeOf_spec : ∀ (maxDepth? : Option ℕ) (forwardHypData : Aesop.ForwardHypData),
  sizeOf { maxDepth? := maxDepth?, forwardHypData := forwardHypData } = 1 + sizeOf maxDepth? + sizeOf forwardHypData
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseMwdSpec : Std.Internal.Parsec.String.Parser Std.Time.TimeZone.TransitionSpec
-- Mathlib.Data.Set.Subset
Set.image_val_union : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, Subtype.val '' (D ∪ E) = Subtype.val '' D ∪ Subtype.val '' E
-- Mathlib.CategoryTheory.IsoCat
/-- The composition `inverse ⋙ functor` is equal to the identity.  -/
CategoryTheory.IsoCat.counit_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (self : CategoryTheory.IsoCat C D),
  self.inverse.comp self.functor = CategoryTheory.Functor.id D
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_and : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {p q : Prop} {f : p ∧ q → α},
  ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- Induction principle for the algebra generated by a set `s`: show that `p x y` holds for any
`x y ∈ adjoin R s` given that it holds for `x y ∈ s` and that it satisfies a number of
natural properties.  -/
Algebra.adjoin_induction₂ : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  {p : (x y : A) → x ∈ Algebra.adjoin R s → y ∈ Algebra.adjoin R s → Prop},
  (∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯) →
      (∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯) →
        (∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯) →
          (∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s),
              p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
            (∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s),
                p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
              (∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s),
                  p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
                (∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s)
                    (hz : z ∈ Algebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                  ∀ {x y : A} (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x y hx hy
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
/-- If `γ : ℝ → M` is $C^1$ on `s : Set ℝ` and `v` is a vector field on `M`,
`IsMIntegralCurveOn γ v s` means `γ t` is tangent to `v (γ t)` for all `t ∈ s`. The value of `γ`
outside of `s` is irrelevant and considered junk.  -/
IsMIntegralCurveOn : {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] → (ℝ → M) → ((x : M) → TangentSpace I x) → Set ℝ → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → β}, Function.Injective g → (∀ x ∉ Set.range g, f x = 1) → (HasProd (f ∘ g) a ↔ HasProd f a)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.modify_eq_alter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α}
  {f : β a → β a} (htb : t.Balanced),
  Std.DTreeMap.Internal.Impl.modify a f t = (Std.DTreeMap.Internal.Impl.alter a (fun x => Option.map f x) t htb).impl
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S : C}
  {R : CategoryTheory.Presieve S}, F.IsPrestackFor R → Nonempty (F.toDescentData fun f => f.obj.hom).FullyFaithful
-- Mathlib.Order.BoundedOrder.Basic
ULift.down_top : ∀ {α : Type u} [inst : Top α], ⊤.down = ⊤
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.erased : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.PHashSet Lean.Meta.Grind.Origin
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.one_eq_closure_one_set : ∀ {R : Type u_2} [inst : AddMonoidWithOne R], 1 = AddSubmonoid.closure 1
-- Mathlib.Algebra.Module.NatInt
map_intCast_smul : ∀ {M : Type u_3} {M₂ : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {F : Type u_5}
  [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [inst_4 : Ring R]
  [inst_5 : Ring S] [inst_6 : Module R M] [inst_7 : Module S M₂] (x : ℤ) (a : M), f (↑x • a) = ↑x • f a
-- Mathlib.Algebra.CharP.Lemmas
add_pow_expChar_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (p : ℕ) [hR : ExpChar R p], Commute x y → (x + y) ^ p = x ^ p + y ^ p
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapAlgHom_single : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B) (m : M)
  (a : A), (MonoidAlgebra.mapAlgHom M f) (MonoidAlgebra.single m a) = MonoidAlgebra.single m (f a)
-- Mathlib.NumberTheory.LucasLehmer
mersenne_mod_three : ∀ {n : ℕ}, Odd n → 3 ≤ n → mersenne n % 3 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α}, (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).size ≤ t.size + l.length
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval_comp_toMvPolynomial : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (f : σ → R) (i : σ),
  (MvPolynomial.eval f).comp ↑(Polynomial.toMvPolynomial i) = Polynomial.evalRingHom (f i)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddActionHom.embMap.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α] {m : Type u_5} {n : Type u_6} (e : m ↪ n),
  AddActionHom.embMap G α e = { toFun := fun i => e.trans i, map_vadd' := ⋯ }
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv : ∀ {r : ℝ},
  0 < r →
    ∀ (x : ℝ),
      ∫⁻ (y : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDF r y =
        ENNReal.ofReal (if 0 ≤ x then 1 - Real.exp (-(r * x)) else 0)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.equivCongr_refl : ∀ {R : Type uR} {A₁ : Type uA₁} {A₁' : Type uA₁'} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₁']
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₁'], AlgEquiv.refl.equivCongr AlgEquiv.refl = Equiv.refl (A₁ ≃ₐ[R] A₁')
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.map_T : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] (f : R →+* R') (n : ℤ),
  Polynomial.map f (Polynomial.Chebyshev.T R n) = Polynomial.Chebyshev.T R' n
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.List.compareLex.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : Unit → motive [] [])
  (h_2 : (x : List α) → motive [] x) (h_3 : (x : List α) → motive x [])
  (h_4 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (x = [] → False) →
    (match x, [] with
      | [], [] => h_1 ()
      | [], x => h_2 x
      | x, [] => h_3 x
      | x :: xs, y :: ys => h_4 x xs y ys) =
      h_3 x
-- Lean.Meta.Iterator
Lean.Meta.Iterator.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (next : Lean.MetaM (Option (α × Lean.Meta.SavedState))), sizeOf { next := next } = 1
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_injective : Function.Injective Cardinal.ord
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit (h.functor.obj c)) (s : CategoryTheory.Limits.Cone G),
  ((CategoryTheory.Limits.IsLimit.ofConeEquiv h) P).lift s =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app s).hom
        (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom)
      (h.unitIso.inv.app c).hom
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_uInt32ToNat : ∀ (n : UInt32) (h : n.toNat < UInt8.size), UInt8.ofNatLT n.toNat h = n.toUInt8
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The postcomposition of an alternating map by a linear map.  -/
ModuleCat.AlternatingMap.postcomp : {R : Type u} →
  [inst : CommRing R] →
    {M : ModuleCat R} →
      {N : ModuleCat R} → {n : ℕ} → M.AlternatingMap N n → {N' : ModuleCat R} → (N ⟶ N') → M.AlternatingMap N' n
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.finSigmaFinEquiv.match_1.eq_1 : ∀ (motive : (m : ℕ) → {n : Fin m → ℕ} → Sort u_1) (n : Fin 0 → ℕ) (h_1 : (n : Fin 0 → ℕ) → motive 0)
  (h_2 : (m : ℕ) → (n : Fin m.succ → ℕ) → motive m.succ),
  (match 0, n with
    | 0, n => h_1 n
    | m.succ, n => h_2 m n) =
    h_1 n
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.isRegular : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [WellFoundedLT α]
  (f : P.RankFunction α) [P.IsProper], P.IsRegular
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A]
  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal], NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
-- Init.Data.String.Defs
String.toUTF8_eq_toByteArray : ∀ {s : String}, s.toUTF8 = s.toByteArray
-- Std.Http.Data.Extensions
/-- An ordering for `Name` keys used by `Extensions`.
 -/
Std.Http.Extensions.compareName : Lean.Name → Lean.Name → Ordering
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.isRepresentation.toEnd_represents : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤)
  (A : ↥(Matrix.isRepresentation R b)), Matrix.Represents b (↑A) ((Matrix.isRepresentation.toEnd R b hb) A)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalCommSemiring : {R : Type u_1} →
  {M : Type u_4} → [inst : CommSemiring R] → [AddCommSemigroup M] → NonUnitalCommSemiring (AddMonoidAlgebra R M)
-- Init.Data.Float.Float32
/-- Obtains a `Float32` whose value is near the given `USize`.

It will be exactly the value of the given `USize` if such a `Float32` exists. If no such `Float32`
exists, the returned value will either be the smallest `Float32` that is larger than the given
value, or the largest `Float32` that is smaller than the given value.

This function has a logical model in terms of `Float32.Model`, but is overridden at runtime with an
efficient implementation.
 -/
USize.toFloat32 : USize → Float32