mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Smooth.Fiber
/-- [Stacks Tag 08WD](https://stacks.math.columbia.edu/tag/08WD) ((3) => (1)) -/
Algebra.Etale.of_formallyUnramified_of_flat : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] [Module.Flat R S] [Algebra.FormallyUnramified R S], Algebra.Etale R S
-- Mathlib.NumberTheory.LucasLehmer
modEq_mersenne : ∀ (n k : ℕ), k ≡ k / 2 ^ n + k % 2 ^ n [MOD 2 ^ n - 1]
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
CovariantDerivative.derivMetricTensor_apply : ∀ {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] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] {σ τ : (x : M) → V x}
  (cov : CovariantDerivative I F V) [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
  {X : (x : M) → TangentSpace I x} [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F] (x : M),
  MDiffAt (T% σ) x →
    MDiffAt (T% τ) x →
      (((cov.derivMetricTensor x) (σ x)) (τ x)) (X x) =
        ((d% fun x => inner ℝ (σ x) (τ x)) x) (X x) - (fun x => inner ℝ ((fun x => (↑cov σ x) (X x)) x) (τ x)) x -
          (fun x => inner ℝ (σ x) ((fun x => (↑cov τ x) (X x)) x)) x
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.measurable_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (x : ℝ),
  Measurable fun a => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearMap.inl` as an isometry.  -/
QuadraticMap.Isometry.inl : {R : Type u_2} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {P : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R P] → (Q₁ : QuadraticMap R M₁ P) → (Q₂ : QuadraticMap R M₂ P) → Q₁ →qᵢ Q₁.prod Q₂
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.equivCongrLeft_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι ≃ κ)
  (f : DirectSum ι fun i => β i) (k : κ), ((DirectSum.equivCongrLeft h) f) k = f (h.symm k)
-- Mathlib.Algebra.Algebra.Basic
Algebra.mem_algebraMapSubmonoid_of_mem : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submonoid R}
  (x : ↥M), (algebraMap R S) ↑x ∈ Algebra.algebraMapSubmonoid S M
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The image of the unit ball under a continuous multilinear map is bounded.  -/
ContinuousMultilinearMap.unit_le_opNorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i}, ‖m‖ ≤ 1 → ‖f m‖ ≤ ‖f‖
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.r400 : String
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- The homeomorphism between `AddCircle (2 * π)` and `Circle`.  -/
AddCircle.homeomorphCircle' : AddCircle (2 * Real.pi) ≃ₜ Circle
-- Init.Data.UInt.Lemmas
UInt32.toFin_toBitVec : ∀ (x : UInt32), x.toBitVec.toFin = x.toFin
-- Mathlib.Order.Partition.Basic
Partition.mem_partOf_iff : ∀ {α : Type u_1} {x y : α} {u : Set α} {P : Partition u}, x ∈ P.partOf y ↔ P.Rel y x
-- Init.Data.UInt.Lemmas
UInt64.toUSize_div_of_toNat_lt : ∀ (a b : UInt64), a.toNat < USize.size → b.toNat < USize.size → (a / b).toUSize = a.toUSize / b.toUSize
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.e.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  (i : ↥b.support),
  RootPairing.GeckConstruction.e i =
    Matrix.fromBlocks 0 (Matrix.of fun i' j => if i' = i ∧ j = -↑i then 1 else 0)
      (Matrix.of fun i' j => if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
      (Matrix.of fun i' j => if P.root i' = P.root ↑i + P.root j then ↑(RootPairing.chainBotCoeff (↑i) j) + 1 else 0)
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.projectiveDimension_le_projectiveDimension_of_isLocalizedModule : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R) (M : ModuleCat R),
  CategoryTheory.projectiveDimension (M.localizedModule S) ≤ CategoryTheory.projectiveDimension M
-- Mathlib.Order.LatticeIntervals
/-- `Icc a b` has a bottom element whenever `a ≤ b`.  -/
Set.Icc.instOrderBotElemOfFactLe : {α : Type u_1} → {a b : α} → [inst : Preorder α] → [Fact (a ≤ b)] → OrderBot ↑(Set.Icc a b)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.dual : ∀ {α : Type u_1} {t : Ordnode α}, t.Sized → t.dual.Sized
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.brecOn.eq : ∀ {α : Type u} {β : α → Type v} {motive : Std.DTreeMap.Internal.Zipper α β → Sort u_1}
  (t : Std.DTreeMap.Internal.Zipper α β)
  (F_1 : (t : Std.DTreeMap.Internal.Zipper α β) → Std.DTreeMap.Internal.Zipper.below t → motive t),
  Std.DTreeMap.Internal.Zipper.brecOn t F_1 = F_1 t (Std.DTreeMap.Internal.Zipper.brecOn.go t F_1).2
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {kmi : α}, (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `G n` tends to `f` a.e., each `G n` is `AEStronglyMeasurable` and the liminf of the lower
Lebesgue integral of `‖G n ·‖ₑ` is finite, then `f` is Lebesgue integrable.  -/
MeasureTheory.integrable_of_tendsto : ∀ {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  (∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (f x))) →
    (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) μ) →
      Filter.liminf (fun n => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop ≠ ⊤ → MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms D] (F G : CategoryTheory.Functor C D) (j : C),
  CategoryTheory.NatTrans.app 0 j = 0
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Module.FaithfullyFlat.isLocalHom : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B], IsLocalHom (algebraMap A B)
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_norm_div' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u / v‖
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `eraseMany` which can be used in absence of balance information but still
assumes the preconditions of `eraseMany`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.eraseMany! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} → [ForIn Id ρ α] → (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.IteratedSlowErasureFrom
-- Mathlib.Topology.Algebra.UniformConvergence
instIsScalarTowerUniformOnFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} {N : Type u_6} [inst : SMul M N] [inst_1 : SMul M β]
  [inst_2 : SMul N β] [IsScalarTower M N β], IsScalarTower M N (UniformOnFun α β 𝔖)
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.iff_of_equiv : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B),
  Algebra.FormallyUnramified R A ↔ Algebra.FormallyUnramified R B
-- Init.Data.Vector.Lemmas
Vector.insertIdx.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n),
  xs = xs_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (x x_1 : α), x = x_1 → ∀ (h : i ≤ n), xs.insertIdx i x h = xs_1.insertIdx i_1 x_1 ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ [Inhabited α] {k fallback : α} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₀_inverse : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A')
  (e' : A' ≌ B'), (AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').inverse = e'.inverse.comp eA.inverse
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Adjunction.mapMon_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [inst_6 : a.IsMonoidal],
  a.mapMon.unit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapMonIdIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapMonNatTrans a.unit)
        CategoryTheory.Functor.mapMonCompIso.hom)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsAddUnit.sum_univ_iff : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] {f : ι → M},
  IsAddUnit (∑ a, f a) ↔ ∀ (a : ι), IsAddUnit (f a)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_smul_self : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : StarMul α] (c : α) (M : Matrix m n α),
  (c • M).conjTranspose = MulOpposite.op (star c) • M.conjTranspose
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.map_eq_top_iff_of_ker_le : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {I : Ideal R},
  RingHom.ker f ≤ I → f.IsIntegral → (Ideal.map f I = ⊤ ↔ I = ⊤)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toAddEquiv : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  ⇑↑f = ⇑f
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f),
  HomotopicalAlgebra.Fibration h.p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_map : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] [Std.LawfulEqOrd α] {f : α → β → γ} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.map f t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.map f t) k h' =
    f k (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)
-- Mathlib.Order.Filter.Bases.Basic
Filter.notMem_iff_inf_principal_compl : ∀ {α : Type u_1} {f : Filter α} {s : Set α}, s ∉ f ↔ (f ⊓ Filter.principal sᶜ).NeBot
-- Init.Data.SInt.Lemmas
Int8.toInt16_ofNat : ∀ {n : ℕ}, n ≤ 127 → (OfNat.ofNat n).toInt16 = OfNat.ofNat n
-- Lean.Server.Snapshots
/-- Run a `CoreM` computation using the data in the given snapshot. -/
Lean.Server.Snapshots.Snapshot.runCoreM : {α : Type} → Lean.Server.Snapshots.Snapshot → Lean.Server.DocumentMeta → Lean.CoreM α → EIO Lean.Exception α
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure_singleton_le_iff_mem : ∀ {M : Type u_1} [inst : Mul M] (m : M) (p : Subsemigroup M), Subsemigroup.closure {m} ≤ p ↔ m ∈ p
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies an expression `Nat.cast n`, returning `n`.  -/
Mathlib.Meta.NormNum.evalNatCast : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Multiset.stronglyMeasurable_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} (l : Multiset (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) → MeasureTheory.StronglyMeasurable l.prod
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : NonUnitalNonAssocSemiring S] (b : S)
  (s : SkewMonoidAlgebra k G) {f : G → k → S}, s.sum f * b = s.sum fun a c => f a c * b
-- Init.Grind.AC
Lean.Grind.AC.diseq_unsat : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.diseq_unsat_cert lhs rhs = true →
    Lean.Grind.AC.Seq.denote ctx lhs ≠ Lean.Grind.AC.Seq.denote ctx rhs → False
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.zero_comp : ∀ {β : Type v} {γ : Type w} {δ : Type u_2} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace δ] [inst_3 : Zero δ] (g : CocompactMap β γ), ZeroAtInftyContinuousMap.comp 0 g = 0
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iff : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W] (X : C), F.HasPointwiseLeftDerivedFunctorAt W X ↔ L.HasPointwiseRightKanExtensionAt F (L.obj X)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_strict_mono_or_ker_sup_lt_ker_sup : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Ring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {p p' : Submodule R M} (f : M →ₛₗ[τ₁₂] M₂),
  p < p' → Submodule.map f p < Submodule.map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G),
  (∀ (x : G), x ∈ Subgroup.zpowers g) →
    (Rep.Hom.hom (Rep.leftRegular k G).norm).range =
      (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).ker
-- Init.Data.Int.Lemmas
Int.negSucc_mul_negOfNat : ∀ (m n : ℕ), Int.negSucc m * Int.negOfNat n = Int.ofNat (m.succ * n)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral_const : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (c : E),
  BoxIntegral.integral I l (fun x => c) vol = (vol I) c
-- Mathlib.Logic.Equiv.Option
/-- The bijection `{ i // i ≠ i₀ } ⊕ PUnit ≃ α` for any `i₀ : α`.  -/
Equiv.subtypeNeSumPUnit : {α : Type u_1} → [DecidableEq α] → (i₀ : α) → { i // i ≠ i₀ } ⊕ PUnit.{u + 1} ≃ α
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc : ∀ (R : CommRingCat) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec R).toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).inv) h) =
    h
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKey_eq_getKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {h : m.contains a = true},
  m.getKey a h = Std.Internal.List.getKey a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Mathlib.Tactic.FunProp.FunctionData
/-- Decompose function `fun x ↦ f y₁ ... yₙ` over specified argument indices `#[i, j, ...]`.

The result is:
```
(fun (yᵢ',yⱼ',...) ↦ f y₁ .. yᵢ' .. yⱼ' .. yₙ) ∘ (fun x ↦ (yᵢ, yⱼ, ...))
```

This is not possible if `yₗ` for `l ∉ #[i,j,...]` still contains `x`.
In such case `none` is returned.
 -/
Mathlib.Meta.FunProp.FunctionData.decompositionOverArgs : Mathlib.Meta.FunProp.FunctionData → Array ℕ → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, `AddGrpCat.{u}` has limits of shape `J`.  -/
AddGrpCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J AddGrpCat
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_piCurry_symm : ∀ {ι : Type u_6} {κ : ι → Type u_7} (X : (i : ι) → κ i → Type u_8)
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)], ⇑(MeasurableEquiv.piCurry X).symm = Sigma.uncurry
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.multiplicity_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  Besicovitch.multiplicity E ≤ 5 ^ Module.finrank ℝ E
-- Mathlib.Algebra.Module.Presentation.Free
Module.Relations.Solution.IsPresentation.free : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} (M : Type v) [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] [IsEmpty relations.R] {solution : relations.Solution M},
  solution.IsPresentation → Module.Free A M
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.category.inj : ∀ {catName declName : Lean.Name} {behavior : Lean.Parser.LeadingIdentBehavior} {catName_1 declName_1 : Lean.Name}
  {behavior_1 : Lean.Parser.LeadingIdentBehavior},
  Lean.Parser.ParserExtension.OLeanEntry.category catName declName behavior =
      Lean.Parser.ParserExtension.OLeanEntry.category catName_1 declName_1 behavior_1 →
    catName = catName_1 ∧ declName = declName_1 ∧ behavior = behavior_1
-- Mathlib.Logic.Equiv.Defs
Equiv.equivCongr_apply_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) (e : α ≃ γ) (x : β),
  ((ab.equivCongr cd) e) x = cd (e (ab.symm x))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerRight_left_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.Limits.pullback.fst T.hom R.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom R.hom) (CategoryTheory.Over.Hom.left f)
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.empty : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α], DirSupClosedOn D ∅
-- Mathlib.Probability.Martingale.Basic
/-- A family of integrable functions `f : ι → Ω → E` is a supermartingale with respect to a
filtration `ℱ` if `f` is strongly adapted with respect to `ℱ` and for all `i ≤ j`,
`μ[f j | ℱ.le i] ≤ᵐ[μ] f i`.  -/
MeasureTheory.Supermartingale : {Ω : Type u_1} →
  {E : Type u_2} →
    {ι : Type u_3} →
      [inst : Preorder ι] →
        {m0 : MeasurableSpace Ω} →
          [inst_1 : NormedAddCommGroup E] →
            [NormedSpace ℝ E] → [LE E] → (ι → Ω → E) → MeasureTheory.Filtration ι m0 → MeasureTheory.Measure Ω → Prop
-- Mathlib.Algebra.Group.Units.Hom
Units.map_mk : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (val inv : M) (val_inv : val * inv = 1)
  (inv_val : inv * val = 1),
  (Units.map f) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
    { val := f val, inv := f inv, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.instFormallyEtaleRing : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R), Algebra.FormallyEtale R P.Ring
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.comap_upperCentralSeries_quotient_center`. -/
comap_upperCentralSeries_quotient_center : ∀ {G : Type u_1} [inst : Group G] (n : ℕ),
  Subgroup.comap (QuotientGroup.mk' (Subgroup.center G)) (Subgroup.upperCentralSeries (G ⧸ Subgroup.center G) n) =
    Subgroup.upperCentralSeries G n.succ
-- Mathlib.LinearAlgebra.TensorPower.Pairing
/-- The canonical multilinear map from `n` copies of the dual of the module `M`
to the dual of `⨂[R]^n M`.  -/
TensorPower.multilinearMapToDual : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (n : ℕ) → MultilinearMap R (fun x => Module.Dual R M) (Module.Dual R (TensorPower R n M))
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.injective_of_surjective_of_submodule : ∀ {R : Type u} [inst : Semiring R] [OrzechProperty R] {M : Type v} [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- **Alias** of `infEDist_smul₀`. -/
infEdist_smul₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] {c : 𝕜},
  c ≠ 0 → ∀ (s : Set E) (x : E), Metric.infEDist (c • x) (c • s) = ‖c‖₊ • Metric.infEDist x s
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- **Alias** of `Ideal.finite_setOfPred_absNorm_le₀`. -/
Ideal.finite_setOf_absNorm_le₀ : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  [CharZero S] (n : ℕ), {I | Ideal.absNorm ↑I ≤ n}.Finite
-- Mathlib.RingTheory.MatrixAlgebra
kroneckerLinearEquiv_tmul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_5} [inst : CommSemiring R]
  [inst_1 : Fintype l] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Fintype p] [inst_5 : DecidableEq l]
  [inst_6 : DecidableEq m] [inst_7 : DecidableEq n] [inst_8 : DecidableEq p] (x : Matrix l m R) (y : Matrix n p R),
  (kroneckerLinearEquiv l m n p R) (x ⊗ₜ[R] y) = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.ne_zero_of_not_supDegree_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p : AddMonoidAlgebra R A} {b : B}, ¬AddMonoidAlgebra.supDegree D p ≤ b → p ≠ 0
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedCommRing.toNonUnitalCommRing : {α : Type u_5} → [self : NonUnitalSeminormedCommRing α] → NonUnitalCommRing α
-- Mathlib.Algebra.Group.Submonoid.Finsupp
Submonoid.mem_closure_range_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {ι : Type u_2} {f : ι → M} {x : M},
  x ∈ Submonoid.closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2