mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.ringHom_ext : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {I : Ideal R} [inst_2 : I.IsPrime]
  {f g : I.ResidueField →+* S}, f.comp (algebraMap R I.ResidueField) = g.comp (algebraMap R I.ResidueField) → f = g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_addXYZ : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'.baseChange A).addXYZ P Q
-- Mathlib.SetTheory.Cardinal.Finite
Cardinal.toENat_le_natCast_iff : ∀ {c : Cardinal.{u_3}} {n : ℕ}, Cardinal.toENat c ≤ ↑n ↔ c ≤ ↑n
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.convolution_indicator_one_left : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [inst : Monoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : Module S E] [inst_5 : Module S F]
  [inst_6 : TopologicalSpace F] (L : E →ₗ[S] F →ₗ[S] F) (e : E) (f : M → F),
  (∀ (y : F), (L e) y = y) → DiscreteConvolution.convolution L ({1}.indicator fun x => e) f = f
-- Mathlib.Topology.Algebra.Order.UpperLower
HasUpperLowerClosure.isOpen_lowerClosure : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α),
  IsOpen s → IsOpen ↑(lowerClosure s)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y)
  [inst_2 : AlgebraicGeometry.IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁ f₂ H)
      (CategoryTheory.CategoryStruct.comp f₂ h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization f) h
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.of_subsingleton : ∀ {α : Type u} [Subsingleton α] (s : Set α), s.Finite
-- Lean.Elab.AutoBound
Lean.Elab.AutoBoundImplicitContext.mk.sizeOf_spec : ∀ (autoImplicitEnabled : Bool) (boundVariables : Lean.PArray Lean.Expr),
  sizeOf { autoImplicitEnabled := autoImplicitEnabled, boundVariables := boundVariables } =
    1 + sizeOf autoImplicitEnabled + sizeOf boundVariables
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- The `Lp`-norm of a bounded continuous function is at most a constant (depending on the measure
of the whole space) times its sup-norm.  -/
BoundedContinuousFunction.Lp_norm_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ]
  (f : BoundedContinuousFunction α E),
  ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * ‖f‖
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryApproxSelfMax.solve : Lean.Level → Lean.Level → ℕ → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_mapComp_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  {a b c_1 : B} (f : a ⟶ b) (g : b ⟶ c_1),
  ((CategoryTheory.Bicategory.Prod.sectL B c).mapComp f g).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id c)).inv
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [inst_4 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (Std.ExtDTreeMap.ofList l cmp).get! k = default
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Poly.numTerms.go : Lean.Grind.CommRing.Poly → ℕ → ℕ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- The Radon-Nikodym derivative between a signed measure and a positive measure.

`rnDeriv s μ` satisfies `μ.withDensityᵥ (s.rnDeriv μ) = s`
if and only if `s` is absolutely continuous with respect to `μ` and this fact is known as
`MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensity_rnDeriv_eq`
and can be found in `Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean`.  -/
MeasureTheory.SignedMeasure.rnDeriv : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.SignedMeasure α → MeasureTheory.Measure α → α → ℝ
-- Mathlib.Algebra.Group.Prod
Prod.instInvolutiveInv.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : InvolutiveInv M] [inst_1 : InvolutiveInv N],
  Prod.instInvolutiveInv = { toInv := Prod.instInv, inv_inv := ⋯ }
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsThetaOTVSIsBigOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsThetaTVS 𝕜 l) (Asymptotics.IsBigOTVS 𝕜 l)
                                  (Asymptotics.IsBigOTVS 𝕜 l)
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then the distance from
`f n` to the limit of `f` is bounded above by `C * r^n / (1 - r)`.  -/
dist_le_of_le_geometric_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (r C : ℝ) {f : ℕ → α},
  r < 1 →
    (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) →
      ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → dist (f 0) a ≤ C / (1 - r)
-- Mathlib.Data.Set.Basic
Set.instBoundedOrder : {α : Type u} → BoundedOrder (Set α)
-- Mathlib.Order.Lattice
Pi.instSemilatticeInf : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → SemilatticeInf (α' i)] → SemilatticeInf ((i : ι) → α' i)
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_add_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel β γ),
  η.comp (μ + κ) = η.comp μ + η.comp κ
-- Init.Data.Array.Lemmas
Array.setIfInBounds_replicate_self : ∀ {n : ℕ} {α : Type u_1} {a : α} {i : ℕ}, (Array.replicate n a).setIfInBounds i a = Array.replicate n a
-- Mathlib.Topology.GDelta.Basic
/-- A union of two meagre sets is meagre.  -/
IsMeagre.union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsMeagre s → IsMeagre t → IsMeagre (s ∪ t)
-- Mathlib.Order.WithBot
WithBot.coe_min : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), ↑(min a b) = min ↑a ↑b
-- Mathlib.NumberTheory.Padics.Hensel
/-- `T` is an auxiliary value that is used to control the behavior of the polynomial `F`.  -/
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_gen : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} → [inst_1 : CommSemiring R] → [Algebra R ℤ_[p]] → Polynomial R → ℤ_[p] → ℝ
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (l : σ → Λ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.goto l) = Turing.TM1.Stmt.goto fun x s => Turing.TM2to1.Λ'.normal (l s)
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to a `USize`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toUSize : Float.Model → USize
-- Init.Data.UInt.Lemmas
UInt32.toUSize_inj : ∀ {a b : UInt32}, a.toUSize = b.toUSize ↔ a = b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited α] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (t.insertMany l).get! k = default
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_add_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] (a b : α), min a b + max a b = a + b
-- Init.Data.Array.Lemmas
Array.toList_fst_unzip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip.1.toList = xs.toList.unzip.1
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- Being differentiable in the model space is a local property, invariant under smooth maps.
Therefore, it will lift nicely to manifolds.  -/
differentiableWithinAt_localInvariantProp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'},
  (contDiffGroupoid 1 I).LocalInvariantProp (contDiffGroupoid 1 I') (DifferentiableWithinAtProp I I')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.negAddY_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.mkCone_pt : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none)
  (π : (j : J) → X ⟶ F.obj (some j))
  (w :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (π j) (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) = f),
  (CategoryTheory.Limits.WidePullbackShape.mkCone f π w).pt = X
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instLeast? : Std.PRange.Least? Int8
-- Mathlib.Analysis.Convex.Extreme
extremePoints_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E}, Set.extremePoints 𝕜 A ⊆ A
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Theorems.mkEmpty : (α : Type) → Lean.Meta.Grind.Theorems α
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instSMulCommClass : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass R S M] [inst_6 : SMul S R]
  [IsScalarTower S R M], SMulCommClass S (Module.End R M) (Module.End R M)
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.vadd_apply : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G β] (g : G) (f : α ↪ β) (a : α),
  (g +ᵥ f) a = g +ᵥ f a
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_xor : ∀ (a b : UInt32), (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
-- Mathlib.Topology.Order.ProjIcc
Filter.Tendsto.IccExtend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LinearOrder α] {a b : α} {h : a ≤ b} (f : γ → ↑(Set.Icc a b) → β)
  {la : Filter α} {lb : Filter β} {lc : Filter γ},
  Filter.Tendsto (↿f) (lc ×ˢ Filter.map (Set.projIcc a b h) la) lb →
    Filter.Tendsto (↿(Set.IccExtend h ∘ f)) (lc ×ˢ la) lb
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.sigma_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S), 𝒰.sigma.I₀ = PUnit.{v + 1}
-- Std.Sync.Channel
Std.CloseableChannel.instReprError : Repr Std.CloseableChannel.Error
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_ofReal_re : ∀ (x : ℝ), (Complex.sin ↑x).re = Real.sin x
-- Init.Data.String.Lemmas.Iterate
/-- A list of all positions strictly before `p`, ordered from largest to smallest.

This function is not meant to be used in actual programs. Actual programs should use
`Slice.revPositionsFrom` and `Slice.revPositions`.
 -/
String.Slice.Model.revPositionsFrom : {s : String.Slice} → s.Pos → List { p // p ≠ s.endPos }
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.pap.inj : ∀ {c : Lean.IR.FunId} {ys : Array Lean.IR.Arg} {c_1 : Lean.IR.FunId} {ys_1 : Array Lean.IR.Arg},
  Lean.IR.Expr.pap c ys = Lean.IR.Expr.pap c_1 ys_1 → c = c_1 ∧ ys = ys_1
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.getBoundedAppArgsAux : Lean.Expr → Array Lean.Expr → ℕ → Array Lean.Expr
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `antivaryOn_iff_exists_monotoneOn_antitoneOn`. -/
AntivaryOn.exists_monotoneOn_antitoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → ∃ x, MonotoneOn f s ∧ AntitoneOn g s
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- An isomorphism of short complexes `S₁ ≅ S₂` induces an isomorphism on the `K` fields
of left homology data of `S₁` and `S₂`.  -/
CategoryTheory.ShortComplex.cyclesMapIso' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → (h₁ : S₁.LeftHomologyData) → (h₂ : S₂.LeftHomologyData) → h₁.K ≅ h₂.K
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y : CategoryTheory.Subobject B) (h : X ≤ Y),
  X.ofLE Y h = CategoryTheory.Subobject.underlying.map h.hom
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.coe_toPartialHomeomorph_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.symm = ↑e.symm
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.eq_def : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n → α → α) (j : ℕ) (a : j ≤ n) (a_1 : α),
  Nat.foldTR.loop✝ n f j a a_1 =
    match j, a, a_1 with
    | 0, h, a => a
    | m.succ, h, a => Nat.foldTR.loop✝ n f m ⋯ (f (n - m.succ) ⋯ a)
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.mk.injEq : ∀ (id method : String) (registerOptions : Option Lean.Json) (id_1 method_1 : String)
  (registerOptions_1 : Option Lean.Json),
  ({ id := id, method := method, registerOptions := registerOptions } =
      { id := id_1, method := method_1, registerOptions := registerOptions_1 }) =
    (id = id_1 ∧ method = method_1 ∧ registerOptions = registerOptions_1)
-- Init.Data.UInt.IntToBitVec
USize.ne_iff_toBitVec32_ne : ∀ {a b : USize} (h : System.Platform.numBits = 32), a ≠ b ↔ a.toBitVec32 h ≠ b.toBitVec32 h
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk.injEq : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier)
  (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R)
  (neg_mem'_1 : ∀ {x : R}, x ∈ toNonUnitalSubsemiring_1.carrier → -x ∈ toNonUnitalSubsemiring_1.carrier),
  ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := neg_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := neg_mem'_1 }) =
    (toNonUnitalSubsemiring = toNonUnitalSubsemiring_1)
-- Lean.Compiler.CSimpAttr
/-- Map from `e.fromDeclName` to `e`  -/
Lean.Compiler.CSimp.State.map : Lean.Compiler.CSimp.State → Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry
-- Mathlib.Data.Multiset.Bind
Multiset.bind_bind : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : α → β → Multiset γ},
  (m.bind fun a => n.bind fun b => f a b) = n.bind fun b => m.bind fun a => f a b
-- Mathlib.Algebra.Module.BigOperators
Fintype.sum_piFinset_apply : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : AddCommMonoid α]
  (f : κ → α) (s : Finset κ) (i : ι),
  ∑ g ∈ Fintype.piFinset fun x => s, f (g i) = s.card ^ (Fintype.card ι - 1) • ∑ b ∈ s, f b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.pow_eq_one_iff : ∀ {β : Type u_3} [Finite β] {f : Equiv.Perm β}, f.IsCycle → ∀ {n : ℕ}, f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_union_eq_left_of_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  (∀ᵐ (x : X) ∂μ.restrict t, f x = 0) → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instHasColimitsOfShapeOppositeElementsFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  CategoryTheory.Limits.HasColimitsOfShape Φ.fiber.Elementsᵒᵖ A
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_uIoo : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.uIoo i j = Set.uIoo i.castSucc j.castSucc
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofIsoComp_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X)
  [inst_1 : CategoryTheory.IsIso g]
  (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)),
  (CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).m = F.m
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearMap_id : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₂ : ι → Type u_9} [inst_1 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_2 : (i : ι) → Module R (β₂ i)], (DFinsupp.mapRange.linearMap fun i => LinearMap.id) = LinearMap.id
-- Mathlib.Algebra.Group.Prod
Prod.instAddRightCancelSemigroup : {G : Type u_1} →
  {H : Type u_2} → [AddRightCancelSemigroup G] → [AddRightCancelSemigroup H] → AddRightCancelSemigroup (G × H)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.self_trans_symm : ∀ {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₂] (e : A₁ ≃ₐ[R] A₂), e.trans e.symm = AlgEquiv.refl
-- Mathlib.Order.SymmDiff
/-- **Alias** of `symmDiff_eq_xor`. -/
symmDiff_eq_Xor' : ∀ (p q : Prop), symmDiff p q = Xor p q
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.exists_forall_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Nonempty β] [inst_2 : Preorder β] [IsDirectedOrder β]
  (f : MeasureTheory.SimpleFunc α β), ∃ C, ∀ (x : α), f x ≤ C
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.pow_eq_eval : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {l : Mathlib.Tactic.FieldSimp.NF M} {r : ℕ},
  r ≠ 0 → ∀ {x : M}, x = l.eval → x ^ r = (l ^ r).eval
-- Mathlib.Algebra.BigOperators.Finprod
finsum_subtype_eq_finsum_cond : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} (p : α → Prop),
  ∑ᶠ (j : Subtype p), f ↑j = ∑ᶠ (i : α) (_ : p i), f i
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonDocumentFilter : Lean.FromJson Lean.Lsp.DocumentFilter
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `φ` is a monomorphism in `CommRingCat`, it is not in general true that `Spec φ` is epi.
(`ℤ ⊆ ℤ[1/2]` but `Spec ℤ[1/2] ⟶ Spec ℤ` is not epi, since epi open immersions are isomorphisms)
But if the range of `f g : Spec R ⟶ X` are contained in an common affine open `U`, one can still
cancel `Spec.map φ ≫ f = Spec.map φ ≫ g` to get `f = g`.  -/
AlgebraicGeometry.eq_of_SpecMap_comp_eq_of_isAffineOpen : ∀ {R S : CommRingCat} {X : AlgebraicGeometry.Scheme} (φ : R ⟶ S),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom φ) →
    ∀ {f g : AlgebraicGeometry.Spec R ⟶ X} (U : X.Opens),
      AlgebraicGeometry.IsAffineOpen U →
        (TopologicalSpace.Opens.map f.base).obj U = ⊤ →
          (TopologicalSpace.Opens.map g.base).obj U = ⊤ →
            CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) f =
                CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) g →
              f = g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.ext : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I J : HomogeneousIdeal 𝒜}, I.toIdeal = J.toIdeal → I = J
-- Lean.Meta.Order
/-- Given an array of CCPO instances `insts = #[CCPO α₁, ..., CCPO αₙ]`, constructs an instance
of the type `CCPO (α₁ × ... × αₙ)`.
Can handle `CompleteLattice` as well.
 -/
Lean.Meta.mkPackedPPRodInstance : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a closed range `lo<...*`.
This is an internal function.
Use `Roi.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Roi.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Roi α → Std.Iter α
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- An inequality `P ≤ P'` between monoidal properties of objects induces
a braided functor between full braided subcategories.  -/
CategoryTheory.ObjectProperty.instBraidedFullSubcategoryιOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {P : CategoryTheory.ObjectProperty C} →
        [inst_2 : P.IsMonoidal] →
          [inst_3 : CategoryTheory.BraidedCategory C] →
            {P' : CategoryTheory.ObjectProperty C} →
              [inst_4 : P'.IsMonoidal] → (h : P ≤ P') → (CategoryTheory.ObjectProperty.ιOfLE h).Braided
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.toBotHom : {α : Type u_6} →
  {β : Type u_7} → [inst : Max α] → [inst_1 : Max β] → [inst_2 : Bot α] → [inst_3 : Bot β] → SupBotHom α β → BotHom α β
-- Init.Data.UInt.Lemmas
UInt32.add_right_neg : ∀ (a : UInt32), a + -a = 0
-- Mathlib.CategoryTheory.Yoneda
/-- When `C` is a category such that `Category.{v₁} C`, then
the functor `uliftYoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type (max w v₁)` is fully faithful.  -/
CategoryTheory.ULiftYoneda.fullyFaithful : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.uliftYoneda.{w, v₁, u₁}.FullyFaithful
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
CategoryTheory.Functor.instIsLeftAdjointDiscreteTensorLeftCompIncl : ∀ (I : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor I C),
  (CategoryTheory.MonoidalCategory.tensorLeft ((CategoryTheory.Functor.incl✝ I).comp F)).IsLeftAdjoint