mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v).getKey k ⋯ = k
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_eq_sSup : ∀ {x : ℝ*}, x.st = sSup {y | ↑y < x}
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.freeRefl_obj : ∀ (V : CategoryTheory.ReflQuiv),
  CategoryTheory.Cat.freeRefl.obj V = CategoryTheory.Cat.of (CategoryTheory.Cat.FreeRefl ↑V)
-- Aesop.Index.Forward
Aesop.ForwardIndex.mk.inj : ∀ {tree : Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex)}
  {nameToRule : Lean.PHashMap Aesop.RuleName Aesop.ForwardRule} {constRules : Lean.PHashSet Aesop.ForwardRule}
  {tree_1 : Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex)}
  {nameToRule_1 : Lean.PHashMap Aesop.RuleName Aesop.ForwardRule} {constRules_1 : Lean.PHashSet Aesop.ForwardRule},
  { tree := tree, nameToRule := nameToRule, constRules := constRules } =
      { tree := tree_1, nameToRule := nameToRule_1, constRules := constRules_1 } →
    tree = tree_1 ∧ nameToRule = nameToRule_1 ∧ constRules = constRules_1
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.subst : Lean.Meta.UnifyEqResult → Lean.Meta.FVarSubst
-- Init.Data.Repr
Nat.toSubDigitsAux : ℕ → List Char → List Char
-- Mathlib.LinearAlgebra.Matrix.Integer
/-- The numerator of a matrix of rationals (a matrix of integers, defined so that
`A.num / A.den = A`).  -/
Matrix.num : {m : Type u_1} → {n : Type u_2} → [Fintype m] → [Fintype n] → Matrix m n ℚ → Matrix m n ℤ
-- Init.Data.String.Iterate
String.Slice.ByteIterator.mk.injEq : ∀ (s : String.Slice) (offset : String.Pos.Raw) (s_1 : String.Slice) (offset_1 : String.Pos.Raw),
  ({ s := s, offset := offset } = { s := s_1, offset := offset_1 }) = (s = s_1 ∧ offset = offset_1)
-- Mathlib.Data.Set.Prod
Set.subset_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)}, s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.discrete_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.GrothendieckTopology.discrete C = ⊤
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens),
  IsCompact U.carrier →
    IsQuasiSeparated U.carrier →
      ∀ (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))),
        ∃ n y,
          TopCat.Presheaf.restrictOpen y (X.basicOpen f) ⋯ = TopCat.Presheaf.restrictOpen f (X.basicOpen f) ⋯ ^ n * x
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
RatFunc.liftAlgHom.eq_1 : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)),
  RatFunc.liftAlgHom φ hφ = { toRingHom := RatFunc.liftRingHom φ.toRingHom hφ, commutes' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  {f : α → ENNReal}, (∃ c, ∀ (x : α), f x ≤ ↑c) → ∫⁻ (x : α), f x ∂μ < ⊤
-- Batteries.Lean.AttributeExtra
Lean.ParametricAttributeExtra.mk.injEq : ∀ {α : Type} (attr : Lean.ParametricAttribute α) (base : Std.HashMap Lean.Name α) (attr_1 : Lean.ParametricAttribute α)
  (base_1 : Std.HashMap Lean.Name α),
  ({ attr := attr, base := base } = { attr := attr_1, base := base_1 }) = (attr = attr_1 ∧ base = base_1)
-- Mathlib.GroupTheory.Finiteness
QuotientAddGroup.fg : ∀ {G : Type u_3} [inst : AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [inst_2 : N.Normal], AddGroup.FG (G ⧸ N)
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_zero_of_zero_at_inf : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h → (Filter.comap Complex.im Filter.atTop).ZeroAtFilter f → Function.Periodic.cuspFunction h f 0 = 0
-- Mathlib.Topology.Covering.Quotient
isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul : ∀ {E : Type u_1} [inst : TopologicalSpace E] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G E]
  [ContinuousConstSMul G E] [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E],
  IsCoveringMapOn (Quotient.mk (MulAction.orbitRel G E))
    (Quotient.mk (MulAction.orbitRel G E) '' {e | MulAction.stabilizer G e = ⊥})
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.mk : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} →
          {b : H} → (toEquiv : G ≃ H) → (∀ (x : G), toEquiv.toFun (x + a) = toEquiv.toFun x + b) → AddConstEquiv G H a b
-- Mathlib.Topology.MetricSpace.IsometricSMul
Additive.isIsIsometricVAdd'' : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M],
  IsIsometricVAdd (Additive M)ᵃᵒᵖ (Additive M)
-- Mathlib.Algebra.Algebra.Equiv
/-- If an algebra morphism has an inverse, it is an algebra isomorphism.  -/
AlgEquiv.ofAlgHom : {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₂] →
                (f : A₁ →ₐ[R] A₂) →
                  (g : A₂ →ₐ[R] A₁) → f.comp g = AlgHom.id R A₂ → g.comp f = AlgHom.id R A₁ → A₁ ≃ₐ[R] A₂
-- Lean.Data.Lsp.Basic
Lean.Lsp.instCoeTextEditTextEditBatch : Coe Lean.Lsp.TextEdit Lean.Lsp.TextEditBatch
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.isNaN.eq_1 : Float.Model.UnpackedFloat.notANumber.isNaN = true
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_add_Q_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ),
  (AlgebraicTopology.DoldKan.P q).f n + (AlgebraicTopology.DoldKan.Q q).f n =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Mathlib.Order.BoundedOrder.Basic
eq_top_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a = ⊤ ↔ ⊤ ≤ a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {fallback : α}
  {hc : t.minKeyD fallback ∈ t}, t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.ofCone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.PullbackCone.ofCone t).pt = t.pt
-- Mathlib.Algebra.Order.Group.PosPart
sup_eq_add_posPart_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), a ⊔ b = b + (a - b)⁺
-- Mathlib.Logic.Encodable.Basic
/-- Encoding from Type α to ℕ  -/
Encodable.encode : {α : Type u_1} → [self : Encodable α] → α → ℕ
-- Init.Control.State
StateT.instMonadLift : {σ : Type u} → {m : Type u → Type v} → [Monad m] → MonadLift m (StateT σ m)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.continuous : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q), Continuous ⇑f
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciSup_add_le_ciSup_add_ciSup : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Add α] [AddLeftMono α]
  [AddRightMono α] {f g : ι → α},
  BddAbove (Set.range f) → BddAbove (Set.range g) → ⨆ i, f i + g i ≤ (⨆ i, f i) + ⨆ i, g i
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype n] [inst_1 : NonUnitalNonAssocSemiring α]
  [inst_2 : StarRing α] (M : Matrix m n α) (N : Matrix n l α), (M * N).conjTranspose = N.conjTranspose * M.conjTranspose
-- Mathlib.Data.Finset.Basic
Equiv.Finset.disjUnionEquiv_inr : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) (y : ↥t),
  (Equiv.Finset.disjUnionEquiv s t h) (Sum.inr y) = ⟨↑y, ⋯⟩
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (structural : Bool) (vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]) (body : Lean.Term)
  (synthetic : Bool),
  sizeOf { ref := ref, structural := structural, vars := vars, body := body, synthetic := synthetic } =
    1 + sizeOf ref + sizeOf structural + sizeOf vars + sizeOf body + sizeOf synthetic
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_induction : ∀ {α : Type u_1} (f : α → α → α) [inst : LeftCommutative f] (x : α) (p : α → Prop) (s : Multiset α),
  (∀ (a b : α), p a → p b → p (f a b)) → p x → (∀ a ∈ s, p a) → p (Multiset.foldr f x s)
-- Mathlib.FieldTheory.Perfect
instPerfectRingProd : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [ExpChar R p] [PerfectRing R p] (S : Type u_2)
  [inst_3 : CommSemiring S] [ExpChar S p] [PerfectRing S p], PerfectRing (R × S) p
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Rewrites `∏ i : Fin n, f i` as `f 0 * f 1 * ... * f (n - 1)` when `n` is a numeral.  -/
Fin.prod_univ_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_zero_eq_div : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α), Mathlib.Tactic.FieldSimp.zpow' a 0 = a / a
-- Lean.Meta.LetToHave
/-- The dependent lets we are currently under.
If this list is nonempty, then full typechecking is necessary.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context.letFVars : Lean.Meta.LetToHave.Context✝ → List Lean.FVarId
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_sdiff_sdiff : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], Disjoint (x \ y) (y \ x)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.kerFun_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (y : X) (v : V) (x : X),
  ((RKHS.kerFun H y) v) x = (RKHS.kernel H x y) v
-- Mathlib.Data.Set.Image
Set.image_swap_eq_preimage_swap : ∀ {α : Type u_1} {β : Type u_2}, Set.image Prod.swap = Set.preimage Prod.swap
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.overrideConstructors : Lean.Elab.ComputedFields.M Unit
-- Lean.Widget.InteractiveDiagnostic
/-- The `message` field is the text of a message
possibly containing interactive *embeds* of type `MsgEmbed`.
We maintain the invariant that embeds are stored in `.tag`s with empty `.text` subtrees,
i.e., `.tag embed (.text "")`.

Client-side display algorithms render tags in a custom way,
ignoring the nested text.  -/
Lean.Widget.InteractiveDiagnostic : Type
-- Mathlib.Algebra.GradedMulAction
GradedMonoid.GMulAction.toMulAction : {ιA : Type u_1} →
  {ιM : Type u_3} →
    (A : ιA → Type u_4) →
      (M : ιM → Type u_5) →
        [inst : AddMonoid ιA] →
          [inst_1 : GradedMonoid.GMonoid A] →
            [inst_2 : VAdd ιA ιM] → [GradedMonoid.GMulAction A M] → MulAction (GradedMonoid A) (GradedMonoid M)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km kme : α} (hkme : (t.erase k).minKey? = some kme), t.minKey?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.Algebra.RingQuot
/-- The ring equivalence between `RingQuot r` and `(Ideal.ofRel r).quotient`
 -/
RingQuot.ringQuotEquivIdealQuotient : {B : Type uR} → [inst : CommRing B] → (r : B → B → Prop) → RingQuot r ≃+* B ⧸ Ideal.ofRel r
-- Init.Data.BitVec.Lemmas
BitVec.toFin_setWidth' : ∀ {m n : ℕ} (p : m ≤ n) (x : BitVec m), (BitVec.setWidth' p x).toFin = Fin.castLE ⋯ x.toFin
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- Composition of a continuous alternating map and a continuous linear map
as a bundled continuous linear map.

Note that for general topological vector spaces,
this function does not need to be continuous in `f`.  -/
ContinuousAlternatingMap.compContinuousLinearMapCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        [inst_8 : ContinuousConstSMul 𝕜 F] →
                          {E' : Type u_6} →
                            [inst_9 : AddCommGroup E'] →
                              [inst_10 : Module 𝕜 E'] →
                                [inst_11 : TopologicalSpace E'] → (E →L[𝕜] E') → E' [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] F
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
/-- **Alias** of the reverse direction of `MeasureTheory.integrable_piLp_iff`. -/
MeasureTheory.Integrable.of_eval_piLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E}, (∀ (i : ι), MeasureTheory.Integrable (fun x => (f x).ofLp i) μ) → MeasureTheory.Integrable f μ
-- Mathlib.ModelTheory.Definability
Set.definable_iff_empty_definable_with_params : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s : Set (α → M)},
  A.Definable L s ↔ ∅.Definable (L.withConstants ↑A) s
-- Mathlib.Probability.Process.Stopping
MeasureTheory.isStoppingTime_of_measurableSet_eq : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] [Countable ι]
  {f : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι},
  (∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}) → MeasureTheory.IsStoppingTime f τ
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Given an additive isometric action of `G` on `X`, the image of a bounded set in
`X` under translation by `c : G` is bounded.  -/
Bornology.IsBounded.vadd : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd G X] [IsIsometricVAdd G X] {s : Set X},
  Bornology.IsBounded s → ∀ (c : G), Bornology.IsBounded (c +ᵥ s)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.of`.

---

Constructor for objects in `CardinalFilteredPoset κ`.  -/
CategoryTheory.CardinalFilteredPoset.of : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : PartOrdEmb) → [CategoryTheory.IsCardinalFiltered (↑J) κ] → CategoryTheory.CardinalDirectedPoset κ
-- Mathlib.Computability.Partrec
Computable.vector_toList : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable List.Vector.toList
-- Mathlib.Data.Vector.Basic
List.Vector.toList_set : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n) (a : α), (v.set i a).toList = v.toList.set (↑i) a
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.popKind : (q : Lean.Json.CompressWorkItemQueue✝) →
  (Lean.Json.CompressWorkItemQueue.kinds✝ q).size ≠ 0 →
    Lean.Json.CompressWorkItemKind✝ × Lean.Json.CompressWorkItemQueue✝
-- Init.Data.Vector.Lemmas
Vector.drop_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {i : ℕ}, (Vector.mk xs h).drop i = Vector.mk (xs.extract i) ⋯
-- Mathlib.Topology.UnitInterval
unitInterval.univ_eq_Icc : Set.univ = Set.Icc 0 1
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
_private.Mathlib.NumberTheory.RamificationInertia.HilbertTheory.0.IsDecompositionField.ramificationIdxIn_eq_and_inertiaDegIn_eq : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [inst_7 : Algebra A K] [IsFractionRing A K] [inst_9 : Algebra A L] [IsScalarTower A K L] [inst_11 : Algebra B L]
  [IsScalarTower A B L] [IsFractionRing B L] [inst_14 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L]
  (D : Type u_5) (𝓞D : Type u_6) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D]
  [inst_19 : CommRing 𝓞D] [inst_20 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_22 : Algebra 𝓞D B]
  [inst_23 : Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D]
  [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B]
  [inst_31 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p]
  [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal],
  p ≠ ⊥ → 𝓟D.ramificationIdxIn B = p.ramificationIdxIn B ∧ 𝓟D.inertiaDegIn B = p.inertiaDegIn B
-- Mathlib.Data.Set.Image
Subtype.preimage_val_eq_preimage_val_iff : ∀ {α : Type u_1} (s t u : Set α), Subtype.val ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u
-- Init.System.IO
/-- Symbolic links that are pointers to other named files. Note that `System.FilePath.metadata` never
indicates this type as it follows symlinks; use `System.FilePath.symlinkMetadata` instead.
 -/
IO.FS.FileType.symlink : IO.FS.FileType
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.Ref → aig.Ref → aig.Ref → aig.TernaryInput
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.inv_left_hom_left_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (e : f ≅ g) {Z : T}
  (h : g.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.hom) h) =
    h
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.proj.inj : ∀ {a : Lean.Name} {a_1 a_2 : ℕ} {a_3 : Lean.Name} {a_4 a_5 : ℕ},
  Lean.Meta.LazyDiscrTree.Key.proj a a_1 a_2 = Lean.Meta.LazyDiscrTree.Key.proj a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeMapCocone_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D}
  {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Functor.mapCoconeMapCocone c).hom.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
-- Std.Sync.RecursiveMutex
/-- `mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex.

Calling `mutex.atomically` while already holding the underlying `BaseRecursiveMutex` in the same
thread does not block.
 -/
Std.RecursiveMutex.atomically : {m : Type → Type} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.RecursiveMutex α → Std.AtomicT α m β → m β
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.append : ∀ {α : Type u_1} {l r : RBTree.RBNode α} {p : α → Prop},
  RBTree.RBNode.All p l → RBTree.RBNode.All p r → RBTree.RBNode.All p (l.append r)
-- Mathlib.Dynamics.Ergodic.Function
/-- Let `f : α → α` be a (pre)ergodic map.
Let `g : α → X` be a measurable function from `α` to a nonempty measurable space
with a countable family of measurable sets separating the points of `X`.
If `g` is invariant under `f`, then `g` is a.e. constant.  -/
PreErgodic.ae_eq_const_of_ae_eq_comp : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X]
  [inst_2 : MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : α → α} {g : α → X},
  PreErgodic f μ → Measurable g → g ∘ f = g → ∃ c, g =ᵐ[μ] Function.const α c
-- Batteries.Data.Stream
Std.Stream.snd_takeTR_loop : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (acc : List α) (n : ℕ),
  (Std.Stream.takeTR.loop s acc n).2 = Std.Stream.drop s n
-- Mathlib.RingTheory.HopfAlgebra.Quotient
/-- Transfer the Hopf algebra axioms along a surjective bialgebra homomorphism intertwining
the antipodes.  -/
HopfAlgebra.ofSurjective : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : HopfAlgebra R A] →
              [inst_4 : HopfAlgebraStruct R B] →
                (f : A →ₐc[R] B) →
                  Function.Surjective ⇑f →
                    HopfAlgebraStruct.antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ HopfAlgebraStruct.antipode R →
                      HopfAlgebra R B
-- Mathlib.Algebra.Order.Sub.Defs
/-- `a - b` provides a lower bound on `c` such that `a ≤ c + b`.  -/
OrderedSub.tsub_le_iff_right : ∀ {α : Type u_2} {inst : LE α} {inst_1 : Add α} {inst_2 : Sub α} [self : OrderedSub α] (a b c : α),
  a - b ≤ c ↔ a ≤ c + b
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The pushout of `L₂.X₂` and `L₃.X₁` along `L₂.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.P' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → C
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.ceil.eq_1 : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E),
  ZSpan.ceil b m = ∑ i, ⌈(b.repr m) i⌉ • (Module.Basis.restrictScalars ℤ b) i
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_succ_right_eq_cons_map : ∀ {m n : ℤ}, m ≤ n + 1 → (m...=n + 1).toList = m :: List.map (fun x => x + 1) (m...=n).toList
-- Mathlib.Order.RelIso.Basic
RelHom.mk : {α : Type u_5} →
  {β : Type u_6} →
    {r : α → α → Prop} → {s : β → β → Prop} → (toFun : α → β) → (∀ {a b : α}, r a b → s (toFun a) (toFun b)) → r →r s
-- Mathlib.GroupTheory.SemidirectProduct
/-- The group isomorphism between a semidirect product with respect to the trivial map
and the product.  -/
SemidirectProduct.mulEquivProd : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → N ⋊[1] G ≃* N × G
-- Mathlib.Analysis.Normed.Module.Convex
/-- Diameter of the convex hull of a set `s` equals the emetric diameter of `s`.  -/
convexHull_diam : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E),
  Metric.diam ((convexHull ℝ) s) = Metric.diam s
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.add_one_le_of_lt : ∀ {a b : Cardinal.{u_1}}, a < b → a + 1 ≤ b
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.denseRange_coe₃ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ], DenseRange fun x => (↑x.1, ↑x.2.1, ↑x.2.2)