mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Regular
Subtype.instT25Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T25Space X] {p : X → Prop}, T25Space { x // p x }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.cond : Lean.Elab.Term.Do.DoIfView → Lean.Syntax
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toLinearOrder : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → LinearOrder α
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.coe_liftRight : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] {f : M →+ N} {g : M → AddUnits N}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), ↑((AddUnits.liftRight f g h) x) = f x
-- Mathlib.Analysis.Convex.Basic
Convex.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → Convex 𝕜 (-s)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₂_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝) (app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝)
  (app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          app₁.hom =
        CategoryTheory.CategoryStruct.comp app₀.hom
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
      CategoryTheory.ComposableArrows.isoMk₂._auto_1)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂.hom =
        CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_247✝))
      CategoryTheory.ComposableArrows.isoMk₂._auto_3),
  (CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).inv =
    CategoryTheory.ComposableArrows.homMk₂ app₀.inv app₁.inv app₂.inv ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- Formal compositions and tensor products of identities, unitors and associators. The morphisms
of the free monoidal category are obtained as a quotient of these formal morphisms by the
relations defining a monoidal category.  -/
CategoryTheory.FreeMonoidalCategory.Hom : {C : Type u} → CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory C → Type u
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_smul`

---

The order is additive when multiplying scalar-valued and vector-valued meromorphic functions.  -/
fun_meromorphicOrderAt_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : NormedRing R] [NoZeroDivisors R] [inst_5 : Module R E]
  [IsBoundedSMul R E] [Module.IsTorsionFree R E] {x : 𝕜} [inst_8 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {f : 𝕜 → R}
  {g : 𝕜 → E},
  MeromorphicAt f x →
    MeromorphicAt g x → meromorphicOrderAt (fun i => f i • g i) x = meromorphicOrderAt f x + meromorphicOrderAt g x
-- Init.Prelude
/-- Creates a `UInt8` from a `BitVec 8`. This function is overridden with a native implementation.
 -/
UInt8.ofBitVec : BitVec 8 → UInt8
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_one : ∀ {α : Type u_1} (s : Multiset α), Multiset.powersetCard 1 s = Multiset.map singleton s
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.instGroupoid : {C : Type u} → CategoryTheory.Groupoid (CategoryTheory.FreeMonoidalCategory C)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.smul_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
  [inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal]
  (c : R) (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω), (c • μ) s = c • μ s
-- Mathlib.Combinatorics.Matroid.Map
/-- Map a matroid `M` to an isomorphic copy in `β` using an embedding `M.E ↪ β`.  -/
Matroid.mapSetEmbedding : {α : Type u_1} → {β : Type u_2} → (M : Matroid α) → (↑M.E ↪ β) → Matroid β
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_eq_getElem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {he : t.isEmpty = false},
  t.min he = t.toArray[0]
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The sum of strongly measurable functions is measurable.  -/
MeasureTheory.StronglyMeasurable.tsum' : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousAdd E] {L : SummationFilter ι}
  [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable (∑'[L] (i : ι), f i)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_one_smul : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X] (r : R) (x : OreLocalization S X), (r • 1) • x = r • x
-- Mathlib.Order.SupIndep
/-- **Alias** of the forward direction of `iSupIndep_iff_supIndep_univ`.

---

A variant of `iSupIndep_comp_coe_iff_supIndep` for `Fintype`s.  -/
iSupIndep.sup_indep_univ : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [inst_1 : Fintype ι] {f : ι → α},
  iSupIndep f → Finset.univ.SupIndep f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ordered_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a b = Ordering.lt) t.keys
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_eq_zero_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ {f : α → ENNReal}, Measurable f → (∫⁻ (a : α) in s, f a ∂μ = 0 ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_inter_nonempty_iff' : ∀ {α : Type u_2} [inst : Group α] {s t : Set α} {x : α}, (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
-- Init.Data.SInt.Lemmas
Int16.toBitVec_zero : Int16.toBitVec 0 = 0#16
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)},
  ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_lt_toENNReal : ∀ {x y : EReal}, 0 ≤ x → x < y → x.toENNReal < y.toENNReal
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_sub : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p q : ℚ), ↑(p - q) = ↑p - ↑q
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- `Proj` restrict to some open set  -/
AlgebraicGeometry.«termProj|_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows.exists : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X}
  {W : C} {g : W ⟶ X},
  (CategoryTheory.Sieve.ofArrows Y f).arrows g → ∃ i h, g = CategoryTheory.CategoryStruct.comp h (f i)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
/-- Given a simplicial object `E` in the category `FormalCoproduct C`, this is the
functor `(Cᵒᵖ ⥤ A) ⥤ CochainComplex A ℕ` which sends `P : Cᵒᵖ ⥤ A` to the
cochain complex which in degree `n` consists of the "evaluation" of `P` on `E _⦋n⦌`.  -/
CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [CategoryTheory.Limits.HasProducts A] →
          CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C) →
            [inst_3 : CategoryTheory.Preadditive A] →
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CochainComplex A ℕ)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_mul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f g : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) _auto_371✝ →
    autoParam (f 0 = 0) _auto_373✝ →
      autoParam (ContinuousOn g (quasispectrum R a)) _auto_375✝ →
        autoParam (g 0 = 0) _auto_377✝ → cfcₙ (fun x => f x * g x) a = cfcₙ f a * cfcₙ g a
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
_private.Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum.0.ZMod.χ₄.match_1.splitter : (motive : ZMod 4 → Sort u_1) →
  (a : ZMod 4) → (Unit → motive 0) → (Unit → motive 2) → (Unit → motive 1) → (Unit → motive 3) → motive a
-- Init.Data.Option.Attach
Option.unattach_some : ∀ {α : Type u_1} {p : α → Prop} {a : { x // p x }}, (some a).unattach = some ↑a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.comp_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G H : CategoryTheory.LaxBraidedFunctor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : CategoryTheory.LaxMonoidalFunctor C D}
  (h : H.toLaxMonoidalFunctor ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β).hom h =
    CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp β.hom h)
-- Mathlib.Order.Cofinal
IsCofinal.nonempty : ∀ {α : Type u_1} [inst : LE α] [Nonempty α] {s : Set α}, IsCofinal s → s.Nonempty
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.quotient_map : ∀ {R : Type u_1} [inst : CommRing R] (B : Type u_3) [inst_1 : CommRing B] [inst_2 : Algebra R B]
  [Algebra.FormallyUnramified R B] (p : Ideal R), Algebra.FormallyUnramified (R ⧸ p) (B ⧸ Ideal.map (algebraMap R B) p)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.of_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).Flat) → AlgebraicGeometry.Flat f
-- Lean.Meta.Tactic.Grind.Util
Lean.Meta.Grind.isIte : Lean.Expr → Bool
-- Aesop.RuleTac.Basic
Aesop.instInhabitedCasesPattern : Inhabited Aesop.CasesPattern
-- Mathlib.LinearAlgebra.DFinsupp
/-- A variant of `Submodule.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded.

See also `Submodule.mem_iSup_iff_exists_finsupp`.  -/
Submodule.mem_iSup_iff_exists_dfinsupp' : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Submodule R N) [inst_4 : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)] (x : N),
  x ∈ iSup p ↔ ∃ f, (f.sum fun x xi => ↑xi) = x
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_eq_bot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β}, f +ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonAssocSemiring : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonAssocSemiring R] → NonAssocSemiring (HahnSeries Γ R)
-- Mathlib.RingTheory.AdjoinRoot
/-- `R[x]/(f)` is `R`-algebra  -/
AdjoinRoot.instAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] → (f : Polynomial R) → [inst_1 : CommSemiring S] → [Algebra S R] → Algebra S (AdjoinRoot f)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A block diagonal matrix is Hermitian if and only if each block is Hermitian.  -/
Matrix.isHermitian_blockDiagonal'_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : DecidableEq n]
  {p : n → Type u_5} {M : (i : n) → Matrix (p i) (p i) α},
  (Matrix.blockDiagonal' M).IsHermitian ↔ ∀ (i : n), (M i).IsHermitian
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_finsetProd : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : CommMonoid γ] [inst_3 : ContinuousMul γ] {ι : Type u_5} (s : Finset ι) (f : ι → α →ₘ[μ] γ),
  ↑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_div_comm : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a b : M),
  MulArchimedeanClass.mk (a / b) = MulArchimedeanClass.mk (b / a)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.hw : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (self : Φ.LeftResolution X₂), W₂ self.w
-- Mathlib.Order.Hom.Bounded
TopHom.coe_id : ∀ (α : Type u_2) [inst : Top α], ⇑(TopHom.id α) = id
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.toOpenPartialHomeomorph : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] →
            {proj : Z → B} → Bundle.Trivialization F proj → OpenPartialHomeomorph Z (B × F)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.ae_le_lpNorm_exponent_top : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {f : α → E}, MeasureTheory.MemLp f ⊤ μ → ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ MeasureTheory.lpNorm f ⊤ μ
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.commSemiring : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → CommSemiring (FractionalIdeal S P)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d') {Z : D} (h : d' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d').hom h)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ico_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Ico (Fin.castLE h a) (Fin.castLE h b), f i = ∏ i ∈ Finset.Ico a b, f (Fin.castLE h i)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.step_eq_monadicStep : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.Iter α},
  Std.Rxo.Iterator.step it = Std.IterStep.mapIterator Std.IterM.toIter (Std.Rxo.Iterator.Monadic.step it.toIterM)
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instCategoryWithFibrationsOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (S : C) →
      [HomotopicalAlgebra.CategoryWithFibrations C] → HomotopicalAlgebra.CategoryWithFibrations (CategoryTheory.Over S)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_map_self_eq_one`. -/
Ideal.ramificationIdx_map_self_eq_one : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊤ →
    Ideal.map (algebraMap R S) p ≠ ⊥ → p.ramificationIdx' (Ideal.map (algebraMap R S) p) = 1
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  (φ' : S' ⟶ R) {X Y : Dᵒᵖ} (f : X ⟶ Y),
  (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f = CommRingCat.KaehlerDifferential.map ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- The linear map from `(M →ₛₗ[σ₁₂] M₂) ⊗ (N →ₛₗ[σ₁₂] N₂)` to `M ⊗ N →ₛₗ[σ₁₂] M₂ ⊗ N₂`
sending `f ⊗ₜ g` to `TensorProduct.map f g`, the tensor product of the two maps.  -/
TensorProduct.homTensorHomMap : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (M : Type u_7) →
            (N : Type u_8) →
              (M₂ : Type u_12) →
                (N₂ : Type u_14) →
                  [inst_2 : AddCommMonoid M] →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : AddCommMonoid N₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R N] →
                              [inst_8 : Module R₂ M₂] →
                                [inst_9 : Module R₂ N₂] →
                                  TensorProduct R₂ (M →ₛₗ[σ₁₂] M₂) (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂]
                                    TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).size =
    if k ∈ t ∧ (f (t.get? k)).isNone = true then t.size - 1
    else if k ∉ t ∧ (f (t.get? k)).isSome = true then t.size + 1 else t.size
-- Mathlib.Topology.Order.DenselyOrdered
left_nhdsWithin_Ioc_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a < b → (nhdsWithin a (Set.Ioc a b)).NeBot
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_eq_range' : ∀ (a b : ℕ), Finset.Ico a b = { val := ↑(List.range' a (b - a)), nodup := ⋯ }
-- Init.Data.SInt.Basic
/-- Converts a word-sized signed integer to a 32-bit signed integer.

On 32-bit platforms, this conversion is lossless. On 64-bit platforms, the integer's bitvector
representation is truncated to 32 bits. This function is overridden at runtime with an efficient
implementation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.toInt32 : ISize → Int32
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldl_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.DTreeMap.Raw.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Lean.Meta.Grind.Origin.fvar fvarId = Lean.Meta.Grind.Origin.fvar fvarId_1 → fvarId = fvarId_1
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.tprod_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousMul α] [L.NeBot],
  Multipliable f L → Multipliable g L → ∏'[L] (b : β), f b * g b = (∏'[L] (b : β), f b) * ∏'[L] (b : β), g b
-- Mathlib.Data.Finset.Sym
Finset.sym_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (n : ℕ), s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Rio.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Rio.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Rio.HasRcoIntersection α] → Prop
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForDiagnosticsParams : Lean.FromJson Lean.Lsp.WaitForDiagnosticsParams
-- Std.Data.TreeMap.Basic
Std.TreeMap.mk.inj : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.TreeMap._auto_1}
  {inner inner_1 : Std.DTreeMap α (fun x => β) cmp}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD_zero : ∀ {α : Type u} (d : α), WithZero.unzeroD d 0 = d
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a finite affinely independent family whose
cardinality is one more than that of the finite-dimensional space is
`⊤`.  -/
AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [FiniteDimensional k V] [inst_5 : Fintype ι] {p : ι → P},
  AffineIndependent k p → Fintype.card ι = Module.finrank k V + 1 → vectorSpan k (Set.range p) = ⊤
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.category : Lean.Name → Lean.Name → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserExtension.OLeanEntry
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, (Set.uIcc a b).OrdConnected
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.one_coe_eq_one : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne], ⇑1 = 1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.instFiniteSubtypeMemSubmoduleCorootSpanOfFinite : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S N] [Finite ι], Module.Finite S ↥(P.corootSpan S)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_smul : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : CommRing k] [inst_2 : Monoid G] {A B : TopRep k G}
  (r : k) (f : A ⟶ B), TopRep.Hom.hom (r • f) = r • TopRep.Hom.hom f
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux.eq_2 : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g)
  (hg : Function.Surjective ⇑g) {k : ℕ} (hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range))
  (x : AdicCompletion.AdicCauchySequence I N) (hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤) (n : ℕ),
  AdicCompletion.mapExactAux✝ hf hfg hg hkn x hker n.succ =
    match AdicCompletion.mapExactAux✝ hf hfg hg hkn x hker n with
    | ⟨yₙ, hyₙ⟩ =>
      match AdicCompletion.mapExactAuxDelta✝ hf hkn x ⋯ ⋯ hyₙ with
      | ⟨d, hd⟩ => ⟨yₙ + ↑d, hd⟩
-- Lean.Data.Lsp.Extra
Lean.Lsp.ModuleHierarchyOptions.mk : Lean.Lsp.ModuleHierarchyOptions