mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerLeft_comm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C) {Y₁ Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂) (U : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj U (X.tensorObj Y₂).fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.fst f.f)
        U)
      (CategoryTheory.CategoryStruct.comp ((X.tensorObj Y₂).snd.β U).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((X.tensorObj Y₁).snd.β U).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.fst f.f)))
      h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k k' : α} [hi : Inhabited β] {f : β → β},
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.modify t k f) k' =
        if cmp k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Raw.Const.get? t k)).get!
        else Std.DTreeMap.Raw.Const.get! t k'
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidMap_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (M' : Submonoid M),
  Function.Surjective ⇑(f.submonoidMap M')
-- Mathlib.Data.Nat.DvdSequence
/-- A function `f : ℕ → ℕ` is a strong divisibility sequence if `gcd (f a) (f b) = f (gcd a b)`.  -/
Nat.IsStrongDvdSequence : (ℕ → ℕ) → Prop
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  (η : ProbabilityTheory.Kernel γ δ), ¬ProbabilityTheory.IsSFiniteKernel κ → κ.parallelComp η = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Being `Cⁿ` in the model space is a local property, invariant under `Cⁿ` maps. Therefore,
it lifts nicely to manifolds.  -/
contDiffWithinAt_localInvariantProp_of_le : ∀ {𝕜 : 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'} (n m : WithTop ℕ∞),
  m ≤ n → (contDiffGroupoid n I).LocalInvariantProp (contDiffGroupoid n I') (ContDiffWithinAtProp I I' m)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.minKey (Std.Internal.List.insertEntryIfNew k v l) ⋯ =
        (Std.Internal.List.minKey? l).elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.run? : {α : Type} → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM α → Lean.Meta.Grind.GoalM (Option α)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (K H : C) (i : K ⟶ S.X₂) (π : K ⟶ H)
  (wi : CategoryTheory.CategoryStruct.comp i S.g = 0)
  (hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i wi))
  (wπ : CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π = 0)
  (hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π wπ)) (K_1 H_1 : C)
  (i_1 : K_1 ⟶ S.X₂) (π_1 : K_1 ⟶ H_1) (wi_1 : CategoryTheory.CategoryStruct.comp i_1 S.g = 0)
  (hi_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i_1 wi_1))
  (wπ_1 : CategoryTheory.CategoryStruct.comp (hi_1.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π_1 = 0)
  (hπ_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π_1 wπ_1)),
  ({ K := K, H := H, i := i, π := π, wi := wi, hi := hi, wπ := wπ, hπ := hπ } =
      { K := K_1, H := H_1, i := i_1, π := π_1, wi := wi_1, hi := hi_1, wπ := wπ_1, hπ := hπ_1 }) =
    (K = K_1 ∧ H = H_1 ∧ i ≍ i_1 ∧ π ≍ π_1 ∧ hi ≍ hi_1 ∧ hπ ≍ hπ_1)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- `adicCompletion.toCompletion` and `adicCompletion.ofCompletion` as an equivalence.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃
                  (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.target_subset_preimage_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.target ⊆ ↑e.symm ⁻¹' e.source
-- Mathlib.Order.Hom.BoundedLattice
/-- `SupBotHomClass F α β` states that `F` is a type of finitary supremum-preserving morphisms.

You should extend this class when you extend `SupBotHom`.  -/
SupBotHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [Max α] → [Max β] → [Bot α] → [Bot β] → [FunLike F α β] → Prop
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.exact : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂
-- Mathlib.Analysis.Convex.Intrinsic
ContinuousAffineEquiv.intrinsicInterior_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup W] [inst_3 : Module 𝕜 V] [inst_4 : Module 𝕜 W] [inst_5 : TopologicalSpace P]
  [inst_6 : TopologicalSpace Q] [inst_7 : AddTorsor V P] [inst_8 : AddTorsor W Q] (φ : P ≃ᴬ[𝕜] Q) (s : Set P),
  intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.sSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {ℐ : Set (Ideal A)},
  (∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I) → Ideal.IsHomogeneous 𝒜 (sSup ℐ)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ), (p.drop n).getVert m = p.getVert (n + m)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Ioi : ∀ {n : ℕ} (i : Fin n), Fin.val '' Set.Ioi i = Set.Ioo (↑i) n
-- Lean.Meta.AppBuilder
Lean.Meta.mkEqMP : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Server.Requests
/-- `onDidChange` with explicit state management for chaining request handlers.
This function is pure w.r.t. `lastTaskMutex` and `stateRef`, but not `RequestM`.
 -/
Lean.Server.StatefulRequestHandler.pureOnDidChange : Lean.Server.StatefulRequestHandler → Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit
-- Mathlib.Data.Num.ZNum
ZNum.nontrivial : Nontrivial ZNum
-- Batteries.Data.List.Basic
/-- Transpose of a list of lists, treated as a matrix.
```
transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]
```
 -/
List.transpose : {α : Type u_1} → List (List α) → List (List α)
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.map_mk : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {n : ℕ} (x : Fin n → ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.exteriorPower.map f n)) (ModuleCat.exteriorPower.mk x) =
    ModuleCat.exteriorPower.mk (⇑(CategoryTheory.ConcreteCategory.hom f) ∘ x)
-- Init.Data.Iterators.Producers.Monadic.List
/-- Returns a finite iterator for the given list.
The iterator yields the elements of the list in order and then terminates.

The non-monadic version of this iterator is `List.iter`.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
List.iterM : {α : Type w} → List α → (m : Type w → Type w') → [Pure m] → Std.IterM m α
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_X_pow_char_pow_sub_C : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] [inst_3 : PerfectRing R p]
  {y : R}, (Polynomial.X ^ p ^ n - Polynomial.C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.instIsPushout' : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : AddCommMonoid M] [inst_8 : Algebra S B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower R S B] [Algebra.IsPushout R A S B],
  Algebra.IsPushout R (AddMonoidAlgebra A M) S (AddMonoidAlgebra B M)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {carrier : Set α} {isIrreducible' : IsIrreducible carrier}
  {isClosed' : IsClosed carrier} {carrier_1 : Set α} {isIrreducible'_1 : IsIrreducible carrier_1}
  {isClosed'_1 : IsClosed carrier_1},
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' } =
      { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 } →
    carrier = carrier_1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSet_subset : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.incidenceSet v ⊆ G.edgeSet
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.eq_3 : ∀ (fuel_2 : ℕ) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m) =
    Ordering.gt
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.mul_antipode_rTensor_comul_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a : A),
  (LinearMap.mul' R A) ((LinearMap.rTensor A (HopfAlgebraStruct.antipode R)) (CoalgebraStruct.comul a)) =
    (algebraMap R A) (CoalgebraStruct.counit a)
-- Mathlib.Data.ENat.Basic
ENat.natCast_zero : ↑0 = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.laplacianCLM_eq' : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] (f : SchwartzMap E F),
  (LineDeriv.laplacianCLM ℝ E (SchwartzMap E F)) f = Laplacian.laplacian f
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHomClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : FunLike F α β]
  [toContinuousOrderHomClass : ContinuousOrderHomClass F α β],
  (∀ (f : F) ⦃a : α⦄ ⦃b : β⦄, f a ≤ b → ∃ c, a ≤ c ∧ f c = b) → EsakiaHomClass F α β
-- Mathlib.CategoryTheory.Filtered.Final
/-- The diagonal functor on any filtered category is final.  -/
CategoryTheory.Functor.final_diag_of_isFiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C],
  (CategoryTheory.Functor.diag C).Final
-- Mathlib.Util.Export
Lean.Export.Entry.defn.inj : ∀ {n n_1 : Lean.Name}, Lean.Export.Entry.defn n = Lean.Export.Entry.defn n_1 → n = n_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.toList_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.toArray.toList = t.toList
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.support_ofCoeff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (p : G →₀ k), { coeff := p }.support = p.support
-- Lean.Parser.Term
Lean.Parser.Term.letOptEq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listEncode.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (n l : ℕ)
  (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n))
  (h_1 : (n : ℕ) → motive n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (n l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (φ₁ φ₂ : L.BoundedFormula α x) → motive x (φ₁.imp φ₂))
  (h_5 : (x : ℕ) → (φ : L.BoundedFormula α (x + 1)) → motive x φ.all),
  (match n, FirstOrder.Language.BoundedFormula.rel R ts with
    | n, FirstOrder.Language.BoundedFormula.falsum => h_1 n
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | n, FirstOrder.Language.BoundedFormula.rel R ts => h_3 n l R ts
    | x, φ₁.imp φ₂ => h_4 x φ₁ φ₂
    | x, φ.all => h_5 x φ) =
    h_3 n l R ts
-- Mathlib.Topology.Algebra.Support
/-- The additive submonoid of functions `α → β` with compact support.  -/
HasCompactSupport.addSubmonoid : (α : Type u_2) → (β : Type u_4) → [TopologicalSpace α] → [inst : AddZeroClass β] → AddSubmonoid (α → β)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_map_sectL : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a b : α) (c : β),
  Finset.map (Function.Embedding.sectL α c) (Finset.Icc a b) = Finset.Icc (a, c) (b, c)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_inj : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : PolynomialModule R M}, x.coeff = y.coeff ↔ x = y
-- Mathlib.Data.PFun
PFun.mem_image : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : Set α), y ∈ f.image s ↔ ∃ x ∈ s, y ∈ f x
-- Mathlib.Tactic.CasesM
/-- `constructorm p_1, ..., p_n`, where the main goal has type `type`, applies the first matching
constructor for `type`, if `type` matches one of the given patterns. If `type` does not match any
of the patterns, `constructorm` fails.

* `constructorm* p_1, ..., p_n` repeatedly applies a constructor until the goal no longer matches
  `p_1`, ..., `p_n`. This is a more efficient and compact version of
  `· repeat constructorm p_1, ..., p_n`. It is more efficient because the pattern is compiled once.

Examples:
```
example : True ∧ (True ∨ True) := by
  constructorm* _ ∨ _, _ ∧ _, True
```
 -/
Mathlib.Tactic.constructorM : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter_of_compare_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  compare k k' = Ordering.eq →
    (k' ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl ↔
      (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true)
-- Init.Classical
Classical.inhabited_of_nonempty : {α : Sort u} → Nonempty α → Inhabited α
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.contravariantSequence_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ)
  (h : 1 + n₀ = n₁), (CategoryTheory.Abelian.Ext.contravariantSequence hS Y n₀ n₁ h).Exact
-- Qq.SortLocalDecls
Qq.SortLocalDecls.Context.mk.inj : ∀ {localDecls localDecls_1 : Lean.NameMap Lean.LocalDecl},
  { localDecls := localDecls } = { localDecls := localDecls_1 } → localDecls = localDecls_1
-- Init.Data.List.Basic
/-- Returns the first non-`none` result of applying `f` to each element of the list in order. Returns
`none` if `f` returns `none` for all elements of the list.

`O(|l|)`.

Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
 * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
List.findSome? : {α : Type u} → {β : Type v} → (α → Option β) → List α → Option β
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- If `p` is a maximal ideal of `R`, and `S` is the integral closure of `R` in `L`,
then the dimension `[S/pS : R/p]` is equal to `[Frac(S) : Frac(R)]`.  -/
Ideal.finrank_quotient_map : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (K : Type u_1) [inst_3 : Field K] [inst_4 : Algebra R K] (L : Type u_2) [inst_5 : Field L] [inst_6 : Algebra S L]
  [IsFractionRing S L] [hRK : IsFractionRing R K] [IsDomain S] [IsDedekindDomain R] [inst_10 : Algebra K L]
  [inst_11 : Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S],
  Module.finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = Module.finrank K L
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_lt_one_of_one_lt₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 1 < a → a⁻¹ < 1
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.PredTrans.pushOption.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Computability.Partrec
Computable.vector_get : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable₂ List.Vector.get
-- Mathlib.Order.SupClosed
supClosure.eq_1 : ∀ {α : Type u_3} [inst : SemilatticeSup α],
  supClosure =
    ClosureOperator.ofPred (fun s => {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a}) SupClosed ⋯ ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.left_nonuniformWitnesses_card : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t → ↑s.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).1.card
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symmEquiv.eq_1 : ∀ (P : Type u_9) (Q : Type u_10) [inst : Add P] [inst_1 : Add Q],
  AddEquiv.symmEquiv P Q = { toFun := AddEquiv.symm, invFun := AddEquiv.symm, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.eq_3 : ∀ (coeff : ℕ) (a b : Nat.Internal.Linear.Expr),
  Nat.Internal.Linear.Expr.toPoly.go coeff (a.add b) =
    Nat.Internal.Linear.Expr.toPoly.go coeff a ∘ Nat.Internal.Linear.Expr.toPoly.go coeff b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp.instMonoidal.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  [inst_4 : CategoryTheory.BraidedCategory C] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided],
  CategoryTheory.Functor.mapGrp.instMonoidal F =
    {
        εIso :=
          (CategoryTheory.Grp.fullyFaithfulForget₂Mon D).preimageIso (CategoryTheory.Functor.Monoidal.εIso F.mapMon),
        μIso := fun X Y =>
          (CategoryTheory.Grp.fullyFaithfulForget₂Mon D).preimageIso
            (CategoryTheory.Functor.Monoidal.μIso F.mapMon X.toMon Y.toMon),
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Init.Data.List.Find
List.find?_replicate : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α},
  List.find? p (List.replicate n a) = if n = 0 then none else if p a = true then some a else none
-- Mathlib.Algebra.Order.Hom.Ring
/-- This lemma used to be generated by [simps] on `trans`, but the lhs of this simplifies under
simp. Removed [simps] attribute and added aux version below.  -/
OrderRingIso.trans_toRingEquiv : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β]
  [inst_4 : Add β] [inst_5 : LE β] [inst_6 : Mul γ] [inst_7 : Add γ] [inst_8 : LE γ] (f : α ≃+*o β) (g : β ≃+*o γ),
  (f.trans g).toRingEquiv = f.trans g.toRingEquiv
-- Mathlib.Topology.CompactOpen
ContinuousMap.continuous_mkD_restrict_of_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {T : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace T] {t : Set X} (f : T → X → Y) (g : C(↑t, Y)),
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ t) → Continuous fun x => ContinuousMap.mkD (t.domRestrict (f x)) g
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedMonoid.enorm_zero : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ESeminormedMonoid E], ‖1‖ₑ = 0
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveOn.isMIntegralCurveAt : ∀ {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}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ} {t₀ : ℝ},
  IsMIntegralCurveOn γ v s → s ∈ nhds t₀ → IsMIntegralCurveAt γ v t₀
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- "iff" version of `Multipliable.of_nat_of_neg`.  -/
multipliable_int_iff_multipliable_nat_and_neg : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] [CompleteSpace G] {f : ℤ → G},
  Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-↑n)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tendsto_double_sum_S_act : ∀ (z : UpperHalfPlane),
  Filter.Tendsto (fun N => ∑' (n : ℤ), ∑ m ∈ Finset.Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) Filter.atTop
    (nhds ((↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z)))
-- Mathlib.Algebra.Homology.Linear
HomologicalComplex.instSMulHom : {R : Type u_1} →
  [inst : Semiring R] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] →
            {ι : Type u_4} → {c : ComplexShape ι} → {X Y : HomologicalComplex C c} → SMul R (X ⟶ Y)