mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.mk.injEq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (f : P.toExtension.Cotangent → ↥P.toExtension.ker)
  (hf : ∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f b) = b) (g : P.Ring) (hgmem : g - 1 ∈ P.ker)
  (hg : g • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f ∘ ⇑b))) (f_1 : P.toExtension.Cotangent → ↥P.toExtension.ker)
  (hf_1 : ∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f_1 b) = b) (g_1 : P.Ring)
  (hgmem_1 : g_1 - 1 ∈ P.ker) (hg_1 : g_1 • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f_1 ∘ ⇑b))),
  ({ f := f, hf := hf, g := g, hgmem := hgmem, hg := hg } =
      { f := f_1, hf := hf_1, g := g_1, hgmem := hgmem_1, hg := hg_1 }) =
    (f = f_1 ∧ g = g_1)
-- Mathlib.Analysis.Real.Sqrt
NNReal.sq_sqrt : ∀ (x : NNReal), NNReal.sqrt x ^ 2 = x
-- Mathlib.Data.Finsupp.Sigma
/-- Values of `embSigma f` at indices outside the `k`-th summand are zero.  -/
Finsupp.embSigma_apply_of_ne : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k k' : κ} (f : ι k →₀ M),
  k' ≠ k → ∀ (i : ι k'), f.embSigma ⟨k', i⟩ = 0
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
FredholmDecomposition.mk.injEq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (X₀ X₁ : Submodule 𝕜 E) (isTopCompl : Submodule.IsTopCompl X₁ X₀)
  (finite_X₀ : FiniteDimensional 𝕜 ↥X₀) (X₀_1 X₁_1 : Submodule 𝕜 E) (isTopCompl_1 : Submodule.IsTopCompl X₁_1 X₀_1)
  (finite_X₀_1 : FiniteDimensional 𝕜 ↥X₀_1),
  ({ X₀ := X₀, X₁ := X₁, isTopCompl := isTopCompl, finite_X₀ := finite_X₀ } =
      { X₀ := X₀_1, X₁ := X₁_1, isTopCompl := isTopCompl_1, finite_X₀ := finite_X₀_1 }) =
    (X₀ = X₀_1 ∧ X₁ = X₁_1)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.op_map_id_obj : ∀ {X : TopCat} (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).op.obj U = U
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_subsingleton : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} {f : (i : α) → Finset (δ i)},
  (∀ (i : α), (↑(f i)).Subsingleton) → (↑(Fintype.piFinset f)).Subsingleton
-- Mathlib.Order.GameAdd
/-- The `Sym2.GameAdd` relation on well-founded inputs is well-founded.  -/
WellFounded.sym2_gameAdd : ∀ {α : Type u_1} {rα : α → α → Prop}, WellFounded rα → WellFounded (Sym2.GameAdd rα)
-- Init.Data.UInt.Lemmas
USize.toFin_mul : ∀ (a b : USize), (a * b).toFin = a.toFin * b.toFin
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_ofEqAppend : ∀ {s t₁ t₂ : String} (h : s = t₁ ++ t₂), (String.Pos.ofEqAppend h).Splits t₁ t₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.isPullback₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- A section `s` is a gluing for a family of sections `sf` if it restricts to `sf i` on `U i`,
for all `i`
 -/
TopCat.Presheaf.IsGluing : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type u_3} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X : TopCat} →
              (F : TopCat.Presheaf C X) →
                {ι : Type u_4} →
                  (U : ι → TopologicalSpace.Opens ↑X) →
                    ((i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))) →
                      CategoryTheory.ToType (F.obj (Opposite.op (iSup U))) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.hasImage_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C}, CategoryTheory.Limits.HasImage 0
-- Mathlib.Order.KrullDimension
/-- In a maximally long series, i.e one as long as the height of the last element, the height of each
element is its index in the series.
 -/
Order.height_eq_index_of_length_eq_height_last : ∀ {α : Type u_1} [inst : Preorder α] {p : LTSeries α},
  ↑p.length = Order.height (RelSeries.last p) → ∀ (i : Fin (p.length + 1)), Order.height (p.toFun i) = ↑↑i
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify the step branch of `BirdDet.sumFrom`.

This corresponds to the `lo < n` branch of:

```
sumFrom n lo f = if lo < n then f lo + sumFrom n (lo + 1) f else 0
```

Throws a meta-level error if called with `lo` such that `¬ lo < ctx.dimension`.
 -/
Mathlib.Tactic.Determinant.certSumFromStep : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      ℕ →
        Q(ℕ → «$α») →
          Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα) →
            Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα) →
              Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A group of order `p ^ 2` is not cyclic if and only if its exponent is `p`.  -/
not_isCyclic_iff_exponent_eq_prime : ∀ {α : Type u_1} [inst : Group α] {p : ℕ}, Nat.Prime p → Nat.card α = p ^ 2 → (¬IsCyclic α ↔ Monoid.exponent α = p)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_lid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {N' : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N'] (f : N →ₗ[R] N')
  (g : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.assoc R R M N') ∘ₗ TensorProduct.map (↑(TensorProduct.lid R M).symm) f ∘ₗ g =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ
      ↑(TensorProduct.lid R (TensorProduct R M N)).symm ∘ₗ g
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- The Weierstrass curve `Y² + (j - 1728)XY = X³ - 36(j - 1728)³X - (j - 1728)⁵`.
It is a modification of the curve in [silverman2009], Chapter III, Proposition 1.4 (c) to avoid
denominators. It is of j-invariant j if it is an elliptic curve.  -/
WeierstrassCurve.ofJNe0Or1728 : {R : Type u_1} → [CommRing R] → R → WeierstrassCurve R
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.union_ae_eq_left_iff_ae_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ∪ t =ᵐ[μ] s ↔ t ≤ᵐ[μ] s
-- Mathlib.Tactic.Clean
/-- Clean an expression by eliminating identify functions listed in `cleanConsts`.
Also eliminates `fun x => x` applications and tautological `let`/`have` bindings.  -/
Lean.Expr.clean : Lean.Expr → Lean.Expr
-- Mathlib.Analysis.RCLike.ContinuousMap
/-- Mapping `C(X, 𝕜)` to `C(X, ℝ)` using `RCLike.re`.  -/
ContinuousMap.rclikeToReal : {X : Type u_1} → {𝕜 : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : RCLike 𝕜] → C(X, 𝕜) → C(X, ℝ)
-- Mathlib.RingTheory.AdjoinRoot
PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S)
  (I : Ideal R) (g : Polynomial R),
  (pb.quotientEquivQuotientMinpolyMap I)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)) =
    (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.Options.mk.sizeOf_spec : ∀ (recursive ignoreIfNotExists : Bool),
  sizeOf { recursive := recursive, ignoreIfNotExists := ignoreIfNotExists } =
    1 + sizeOf recursive + sizeOf ignoreIfNotExists
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_toList_rco : ∀ {m n : ℕ}, (m...n).toList.toArray = (m...n).toArray
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.mk_eq_of_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g f' : C}
  {η θ : f ⟶ g} {η' θ' : f ≅ g}
  (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f ≅ f')
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g ≅ f'),
  η'.hom = η →
    θ'.hom = θ →
      CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) η' ≪≫ η_g =
          η_f →
        CategoryTheory.MonoidalCategory.whiskerLeftIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) θ' ≪≫ η_g =
            η_f →
          η = θ
-- Batteries.Data.Int
/-- Construct an integer from a sequence of bits using little endian convention.

The sign is determined using the two's complement convention: the result is negative if and only if
`n > 0` and `f (n-1) = true`.
 -/
Int.ofBits : {n : ℕ} → (Fin n → Bool) → ℤ
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.mapPiLocalization_comp : ∀ {R : Type u_1} {S : Type u_2} (P : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring P] (f : R →+* S) (g : S →+* P),
  PrimeSpectrum.mapPiLocalization (g.comp f) =
    (PrimeSpectrum.mapPiLocalization g).comp (PrimeSpectrum.mapPiLocalization f)
-- Std.Http.Protocol.H1
/-- The state of the reader.
 -/
Std.Http.Protocol.H1.Machine.reader : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`.  -/
Orientation.inner_mul_areaForm_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a x y : E),
  inner ℝ a x * (o.areaForm a) y - (o.areaForm a) x * inner ℝ a y = ‖a‖ ^ 2 * (o.areaForm x) y
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opEquivalence_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C],
  SimplicialObject.opEquivalence.counitIso = SimplicialObject.opFunctorCompOpFunctorIso
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey.mk.inj : ∀ {localInsts : Lean.LocalInstances} {type : Lean.Expr} {synthPendingDepth : ℕ} {localInsts_1 : Lean.LocalInstances}
  {type_1 : Lean.Expr} {synthPendingDepth_1 : ℕ},
  { localInsts := localInsts, type := type, synthPendingDepth := synthPendingDepth } =
      { localInsts := localInsts_1, type := type_1, synthPendingDepth := synthPendingDepth_1 } →
    localInsts = localInsts_1 ∧ type = type_1 ∧ synthPendingDepth = synthPendingDepth_1
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.smul_mk : ∀ {G : Type u_1} {K : Type u_2} {V : Type u_3} [inst : AddCommGroup V] [inst_1 : DivisionRing K] [inst_2 : Module K V]
  [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G K V] (g : G) {v : V} (hv : v ≠ 0),
  g • Projectivization.mk K v hv = Projectivization.mk K (g • v) ⋯
-- Mathlib.Combinatorics.Configuration
Configuration.Nondegenerate.eq_or_eq : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.Nondegenerate P L] {p₁ p₂ : P}
  {l₁ l₂ : L}, p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Each prefix has at least as many `U`s as `D`s  -/
DyckWord.count_D_le_count_U : ∀ (self : DyckWord) (i : ℕ), List.count DyckStep.D (List.take i ↑self) ≤ List.count DyckStep.U (List.take i ↑self)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_one : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.constantCoeff 1 = 1
-- Lean.Message
Lean.MessageLog.getInfoMessages : Lean.MessageLog → Lean.MessageLog
-- Lean.SubExpr
Lean.SubExpr.Pos.pushBindingBody : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_const : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R}, ∑ j ∈ t, w j ≠ 0 → ∀ (c : E), t.centerMass w (Function.const ι c) = c
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The torsion submodule is always a torsion module.  -/
Submodule.torsion_isTorsion : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.IsTorsion R ↥(Submodule.torsion R M)
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.startsWith.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (w : α × Bool), FreeGroup.startsWith w = {g | g.toWord[0]? = some w}
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a basemap `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.  -/
ContinuousWithinAt.clm_bundle_apply : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B] [inst_14 : TopologicalSpace M] [inst_15 : FiberBundle F₁ E₁]
  [inst_16 : VectorBundle 𝕜 F₁ E₁] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] {b : M → B}
  {v : (x : M) → E₁ (b x)} {s : Set M} {x : M} [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  ContinuousWithinAt (fun m => ⟨b m, ϕ m⟩) s x →
    ContinuousWithinAt (fun m => ⟨b m, v m⟩) s x → ContinuousWithinAt (fun m => ⟨b m, (ϕ m) (v m)⟩) s x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filterMap f m).get? k = (m.get? k).bind (f k)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- A continuous linear map admits a left inverse which is a continuous linear map itself.  -/
ContinuousLinearMap.HasLeftInverse : {R : Type u_1} →
  [inst : Semiring R] →
    {E : Type u_2} →
      {F : Type u_4} →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : TopologicalSpace F] → [inst_5 : AddCommMonoid F] → [inst_6 : Module R F] → (E →L[R] F) → Prop
-- Std.Http.Protocol.H1.Reader
/-- Feeds new data into the reader's input buffer.
If the current input is exhausted, replaces it; otherwise compacts the buffer
by discarding already-parsed bytes before appending.
 -/
Std.Http.Protocol.H1.Reader.feed : {dir : Std.Http.Protocol.H1.Direction} → ByteArray → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Topology.Algebra.Module.Basic
/-- Construct a bundled linear map from a pointwise limit of linear maps  -/
linearMapOfTendsto : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    {α : Type u_3} →
      {R : Type u_4} →
        {S : Type u_5} →
          [inst : TopologicalSpace M₂] →
            [T2Space M₂] →
              [inst_2 : Semiring R] →
                [inst_3 : Semiring S] →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module S M₂] →
                          [ContinuousConstSMul S M₂] →
                            [ContinuousAdd M₂] →
                              {σ : R →+* S} →
                                {l : Filter α} →
                                  (f : M₁ → M₂) →
                                    (g : α → M₁ →ₛₗ[σ] M₂) →
                                      [l.NeBot] → Filter.Tendsto (fun a x => (g a) x) l (nhds f) → M₁ →ₛₗ[σ] M₂
-- Mathlib.Data.Nat.Nth
Nat.nth_add_one_eq_sub : ∀ {p : ℕ → Prop} {n : ℕ}, ¬p 0 → Nat.nth p n ≠ 0 → Nat.nth (fun i => p (i + 1)) n = Nat.nth p n - 1
-- Mathlib.CategoryTheory.Category.Init
/-- Option to control whether the category theory library should use `grind` or `aesop`
in the `cat_disch` tactic, which is widely used as an autoparameter.  -/
mathlib.tactic.category.grind : Lean.Option Bool
-- Mathlib.Algebra.Ring.Ext
NonAssocSemiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonAssocSemiring R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.seq_zero : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A), H.seq f 0 = 0
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_lt_sum' : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {ι : Type u_6} {s : Finset ι} {f : ι → R} {g : Γ₀}, g < ⊤ → (∀ i ∈ s, g < v (f i)) → g < v (∑ i ∈ s, f i)
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.isUnit_one_sub : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsNilpotent r → IsUnit (1 - r)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_5 : ∀ (a b : Lean.Grind.CommRing.Expr), (a.add b).toPoly = a.toPoly.combine b.toPoly
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Given an `A`-algebra `B` and `S : Set ℕ`, we define `IsCyclotomicExtension S A B` requiring
that there is an `n`-th primitive root of unity in `B` for all nonzero `n ∈ S` and that
`B` is generated over `A` by the roots of `X ^ n - 1`.  -/
IsCyclotomicExtension : Set ℕ → (A : Type u) → (B : Type v) → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → Prop
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app_hom_apply : ∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor J C) (X_1 : Cᵒᵖ) (t : (CategoryTheory.Functor.const J).obj (Opposite.unop X_1) ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).inv.app X).app X_1))
      t =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.lift (X.comp (CategoryTheory.coyoneda.obj X_1))
          (CategoryTheory.Limits.Types.coneOfSection ⋯)))
      PUnit.unit
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedState.mk.inj : ∀ {parserState : Lean.Parser.ModuleParserState}
  {processedSnap : Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot}
  {parserState_1 : Lean.Parser.ModuleParserState}
  {processedSnap_1 : Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot},
  { parserState := parserState, processedSnap := processedSnap } =
      { parserState := parserState_1, processedSnap := processedSnap_1 } →
    parserState = parserState_1 ∧ processedSnap = processedSnap_1
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.isUnit_iff_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X),
  IsUnit f ↔ CategoryTheory.IsIso f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α], Measurable fun p => dist p.1 p.2
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.zariskisMainProperty_iff' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S},
  Algebra.ZariskisMainProperty R p ↔ ∃ r ∉ p, ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  (it : Std.IterM m (β₁ × β₂)) (motive : it.internalState.left.Step → Sort u_3) (it₁' : Std.IterM m β₁) (out : β₁)
  (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) →
        (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it₁' out)) →
          motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) →
      (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it.internalState.left.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.yield it₁' out, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_1 it₁' out hp
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.smulConst.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalTorsor P] (p : P),
  Homeomorph.smulConst p = { toEquiv := Equiv.smulConst p, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Dual
/-- For each `x : E`, the kernel of `⟪x, ⬝⟫` includes the null space.  -/
InnerProductSpace.nullSubmodule_le_ker_toDualMap_right : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), nullSubmodule 𝕜 E ≤ (↑((InnerProductSpace.toDualMap 𝕜 E) x)).ker
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.quoteList : {α : Type} → [Lean.Quote α] → List α → Lean.Term
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.of_arrow : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.Arrow C} (h : f ⟶ g),
  CategoryTheory.CommSq f.hom (CategoryTheory.Arrow.Hom.left h) (CategoryTheory.Arrow.Hom.right h) g.hom
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_const_vadd : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [MeasurableConstVAdd G α] (c : G), MeasurableEmbedding fun x => c +ᵥ x
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- An `AddSubmonoid` is either the trivial `AddSubmonoid` or contains a nonzero element.  -/
AddSubmonoid.bot_or_exists_ne_zero : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊥ ∨ ∃ x ∈ S, x ≠ 0
-- Mathlib.CategoryTheory.Triangulated.Yoneda
CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (B : C)
  {X Y : Cᵒᵖ} (n : ℤ) (f : X ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj Y) (a a' : ℤ) (h : n + a = a')
  (z : Opposite.unop X ⟶ (CategoryTheory.shiftFunctor C a).obj B),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.preadditiveYoneda.obj B).shiftMap f a a' h)) z =
    ((CategoryTheory.ShiftedHom.opEquiv n).symm f).comp z ⋯
-- Mathlib.Algebra.Category.ModuleCat.Localization
/-- Shrink of `LocalizedModule S M` in category which `M` belongs.  -/
ModuleCat.localizedModule : {R : Type u} → [inst : CommRing R] → [Small.{v, u} R] → ModuleCat R → (S : Submonoid R) → ModuleCat (Localization S)